From: Liana Hadarean <lianahady@gmail.com>
Date: Fri, 19 Oct 2012 18:38:54 +0000 (+0000)
Subject: BV theory model fix
X-Git-Tag: cvc5-1.0.0~7696
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6f8d2ea6e8b6a8ff43352740131486bee6b2da27;p=cvc5.git

BV theory model fix
---

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index a6cd0af29..5d0ef8aa5 100644
--- 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 19f80bb44..593189e56 100644
--- 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 792f9d169..21b389508 100644
--- 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: