diff options
Diffstat (limited to 'src/theory/arith/linear_equality.cpp')
-rw-r--r-- | src/theory/arith/linear_equality.cpp | 19 |
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); |