fixed some model stuff

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index 773685997a099a95a67d82b379886e7ad4ea57d6..a952b2929fbe6764fe683046868c9aa25ee59486 100644 (file)
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -346,7 +346,7 @@ void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
     Debug("bitvector-bb") << "                           with bits  " << toString(bits); 
   }
 
-  bb->storeVariable(node);
+   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 6da3b8efca5fa224cfd9cf5a7c08d3477d46bcdc..9a52a05a5f1c590d4c2e532fed51fd008543ae7d 100644 (file)
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -428,9 +428,18 @@ bool Bitblaster::hasValue(TNode a) {
   }
   return true; 
 }
-
+/** 
+ * Returns the value a is currently assigned to in the SAT solver
+ * or null if the value is completely unassigned. 
+ * 
+ * @param a 
+ * 
+ * @return 
+ */
 Node Bitblaster::getVarValue(TNode a) {
-  Assert (d_termCache.find(a) != d_termCache.end()); 
+  if (d_termCache.find(a) == d_termCache.end()) {
+    return Node(); 
+  }
   Bits bits = d_termCache[a];
   Integer value(0); 
   for (int i = bits.size() -1; i >= 0; --i) {
@@ -455,6 +464,10 @@ void Bitblaster::collectModelInfo(TheoryModel* m) {
     TNode var = *it;
     if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var))  {
       Node const_value = getVarValue(var);
+      if(const_value == Node()) {
+        // if the value is unassigned just set it to zero
+        const_value = utils::mkConst(BitVector(utils::getSize(var), 0u)); 
+      }
       Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
                                 << var << " "
                                 << const_value << "))\n";

diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 9c4a5c5b66c284368f6a1420398af3404f110160..30eaaa764a7f53bea76c14d1dd2b4827704d13be 100644 (file)
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -141,5 +141,7 @@ void BitblastSolver::collectModelInfo(TheoryModel* m) {
 }
 
 Node BitblastSolver::getModelValue(TNode node) {
-  return d_bitblaster->getVarValue(node);
+  Node val = d_bitblaster->getVarValue(node);
+  Assert (val != Node() || d_bv->isSharedTerm(node));
+  return val; 
 }

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index c4f1b1b86b25a6467c2cd85fdae3cb016a4409b3..91fed8a672eabfbf81b91c25436ffd8524dd0aec 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -407,7 +407,11 @@ Node CoreSolver::getModelValue(TNode var) {
   if (repr.getKind() == kind::CONST_BITVECTOR) {
     return repr; 
   }
-  Assert (d_modelValues.find(repr) != d_modelValues.end()); 
+  if (d_modelValues.find(repr) == d_modelValues.end()) {
+    // it may be a shared term that never gets asserted
+    Assert(d_bv->isSharedTerm(var));
+    return Node(); 
+  }
   return d_modelValues[repr]; 
 }
 

diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 9f7760608f8570fb59984058995cccaa8d3e9574..5504dbc11e60fe23af09adb7a5dd362eeeb3ecc4 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -181,7 +181,10 @@ void InequalitySolver::collectModelInfo(TheoryModel* m) {
 
 Node InequalitySolver::getModelValue(TNode var) {
   Assert (isComplete());
-  Assert (d_inequalityGraph.hasValueInModel(var)); 
+  if (!d_inequalityGraph.hasValueInModel(var)) {
+    Assert (d_bv->isSharedTerm(var));
+    return Node(); 
+  }
   BitVector val = d_inequalityGraph.getValueInModel(var);
   return utils::mkConst(val); 
 }