From a35201d7066863a9cb58f765d346ac7ae4a4d309 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 13 Jun 2012 21:30:05 +0000
Subject: [PATCH] Added witnesses to Constraints.

---
 src/theory/arith/constraint.cpp   | 11 ++++++-----
 src/theory/arith/constraint.h     | 28 ++++++++++++++++++++--------
 src/theory/arith/theory_arith.cpp |  5 ++---
 3 files changed, 28 insertions(+), 16 deletions(-)

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index bedb91756..b44105895 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -56,7 +56,8 @@ ConstraintValue::ConstraintValue(ArithVar x,  ConstraintType t, const DeltaRatio
     d_literal(Node::null()),
     d_negation(NullConstraint),
     d_canBePropagated(false),
-    d_assertionOrder(AssertionOrderSentinel),
+    _d_assertionOrder(AssertionOrderSentinel),
+    d_witness(TNode::null()),
     d_proof(ProofIdSentinel),
     d_split(false),
     d_variablePosition()
@@ -347,11 +348,11 @@ void ConstraintValue::setCanBePropagated() {
   d_database->pushCanBePropagatedWatch(this);
 }
 
-void ConstraintValue::setAssertedToTheTheory() {
+void ConstraintValue::setAssertedToTheTheory(TNode witness) {
   Assert(hasLiteral());
   Assert(!assertedToTheTheory());
   Assert(!d_negation->assertedToTheTheory());
-  d_database->pushAssertionOrderWatch(this);
+  d_database->pushAssertionOrderWatch(this, witness);
 }
 
 bool ConstraintValue::isSelfExplaining() const {
@@ -853,7 +854,7 @@ void ConstraintValue::explainBefore(NodeBuilder<>& nb, AssertionOrder order) con
   Assert(!isSelfExplaining() || assertedToTheTheory());
 
   if(assertedBefore(order)){
-    nb << getLiteral();
+    nb << getWitness();
   }else if(hasEqualityEngineProof()){
     d_database->eeExplain(this, nb);
   }else{
@@ -870,7 +871,7 @@ Node ConstraintValue::explainBefore(AssertionOrder order) const{
   Assert(hasProof());
   Assert(!isSelfExplaining() || assertedBefore(order));
   if(assertedBefore(order)){
-    return getLiteral();
+    return getWitness();
   }else if(hasEqualityEngineProof()){
     return d_database->eeExplain(this);
   }else{
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index dcc3bf8bb..be4197a26 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -273,7 +273,12 @@ private:
    * Sat Context Dependent.
    * This is initially AssertionOrderSentinel.
    */
-  AssertionOrder d_assertionOrder;
+  AssertionOrder _d_assertionOrder;
+  /**
+   * This is guarenteed to be on the fact queue.
+   * For example if x + y = x + 1 is on the fact queue, then use this 
+   */
+  TNode d_witness;
 
   /**
    * This points at the proof for the constraint in the current context.
@@ -347,7 +352,8 @@ private:
     inline void operator()(Constraint* p){
       Constraint constraint = *p;
       Assert(constraint->assertedToTheTheory());
-      constraint->d_assertionOrder = AssertionOrderSentinel;
+      constraint->_d_assertionOrder = AssertionOrderSentinel;
+      constraint->d_witness = TNode::null();
       Assert(!constraint->assertedToTheTheory());
     }
   };
@@ -439,15 +445,20 @@ public:
   }
 
   bool assertedToTheTheory() const {
-    return d_assertionOrder < AssertionOrderSentinel;
+    Assert((_d_assertionOrder < AssertionOrderSentinel) != d_witness.isNull());
+    return _d_assertionOrder < AssertionOrderSentinel;
+  }
+  TNode getWitness() const {
+    Assert(assertedToTheTheory());
+    return d_witness;
   }
 
   bool assertedBefore(AssertionOrder time) const {
-    return d_assertionOrder < time;
+    return _d_assertionOrder < time;
   }
 
 
-  void setAssertedToTheTheory();
+  void setAssertedToTheTheory(TNode witness);
 
 
   bool hasLiteral() const {
@@ -518,7 +529,7 @@ public:
   Node explainForPropagation() const {
     Assert(hasProof());
     Assert(!isSelfExplaining());
-    return explainBefore(d_assertionOrder);
+    return explainBefore(_d_assertionOrder);
   }
 
 private:
@@ -733,9 +744,10 @@ private:
     d_watches->d_canBePropagatedWatches.push_back(c);
   }
 
-  void pushAssertionOrderWatch(Constraint c){
+  void pushAssertionOrderWatch(Constraint c, TNode witness){
     Assert(!c->assertedToTheTheory());
-    c->d_assertionOrder = d_watches->d_assertionOrderWatches.size();
+    c->_d_assertionOrder = d_watches->d_assertionOrderWatches.size();
+    c->d_witness = witness;
     d_watches->d_assertionOrderWatches.push_back(c);
   }
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index faf0e3563..3ba987124 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1132,7 +1132,7 @@ Constraint TheoryArith::constraintFromFactQueue(){
     return NullConstraint;
   }else{
     Debug("arith::constraint") << "arith constraint " << constraint << std::endl;
-    constraint->setAssertedToTheTheory();
+    constraint->setAssertedToTheTheory(assertion);
 
     if(!constraint->hasProof()){
       Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
@@ -1661,8 +1661,7 @@ void TheoryArith::propagate(Effort e) {
 
       d_out->propagate(literal);
     }else{
-      Node literal = c->getLiteral();
-      Debug("arith::prop") << "already asserted to the theory " << literal << endl;
+      Debug("arith::prop") << "already asserted to the theory " <<  c->getLiteral() << endl;
     }
   }
 
-- 
2.30.2