Fixing a bug related to explaining propagations with non-normalized witnesses.

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 14d2370abef34b673b07feb2c8a08e10ebfb3085..52f4c701421bc0813d1b366a71b0afa3833026ad 100644 (file)
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -160,7 +160,11 @@ bool ArithCongruenceManager::propagate(TNode x){
   // 11* : drop the constraint, do not propagate x or c
 
   if(!c->hasProof() && x != rewritten){
-    pushBack(x, rewritten);
+    if(c->assertedToTheTheory()){
+      pushBack(x, rewritten, c->getWitness());
+    }else{
+      pushBack(x, rewritten);
+    }
 
     c->setEqualityEngineProof();
     if(c->canBePropagated() && !c->assertedToTheTheory()){
@@ -169,10 +173,18 @@ bool ArithCongruenceManager::propagate(TNode x){
       c->propagate();
     }
   }else if(!c->hasProof() && x == rewritten){
-    pushBack(x, rewritten);
+    if(c->assertedToTheTheory()){
+      pushBack(x, c->getWitness());
+    }else{
+      pushBack(x);
+    }
     c->setEqualityEngineProof();
   }else if(c->hasProof() && x != rewritten){
-    pushBack(x, rewritten);
+    if(c->assertedToTheTheory()){
+      pushBack(x, rewritten, c->getWitness());
+    }else{
+      pushBack(x, rewritten);
+    }
   }else{
     Assert(c->hasProof() && x == rewritten);
   }

diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 1864bc89e85dfd6f3d7c3c7305e55b0d6cd6130c..fd8eef1f1e5bf596d4ec8e23e135c9f462e7c9ba 100644 (file)
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -152,6 +152,15 @@ private:
     ++(d_statistics.d_propagations);
   }
 
+  void pushBack(TNode n, TNode r, TNode w){
+    d_explanationMap.insert(w, d_propagatations.size());
+    d_explanationMap.insert(r, d_propagatations.size());
+    d_explanationMap.insert(n, d_propagatations.size());
+    d_propagatations.enqueue(n);
+
+    ++(d_statistics.d_propagations);
+  }
+
   bool propagate(TNode x);
   void explain(TNode literal, std::vector<TNode>& assumptions);
 

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 4bc066e08544e2f70e2be1e74162aa4568cd2fc9..2c863ba841b08b461e40e1ff0c1ab36b90be30b4 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -60,6 +60,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_hasDoneWorkSinceCut(false),
   d_learner(d_pbSubstitutions),
   d_setupLiteralCallback(this),
+  d_assertionsThatDoNotMatchTheirLiterals(c),
   d_nextIntegerCheckVar(0),
   d_constantIntegerVariables(c),
   d_diseqQueue(c, false),
@@ -1116,6 +1117,12 @@ Constraint TheoryArith::constraintFromFactQueue(){
     }
     Node reAssertion = isDistinct ? reEq.notNode() : reEq;
     constraint = d_constraintDatabase.lookup(reAssertion);
+
+    if(assertion != reAssertion){
+      Debug("arith::nf") << "getting non-nf assertion " << assertion << " |-> " <<  reAssertion << endl;
+      Assert(constraint != NullConstraint);
+      d_assertionsThatDoNotMatchTheirLiterals[assertion] = constraint;
+    }
   }
 
   // Kind simpleKind = Comparison::comparisonKind(assertion);
@@ -1714,6 +1721,11 @@ Node TheoryArith::explain(TNode n) {
     Node exp = c->explainForPropagation();
     Debug("arith::explain") << "constraint explanation" << n << ":" << exp << endl;
     return exp;
+  }else if(d_assertionsThatDoNotMatchTheirLiterals.find(n) != d_assertionsThatDoNotMatchTheirLiterals.end()){
+    c = d_assertionsThatDoNotMatchTheirLiterals[n];
+    Node exp = c->explainForPropagation();
+    Debug("arith::explain") << "assertions explanation" << n << ":" << exp << endl;
+    return exp;
   }else{
     Assert(d_congruenceManager.canExplain(n));
     Debug("arith::explain") << "dm explanation" << n << endl;

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 4983b0557d638d91499c46e73de6f3e4f9dfb5b4..d3b0964cf0625c64c04fe41f2d77f1483ca5ef1e 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -123,7 +123,11 @@ private:
     }
   } d_setupLiteralCallback;
 
-
+  /**
+   * A superset of all of the assertions that currently are not the literal for
+   * their constraint do not match constraint literals. Not just the witnesses.
+   */
+  context::CDHashMap<TNode, Constraint, TNodeHashFunction> d_assertionsThatDoNotMatchTheirLiterals;
 
   /**
    * (For the moment) the type hierarchy goes as: