1 files changed, 144 insertions, 25 deletions

diff --git a/src/theory/arith/difference_manager.cpp b/src/theory/arith/difference_manager.cpp
index b67240d4c..70588bc16 100644
--- a/src/theory/arith/difference_manager.cpp
+++ b/src/theory/arith/difference_manager.cpp
@@ -1,23 +1,131 @@
 #include "theory/arith/difference_manager.h"
 #include "theory/uf/equality_engine_impl.h"
 
+#include "theory/arith/constraint.h"
+#include "theory/arith/arith_utilities.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
-DifferenceManager::DifferenceManager(context::Context* c, PropManager& pm)
-  : d_literalsQueue(c),
-    d_queue(pm),
+DifferenceManager::DifferenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup)
+  : d_conflict(c),
+    d_literalsQueue(c),
+    d_propagatations(c),
+    d_explanationMap(c),
+    d_constraintDatabase(cd),
+    d_setupLiteral(setup),
     d_notify(*this),
     d_ee(d_notify, c, "theory::arith::DifferenceManager"),
     d_false(NodeManager::currentNM()->mkConst<bool>(false)),
     d_hasSharedTerms(c, false)
 {}
 
-void DifferenceManager::propagate(TNode x){
+void DifferenceManager::differenceIsZero(Constraint lb, Constraint ub){
+  Assert(lb->isLowerBound());
+  Assert(ub->isUpperBound());
+  Assert(lb->getVariable() == ub->getVariable());
+  Assert(lb->getValue().sgn() == 0);
+  Assert(ub->getValue().sgn() == 0);
+
+  ArithVar s = lb->getVariable();
+  Node reason = ConstraintValue::explainConflict(lb,ub);
+
+  assertLiteral(true, s, reason);
+}
+
+void DifferenceManager::differenceIsZero(Constraint eq){
+  Assert(eq->isEquality());
+  Assert(eq->getValue().sgn() == 0);
+
+  ArithVar s = eq->getVariable();
+
+  //Explain for conflict is correct as these proofs are generated and stored eagerly
+  //These will be safe for propagation later as well
+  Node reason = eq->explainForConflict();
+
+  assertLiteral(true, s, reason);
+}
+
+void DifferenceManager::differenceCannotBeZero(Constraint c){
+  ArithVar s = c->getVariable();
+
+  //Explain for conflict is correct as these proofs are generated and stored eagerly
+  //These will be safe for propagation later as well
+  Node reason = c->explainForConflict();
+  assertLiteral(false, s, reason);
+}
+
+
+bool DifferenceManager::propagate(TNode x){
   Debug("arith::differenceManager")<< "DifferenceManager::propagate("<<x<<")"<<std::endl;
+  if(inConflict()){
+    return true;
+  }
+
+  Node rewritten = Rewriter::rewrite(x);
+
+  //Need to still propagate this!
+  if(rewritten.getKind() == kind::CONST_BOOLEAN){
+    pushBack(x);
+  }
 
-  d_queue.propagate(x, explain(x), true);
+  Assert(rewritten.getKind() != kind::CONST_BOOLEAN);
+
+  Constraint c = d_constraintDatabase.lookup(rewritten);
+  if(c == NullConstraint){
+    //using setup as there may not be a corresponding difference literal yet
+    d_setupLiteral(rewritten);
+    c = d_constraintDatabase.lookup(rewritten);
+    Assert(c != NullConstraint);
+    //c = d_constraintDatabase.addLiteral(rewritten);
+  }
+
+  Debug("arith::differenceManager")<< "x is "
+                                   <<  c->hasProof() << " "
+                                   << (x == rewritten) << " "
+                                   << c->canBePropagated() << " "
+                                   << c->negationHasProof() << std::endl;
+
+  if(c->negationHasProof()){
+    Node expC = explainInternal(x);
+    Node neg = c->getNegation()->explainForConflict();
+    Node conf = expC.andNode(neg);
+    Node final = flattenAnd(conf);
+
+    d_conflict.set(final);
+    Debug("arith::differenceManager") << "differenceManager found a conflict " << final << std::endl;
+    return false;
+  }
+
+  // Cases for propagation
+  // C : c has a proof
+  // S : x == rewritten
+  // P : c can be propagated
+  //
+  // CSP
+  // 000 : propagate x, and mark C it as being explained
+  // 001 : propagate x, and propagate c after marking it as being explained
+  // 01* : propagate x, mark c but do not propagate c
+  // 10* : propagate x, do not mark c and do not propagate c
+  // 11* : drop the constraint, do not propagate x or c
+
+  if(!c->hasProof() && x != rewritten){
+    pushBack(x, rewritten);
+
+    c->setEqualityEngineProof();
+    if(c->canBePropagated() && !c->assertedToTheTheory()){
+      c->propagate();
+    }
+  }else if(!c->hasProof() && x == rewritten){
+    pushBack(x, rewritten);
+    c->setEqualityEngineProof();
+  }else if(c->hasProof() && x != rewritten){
+    pushBack(x, rewritten);
+  }else{
+    Assert(c->hasProof() && x == rewritten);
+  }
+  return true;
 }
 
 void DifferenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
@@ -37,33 +145,44 @@ void DifferenceManager::explain(TNode literal, std::vector<TNode>& assumptions)
   d_ee.explainEquality(lhs, rhs, assumptions);
 }
 
