BV theory model fix

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index a6cd0af29b1fc738cbdb3d6a4d37d96aa5ad5dff..5d0ef8aa516c01723611fe50a7d60cffc45a7f95 100644 (file)
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -345,9 +345,11 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
     BVDebug("bitvector-bb") << "theory::bv::DefaultVarBB bitblasting  " << node << "\n";
     BVDebug("bitvector-bb") << "                           with bits  " << toString(bits); 
   }
-  // this is not necessairily a variable, but it is a term the theory of bitvectors treads as one
-  // e.g. a select over a bv array 
-  bb->storeVariable(node); 
+
+    if (Theory::theoryOf(node) == theory::THEORY_BV ||
+        bb->isSharedTerm(node)) {
+    bb->storeVariable(node);
+    }
 
 }
 

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 19f80bb44cbfdf493bb35d7ad30caa0471743039..593189e5672ac2ff2348e211587e816d9f457adb 100644 (file)
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -53,6 +53,7 @@ std::string toString(Bits&  bits) {
 /////// Bitblaster 
 
 Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) :
+    d_bv(bv),
     d_bvOutput(bv->d_out),
     d_termCache(),
     d_bitblastedAtoms(),
@@ -397,6 +398,11 @@ EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) {
   }
 }
 
+
+bool Bitblaster::isSharedTerm(TNode node) {
+  return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); 
+}
+
 Node Bitblaster::getVarValue(TNode a) {
   Assert (d_termCache.find(a) != d_termCache.end()); 
   Bits bits = d_termCache[a];

diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index 792f9d1693089533b9a20c9614a787a90bc9cd52..21b389508fa491d698f7cae8859738ca1c821c56 100644 (file)
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -80,6 +80,7 @@ class Bitblaster {
     void safePoint();
   };
   
+  
   typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction >              TermDefMap;
   typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>                      AtomSet;
   typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>                      VarSet; 
@@ -87,6 +88,8 @@ class Bitblaster {
   typedef void   (*TermBBStrategy) (TNode, Bits&, Bitblaster*); 
   typedef Node   (*AtomBBStrategy) (TNode, Bitblaster*); 
 
+  TheoryBV *d_bv;
+  
   // sat solver used for bitblasting and associated CnfStream
   theory::OutputChannel*             d_bvOutput;
   prop::BVSatSolverInterface*        d_satSolver; 
@@ -158,7 +161,9 @@ public:
    */
   void storeVariable(TNode var) {
     d_variables.insert(var); 
-  } 
+  }
+
+  bool isSharedTerm(TNode node);
 private: