Changed how assignments are saved during check. These are now backed by an attribute. There is now a priority queue for selecting the smallest inconsistent basic variable. normal.h has been removed. A large chunk of the registerTerm() stuff has been moved into preregister. The lazy splitting code is now been commented out so that it stops showing up in profiling.

1 files changed, 172 insertions, 122 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e99a3e823..92781e0ba 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -30,7 +30,7 @@
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/tableau.h"
-#include "theory/arith/normal.h"
+//#include "theory/arith/normal.h"
 #include "theory/arith/slack.h"
 #include "theory/arith/basic.h"
 
@@ -63,7 +63,6 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
   uint64_t ass_id = partial_model::Assignment::getId();
   Debug("arithsetup") << "Assignment: " << ass_id << std::endl;
 
-  d_partialModel.beginRecordingAssignments();
 }
 TheoryArith::~TheoryArith(){
   for(vector<Node>::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){
@@ -72,6 +71,40 @@ TheoryArith::~TheoryArith(){
   }
 }
 
+bool isBasicSum(TNode n){
+  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;
+}
+
+bool isNormalAtom(TNode n){
+  
+  if(!(n.getKind() == LEQ|| n.getKind() == GEQ || n.getKind() == EQUAL)){
+    return false;
+  }
+  TNode left = n[0];
+  TNode right = n[1];
+  if(right.getKind() != CONST_RATIONAL){
+    return false;
+  }
+  if(left.getMetaKind() == metakind::VARIABLE){
+    return true;
+  }else if(isBasicSum(left)){
+    return true;
+  }else{
+    return false;
+  }
+
+}
 void TheoryArith::preRegisterTerm(TNode n) {
   Debug("arith_preregister") << "arith: begin TheoryArith::preRegisterTerm("
                              << n << ")" << endl;
@@ -98,31 +131,63 @@ void TheoryArith::preRegisterTerm(TNode n) {
     setupVariable(n);
   }
 
-  Debug("arith_preregister") << "arith: end TheoryArith::preRegisterTerm("
-                             << n << ")" << endl;
-}
+  //TODO is an atom
+  if(isRelationOperator(n.getKind())){
 
-bool isBasicSum(TNode n){
-  if(n.getKind() != kind::PLUS) return false;
+    Assert(isNormalAtom(n));
+    Node normalForm(n);
 
-  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;
+    if(normalForm.getKind() == NOT){
+      normalForm = pushInNegation(normalForm);
+    }
+    Kind k = normalForm.getKind();
+
+    if(k != kind::CONST_BOOLEAN){
+      Assert(isRelationOperator(k));
+      TNode left  = normalForm[0];
+      TNode right = normalForm[1];
+      if(left.getKind() == PLUS){
+        //We may need to introduce a slack variable.
+        Assert(left.getNumChildren() >= 2);
+        Assert(isBasicSum(left));
+        Node slack;
+        if(!left.getAttribute(Slack(), slack)){
+          //TODO
+          TypeNode real_type = NodeManager::currentNM()->realType();
+          slack = NodeManager::currentNM()->mkVar(real_type);
+
+          left.setAttribute(Slack(), slack);
+          makeBasic(slack);
+
+
+
+          Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left);
+          slackEqLeft.setAttribute(TheoryArithPropagated(), true);
+          //TODO this has to be wrong no? YES (dejan)
+          // d_out->lemma(slackEqLeft);
+
+          Debug("slack") << "slack " << slackEqLeft << endl;
+
+          d_tableau.addRow(slackEqLeft);
+
+          setupVariable(slack);
+        }
+      }
     }
   }
-  return true;
+
+  Debug("arith_preregister") << "arith: end TheoryArith::preRegisterTerm("
+                             << n << ")" << endl;
 }
 
 
 
-void registerAtom(TNode rel){
-  //addBound(rel);
-  //Anything else?
 
+void TheoryArith::checkBasicVariable(TNode basic){
+  Assert(isBasic(basic));
+  if(!d_partialModel.assignmentIsConsistent(basic)){
+    d_possiblyInconsistent.push(basic);
+  }
 }
 
 /* Requirements:
@@ -153,6 +218,8 @@ void TheoryArith::setupVariable(TNode x){
       Debug("arith_setup") << "setup("<<x<< " " <<q<<")"<<std::endl;
     }
     d_partialModel.setAssignment(x,q);
+
+    checkBasicVariable(x);
   }
   Debug("arithgc") << "setupVariable("<<x<<")"<<std::endl;
 };
@@ -185,7 +252,7 @@ DeltaRational TheoryArith::computeRowValueUsingSavedAssignment(TNode x){
   for(std::set<TNode>::iterator i = row->begin(); i != row->end();++i){
     TNode nonbasic = *i;
     Rational& coeff = row->lookup(nonbasic);
-    DeltaRational assignment = d_partialModel.getSavedAssignment(nonbasic);
+    DeltaRational assignment = d_partialModel.getSafeAssignment(nonbasic);
     sum = sum + (assignment * coeff);
   }
   return sum;
@@ -208,56 +275,6 @@ void TheoryArith::registerTerm(TNode tn){
   if(tn.getKind() == kind::BUILTIN) return;
 
 
-  //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){
-      Assert(isRelationOperator(k));
-      TNode left  = normalForm[0];
-      TNode right = normalForm[1];
-      if(left.getKind() == PLUS){
-        //We may need to introduce a slack variable.
-        Assert(left.getNumChildren() >= 2);
-        Assert(isBasicSum(left));
-        Node slack;
-        if(!left.getAttribute(Slack(), slack)){
-          //TODO
-          TypeNode real_type = NodeManager::currentNM()->realType();
-          slack = NodeManager::currentNM()->mkVar(real_type);
-
-          left.setAttribute(Slack(), slack);
-          makeBasic(slack);
-
-
-
-          Node slackEqLeft = NodeManager::currentNM()->mkNode(EQUAL,slack,left);
-          slackEqLeft.setAttribute(TheoryArithPropagated(), true);
-          //TODO this has to be wrong no? YES (dejan)
-          // d_out->lemma(slackEqLeft);
-
-          Debug("slack") << "slack " << slackEqLeft << endl;
-
-          d_tableau.addRow(slackEqLeft);
-
-          setupVariable(slack);
-
-          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);
-        registerAtom(normalForm);
-      }
-    }
-  }
 }
 
 /* procedure AssertUpper( x_i <= c_i) */
@@ -288,6 +305,8 @@ bool TheoryArith::AssertUpper(TNode n, TNode original){
     if(d_partialModel.getAssignment(x_i) > c_i){
       update(x_i, c_i);
     }
+  }else{
+    checkBasicVariable(x_i);
   }
   d_partialModel.printModel(x_i);
   return false;
@@ -319,6 +338,8 @@ bool TheoryArith::AssertLower(TNode n, TNode original){
     if(d_partialModel.getAssignment(x_i) < c_i){
       update(x_i, c_i);
     }
+  }else{
+    checkBasicVariable(x_i);
   }
   //d_partialModel.printModel(x_i);
 
@@ -326,7 +347,7 @@ bool TheoryArith::AssertLower(TNode n, TNode original){
 }
 
 void TheoryArith::update(TNode x_i, DeltaRational& v){
-
+  Assert(!isBasic(x_i));
   DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
 
   Debug("arith") <<"update " << x_i << ": "
@@ -345,6 +366,7 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){
       DeltaRational assignment = d_partialModel.getAssignment(x_j);
       DeltaRational  nAssignment = assignment+(diff * a_ji);
       d_partialModel.setAssignment(x_j, nAssignment);
+      checkBasicVariable(x_j);
     }
   }
 
@@ -383,25 +405,45 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
       Rational a_kj = row_k->lookup(x_j);
       DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
       d_partialModel.setAssignment(x_k, nextAssignment);
+      checkBasicVariable(x_k);
     }
   }
 
   d_tableau.pivot(x_i, x_j);
 
