extract instantiate_var_mapt into a separate header file

src/trans-netlist/Makefile

@@ -9,6 +9,7 @@ SRC = aig.cpp \
       ldg.cpp \
       map_aigs.cpp \
       netlist.cpp \
+      netlist_boolbv.cpp \
       smv_netlist.cpp \
       trans_to_netlist.cpp \
       trans_trace.cpp \

src/trans-netlist/instantiate_netlist.cpp

@@ -13,48 +13,15 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 
 #include <ebmc/ebmc_error.h>
-#include <solvers/flattening/boolbv.h>
 #include <solvers/prop/literal_expr.h>
 #include <temporal-logic/temporal_logic.h>
 #include <verilog/sva_expr.h>
 
+#include "netlist_boolbv.h"
+
 #include <cassert>
 #include <cstdlib>
 
-/*******************************************************************\
-
-   Class: instantiate_var_mapt
-
- Purpose:
-
-\*******************************************************************/
-
-class instantiate_var_mapt:public boolbvt
-{
-public:
-  instantiate_var_mapt(const namespacet &_ns, propt &solver,
-                       message_handlert &message_handler,
-                       const var_mapt &_var_map)
-      : boolbvt(_ns, solver, message_handler), var_map(_var_map) {}
-
-  typedef boolbvt SUB;
-
-  // overloading
-  using boolbvt::get_literal;
-
-  virtual literalt convert_bool(const exprt &expr);
-  virtual literalt get_literal(const std::string &symbol, const unsigned bit);
-  virtual bvt convert_bitvector(const exprt &expr);
-
-protected:   
-  // disable smart variable allocation,
-  // we already have literals for all variables
-  virtual bool boolbv_set_equality_to_true(const equal_exprt &expr) { return true; }
-  virtual bool set_equality_to_true(const equal_exprt &expr) { return true; }
-
-  const var_mapt &var_map;
-};
-
 /*******************************************************************\
 
 Function: instantiate_constraint
@@ -74,7 +41,7 @@ void instantiate_constraint(
   const namespacet &ns,
   message_handlert &message_handler)
 {
-  instantiate_var_mapt i(ns, solver, message_handler, var_map);
+  netlist_boolbvt i(ns, solver, message_handler, var_map);
 
   try
   {
@@ -113,7 +80,7 @@ literalt instantiate_convert(
   const namespacet &ns,
   message_handlert &message_handler)
 {
-  instantiate_var_mapt i(ns, solver, message_handler, var_map);
+  netlist_boolbvt i(ns, solver, message_handler, var_map);
 
   try
   {
@@ -153,7 +120,7 @@ void instantiate_convert(
   message_handlert &message_handler,
   bvt &bv)
 {
-  instantiate_var_mapt i(ns, solver, message_handler, var_map);
+  netlist_boolbvt i(ns, solver, message_handler, var_map);
 
   try
   {
@@ -175,107 +142,6 @@ void instantiate_convert(
 
 /*******************************************************************\
 
-Function: instantiate_var_mapt::convert_bool
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-literalt instantiate_var_mapt::convert_bool(const exprt &expr)
-{
-  if(expr.id()==ID_symbol || expr.id()==ID_next_symbol)
-  {
-    bvt result=convert_bitvector(expr);
-
-    if(result.size()!=1)
-      throw "expected one-bit result";
-
-    return result[0];
-  }
-  else if(expr.id()==ID_sva_overlapped_implication)
-  {
-    // same as regular implication
-    auto &sva_overlapped_implication = to_sva_overlapped_implication_expr(expr);
-    return prop.limplies(
-      convert_bool(sva_overlapped_implication.lhs()),
-      convert_bool(sva_overlapped_implication.rhs()));
-  }
-  else if(expr.id() == ID_verilog_past)
-  {
-    throw ebmc_errort().with_location(expr.source_location())
-      << "no support for $past when using AIG backends";
-  }
-
-  return SUB::convert_bool(expr);
-}
-
-/*******************************************************************\
-
-Function: instantiate_var_mapt::convert_bitvector
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-bvt instantiate_var_mapt::convert_bitvector(const exprt &expr)
-{
-  if(expr.id()==ID_symbol || expr.id()==ID_next_symbol)
-  {
-    bool next=(expr.id()==ID_next_symbol);
-    const irep_idt &identifier=expr.get(ID_identifier);
-
-    std::size_t width=boolbv_width(expr.type());
-
-    if(width!=0)
-    {
-      bvt bv;
-      bv.resize(width);
-
-      for(std::size_t i=0; i<width; i++)
-        bv[i]=next?var_map.get_next(identifier, i)
-                  :var_map.get_current(identifier, i);
-
-      return bv;
-    }
-  }
-  else if(expr.id() == ID_verilog_past)
-  {
-    throw ebmc_errort().with_location(expr.source_location())
-      << "no support for $past when using AIG backends";
-  }
-
-  return SUB::convert_bitvector(expr);
-}
-
-/*******************************************************************\
-
-Function: instantiate_var_mapt::get_literal
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-literalt instantiate_var_mapt::get_literal(
-  const std::string &symbol,
-  const unsigned bit)
-{
-  return var_map.get_current(symbol, bit);
-}
-
-/*******************************************************************\
-
 Function: netlist_property
 
   Inputs:

src/trans-netlist/netlist_boolbv.cpp

@@ -0,0 +1,112 @@
+/*******************************************************************\
+
+Module: boolbvt for Netlists
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "netlist_boolbv.h"
+
+#include <ebmc/ebmc_error.h>
+#include <verilog/sva_expr.h>
+
+/*******************************************************************\
+
+Function: netlist_boolbvt::convert_bool
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+literalt netlist_boolbvt::convert_bool(const exprt &expr)
+{
+  if(expr.id() == ID_symbol || expr.id() == ID_next_symbol)
+  {
+    bvt result = convert_bitvector(expr);
+
+    if(result.size() != 1)
+      throw "expected one-bit result";
+
+    return result[0];
+  }
+  else if(expr.id() == ID_sva_overlapped_implication)
+  {
+    // same as regular implication
+    auto &sva_overlapped_implication = to_sva_overlapped_implication_expr(expr);
+    return prop.limplies(
+      convert_bool(sva_overlapped_implication.lhs()),
+      convert_bool(sva_overlapped_implication.rhs()));
+  }
+  else if(expr.id() == ID_verilog_past)
+  {
+    throw ebmc_errort().with_location(expr.source_location())
+      << "no support for $past when using AIG backends";
+  }
+
+  return SUB::convert_bool(expr);
+}
+
+/*******************************************************************\
+
+Function: netlist_boolbvt::convert_bitvector
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+bvt netlist_boolbvt::convert_bitvector(const exprt &expr)
+{
+  if(expr.id() == ID_symbol || expr.id() == ID_next_symbol)
+  {
+    bool next = (expr.id() == ID_next_symbol);
+    const irep_idt &identifier = expr.get(ID_identifier);
+
+    std::size_t width = boolbv_width(expr.type());
+
+    if(width != 0)
+    {
+      bvt bv;
+      bv.resize(width);
+
+      for(std::size_t i = 0; i < width; i++)
+        bv[i] = next ? var_map.get_next(identifier, i)
+                     : var_map.get_current(identifier, i);
+
+      return bv;
+    }
+  }
+  else if(expr.id() == ID_verilog_past)
+  {
+    throw ebmc_errort().with_location(expr.source_location())
+      << "no support for $past when using AIG backends";
+  }
+
+  return SUB::convert_bitvector(expr);
+}
+
+/*******************************************************************\
+
+Function: netlist_boolbvt::get_literal
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+literalt
+netlist_boolbvt::get_literal(const std::string &symbol, const unsigned bit)
+{
+  return var_map.get_current(symbol, bit);
+}

src/trans-netlist/netlist_boolbv.h

@@ -0,0 +1,60 @@
+/*******************************************************************\
+
+Module: boolbvt for Netlists
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_TRANS_NETLIST_NETLIST_BOOLBV_H
+#define CPROVER_TRANS_NETLIST_NETLIST_BOOLBV_H
+
+#include <solvers/flattening/boolbv.h>
+
+#include "var_map.h"
+
+/*******************************************************************\
+
+   Class: netlist_boolbvt
+
+ Purpose:
+
+\*******************************************************************/
+
+class netlist_boolbvt : public boolbvt
+{
+public:
+  netlist_boolbvt(
+    const namespacet &_ns,
+    propt &solver,
+    message_handlert &message_handler,
+    const var_mapt &_var_map)
+    : boolbvt(_ns, solver, message_handler), var_map(_var_map)
+  {
+  }
+
+  typedef boolbvt SUB;
+
+  // overloading
+  literalt convert_bool(const exprt &) override;
+  bvt convert_bitvector(const exprt &expr) override;
+
+  using boolbvt::get_literal;
+  literalt get_literal(const std::string &symbol, const unsigned bit);
+
+protected:
+  // disable smart variable allocation,
+  // we already have literals for all variables
+  bool boolbv_set_equality_to_true(const equal_exprt &) override
+  {
+    return true;
+  }
+  bool set_equality_to_true(const equal_exprt &expr) override
+  {
+    return true;
+  }
+
+  const var_mapt &var_map;
+};
+
+#endif // CPROVER_TRANS_NETLIST_NETLIST_BOOLBV_H