Reverts previous commit r1636.

4 files changed, 23 insertions, 47 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 524cdcafe..c22b0019d 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -66,7 +66,7 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valu
   d_presolveHasBeenCalled(false),
   d_tableauResetDensity(1.6),
   d_tableauResetPeriod(10),
-  d_propagator(c),
+  d_propagator(c, out),
   d_simplex(d_partialModel, d_tableau),
   d_DELTA_ZERO(0),
   d_statistics()
@@ -86,9 +86,7 @@ TheoryArith::Statistics::Statistics():
   //d_tableauSizeHistory("theory::arith::tableauSizeHistory"),
   d_currSetToSmaller("theory::arith::currSetToSmaller", 0),
   d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0),
-  d_restartTimer("theory::arith::restartTimer"),
-  d_diseqSplitCalls("theory::arith::diseqSplitCalls", 0),
-  d_diseqSplitTimer("theory::arith::diseqSplitTimer")
+  d_restartTimer("theory::arith::restartTimer")
 {
   StatisticsRegistry::registerStat(&d_statUserVariables);
   StatisticsRegistry::registerStat(&d_statSlackVariables);
@@ -105,9 +103,6 @@ TheoryArith::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_currSetToSmaller);
   StatisticsRegistry::registerStat(&d_smallerSetToCurr);
   StatisticsRegistry::registerStat(&d_restartTimer);
-
-  StatisticsRegistry::registerStat(&d_diseqSplitCalls);
-  StatisticsRegistry::registerStat(&d_diseqSplitTimer);
 }
 
 TheoryArith::Statistics::~Statistics(){
@@ -126,9 +121,6 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_currSetToSmaller);
   StatisticsRegistry::unregisterStat(&d_smallerSetToCurr);
   StatisticsRegistry::unregisterStat(&d_restartTimer);
-
-  StatisticsRegistry::unregisterStat(&d_diseqSplitCalls);
-  StatisticsRegistry::unregisterStat(&d_diseqSplitTimer);
 }
 
 void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) {
@@ -176,15 +168,21 @@ void TheoryArith::preRegisterTerm(TNode n) {
     setupInitialValue(varN);
   }
 
-  if(n.getKind() == PLUS){
-    Assert(!n.hasAttribute(Slack()));
-    setupSlack(n);
-  }
-
   if(isRelationOperator(k)){
     Assert(Comparison::isNormalAtom(n));
-    Assert(n[0].getKind() != PLUS || (n[0]).hasAttribute(Slack()) );
+
+
     d_propagator.addAtom(n);
+
+    TNode left  = n[0];
+    TNode right = n[1];
+    if(left.getKind() == PLUS){
+      //We may need to introduce a slack variable.
+      Assert(left.getNumChildren() >= 2);
+      if(!left.hasAttribute(Slack())){
+        setupSlack(left);
+      }
+    }
   }
   Debug("arith_preregister") << "end arith::preRegisterTerm("<< n <<")"<< endl;
 }
@@ -421,9 +419,6 @@ void TheoryArith::check(Effort effortLevel){
 }
 
 void TheoryArith::splitDisequalities(){
-  TimerStat::CodeTimer codeTimer(d_statistics.d_diseqSplitTimer);
-  ++(d_statistics.d_diseqSplitCalls);
-
   context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
   context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
   for(; it != it_end; ++ it) {
@@ -498,11 +493,6 @@ void TheoryArith::explain(TNode n) {
 }
 
 void TheoryArith::propagate(Effort e) {
-  while(d_propagator.hasMoreLemmas()){
-    Node lemma = d_propagator.getNextLemma();
-    d_out->lemma(lemma);
-  }
-
   if(quickCheckOrMore(e)){
     while(d_simplex.hasMoreLemmas()){
       Node lemma = d_simplex.popLemma();
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index bba2d19c0..85f554849 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -255,9 +255,6 @@ private:
     IntStat d_smallerSetToCurr;
     TimerStat d_restartTimer;
 
-    IntStat d_diseqSplitCalls;
-    TimerStat d_diseqSplitTimer;
-
     Statistics();
     ~Statistics();
   };
diff --git a/src/theory/arith/unate_propagator.cpp b/src/theory/arith/unate_propagator.cpp
index 9c7946712..069f4f0f3 100644
--- a/src/theory/arith/unate_propagator.cpp
+++ b/src/theory/arith/unate_propagator.cpp
@@ -30,8 +30,8 @@ using namespace CVC4::kind;
 
 using namespace std;
 
-ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt) :
-  d_orderedListMap()
+ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt, OutputChannel& out) :
+  d_arithOut(out), d_orderedListMap()
 { }
 
 bool ArithUnatePropagator::leftIsSetup(TNode left){
@@ -393,5 +393,5 @@ void ArithUnatePropagator::addImplication(TNode a, TNode b){
   Debug("arith-propagate") << "ArithUnatePropagator::addImplication";
   Debug("arith-propagate") << "(" << a << ", " << b <<")" << endl;
 
-  addLemma(imp);
+  d_arithOut.lemma(imp);
 }
diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h
index ce78f281a..383b9f8e8 100644
--- a/src/theory/arith/unate_propagator.h
+++ b/src/theory/arith/unate_propagator.h
@@ -55,7 +55,6 @@
 #include "theory/arith/ordered_set.h"
 
 #include <ext/hash_map>
-#include <queue>
 
 namespace CVC4 {
 namespace theory {
@@ -63,9 +62,11 @@ namespace arith {
 
 class ArithUnatePropagator {
 private:
-  typedef std::queue<Node> LemmaQueue;
-  /** Unate implication queue */
-  LemmaQueue d_lemmas;
+  /**
+   * OutputChannel for the theory of arithmetic.
+   * The propagator uses this to pass implications back to the SAT solver.
+   */
+  OutputChannel& d_arithOut;
 
   struct OrderedSetTriple {
     OrderedSet d_leqSet;
@@ -78,7 +79,7 @@ private:
   NodeToOrderedSetMap d_orderedListMap;
 
 public:
-  ArithUnatePropagator(context::Context* cxt);
+  ArithUnatePropagator(context::Context* cxt, OutputChannel& arith);
 
   /**
    * Adds an atom to the propagator.
@@ -89,19 +90,7 @@ public:
   /** Returns true if v has been added as a left hand side in an atom */
   bool hasAnyAtoms(TNode v);
 
-  bool hasMoreLemmas() const { return !d_lemmas.empty(); }
-
-  Node getNextLemma() {
-    Node lemma = d_lemmas.front();
-    d_lemmas.pop();
-    return lemma;
-  }
 private:
-  void addLemma(Node lemma) {
-    d_lemmas.push(lemma);
-  }
-
-
   OrderedSetTriple& getOrderedSetTriple(TNode left);
   OrderedSet& getEqSet(TNode left);
   OrderedSet& getLeqSet(TNode left);