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

4 files changed, 41 insertions, 4 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 14d2370ab..52f4c7014 100644
--- 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 1864bc89e..fd8eef1f1 100644
--- 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 4bc066e08..2c863ba84 100644
--- 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 4983b0557..d3b0964cf 100644
--- 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: