Improved garbage collection for TheoryArith. The merges all of the code over from branches/arithmetic/converge except for the new code for simplex.

1 files changed, 18 insertions, 1 deletions

diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 360e45289..5063a05c7 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -80,7 +80,7 @@ void LinearEqualityModule::update(ArithVar x_i, const DeltaRational& v){
   if(Debug.isOn("paranoid:check_tableau")){  debugCheckTableau(); }
 }
 
-void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
+void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, const DeltaRational& v){
   Assert(x_i != x_j);
 
   TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime);
@@ -188,6 +188,23 @@ void LinearEqualityModule::debugCheckTableau(){
     Assert(sum == shouldBe);
   }
 }
+bool LinearEqualityModule::debugEntireLinEqIsConsistent(const string& s){
+  bool result = true;
+  for(ArithVar var = 0, end = d_tableau.getNumColumns(); var != end; ++var){
+    //  for(VarIter i = d_variables.begin(), end = d_variables.end(); i != end; ++i){
+    //ArithVar var = d_arithvarNodeMap.asArithVar(*i);
+    if(!d_partialModel.assignmentIsConsistent(var)){
+      d_partialModel.printModel(var);
+      Warning() << s << ":" << "Assignment is not consistent for " << var ;
+      if(d_tableau.isBasic(var)){
+        Warning() << " (basic)";
+      }
+      Warning() << endl;
+      result = false;
+    }
+  }
+  return result;
+}
 
 DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound){
   DeltaRational sum(0,0);