implemented collectModelInfo for TheoryBV

9 files changed, 81 insertions, 10 deletions

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index 80b689b8c..08bd3475a 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -338,9 +338,7 @@ void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
-  //  Assert (node.getKind() == kind::VARIABLE);
   Assert(bits.size() == 0);
-  
   for (unsigned i = 0; i < utils::getSize(node); ++i) {
     bits.push_back(utils::mkBitOf(node, i));
   }
@@ -349,6 +347,10 @@ 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); 
+
 }
 
 void DefaultConstBB (TNode node, Bits& bits, Bitblaster* bb) {
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 3beb7c229..4aa52e24c 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -26,6 +26,7 @@
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/options.h"
+#include "theory/model.h"
 
 using namespace std;
 
@@ -398,6 +399,35 @@ EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) {
   }
 }
 
+Node Bitblaster::getVarValue(TNode a) {
+  Assert (d_termCache.find(a) != d_termCache.end()); 
+  Bits bits = d_termCache[a];
+  Integer value(0); 
+  for (int i = bits.size() -1; i >= 0; --i) {
+    SatValue bit_value;
+    if (d_cnfStream->hasLiteral(bits[i])) { 
+      SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
+      bit_value = d_satSolver->value(bit);
+      Assert (bit_value != SAT_VALUE_UNKNOWN);
+    } else {
+      // the bit is unconstrainted so we can give it an arbitrary value 
+      bit_value = SAT_VALUE_FALSE;
+    }
+    Integer bit_int = bit_value == SAT_VALUE_TRUE ? Integer(1) : Integer(0); 
+    value = value * 2 + bit_int;  
+  }
+  return utils::mkConst(BitVector(bits.size(), value));  
+}
+
+void Bitblaster::collectModelInfo(TheoryModel* m) {
+  __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin();
+  for (; it!= d_variables.end(); ++it) {
+    TNode var = *it;
+    Node const_value = getVarValue(var);
+    m->assertEquality(var, const_value, true); 
+  }
+}
+
 } /*bv namespace */
 } /* theory namespace */
 } /* CVC4 namespace*/
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:
 
   
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index f8c763e3f..98b809d85 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -28,6 +28,9 @@
 
 namespace CVC4 {
 namespace theory {
+
+class TheoryModel;
+
 namespace bv {
 
 enum SubTheory {
@@ -82,7 +85,7 @@ public:
   virtual bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) = 0;
   virtual void  explain(TNode literal, std::vector<TNode>& assumptions) = 0;
   virtual void  preRegister(TNode node) {}
-
+  virtual void  collectModelInfo(TheoryModel* m) = 0; 
 }; 
 
 }
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index b0d04f952..e28ec188d 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -125,3 +125,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
 EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
   return d_bitblaster->getEqualityStatus(a, b);
 }
+
+void BitblastSolver::collectModelInfo(TheoryModel* m) {
+  return d_bitblaster->collectModelInfo(m); 
+}
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 33ae5d2ff..a2c77c9f5 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -47,6 +47,7 @@ public:
   bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
   EqualityStatus getEqualityStatus(TNode a, TNode b);
+  void collectModelInfo(TheoryModel* m); 
 };
 
 }
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index cb08a1ad8..56a490747 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -19,7 +19,7 @@
 #include "theory/bv/bv_subtheory_eq.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
-
+#include "theory/model.h"
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::context;
@@ -165,3 +165,6 @@ void EqualitySolver::conflict(TNode a, TNode b) {
   d_bv->setConflict(mkAnd(assumptions));
 }
 
+void EqualitySolver::collectModelInfo(TheoryModel* m) {
+  m->assertEqualityEngine(&d_equalityEngine);
+}
diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h
index d0ba8abca..24d9669db 100644
--- a/src/theory/bv/bv_subtheory_eq.h
+++ b/src/theory/bv/bv_subtheory_eq.h
@@ -19,7 +19,6 @@
 #pragma once
 
 #include "cvc4_private.h"
-
 #include "theory/bv/bv_subtheory.h"
 
 namespace CVC4 {
@@ -68,6 +67,7 @@ public:
   void  preRegister(TNode node);
   bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
   void  explain(TNode literal, std::vector<TNode>& assumptions);
+  void  collectModelInfo(TheoryModel* m);
   void  addSharedTerm(TNode t) {
     d_equalityEngine.addTriggerTerm(t, THEORY_BV);
   }
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index aa5281d2f..51e09ee5a 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -23,7 +23,7 @@
 #include "theory/bv/bitblaster.h"
 #include "theory/bv/options.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
-
+#include "theory/model.h"
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
@@ -126,7 +126,11 @@ void TheoryBV::check(Effort e)
 }
 
 void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
-
+  Assert(!inConflict());
+  Assert (fullModel); // can only query full model
+  d_equalitySolver.collectModelInfo(m); 
+  d_bitblastSolver.collectModelInfo(m); 
+  
 }
 
 void TheoryBV::propagate(Effort e) {