+  checkBasicVariable(x_j);
+
   if(debugTagIsOn("tableau")){
     d_tableau.printTableau();
   }
 }
 
 TNode TheoryArith::selectSmallestInconsistentVar(){
+  Debug("arith_update") << "selectSmallestInconsistentVar()" << endl;
+  Debug("arith_update") << "possiblyInconsistent.size()"
+                        << d_possiblyInconsistent.size() << endl;
+
+  while(!d_possiblyInconsistent.empty()){
+    TNode var = d_possiblyInconsistent.top();
+    Debug("arith_update") << "possiblyInconsistent var" << var << endl;
+    if(isBasic(var)){
+      if(!d_partialModel.assignmentIsConsistent(var)){
+        return var;
+      }
+    }
+    d_possiblyInconsistent.pop();
+  }
 
-  for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
-      basicIter != d_tableau.end();
-      ++basicIter){
+  if(debugTagIsOn("paranoid:variables")){
+    for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
+        basicIter != d_tableau.end();
+        ++basicIter){
 
-    TNode basic = *basicIter;
-    if(!d_partialModel.assignmentIsConsistent(basic)){
-      return basic;
+      TNode basic = *basicIter;
+      Assert(d_partialModel.assignmentIsConsistent(basic));
+      if(!d_partialModel.assignmentIsConsistent(basic)){
+        return basic;
+      }
     }
   }
 
@@ -449,6 +491,7 @@ TNode TheoryArith::selectSlackAbove(TNode x_i){ // beta(x_i) > u_i
 Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
   Debug("arith") << "updateInconsistentVars" << endl;
 
+  d_partialModel.turnOnUnsafeMode();
 
   while(true){
     if(debugTagIsOn("paranoid:check_tableau")){
@@ -464,8 +507,8 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
         checkTableau();
       }
 
-      d_partialModel.stopRecordingAssignments(false);
-      d_partialModel.beginRecordingAssignments();
+      d_partialModel.commitAssignmentChanges();
+      d_partialModel.turnOffUnsafeMode();
 
       if(debugTagIsOn("paranoid:check_tableau")){
         checkTableau();
@@ -487,8 +530,10 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
           checkTableau();
         }
 
-        d_partialModel.stopRecordingAssignments(true);
-        d_partialModel.beginRecordingAssignments();
+        d_partialModel.revertAssignmentChanges();
+        d_partialModel.turnOffUnsafeMode();
+        //d_partialModel.stopRecordingAssignments(true);
+        //d_partialModel.beginRecordingAssignments();
 
         if(debugTagIsOn("paranoid:check_tableau")){
           checkTableau();
@@ -508,8 +553,10 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
           checkTableau();
         }
 
-        d_partialModel.stopRecordingAssignments(true);
-        d_partialModel.beginRecordingAssignments();
+        d_partialModel.revertAssignmentChanges();
+        d_partialModel.turnOffUnsafeMode();
+        //d_partialModel.stopRecordingAssignments(true);
+        //d_partialModel.beginRecordingAssignments();
 
         if(debugTagIsOn("paranoid:check_tableau")){
           checkTableau();
@@ -596,6 +643,7 @@ Node TheoryArith::generateConflictBelow(TNode conflictVar){
   return conflict;
 }
 
+
 //TODO get rid of this!
 Node TheoryArith::simulatePreprocessing(TNode n){
   if(n.getKind() == NOT){
@@ -606,17 +654,19 @@ Node TheoryArith::simulatePreprocessing(TNode n){
       return NodeManager::currentNM()->mkNode(NOT,sub);
     }
   }else{
-    Node rewritten = rewrite(n);
+    Assert(isNormalAtom(n));
+    Node rewritten = n;
     Kind k = rewritten.getKind();
 
-    if(rewritten.getKind() == NOT){
-      Node sub = simulatePreprocessing(rewritten[0]);
-      if(sub.getKind() == NOT){
-        return sub[0];
-      }else{
-        return NodeManager::currentNM()->mkNode(NOT,sub);
-      }
-    } else if(!isRelationOperator(k)){
+//  if(rewritten.getKind() == NOT){
+//       Node sub = simulatePreprocessing(rewritten[0]);
+//       if(sub.getKind() == NOT){
+//         return sub[0];
+//       }else{
+//         return NodeManager::currentNM()->mkNode(NOT,sub);
+//       }
+//     } else 
+    if(!isRelationOperator(k)){
       if(rewritten.getKind() == CONST_BOOLEAN){
         Warning() << "How did I get a const boolean here" << endl;
         Warning() << "offending node has id " << n.getId() << endl;
@@ -719,37 +769,37 @@ void TheoryArith::check(Effort level){
     }
   }
 
-  if(fullEffort(level)){
-    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;
-      Debug("arith") << "splitting"  << assertion << endl;
-      TNode eq = assertion[0];
-      TNode x_i = eq[0];
-      TNode c_i = eq[1];
-      DeltaRational constant =  c_i.getConst<Rational>();
-      Debug("arith") << "broken apart" << endl;
-      if(d_partialModel.getAssignment(x_i) == constant){
-        Debug("arith") << "here" << endl;
-        enqueuedCaseSplit = true;
-        Node lt = NodeManager::currentNM()->mkNode(LT,x_i,c_i);
-        Node gt = NodeManager::currentNM()->mkNode(GT,x_i,c_i);
-        Node caseSplit = NodeManager::currentNM()->mkNode(OR, eq, lt, gt);
-        //d_out->enqueueCaseSplits(caseSplit);
-        Debug("arith") << "finished" << caseSplit << endl;
-      }
-      Debug("arith") << "end of for loop" << endl;
-
-    }
-    Debug("arith") << "finished" << endl;
-
-    if(enqueuedCaseSplit){
-      //d_out->caseSplit();
-      //Warning() << "Outstanding case split in theory arith" << endl;
-    }
-  }
+  // if(fullEffort(level)){
+//     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;
+//       Debug("arith") << "splitting"  << assertion << endl;
+//       TNode eq = assertion[0];
+//       TNode x_i = eq[0];
+//       TNode c_i = eq[1];
+//       DeltaRational constant =  c_i.getConst<Rational>();
+//       Debug("arith") << "broken apart" << endl;
+//       if(d_partialModel.getAssignment(x_i) == constant){
+//         Debug("arith") << "here" << endl;
+//         enqueuedCaseSplit = true;
+//         Node lt = NodeManager::currentNM()->mkNode(LT,x_i,c_i);
+//         Node gt = NodeManager::currentNM()->mkNode(GT,x_i,c_i);
+//         Node caseSplit = NodeManager::currentNM()->mkNode(OR, eq, lt, gt);
+//         //d_out->enqueueCaseSplits(caseSplit);
+//         Debug("arith") << "finished" << caseSplit << endl;
+//       }
+//       Debug("arith") << "end of for loop" << endl;
+
+//     }
+//     Debug("arith") << "finished" << endl;
+
+//     if(enqueuedCaseSplit){
+//       //d_out->caseSplit();
+//       //Warning() << "Outstanding case split in theory arith" << endl;
+//     }
+//   }
 
   Debug("arith") << "TheoryArith::check end" << std::endl;