Fixed bug in bv: one more case where non-shared equality was getting propagated

Added a global push and pop around solving - fixes an assertion failure when
TNodes are still around in a CDHashMap at destruction time.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0d3a220c9838f786ef6e11214d56b07154015a43..64e3e4ae47ae6f1253c14101ae122874f542e71f 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -293,6 +293,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_theoryEngine->setDecisionEngine(d_decisionEngine);
   // d_decisionEngine->setPropEngine(d_propEngine);
 
+  d_context->push();
+
   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
 
   // [MGD 10/20/2011] keep around in incremental mode, due to a
@@ -349,6 +351,8 @@ SmtEngine::~SmtEngine() throw() {
 
     shutdown();
 
+    d_context->pop();
+
     if(d_assignments != NULL) {
       d_assignments->deleteSelf();
     }

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 79ab955aaf9fc718b34ba4a4735d2d18b43a335c..251650bf2983878ba2f8a96eb6f0209b6b68f9cf 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -148,12 +148,13 @@ void TheoryBV::propagate(Effort e) {
     Node normalized = Rewriter::rewrite(literal);
 
     TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;  
-    // check if it's a shared equality in the current context
-    if (atom.getKind() != kind::EQUAL || d_valuation.isSatLiteral(normalized) ||
-        (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() &&
-         d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end())) {
-    
-      bool satValue;
+    bool isSharedLiteral = (atom.getKind() == kind::EQUAL &&
+                            (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() &&
+                             d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end()));
+
+    // Check if this is a SAT literal
+    if (d_valuation.isSatLiteral(normalized)) {
+      bool satValue = false;
       if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
         // check if we already propagated the negation
         Node negLiteral = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal);
@@ -166,11 +167,16 @@ void TheoryBV::propagate(Effort e) {
           setConflict(mkAnd(assumptions)); 
           return;
         }
-        
-        BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << literal << std::endl;
-        d_out->propagate(literal);
-        d_alreadyPropagatedSet.insert(literal); 
+        // If it's not a shared literal and hasn't already been set to true, we propagate the normalized version
+        // shared literals are handled below
+        if (!isSharedLiteral && !satValue) {
+          BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << normalized << std::endl;
+          d_out->propagate(normalized);
+          d_alreadyPropagatedSet.insert(normalized); 
+          return;
+        }
       } else {
+        // 
         Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
         Node negatedLiteral;
         std::vector<TNode> assumptions;
@@ -181,9 +187,16 @@ void TheoryBV::propagate(Effort e) {
         return;
       }
     }
+    // Either it was not a SAT literal or it was but it is also shared - in that case we have to propagate the original literal (not the normalized one)
+    if (isSharedLiteral) {
+      BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << literal << std::endl;
+      d_out->propagate(literal);
+      d_alreadyPropagatedSet.insert(literal); 
+    }
   }
 }
 
+
 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   switch(in.getKind()) {
   case kind::EQUAL: