Partial fix to bug 295.

3 files changed, 21 insertions, 13 deletions

diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h
index 912c4fdf8..bf7564593 100644
--- a/src/theory/arith/arith_prop_manager.h
+++ b/src/theory/arith/arith_prop_manager.h
@@ -31,7 +31,7 @@
 #include "context/cdlist.h"
 #include "context/cdmap.h"
 #include "context/cdo.h"
-
+#include "theory/rewriter.h"
 #include "util/stats.h"
 
 namespace CVC4 {
@@ -42,6 +42,7 @@ class PropManager {
 public:
   struct PropUnit {
     // consequent <= antecedent
+    // i.e. the antecedent is the explanation of the consequent.
     Node consequent;
     Node antecedent;
     bool flag;
@@ -52,10 +53,13 @@ public:
 
 private:
   context::CDList<PropUnit> d_propagated;
-
   context::CDO<uint32_t> d_propagatedPos;
-  typedef context::CDMap<Node, size_t, NodeHashFunction> ExplainMap;
 
+  /* This maps the node a theory engine will request on an explain call to
+   * to its corresponding PropUnit.
+   * This is node is potentially both the consequent or Rewriter::rewrite(consequent).
+   */
+  typedef context::CDMap<Node, size_t, NodeHashFunction> ExplainMap;
   ExplainMap d_explanationMap;
 
   size_t getIndex(TNode n) const {
@@ -86,6 +90,13 @@ public:
   void propagate(TNode n, Node reason, bool flag) {
     Assert(!isPropagated(n));
 
+    if(flag){
+      Node rewritten =  Rewriter::rewrite(n);
+      d_explanationMap.insert(rewritten, d_propagated.size());
+    }else{
+      //If !flag, then the rewriter is idempotent on n.
+      Assert(Rewriter::rewrite(n) == n);
+    }
     d_explanationMap.insert(n, d_propagated.size());
     d_propagated.push_back(PropUnit(n, reason, flag));
 
diff --git a/src/theory/arith/difference_manager.cpp b/src/theory/arith/difference_manager.cpp
index f366116d4..ea2d411b7 100644
--- a/src/theory/arith/difference_manager.cpp
+++ b/src/theory/arith/difference_manager.cpp
@@ -16,7 +16,7 @@ DifferenceManager::DifferenceManager(context::Context* c, PropManager& pm)
 void DifferenceManager::propagate(TNode x){
   Debug("arith::differenceManager")<< "DifferenceManager::propagate("<<x<<")"<<std::endl;
 
-  d_queue.propagate(x, Node::null(), true);
+  d_queue.propagate(x, explain(x), true);
 }
 
 void DifferenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index a99d86a9c..ca0763a0c 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -595,7 +595,8 @@ Node TheoryArith::assertionCases(TNode assertion){
   ArithVar x_i = determineLeftVariable(assertion, simpKind);
   DeltaRational c_i = determineRightConstant(assertion, simpKind);
 
-  Debug("arith::assertions") << "arith assertion(" << assertion
+  Debug("arith::assertions")  << "arith assertion @" << getContext()->getLevel()
+                              <<"(" << assertion
 			     << " \\-> "
 			     << x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl;
   switch(simpKind){
@@ -879,14 +880,10 @@ void TheoryArith::debugPrintModel(){
 }
 
 Node TheoryArith::explain(TNode n) {
-  Debug("explain") << "explain @" << getContext()->getLevel() << ": " << n << endl;
+  Debug("arith::explain") << "explain @" << getContext()->getLevel() << ": " << n << endl;
   Assert(d_propManager.isPropagated(n));
 
-  if(d_propManager.isFlagged(n)){
-    return d_differenceManager.explain(n);
-  }else{
-    return d_propManager.explain(n);
-  }
+  return d_propManager.explain(n);
 }
 
 void flattenAnd(Node n, std::vector<TNode>& out){
@@ -923,7 +920,7 @@ void TheoryArith::propagate(Effort e) {
 
       TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp;
 
-      Debug("arith::propagate") << "propagate " << flag << " " << toProp << endl;
+      Debug("arith::propagate") << "propagate  @" << getContext()->getLevel() <<" flag: "<< flag << " " << toProp << endl;
 
       if(flag) {
         //Currently if the flag is set this came from an equality detected by the
@@ -938,7 +935,7 @@ void TheoryArith::propagate(Effort e) {
           }else{
             Node exp = d_differenceManager.explain(toProp);
             Node lp = flattenAnd(exp.andNode(notNormalized));
-            Debug("arith::propagate") << "propagate conflict" << lp << endl;
+            Debug("arith::propagate") << "propagate conflict" <<  lp << endl;
             d_out->conflict(lp);
 
             propagated = true;