-Node mkAnd(const std::vector<TNode>& conjunctions) {
-  Assert(conjunctions.size() > 0);
+void DifferenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<>& nb){
+  std::set<TNode>::const_iterator it = s.begin();
+  std::set<TNode>::const_iterator it_end = s.end();
+  for(; it != it_end; ++it) {
+    nb << *it;
+  }
+}
 
-  std::set<TNode> all;
-  all.insert(conjunctions.begin(), conjunctions.end());
+Node DifferenceManager::explainInternal(TNode internal){
+  std::vector<TNode> assumptions;
+  explain(internal, assumptions);
 
-  if (all.size() == 1) {
-    // All the same, or just one
-    return conjunctions[0];
-  }
+  std::set<TNode> assumptionSet;
+  assumptionSet.insert(assumptions.begin(), assumptions.end());
 
-  NodeBuilder<> conjunction(kind::AND);
-  std::set<TNode>::const_iterator it = all.begin();
-  std::set<TNode>::const_iterator it_end = all.end();
-  while (it != it_end) {
-    conjunction << *it;
-    ++ it;
+  if (assumptionSet.size() == 1) {
+    // All the same, or just one
+    return assumptions[0];
+  }else{
+    NodeBuilder<> conjunction(kind::AND);
+    enqueueIntoNB(assumptionSet, conjunction);
+    return conjunction;
   }
-
-  return conjunction;
+}
+Node DifferenceManager::explain(TNode external){
+  Node internal = externalToInternal(external);
+  return explainInternal(internal);
 }
 
+void DifferenceManager::explain(TNode external, NodeBuilder<>& out){
+  Node internal = externalToInternal(external);
 
-Node DifferenceManager::explain(TNode lit){
   std::vector<TNode> assumptions;
-  explain(lit, assumptions);
-  return mkAnd(assumptions);
+  explain(internal, assumptions);
+  std::set<TNode> assumptionSet;
+  assumptionSet.insert(assumptions.begin(), assumptions.end());
+
+  enqueueIntoNB(assumptionSet, out);
 }
 
 void DifferenceManager::addDifference(ArithVar s, Node x, Node y){
@@ -90,7 +209,7 @@ void DifferenceManager::addAssertionToEqualityEngine(bool eq, ArithVar s, TNode
 
 void DifferenceManager::dequeueLiterals(){
   Assert(d_hasSharedTerms);
-  while(!d_literalsQueue.empty()){
+  while(!d_literalsQueue.empty() && !inConflict()){
     const LiteralsQueueElem& front = d_literalsQueue.front();
     d_literalsQueue.dequeue();