From 9450e5841a08db3a9529c25e03fc5cea16a8f1f5 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Tue, 28 Feb 2012 20:42:55 +0000
Subject: [PATCH] Improves the arithmetic difference manager to delay any work
 until a shared term is added.

---
 src/theory/arith/difference_manager.cpp | 44 ++++++++++++++++++-------
 src/theory/arith/difference_manager.h   | 42 +++++++++++++++++++++--
 2 files changed, 71 insertions(+), 15 deletions(-)

diff --git a/src/theory/arith/difference_manager.cpp b/src/theory/arith/difference_manager.cpp
index ea2d411b7..b0ea55dec 100644
--- a/src/theory/arith/difference_manager.cpp
+++ b/src/theory/arith/difference_manager.cpp
@@ -6,11 +6,12 @@ namespace theory {
 namespace arith {
 
 DifferenceManager::DifferenceManager(context::Context* c, PropManager& pm)
-  : d_reasons(c),
+  : d_literalsQueue(c),
     d_queue(pm),
     d_notify(*this),
     d_ee(d_notify, c, "theory::arith::DifferenceManager"),
-    d_false(NodeManager::currentNM()->mkConst<bool>(false))
+    d_false(NodeManager::currentNM()->mkConst<bool>(false)),
+    d_hasSharedTerms(c, false)
 {}
 
 void DifferenceManager::propagate(TNode x){
@@ -36,7 +37,6 @@ void DifferenceManager::explain(TNode literal, std::vector<TNode>& assumptions)
   d_ee.explainEquality(lhs, rhs, assumptions);
 }
 
-#warning "Stolen from theory_uf.h verbatim. Generalize me!"
 Node mkAnd(const std::vector<TNode>& conjunctions) {
   Assert(conjunctions.size() > 0);
 
@@ -75,25 +75,45 @@ void DifferenceManager::addDifference(ArithVar s, Node x, Node y){
   d_differences[s] = Difference(x,y);
 }
 
-void DifferenceManager::differenceIsZero(ArithVar s, TNode reason){
+void DifferenceManager::addAssertionToEqualityEngine(bool eq, ArithVar s, TNode reason){
   Assert(isDifferenceSlack(s));
+
   TNode x = d_differences[s].x;
   TNode y = d_differences[s].y;
 
-  d_reasons.push_back(reason);
-  d_ee.addEquality(x, y, reason);
+  if(eq){
+    d_ee.addEquality(x, y, reason);
+  }else{
+    d_ee.addDisequality(x, y, reason);
+  }
 }
 
-void DifferenceManager::differenceCannotBeZero(ArithVar s, TNode reason){
-  Assert(isDifferenceSlack(s));
-  TNode x = d_differences[s].x;
-  TNode y = d_differences[s].y;
+void DifferenceManager::dequeueLiterals(){
+  Assert(d_hasSharedTerms);
+  while(!d_literalsQueue.empty()){
+    const LiteralsQueueElem& front = d_literalsQueue.dequeue();
+
+    addAssertionToEqualityEngine(front.d_eq, front.d_var, front.d_reason);
+  }
+}
+
+void DifferenceManager::enableSharedTerms(){
+  Assert(!d_hasSharedTerms);
+  d_hasSharedTerms = true;
+  dequeueLiterals();
+}
 
-  d_reasons.push_back(reason);
-  d_ee.addDisequality(x, y, reason);
+void DifferenceManager::assertLiteral(bool eq, ArithVar s, TNode reason){
+  d_literalsQueue.enqueue(LiteralsQueueElem(eq, s, reason));
+  if(d_hasSharedTerms){
+    dequeueLiterals();
+  }
 }
 
 void DifferenceManager::addSharedTerm(Node x){
+  if(!d_hasSharedTerms){
+    enableSharedTerms();
+  }
   d_ee.addTriggerTerm(x);
 }
 
diff --git a/src/theory/arith/difference_manager.h b/src/theory/arith/difference_manager.h
index 01f42dcfe..d8a0e2c1c 100644
--- a/src/theory/arith/difference_manager.h
+++ b/src/theory/arith/difference_manager.h
@@ -10,6 +10,7 @@
 #include "context/cdo.h"
 #include "context/cdlist.h"
 #include "context/context.h"
+#include "context/cdqueue.h"
 #include "util/stats.h"
 #include "theory/arith/arith_prop_manager.h"
 
@@ -52,7 +53,16 @@ private:
 
   std::vector< Difference > d_differences;
 
-  context::CDList<Node> d_reasons;
+  struct LiteralsQueueElem {
+    bool d_eq;
+    ArithVar d_var;
+    Node d_reason;
+    LiteralsQueueElem() : d_eq(false), d_var(ARITHVAR_SENTINEL), d_reason() {}
+    LiteralsQueueElem(bool eq, ArithVar v, Node n) : d_eq(eq), d_var(v), d_reason(n) {}
+  };
+
+  /** Stores the queue of assertions. This keeps the Node backing the reasons */
+  context::CDQueue<LiteralsQueueElem> d_literalsQueue;
   PropManager& d_queue;
 
 
@@ -64,6 +74,28 @@ private:
 
   Node d_false;
 
+  /**
+   * This is set to true when the first shared term is added.
+   * When this is set to true in the context, d_queue is emptied
+   * and not used again in the context.
+   */
+  context::CDO<bool> d_hasSharedTerms;
+
+
+  /**
+   * The generalization of asserting an equality or a disequality.
+   * If there are shared equalities, this is added to the equality engine.
+   * Otherwise, this is put on a queue until there is a shared term.
+   */
+  void assertLiteral(bool eq, ArithVar s, TNode reason);
+
+  /** This sends a shared term to the uninterpretted equality engine. */
+  void addAssertionToEqualityEngine(bool eq, ArithVar s, TNode reason);
+
+  /** Dequeues the delay queue and asserts these equalities.*/
+  void enableSharedTerms();
+  void dequeueLiterals();
+
 public:
 
   DifferenceManager(context::Context*, PropManager&);
@@ -80,9 +112,13 @@ public:
     }
   }
 
-  void differenceIsZero(ArithVar s, TNode reason);
+  void differenceIsZero(ArithVar s, TNode reason){
+    assertLiteral(true, s, reason);
+  }
 
-  void differenceCannotBeZero(ArithVar s, TNode reason);
+  void differenceCannotBeZero(ArithVar s, TNode reason){
+    assertLiteral(false, s, reason);
+  }
 
   void addSharedTerm(Node x);
 };/* class DifferenceManager */
-- 
2.30.2