Delayed the addition of unate propagation lemmas until propagation is called. The OutputChannel is now untouched by TheoryArith during preregistration.

5 files changed, 79 insertions, 23 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index c22b0019d..524cdcafe 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, out),
+  d_propagator(c),
   d_simplex(d_partialModel, d_tableau),
   d_DELTA_ZERO(0),
   d_statistics()
@@ -86,7 +86,9 @@ 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_restartTimer("theory::arith::restartTimer"),
+  d_diseqSplitCalls("theory::arith::diseqSplitCalls", 0),
+  d_diseqSplitTimer("theory::arith::diseqSplitTimer")
 {
   StatisticsRegistry::registerStat(&d_statUserVariables);
   StatisticsRegistry::registerStat(&d_statSlackVariables);
@@ -103,6 +105,9 @@ 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(){
@@ -121,6 +126,9 @@ 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) {
@@ -168,21 +176,15 @@ 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;
 }
@@ -419,6 +421,9 @@ 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) {
@@ -493,6 +498,11 @@ 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 85f554849..bba2d19c0 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -255,6 +255,9 @@ 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 069f4f0f3..9c7946712 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, OutputChannel& out) :
-  d_arithOut(out), d_orderedListMap()
+ArithUnatePropagator::ArithUnatePropagator(context::Context* cxt) :
+  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;
 
-  d_arithOut.lemma(imp);
+  addLemma(imp);
 }
diff --git a/src/theory/arith/unate_propagator.h b/src/theory/arith/unate_propagator.h
index 383b9f8e8..ce78f281a 100644
--- a/src/theory/arith/unate_propagator.h
+++ b/src/theory/arith/unate_propagator.h
@@ -55,6 +55,7 @@
 #include "theory/arith/ordered_set.h"
 
 #include <ext/hash_map>
+#include <queue>
 
 namespace CVC4 {
 namespace theory {
@@ -62,11 +63,9 @@ namespace arith {
 
 class ArithUnatePropagator {
 private:
-  /**
-   * OutputChannel for the theory of arithmetic.
-   * The propagator uses this to pass implications back to the SAT solver.
-   */
-  OutputChannel& d_arithOut;
+  typedef std::queue<Node> LemmaQueue;
+  /** Unate implication queue */
+  LemmaQueue d_lemmas;
 
   struct OrderedSetTriple {
     OrderedSet d_leqSet;
@@ -79,7 +78,7 @@ private:
   NodeToOrderedSetMap d_orderedListMap;
 
 public:
-  ArithUnatePropagator(context::Context* cxt, OutputChannel& arith);
+  ArithUnatePropagator(context::Context* cxt);
 
   /**
    * Adds an atom to the propagator.
@@ -90,7 +89,19 @@ 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 9de8f94b4..65437ba0e 100644
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -159,6 +159,8 @@ 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);
@@ -196,6 +198,9 @@ 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;
@@ -230,6 +235,8 @@ 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);
@@ -247,4 +254,29 @@ 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);
+  }
 };