clear model cache in BVQuickCheck clearSolver() (fixes bug 587)

5 files changed, 19 insertions, 11 deletions

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index e13587323..79434102e 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -447,8 +447,10 @@ Node TBitblaster<T>::getTermModel(TNode node, bool fullModel) {
     // if it is a leaf may ask for fullModel
     value = getModelFromSatSolver(node, fullModel); 
     Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from VarValue" << node <<" => " << value <<"\n";
-    Assert (!value.isNull()); 
-    d_modelCache[node] = value;
+    Assert ((fullModel && !value.isNull() && value.isConst()) || !fullModel); 
+    if (!value.isNull()) {
+      d_modelCache[node] = value;
+    }
     return value;
   }
   Assert (node.getType().isBitVector());
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index 9d22a3edf..6231b8e46 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -114,8 +114,8 @@ BVQuickCheck::vars_iterator BVQuickCheck::endVars() {
   return d_bitblaster->endVars(); 
 }
 
-Node BVQuickCheck::getVarValue(TNode var) {
-  return d_bitblaster->getTermModel(var, true); 
+Node BVQuickCheck::getVarValue(TNode var, bool fullModel) {
+  return d_bitblaster->getTermModel(var, fullModel); 
 }
 
 
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index 8a36e6b34..01d772cb9 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -103,7 +103,7 @@ public:
   vars_iterator beginVars(); 
   vars_iterator endVars(); 
 
-  Node getVarValue(TNode var); 
+  Node getVarValue(TNode var, bool fullModel); 
 
 };
 
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 5b139e327..154f3d7f3 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -695,17 +695,22 @@ void AlgebraicSolver::collectModelInfo(TheoryModel* model, bool fullModel) {
   Debug("bitvector-model") << "Model:\n";
   for (BVQuickCheck::vars_iterator it = d_quickSolver->beginVars(); it != d_quickSolver->endVars(); ++it) {
     TNode var = *it;
-    Node value = d_quickSolver->getVarValue(var);
-    Debug("bitvector-model") << "   " << var << " => " << value << "\n";
-    Assert (value.getKind() == kind::CONST_BITVECTOR); 
-    d_modelMap->addSubstitution(var, value); 
+    Node value = d_quickSolver->getVarValue(var, true);
+    Assert (!value.isNull() || !fullModel);
+
+    // may be a shared term that did not appear in the current assertions
+    if (!value.isNull()) {
+      Debug("bitvector-model") << "   " << var << " => " << value << "\n";
+      Assert (value.getKind() == kind::CONST_BITVECTOR); 
+      d_modelMap->addSubstitution(var, value);
+    }
   }
 
   Debug("bitvector-model") << "Final Model:\n";
   for (unsigned i = 0; i < variables.size(); ++i) {
     TNode current = values[i];
     TNode subst = Rewriter::rewrite(d_modelMap->apply(current));
-    Debug("bitvector-model") << "   " << variables[i] << " => " << subst << "\n"; 
+    Debug("bitvector-model") << "AlgebraicSolver:   " << variables[i] << " => " << subst << "\n"; 
     // Doesn't have to be constant as it may be irrelevant
     // Assert (subst.getKind() == kind::CONST_BITVECTOR); 
     model->assertEquality(variables[i], subst, true);
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index e5b5ed664..fbebcd952 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -491,8 +491,9 @@ void TLazyBitblaster::clearSolver() {
   d_explanations = new(true) ExplanationMap(d_ctx);
   d_bbAtoms.clear();
   d_variables.clear();
-  d_termCache.clear(); 
+  d_termCache.clear();
   
+  invalidateModelCache();  
   // recreate sat solver
   d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx);
   d_cnfStream = new prop::TseitinCnfStream(d_satSolver,