Lemmas on demand work, push-pop, some cleanup.

3 files changed, 88 insertions, 32 deletions

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index d50c48552..25aff4e75 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -237,10 +237,12 @@ inline int deltaCoeff(Kind k){
       case  kind::EQUAL:
         return  kind::DISTINCT;
       default:
+        Unreachable();
         return  kind::UNDEFINED_KIND;
       }
     }
   default:
+    Unreachable();
     return kind::UNDEFINED_KIND;
   }
 }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 181632812..7b768d9af 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -103,21 +103,8 @@ ArithVar TheoryArith::findBasicRow(ArithVar variable){
 void TheoryArith::preRegisterTerm(TNode n) {
   Debug("arith_preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl;
   Kind k = n.getKind();
-  if(k == EQUAL){
-    TNode left = n[0];
-    TNode right = n[1];
-
-    Node lt = NodeManager::currentNM()->mkNode(LT, left,right);
-    Node gt = NodeManager::currentNM()->mkNode(GT, left,right);
-    Node eagerSplit = NodeManager::currentNM()->mkNode(OR, n, lt, gt);
-
-    d_splits.push_back(eagerSplit);
 
-
-    d_out->augmentingLemma(eagerSplit);
-  }
-
-  bool isStrictlyVarList = n.getKind() == kind::MULT && VarList::isMember(n);
+  bool isStrictlyVarList = k == kind::MULT && VarList::isMember(n);
 
   if(isStrictlyVarList){
     d_out->setIncomplete();
@@ -307,15 +294,49 @@ bool TheoryArith::assertionCases(TNode assertion){
                             <<x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl;
   switch(simpKind){
   case LEQ:
+    if (d_partialModel.hasLowerBound(x_i) && d_partialModel.getLowerBound(x_i) == c_i) {
+      Node diseq = assertion[0].eqNode(assertion[1]).notNode();
+      if (d_diseq.find(diseq) != d_diseq.end()) {
+        NodeBuilder<3> conflict(kind::AND);
+        conflict << diseq << assertion << d_partialModel.getLowerConstraint(x_i);
+        d_out->conflict((TNode)conflict);
+        return true;
+      }
+    }
   case LT:
     return d_simplex.AssertUpper(x_i, c_i, assertion);
-  case GT:
   case GEQ:
+    if (d_partialModel.hasUpperBound(x_i) && d_partialModel.getUpperBound(x_i) == c_i) {
+      Node diseq = assertion[0].eqNode(assertion[1]).notNode();
+      if (d_diseq.find(diseq) != d_diseq.end()) {
+        NodeBuilder<3> conflict(kind::AND);
+        conflict << diseq << assertion << d_partialModel.getUpperConstraint(x_i);
+        d_out->conflict((TNode)conflict);
+        return true;
+      }
+    }
+  case GT:
     return d_simplex.AssertLower(x_i, c_i, assertion);
   case EQUAL:
     return d_simplex.AssertEquality(x_i, c_i, assertion);
   case DISTINCT:
-    d_diseq.push_back(assertion);
+    {
+      d_diseq.insert(assertion);
+      // Check if it conflicts with the the bounds
+      TNode eq = assertion[0];
+      Assert(eq.getKind() == kind::EQUAL);
+      TNode lhs = eq[0];
+      TNode rhs = eq[1];
+      Assert(rhs.getKind() == CONST_RATIONAL);
+      ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL);
+      DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL);
+      if (d_partialModel.hasLowerBound(lhsVar) && d_partialModel.hasUpperBound(lhsVar) &&
+          d_partialModel.getLowerBound(lhsVar) == rhsValue && d_partialModel.getUpperBound(lhsVar) == rhsValue) {
+        NodeBuilder<3> conflict(kind::AND);
+        conflict << assertion << d_partialModel.getLowerConstraint(lhsVar) << d_partialModel.getUpperConstraint(lhsVar);
+        d_out->conflict((TNode)conflict);
+      }
+    }
     return false;
   default:
     Unreachable();
@@ -323,7 +344,7 @@ bool TheoryArith::assertionCases(TNode assertion){
   }
 }
 
-void TheoryArith::check(Effort level){
+void TheoryArith::check(Effort effortLevel){
   Debug("arith") << "TheoryArith::check begun" << std::endl;
 
   while(!done()){
@@ -339,8 +360,25 @@ void TheoryArith::check(Effort level){
     }
   }
 
-  //TODO This must be done everytime for the time being
-  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+  if(Debug.isOn("arith::print_assertions") && fullEffort(effortLevel)) {
+    Debug("arith::print_assertions") << "Assertions:" << endl;
+    for (ArithVar i = 0; i < d_variables.size(); ++ i) {
+      if (d_partialModel.hasLowerBound(i)) {
+        Node lConstr = d_partialModel.getLowerConstraint(i);
+        Debug("arith::print_assertions") << lConstr.toString() << endl;
+      }
+
+      if (d_partialModel.hasUpperBound(i)) {
+        Node uConstr = d_partialModel.getUpperConstraint(i);
+        Debug("arith::print_assertions") << uConstr.toString() << endl;
+      }
+    }
+    context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
+    context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
+    for(; it != it_end; ++ it) {
+      Debug("arith::print_assertions") << *it << endl;
+    }
+  }
 
   Node possibleConflict = d_simplex.updateInconsistentVars();
   if(possibleConflict != Node::null()){
@@ -355,10 +393,36 @@ void TheoryArith::check(Effort level){
     Debug("arith_conflict") <<"Found a conflict "<< possibleConflict << endl;
   }else{
     d_partialModel.commitAssignmentChanges();
+
+    if (fullEffort(effortLevel)) {
+      context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
+      context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
+      for(; it != it_end; ++ it) {
+        TNode eq = (*it)[0];
+        Assert(eq.getKind() == kind::EQUAL);
+        TNode lhs = eq[0];
+        TNode rhs = eq[1];
+        Assert(rhs.getKind() == CONST_RATIONAL);
+        ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL);
+        if(d_tableau.isEjected(lhsVar)){
+          d_simplex.reinjectVariable(lhsVar);
+        }
+        DeltaRational lhsValue = d_partialModel.getAssignment(lhsVar);
+        DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL);
+        if (lhsValue == rhsValue) {
+          Debug("arith_lemma") << "Splitting on " << eq << endl;
+          Debug("arith_lemma") << "LHS value = " << lhsValue << endl;
+          Debug("arith_lemma") << "RHS value = " << rhsValue << endl;
+          Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs;
+          Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs;
+          Node lemma = NodeBuilder<3>(OR) << eq << ltNode << gtNode;
+          d_out->lemma(lemma);
+        }
+      }
+    }
   }
   if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
 
-
   Debug("arith") << "TheoryArith::check end" << std::endl;
 
   if(Debug.isOn("arith::print_model")) {
@@ -372,17 +436,6 @@ void TheoryArith::check(Effort level){
       Debug("arith::print_model") << endl;
     }
   }
-  if(Debug.isOn("arith::print_assertions")) {
-    Debug("arith::print_assertions") << "Assertions:" << endl;
-    for (ArithVar i = 0; i < d_variables.size(); ++ i) {
-      Node lConstr = d_partialModel.getLowerConstraint(i);
-      Debug("arith::print_assertions") << lConstr.toString() << endl;
-
-      Node uConstr = d_partialModel.getUpperConstraint(i);
-      Debug("arith::print_assertions") << uConstr.toString() << endl;
-
-    }
-  }
 }
 
 void TheoryArith::explain(TNode n, Effort e) {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index af52da444..5c65b993d 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -24,6 +24,7 @@
 #include "theory/theory.h"
 #include "context/context.h"
 #include "context/cdlist.h"
+#include "context/cdset.h"
 #include "expr/node.h"
 
 #include "theory/arith/arith_utilities.h"
@@ -86,7 +87,7 @@ private:
   /**
    * List of all of the inequalities asserted in the current context.
    */
-  context::CDList<Node> d_diseq;
+  context::CDSet<Node, NodeHashFunction> d_diseq;
 
   /**
    * The tableau for all of the constraints seen thus far in the system.