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

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index e13587323314d181528f251261fe4dd1f26ab2ce..79434102e8e550099fb1e9de83f83a7fd4bf41cf 100644 (file)
--- 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 9d22a3edf044c59f5f846e57cfc91bb573ae2a90..6231b8e460b01ff3efceba656d5142859c3da847 100644 (file)
--- 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 8a36e6b344d0ceb1f4a5723f8391548616314559..01d772cb9c15f1786047d31f200ad9ea69549892 100644 (file)
--- 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 5b139e327118792a20f8ef5857fbd8d62da29498..154f3d7f37b86e7a4a7ee2cf2fc53b834bb3f4ed 100644 (file)
--- 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 e5b5ed66414f301ca4d298dcbdc7a9561854653a..fbebcd952670cae3a34b9ac0e21fc34359be389e 100644 (file)
--- 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,