Reverts previous commit r1636.

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 524cdcafeba211f24cc03726048c1114bb5f6bb5..c22b0019d9cdf70625bbbe36600215ae10eb5a9f 100644 (file)
--- 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 bba2d19c03bb4e5f0430805c6d988c7626708030..85f55484962ad3de096b02ae93e32c33cd0a3660 100644 (file)
--- 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 9c79467124cc2bb41710dd7748c0390d3f3f4baf..069f4f0f33a974e0c872c02e4097126cebbf7716 100644 (file)
--- 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 ce78f281aab58c794301bd391b02db473b807e35..383b9f8e82eb71159b78ef65353314510fb4c791 100644 (file)
--- 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);

diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index 65437ba0ea37b589dce6d9b5875c59a8d77c31c3..9de8f94b40265183d151089eaf0701fb41a977b7 100644 (file)
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -159,8 +159,6 @@ public:
 
 
     d_arith->check(d_level);
-    TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u);
-
     d_arith->propagate(d_level);
 
     Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1);
@@ -198,9 +196,6 @@ public:
 
 
     d_arith->check(d_level);
-    TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u);
-
-    d_arith->propagate(d_level);
 
     Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1);
     Node lt1ThenLeq1  = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
@@ -235,8 +230,6 @@ public:
 
 
     d_arith->check(d_level);
-    TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u);
-
     d_arith->propagate(d_level);
 
     Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1);
@@ -254,29 +247,4 @@ public:
     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1);
   }
-
-  void testConflict() {
-    Node x = d_nm->mkVar(*d_realType);
-    Node c0 = d_nm->mkConst<Rational>(d_zero);
-    Node c1 = d_nm->mkConst<Rational>(d_one);
-
-    Node leq0 = d_nm->mkNode(LEQ, x, c0);
-    Node leq1 = d_nm->mkNode(LEQ, x, c1);
-    Node gt1 =  d_nm->mkNode(NOT, leq1);
-
-    fakeTheoryEnginePreprocess(leq0);
-    fakeTheoryEnginePreprocess(leq1);
-
-    d_arith->assertFact(leq0);
-    d_arith->assertFact(gt1);
-
-    d_arith->check(d_level);
-
-
-    Node conf =  d_nm->mkNode(AND, leq0, gt1);
-    TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 1u);
-
-    TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), CONFLICT);
-    TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), conf);
-  }
 };