extract instantiate_var_mapt into a separate header file

Author: kroening

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

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: 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
+  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