implemented collectModelInfo for TheoryBV

1 files changed, 27 insertions, 3 deletions

diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index ada9802bd..3aee0ee1a 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -51,6 +51,7 @@ class BVSatSolverInterface;
 namespace theory {
 
 class OutputChannel;
+class TheoryModel;
 
 namespace bv {
 
@@ -82,7 +83,8 @@ class Bitblaster {
   };
   
   typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction >              TermDefMap;
-  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>                      AtomSet; 
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>                      AtomSet;
+  typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>                      VarSet; 
   
   typedef void   (*TermBBStrategy) (TNode, Bits&, Bitblaster*); 
   typedef Node   (*AtomBBStrategy) (TNode, Bitblaster*); 
@@ -95,7 +97,7 @@ class Bitblaster {
   // caches and mappings
   TermDefMap                   d_termCache;
   AtomSet                      d_bitblastedAtoms;
-  
+  VarSet                       d_variables; 
   context::CDList<prop::SatLiteral>  d_assertedAtoms; /**< context dependent list storing the atoms
                                                        currently asserted by the DPLL SAT solver. */
 
@@ -136,7 +138,29 @@ public:
   void explain(TNode atom, std::vector<TNode>& explanation);
 
   EqualityStatus getEqualityStatus(TNode a, TNode b);
-
+  /** 
+   * Return a constant Node representing the value of a variable
+   * in the current model. 
+   * @param a 
+   * 
+   * @return 
+   */
+  Node getVarValue(TNode a);
+  /** 
+   * Adds a constant value for each bit-blasted variable in the model. 
+   * 
+   * @param m the model 
+   */
+  void collectModelInfo(TheoryModel* m); 
+  /** 
+   * Stores the variable (or non-bv term) and its corresponding bits. 
+   * 
+   * @param var 
+   * @param bits 
+   */
+  void storeVariable(TNode var) {
+    d_variables.insert(var); 
+  } 
 private: