1 files changed, 208 insertions, 77 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 50d4fb633..390cb60aa 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1,6 +1,7 @@
 #include "expr/node.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
+#include "expr/node_builder.h"
 
 #include "util/rational.h"
 #include "util/integer.h"
@@ -12,11 +13,13 @@
 #include "theory/arith/tableau.h"
 #include "theory/arith/normal.h"
 #include "theory/arith/slack.h"
+#include "theory/arith/basic.h"
 
 #include "theory/arith/arith_rewriter.h"
 
 #include "theory/arith/theory_arith.h"
 #include <map>
+#include <stdint.h>
 
 using namespace std;
 
@@ -26,10 +29,33 @@ using namespace CVC4::kind;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
+TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
+  Theory(c, out),
+  d_constants(NodeManager::currentNM()),
+  d_partialModel(c),
+  d_diseq(c),
+  d_preprocessed(c),
+  d_rewriter(&d_constants)
+{
+  uint64_t ass_id = partial_model::Assignment::getId();
+  Debug("arithsetup") << "Assignment: " << ass_id
+                      << std::endl;
+}
+
 
 bool isBasicSum(TNode n){
-  Unimplemented();
-  return false;
+  if(n.getKind() != kind::PLUS) return false;
+
+  for(TNode::const_iterator i=n.begin(); i!=n.end(); ++i){
+    TNode child = *i;
+    if(child.getKind() != MULT) return false;
+    if(child[0].getKind() != CONST_RATIONAL) return false;
+    for(unsigned j=1; j<child.getNumChildren(); ++j){
+      TNode var = child[j];
+      if(var.getMetaKind() != metakind::VARIABLE) return false;
+    }
+  }
+  return true;
 }
 
 Kind multKind(Kind k){
@@ -47,17 +73,33 @@ Kind multKind(Kind k){
 
 
 void registerAtom(TNode rel){
-  addBound(rel);
+  //addBound(rel);
   //Anything else?
 }
 
 Node TheoryArith::rewrite(TNode n){
-  return d_rewriter.rewrite(n);
+  Debug("arith") << "rewrite(" << n << ")" << endl;
+
+  Node result = d_rewriter.rewrite(n);
+  Debug("arith-rewrite") << "rewrite("
+                         << n << " -> " << result
+                         << ")" << endl;
+  return result;
 }
 
 void TheoryArith::registerTerm(TNode tn){
-  if(tn.isAtomic()){
+  Debug("arith") << "registerTerm(" << tn << ")" << endl;
+
+  if(tn.getKind() == kind::BUILTIN) return;
+
+  if(tn.getMetaKind() == metakind::VARIABLE){
+    d_partialModel.setAssignment(tn,d_constants.d_ZERO_DELTA);
+  }
+
+  //TODO is an atom
+  if(isRelationOperator(tn.getKind())){
     Node normalForm = (isNormalized(tn)) ? Node(tn) : rewrite(tn);
+    normalForm = (normalForm.getKind() == NOT) ? pushInNegation(normalForm):normalForm;
     Kind k = normalForm.getKind();
 
     if(k != kind::CONST_BOOLEAN){
@@ -71,7 +113,9 @@ void TheoryArith::registerTerm(TNode tn){
         Node slack;
         if(!left.getAttribute(Slack(), slack)){
           //TODO
-          //slack = NodeManager::currentNM()->mkVar(RealType());
+          TypeNode real_type = NodeManager::currentNM()->realType();
+          slack = NodeManager::currentNM()->mkVar(real_type);
+          d_partialModel.setAssignment(slack,d_constants.d_ZERO_DELTA);
           left.setAttribute(Slack(), slack);
           makeBasic(slack);
 
@@ -81,10 +125,13 @@ void TheoryArith::registerTerm(TNode tn){
           d_out->lemma(slackEqLeft);
 
           d_tableau.addRow(slackEqLeft);
-        }
 
-        Node rewritten = NodeManager::currentNM()->mkNode(k,slack,right);
-        registerAtom(rewritten);
+          Node rewritten = NodeManager::currentNM()->mkNode(k,slack,right);
+          registerAtom(rewritten);
+        }else{
+          Node rewritten = NodeManager::currentNM()->mkNode(k,slack,right);
+          registerAtom(rewritten);
+        }
       }else{
         Assert(left.getMetaKind() == metakind::VARIABLE);
         Assert(right.getKind() == CONST_RATIONAL);
@@ -95,48 +142,56 @@ void TheoryArith::registerTerm(TNode tn){
 }
 
 /* procedure AssertUpper( x_i <= c_i) */
-void TheoryArith::AssertUpper(TNode n){
+void TheoryArith::AssertUpper(TNode n, TNode original){
   TNode x_i = n[0];
   Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
   DeltaRational c_i(n[1].getConst<Rational>(), dcoeff);
 
-  if(aboveUpperBound(x_i, c_i, false) ){
+
+  Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
+
+
+  if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){
     return; //sat
   }
-  if(belowLowerBound(x_i, c_i, true)){
-    d_out->conflict(n);
+  if(d_partialModel.belowLowerBound(x_i, c_i, true)){
+    Node conflict =  NodeManager::currentNM()->mkNode(AND, d_partialModel.getLowerConstraint(x_i), original);
+    d_out->conflict(conflict);
     return;
   }
 
-  setUpperConstraint(n);
-  setUpperBound(x_i, c_i);
+  d_partialModel.setUpperConstraint(x_i,original);
+  d_partialModel.setUpperBound(x_i, c_i);
 
   if(!isBasic(x_i)){
-    if(getAssignment(x_i) > c_i){
+    if(d_partialModel.getAssignment(x_i) > c_i){
       update(x_i, c_i);
     }
   }
 }
 
 /* procedure AssertLower( x_i >= c_i ) */
-void TheoryArith::AssertLower(TNode n){
+void TheoryArith::AssertLower(TNode n, TNode orig){
   TNode x_i = n[0];
   Rational dcoeff = Rational(Integer(deltaCoeff(n.getKind())));
   DeltaRational c_i(n[1].getConst<Rational>(),dcoeff);
 
-  if(belowLowerBound(x_i, c_i, false)){
+  Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
+
+  if(d_partialModel.belowLowerBound(x_i, c_i, false)){
     return; //sat
   }
-  if(aboveUpperBound(x_i, c_i, true)){
-    d_out->conflict(n);
+  if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
+    Node conflict =  NodeManager::currentNM()->mkNode(AND, d_partialModel.getUpperConstraint(x_i), orig);
+    d_out->conflict(conflict);
     return;
   }
 
-  setLowerConstraint(n);
-  setLowerBound(x_i, c_i);
+  d_partialModel.setLowerConstraint(x_i,orig);
+  d_partialModel.setLowerBound(x_i, c_i);
 
   if(!isBasic(x_i)){
-    if(getAssignment(x_i) > c_i){
+    if(d_partialModel.getAssignment(x_i) < c_i){
       update(x_i, c_i);
     }
   }
@@ -144,7 +199,10 @@ void TheoryArith::AssertLower(TNode n){
 
 void TheoryArith::update(TNode x_i, DeltaRational& v){
 
-  DeltaRational assignment_x_i = getAssignment(x_i);
+  DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
+
+  Debug("arith") <<"update " << x_i << ": "
+                 << assignment_x_i << "|-> " << v << endl;
   DeltaRational diff = v - assignment_x_i;
 
   for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
@@ -155,29 +213,29 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){
 
     Rational& a_ji = row_j->lookup(x_i);
 
-    DeltaRational assignment = getAssignment(x_j);
+    DeltaRational assignment = d_partialModel.getAssignment(x_j);
     DeltaRational  nAssignment = assignment+(diff * a_ji);
-    setAssignment(x_j, nAssignment);
+    d_partialModel.setAssignment(x_j, nAssignment);
   }
 
-  setAssignment(x_i, v);
+  d_partialModel.setAssignment(x_i, v);
 }
 
 void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
   Row* row_i = d_tableau.lookup(x_i);
-  Rational& a_ij = row_i->lookup(x_i);
+  Rational& a_ij = row_i->lookup(x_j);
 
 
-  DeltaRational betaX_i = getAssignment(x_i);
+  DeltaRational betaX_i = d_partialModel.getAssignment(x_i);
 
   Rational inv_aij = a_ij.inverse();
   DeltaRational theta = (v - betaX_i)*inv_aij;
 
-  setAssignment(x_i, v);
+  d_partialModel.setAssignment(x_i, v);
 
 
-  DeltaRational tmp = getAssignment(x_j) + theta;
-  setAssignment(x_j, tmp);
+  DeltaRational tmp = d_partialModel.getAssignment(x_j) + theta;
+  d_partialModel.setAssignment(x_j, tmp);
 
   for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
       basicIter != d_tableau.end();
@@ -187,8 +245,8 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
 
     if(x_k != x_i){
       DeltaRational a_kj = row_k->lookup(x_j);
-      DeltaRational nextAssignment = getAssignment(x_k) + theta;
-      setAssignment(x_k, nextAssignment);
+      DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + theta;
+      d_partialModel.setAssignment(x_k, nextAssignment);
     }
   }
 
@@ -202,7 +260,7 @@ TNode TheoryArith::selectSmallestInconsistentVar(){
       ++basicIter){
 
     TNode basic = *basicIter;
-    if(!assignmentIsConsistent(basic)){
+    if(!d_partialModel.assignmentIsConsistent(basic)){
       return basic;
     }
   }
@@ -219,12 +277,10 @@ TNode TheoryArith::selectSlackBelow(TNode x_i){ //beta(x_i) < l_i
     TNode nonbasic = *nbi;
 
     Rational a_ij = row_i->lookup(nonbasic);
-    if(a_ij > d_constants.d_ZERO && strictlyBelowUpperBound(nonbasic)){
+    if(a_ij > d_constants.d_ZERO && d_partialModel.strictlyBelowUpperBound(nonbasic)){
       return nonbasic;
-    }else if(a_ij < d_constants.d_ZERO && strictlyAboveLowerBound(nonbasic)){
+    }else if(a_ij < d_constants.d_ZERO && d_partialModel.strictlyAboveLowerBound(nonbasic)){
       return nonbasic;
-    }else{
-      Unreachable();
     }
   }
   return TNode::null();
@@ -239,38 +295,43 @@ TNode TheoryArith::selectSlackAbove(TNode x_i){ // beta(x_i) > u_i
     TNode nonbasic = *nbi;
 
     Rational a_ij = row_i->lookup(nonbasic);
-    if(a_ij < d_constants.d_ZERO && strictlyBelowUpperBound(nonbasic)){
+    if(a_ij < d_constants.d_ZERO && d_partialModel.strictlyBelowUpperBound(nonbasic)){
       return nonbasic;
-    }else if(a_ij > d_constants.d_ZERO && strictlyAboveLowerBound(nonbasic)){
+    }else if(a_ij > d_constants.d_ZERO && d_partialModel.strictlyAboveLowerBound(nonbasic)){
       return nonbasic;
-    }else{
-      Unreachable();
     }
   }
+
   return TNode::null();
 }
 
 
-TNode TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
+Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
+  Debug("arith") << "updateInconsistentVars" << endl;
 
+  d_partialModel.beginRecordingAssignments();
   while(true){
     TNode x_i = selectSmallestInconsistentVar();
     if(x_i == Node::null()){
+      d_partialModel.stopRecordingAssignments(false);
       return Node::null(); //sat
     }
-    DeltaRational beta_i = getAssignment(x_i);
-    DeltaRational l_i = getLowerBound(x_i);
-    DeltaRational u_i = getUpperBound(x_i);
-    if(belowLowerBound(x_i, beta_i, true)){
+    DeltaRational beta_i = d_partialModel.getAssignment(x_i);
+
+    if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
+      DeltaRational l_i = d_partialModel.getLowerBound(x_i);
       TNode x_j = selectSlackBelow(x_i);
       if(x_j == TNode::null() ){
+        d_partialModel.stopRecordingAssignments(true);
         return generateConflictBelow(x_i); //unsat
       }
       pivotAndUpdate(x_i, x_j, l_i);
-    }else if(aboveUpperBound(x_i, beta_i, true)){
+    }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
+      DeltaRational u_i = d_partialModel.getUpperBound(x_i);
       TNode x_j = selectSlackAbove(x_i);
       if(x_j == TNode::null() ){
-        return generateConflictAbove(x_j); //unsat
+        d_partialModel.stopRecordingAssignments(true);
+        return generateConflictAbove(x_i); //unsat
       }
       pivotAndUpdate(x_i, x_j, u_i);
     }
@@ -281,7 +342,13 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){
   Row* row_i = d_tableau.lookup(conflictVar);
 
   NodeBuilder<> nb(kind::AND);
-  nb << getUpperConstraint(conflictVar);
+  TNode bound = d_partialModel.getUpperConstraint(conflictVar);
+
+  Debug("arith")  << "generateConflictAbove "
+                  << "conflictVar " << conflictVar
+                  << " " << bound << endl;
+
+  nb << bound;
 
   typedef std::set<TNode>::iterator NonBasicIter;
 
@@ -292,19 +359,29 @@ Node TheoryArith::generateConflictAbove(TNode conflictVar){
     Assert(a_ij != d_constants.d_ZERO);
 
     if(a_ij < d_constants.d_ZERO){
-      nb << getUpperConstraint(nonbasic);
+      bound =  d_partialModel.getUpperConstraint(nonbasic);
+      Debug("arith") << "below 0 "<< nonbasic << " " << bound << endl;
+      nb << bound;
     }else{
-      nb << getLowerConstraint(nonbasic);
+      bound =  d_partialModel.getLowerConstraint(nonbasic);
+      Debug("arith") << " above 0 "<< nonbasic << " " << bound << endl;
+      nb << bound;
     }
   }
   Node conflict = nb;
   return conflict;
 }
+
 Node TheoryArith::generateConflictBelow(TNode conflictVar){
   Row* row_i = d_tableau.lookup(conflictVar);
 
   NodeBuilder<> nb(kind::AND);
-  nb << getLowerConstraint(conflictVar);
+  TNode bound = d_partialModel.getLowerConstraint(conflictVar);
+
+  Debug("arith") << "generateConflictBelow "
+                 << "conflictVar " << conflictVar
+                 << " " << bound << endl;
+  nb << bound;
 
   typedef std::set<TNode>::iterator NonBasicIter;
 
@@ -315,40 +392,92 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){
     Assert(a_ij != d_constants.d_ZERO);
 
     if(a_ij < d_constants.d_ZERO){
-      nb << getLowerConstraint(nonbasic);
+      TNode bound = d_partialModel.getLowerConstraint(nonbasic);
+      Debug("arith") << "Lower "<< nonbasic << " " << bound << endl;
+
+      nb << bound;
     }else{
-      nb << getUpperConstraint(nonbasic);
+      TNode bound = d_partialModel.getUpperConstraint(nonbasic);
+      Debug("arith") << "Upper "<< nonbasic << " " << bound << endl;
+
+      nb << bound;
     }
   }
-  Node conflict = nb;
+  Node conflict (nb.constructNode());
   return conflict;
 }
 
+//TODO get rid of this!
+Node TheoryArith::simulatePreprocessing(TNode n){
+  if(n.getKind() == NOT){
+    Node sub = simulatePreprocessing(n[0]);
+    return NodeManager::currentNM()->mkNode(NOT,sub);
+  }else{
+    Node rewritten = rewrite(n);
+    Kind k = rewritten.getKind();
+    if(!isRelationOperator(k)){
+      return rewritten;
+    }else if(rewritten[0].getMetaKind() == metakind::VARIABLE){
+      return rewritten;
+    }else {
+      TNode left = rewritten[0];
+      TNode right = rewritten[1];
+      Node slack;
+      if(!left.getAttribute(Slack(), slack)){
+        Unreachable("Slack must be have been created!");
+      }else{
+        return NodeManager::currentNM()->mkNode(k,slack,right);
+      }
+    }
+  }
+}
+
 void TheoryArith::check(Effort level){
+  Debug("arith") << "TheoryArith::check begun" << std::endl;
+
   while(!done()){
-    Node assertion = get();
+    Node original = get();
+    Node assertion = simulatePreprocessing(original);
+    Debug("arith") << "arith assertion(" << original
+                   << " \\-> " << assertion << ")" << std::endl;
 
-    if(assertion.getKind() == NOT){
-      assertion = pushInNegation(assertion);
-    }
+    d_preprocessed.push_back(assertion);
 
     switch(assertion.getKind()){
-    case LT:
     case LEQ:
-      AssertUpper(assertion);
+      AssertUpper(assertion, original);
       break;
     case GEQ:
-    case GT:
-      AssertLower(assertion);
+      AssertLower(assertion, original);
       break;
     case EQUAL:
-      AssertUpper(assertion);
-      AssertLower(assertion);
+      AssertUpper(assertion, original);
+      AssertLower(assertion, original);
       break;
     case NOT:
-      Assert(assertion[0].getKind() == EQUAL);
-      d_diseq.push_back(assertion);
-      break;
+      {
+        TNode atom = assertion[0];
+        switch(atom.getKind()){
+        case LEQ: //(not (LEQ x c)) <=> (GT x c)
+          {
+            Node pushedin = pushInNegation(assertion);
+            AssertLower(pushedin,original);
+            break;
+          }
+        case GEQ: //(not (GEQ x c) <=> (LT x c)
+          {
+            Node pushedin = pushInNegation(assertion);
+            AssertUpper(pushedin,original);
+            break;
+          }
+        case EQUAL:
+          d_diseq.push_back(assertion);
+          break;
+        default:
+          Unhandled();
+        }
+        break;
+      }
     default:
       Unhandled();
     }
@@ -357,12 +486,13 @@ void TheoryArith::check(Effort level){
   if(fullEffort(level)){
     Node possibleConflict = updateInconsistentVars();
     if(possibleConflict != Node::null()){
+      Debug("arith") << "Found a conflict " << possibleConflict << endl;
       d_out->conflict(possibleConflict);
     }
   }
 
   if(fullEffort(level)){
-    NodeBuilder<> lemmas(AND);
+    bool enqueuedCaseSplit = false;
     typedef context::CDList<Node>::const_iterator diseq_iterator;
     for(diseq_iterator i = d_diseq.begin(); i!= d_diseq.end(); ++i){
       Node assertion = *i;
@@ -370,15 +500,16 @@ void TheoryArith::check(Effort level){
       TNode x_i = eq[0];
       TNode c_i = eq[1];
       DeltaRational constant =  c_i.getConst<Rational>();
-      if(getAssignment(x_i) == constant){
+      if(d_partialModel.getAssignment(x_i) == constant){
+        enqueuedCaseSplit = true;
         Node lt = NodeManager::currentNM()->mkNode(LT,x_i,c_i);
         Node gt = NodeManager::currentNM()->mkNode(GT,x_i,c_i);
-        Node disjunct = NodeManager::currentNM()->mkNode(OR, eq, lt, gt);
-        lemmas<< disjunct;
+        Node caseSplit = NodeManager::currentNM()->mkNode(OR, eq, lt, gt);
+        //d_out->enqueueCaseSplits(caseSplit);
       }
     }
-    Node caseSplits = lemmas;
-    //TODO
-    //DemandCaseSplits(caseSplits);
+    if(enqueuedCaseSplit){
+      //d_out->caseSplit();
+    }
   }
 }