From 23d8c824a5aa9db6bdf6c19fb9270a25bf171043 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Sat, 29 May 2010 02:58:18 +0000
Subject: [PATCH] Couple of fixes to theory arith. pivotAndUpdate now
 multiplies by a_kj. And the tableau now simulates older pivots while adding a
 new row.

---
 src/theory/arith/tableau.h        | 36 ++++++++++++++++++++++++++++++-
 src/theory/arith/theory_arith.cpp | 22 ++++++++++++++-----
 2 files changed, 52 insertions(+), 6 deletions(-)

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index fa0712e7e..76d8aa4f3 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -128,6 +128,17 @@ public:
       }
     }
   }
+
+  void printRow(){
+    Debug("tableau") << d_x_i << " ";
+    for(std::set<TNode>::iterator nonbasicIter = d_nonbasic.begin();
+        nonbasicIter != d_nonbasic.end();
+        ++nonbasicIter){
+      TNode nb = *nonbasicIter;
+      Debug("tableau") << "{" << nb << "," << d_coeffs[nb] << "}";
+    }
+    Debug("tableau") << std::endl;
+  }
 };
 
 class Tableau {
@@ -213,7 +224,23 @@ public:
     //The new basic variable cannot already be a basic variable
     Assert(d_basicVars.find(var) == d_basicVars.end());
     d_basicVars.insert(var);
-    d_rows[var] = new Row(var,sum);
+    Row* row_var = new Row(var,sum);
+    d_rows[var] = row_var;
+
+    //A variable in the row may have been made non-basic already.
+    //fake the pivot of this variable
+    for(TNode::iterator sumIter = sum.begin(); sumIter!=sum.end(); ++sumIter){
+      TNode child = *sumIter; //(MULT (CONST_RATIONAL 1998/1001) x_5)
+      Assert(child.getKind() == kind::MULT);
+      Assert(child.getNumChildren() == 2);
+      Assert(child[0].getKind() == kind::CONST_RATIONAL);
+      TNode c = child[1];
+      Assert(var.getMetaKind() == kind::metakind::VARIABLE);
+      if(contains(c)){
+        Row* row_c = lookup(c);
+        row_var->subsitute(*row_c);
+      }
+    }
   }
 
   /**
@@ -249,6 +276,13 @@ public:
       }
     }
   }
+  void printTableau(){
+    for(VarSet::iterator basicIter = begin(); basicIter != end(); ++basicIter){
+      TNode basic = *basicIter;
+      Row* row_k = lookup(basic);
+      row_k->printRow();
+    }
+  }
 };
 
 }; /* namespace arith  */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index b3c19a040..672675ac8 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -286,13 +286,14 @@ void TheoryArith::pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v){
     Row* row_k = d_tableau.lookup(x_k);
 
     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;
+      Rational a_kj = row_k->lookup(x_j);
+      DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj);
       d_partialModel.setAssignment(x_k, nextAssignment);
     }
   }
 
   d_tableau.pivot(x_i, x_j);
+  d_tableau.printTableau();
 }
 
 TNode TheoryArith::selectSmallestInconsistentVar(){
@@ -369,6 +370,8 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
         d_partialModel.stopRecordingAssignments(true);
         return generateConflictBelow(x_i); //unsat
       }
+      d_partialModel.printModel(x_i);
+      d_partialModel.printModel(x_j);
       pivotAndUpdate(x_i, x_j, l_i);
     }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
       DeltaRational u_i = d_partialModel.getUpperBound(x_i);
@@ -377,6 +380,8 @@ Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06
         d_partialModel.stopRecordingAssignments(true);
         return generateConflictAbove(x_i); //unsat
       }
+      d_partialModel.printModel(x_i);
+      d_partialModel.printModel(x_j);
       pivotAndUpdate(x_i, x_j, u_i);
     }
   }
@@ -501,7 +506,7 @@ void TheoryArith::check(Effort level){
   while(!done()){
     Node original = get();
     Node assertion = simulatePreprocessing(original);
-    Debug("arith") << "arith assertion(" << original
+    Debug("arith_assertions") << "arith assertion(" << original
                    << " \\-> " << assertion << ")" << std::endl;
 
     d_preprocessed.push_back(assertion);
@@ -555,10 +560,10 @@ void TheoryArith::check(Effort level){
   if(fullEffort(level)){
     Node possibleConflict = updateInconsistentVars();
     if(possibleConflict != Node::null()){
-      Debug("arith") << "Found a conflict " << possibleConflict << endl;
+      Debug("arith_conflict") << "Found a conflict " << possibleConflict << endl;
       d_out->conflict(possibleConflict);
     }else{
-      Debug("arith") << "No conflict found" << endl;
+      Debug("arith_conflict") << "No conflict found" << endl;
     }
   }
 
@@ -593,6 +598,13 @@ void TheoryArith::check(Effort level){
       //Warning() << "Outstanding case split in theory arith" << endl;
     }
   }
+  if(fullEffort(level)){
+    for(vector<Node>::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){
+      Node var = *i;
+      d_partialModel.printModel(var);
+    }
+  }
+
   Debug("arith") << "TheoryArith::check end" << std::endl;
 
 }
-- 
2.30.2