Preregistration has been turned on. Highly experimental eager splitting support has been added. Also a few bug fixes to Tableau.

3 files changed, 72 insertions, 10 deletions

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 7237c3a54..fa0712e7e 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -36,6 +36,7 @@ public:
 
     //TODO Assert(d_x_i.getType() == REAL);
     Assert(sum.getKind() == PLUS);
+    Rational zero(0,1);
 
     for(TNode::iterator iter=sum.begin(); iter != sum.end(); ++iter){
       TNode pair = *iter;
@@ -48,7 +49,10 @@ public:
       //TODO Assert(var_i.getKind() == REAL);
       Assert(!has(var_i));
       d_nonbasic.insert(var_i);
-      d_coeffs[var_i] = coeff.getConst<Rational>();
+      Rational q = coeff.getConst<Rational>();
+      d_coeffs[var_i] = q;
+      Assert(q != zero);
+      Assert(d_coeffs[var_i] != zero);
     }
   }
 
@@ -66,12 +70,13 @@ public:
 
   bool has(TNode x_j){
     CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
-
     return x_jPos != d_coeffs.end();
   }
 
   Rational& lookup(TNode x_j){
-    return d_coeffs[x_j];
+    CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
+    Assert(x_jPos !=  d_coeffs.end());
+    return (*x_jPos).second;
   }
 
   void pivot(TNode x_j){
@@ -89,17 +94,22 @@ public:
       TNode nb = *nonbasicIter;
       d_coeffs[nb] = d_coeffs[nb] * negInverseA_rs;
     }
+
   }
 
   void subsitute(Row& row_s){
     TNode x_s = row_s.basicVar();
 
     Assert(has(x_s));
+    Assert(d_nonbasic.find(x_s) != d_nonbasic.end());
     Assert(x_s != d_x_i);
 
+    Rational zero(0,1);
 
     Rational a_rs = lookup(x_s);
+    Assert(a_rs != zero);
     d_coeffs.erase(x_s);
+    d_nonbasic.erase(x_s);
 
     for(std::set<TNode>::iterator iter = row_s.d_nonbasic.begin();
         iter != row_s.d_nonbasic.end();
@@ -108,6 +118,10 @@ public:
       Rational a_sj = a_rs * row_s.lookup(x_j);
       if(has(x_j)){
         d_coeffs[x_j] = d_coeffs[x_j] + a_sj;
+        if(d_coeffs[x_j] == zero){
+          d_coeffs.erase(x_j);
+          d_nonbasic.erase(x_j);
+        }
       }else{
         d_nonbasic.insert(x_j);
         d_coeffs[x_j] = a_sj;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6ff74f0f9..08b609ba4 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -29,6 +29,10 @@ using namespace CVC4::kind;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
+struct EagerSplittingTag {};
+typedef expr::Attribute<EagerSplittingTag, bool> EagerlySplitUpon;
+
+
 TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
   Theory(c, out),
   d_preprocessed(c),
@@ -47,6 +51,29 @@ TheoryArith::~TheoryArith(){
   }
 }
 
+void TheoryArith::preRegisterTerm(TNode n) {
+  Debug("arith_preregister") << "arith: begin TheoryArith::preRegisterTerm("
+                             << n << ")" << endl;
+
+  if(n.getKind() == EQUAL){
+    if(!n.getAttribute(EagerlySplitUpon())){
+      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);
+
+      n.setAttribute(EagerlySplitUpon(), true);
+      d_out->augmentingLemma(eagerSplit);
+    }
+  }
+
+  Debug("arith_preregister") << "arith: end TheoryArith::preRegisterTerm("
+                             << n << ")" << endl;
+}
 
 bool isBasicSum(TNode n){
   if(n.getKind() != kind::PLUS) return false;
@@ -220,11 +247,13 @@ void TheoryArith::update(TNode x_i, DeltaRational& v){
     TNode x_j = *basicIter;
     Row* row_j = d_tableau.lookup(x_j);
 
-    Rational& a_ji = row_j->lookup(x_i);
+    if(row_j->has(x_i)){
+      Rational& a_ji = row_j->lookup(x_i);
 
-    DeltaRational assignment = d_partialModel.getAssignment(x_j);
-    DeltaRational  nAssignment = assignment+(diff * a_ji);
-    d_partialModel.setAssignment(x_j, nAssignment);
+      DeltaRational assignment = d_partialModel.getAssignment(x_j);
+      DeltaRational  nAssignment = assignment+(diff * a_ji);
+      d_partialModel.setAssignment(x_j, nAssignment);
+    }
   }
 
   d_partialModel.setAssignment(x_i, v);
@@ -252,7 +281,7 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
     TNode x_k = *basicIter;
     Row* row_k = d_tableau.lookup(x_k);
 
-    if(x_k != x_i){
+    if(x_k != x_i && row_k->has(x_j)){
       DeltaRational a_kj = row_k->lookup(x_j);
       DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + theta;
       d_partialModel.setAssignment(x_k, nextAssignment);
@@ -321,7 +350,9 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
   d_partialModel.beginRecordingAssignments();
   while(true){
     TNode x_i = selectSmallestInconsistentVar();
+    Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl;
     if(x_i == Node::null()){
+      Debug("arith_update") << "No inconsistent variables" << endl;
       d_partialModel.stopRecordingAssignments(false);
       return Node::null(); //sat
     }
@@ -509,6 +540,8 @@ void TheoryArith::check(Effort level){
     if(possibleConflict != Node::null()){
       Debug("arith") << "Found a conflict " << possibleConflict << endl;
       d_out->conflict(possibleConflict);
+    }else{
+      Debug("arith") << "No conflict found" << endl;
     }
   }
 
@@ -516,22 +549,33 @@ void TheoryArith::check(Effort 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;
+      //Warning() << "Outstanding case split in theory arith" << endl;
     }
   }
+  Debug("arith") << "TheoryArith::check end" << std::endl;
+
 }
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 7bfa535a8..1d6cca5cc 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -38,6 +38,10 @@ class TheoryArith : public Theory {
 private:
   /* Chopping block begins */
 
+  std::vector<Node> d_splits;
+  //This stores the eager splits sent out of the theory.
+  //TODO get rid of this.
+
   context::CDList<Node> d_preprocessed;
   //TODO This is currently needed to save preprocessed nodes that may not
   //currently have an outisde reference. Get rid of when preprocessing is occuring
@@ -65,7 +69,7 @@ public:
 
   Node rewrite(TNode n);
 
-  void preRegisterTerm(TNode n) { Unimplemented(); }
+  void preRegisterTerm(TNode n);
   void registerTerm(TNode n);
   void check(Effort e);
   void propagate(Effort e) { Unimplemented(); }