From cde31cf615ccd7f8e090f1713022e5aeae31ccb5 Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 27 Jun 2012 21:06:29 +0000 Subject: [PATCH] This adds TheoryArith::safeToReset(). This fixes bug 363. --- src/theory/arith/theory_arith.cpp | 111 +++++++++++++++++++++++++----- src/theory/arith/theory_arith.h | 18 ++++- 2 files changed, 109 insertions(+), 20 deletions(-) diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index e4284286e..badfe4c41 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -302,6 +302,12 @@ bool TheoryArith::AssertLower(Constraint constraint){ d_updatedBounds.softAdd(x_i); + if(Debug.isOn("model")) { + Debug("model") << "before" << endl; + d_partialModel.printModel(x_i); + d_tableau.debugPrintIsBasic(x_i); + } + if(!d_tableau.isBasic(x_i)){ if(d_partialModel.getAssignment(x_i) < c_i){ d_linEq.update(x_i, c_i); @@ -310,7 +316,11 @@ bool TheoryArith::AssertLower(Constraint constraint){ d_simplex.updateBasic(x_i); } - if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } + if(Debug.isOn("model")) { + Debug("model") << "after" << endl; + d_partialModel.printModel(x_i); + d_tableau.debugPrintIsBasic(x_i); + } return false; //sat } @@ -412,6 +422,12 @@ bool TheoryArith::AssertUpper(Constraint constraint){ d_updatedBounds.softAdd(x_i); + if(Debug.isOn("model")) { + Debug("model") << "before" << endl; + d_partialModel.printModel(x_i); + d_tableau.debugPrintIsBasic(x_i); + } + if(!d_tableau.isBasic(x_i)){ if(d_partialModel.getAssignment(x_i) > c_i){ d_linEq.update(x_i, c_i); @@ -420,7 +436,11 @@ bool TheoryArith::AssertUpper(Constraint constraint){ d_simplex.updateBasic(x_i); } - if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } + if(Debug.isOn("model")) { + Debug("model") << "after" << endl; + d_partialModel.printModel(x_i); + d_tableau.debugPrintIsBasic(x_i); + } return false; //sat } @@ -497,6 +517,12 @@ bool TheoryArith::AssertEquality(Constraint constraint){ d_updatedBounds.softAdd(x_i); + if(Debug.isOn("model")) { + Debug("model") << "before" << endl; + d_partialModel.printModel(x_i); + d_tableau.debugPrintIsBasic(x_i); + } + if(!d_tableau.isBasic(x_i)){ if(!(d_partialModel.getAssignment(x_i) == c_i)){ d_linEq.update(x_i, c_i); @@ -504,6 +530,13 @@ bool TheoryArith::AssertEquality(Constraint constraint){ }else{ d_simplex.updateBasic(x_i); } + + if(Debug.isOn("model")) { + Debug("model") << "after" << endl; + d_partialModel.printModel(x_i); + d_tableau.debugPrintIsBasic(x_i); + } + return false; } @@ -1431,11 +1464,12 @@ void TheoryArith::check(Effort effortLevel){ d_qflraStatus = Result::UNSAT; if(previous == Result::SAT){ ++d_statistics.d_revertsOnConflicts; + Debug("arith::bt") << "clearing here " << " " << newFacts << " " << previous << " " << d_qflraStatus << endl; revertOutOfConflict(); d_simplex.clearQueue(); }else{ ++d_statistics.d_commitsOnConflicts; - + Debug("arith::bt") << "committing here " << " " << newFacts << " " << previous << " " << d_qflraStatus << endl; d_partialModel.commitAssignmentChanges(); revertOutOfConflict(); } @@ -1457,16 +1491,19 @@ void TheoryArith::check(Effort effortLevel){ if(newFacts){ ++d_statistics.d_nontrivialSatChecks; } + + Debug("arith::bt") << "committing sap inConflit" << " " << newFacts << " " << previous << " " << d_qflraStatus << endl; d_partialModel.commitAssignmentChanges(); d_unknownsInARow = 0; if(Debug.isOn("arith::consistency")){ - Assert(entireStateIsConsistent()); + Assert(entireStateIsConsistent("sat comit")); } break; case Result::SAT_UNKNOWN: ++d_unknownsInARow; ++(d_statistics.d_unknownChecks); Assert(!fullEffort(effortLevel)); + Debug("arith::bt") << "committing unknown" << " " << newFacts << " " << previous << " " << d_qflraStatus << endl; d_partialModel.commitAssignmentChanges(); d_statistics.d_maxUnknownsInARow.maxAssign(d_unknownsInARow); break; @@ -1474,13 +1511,19 @@ void TheoryArith::check(Effort effortLevel){ d_unknownsInARow = 0; if(previous == Result::SAT){ ++d_statistics.d_revertsOnConflicts; + Debug("arith::bt") << "clearing on conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus << endl; revertOutOfConflict(); d_simplex.clearQueue(); }else{ ++d_statistics.d_commitsOnConflicts; + Debug("arith::bt") << "committing on conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus << endl; d_partialModel.commitAssignmentChanges(); revertOutOfConflict(); + + if(Debug.isOn("arith::consistency")){ + entireStateIsConsistent("commit on conflict"); + } } outputConflicts(); emmittedConflictOrSplit = true; @@ -1540,6 +1583,8 @@ void TheoryArith::check(Effort effortLevel){ d_qflraStatus = Result::UNSAT; outputConflicts(); emmittedConflictOrSplit = true; + Debug("arith::bt") << "committing on unate conflict" << " " << newFacts << " " << previous << " " << d_qflraStatus << endl; + } }else{ TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime); @@ -1953,6 +1998,21 @@ Node TheoryArith::getValue(TNode n) { } } +bool TheoryArith::safeToReset() const { + Assert(!d_tableauSizeHasBeenModified); + + ArithPriorityQueue::const_iterator conf_iter = d_simplex.queueBegin(); + ArithPriorityQueue::const_iterator conf_end = d_simplex.queueEnd(); + for(; conf_iter != conf_end; ++conf_iter){ + ArithVar basic = *conf_iter; + if(!d_smallTableauCopy.isBasic(basic)){ + return false; + } + } + + return true; +} + void TheoryArith::notifyRestart(){ TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer); @@ -1963,6 +2023,7 @@ void TheoryArith::notifyRestart(){ uint32_t currSize = d_tableau.size(); uint32_t copySize = d_smallTableauCopy.size(); + Debug("arith::reset") << "resetting" << d_restartsCounter << endl; Debug("arith::reset") << "curr " << currSize << " copy " << copySize << endl; Debug("arith::reset") << "tableauSizeHasBeenModified " << d_tableauSizeHasBeenModified << endl; @@ -1972,23 +2033,31 @@ void TheoryArith::notifyRestart(){ d_tableauSizeHasBeenModified = false; }else if( d_restartsCounter >= RESET_START){ if(copySize >= currSize * 1.1 ){ + Debug("arith::reset") << "size has shrunk " << d_restartsCounter << endl; ++d_statistics.d_smallerSetToCurr; d_smallTableauCopy = d_tableau; }else if(d_tableauResetDensity * copySize <= currSize){ - ++d_statistics.d_currSetToSmaller; - d_tableau = d_smallTableauCopy; + d_simplex.reduceQueue(); + if(safeToReset()){ + Debug("arith::reset") << "resetting " << d_restartsCounter << endl; + ++d_statistics.d_currSetToSmaller; + d_tableau = d_smallTableauCopy; + }else{ + Debug("arith::reset") << "not safe to reset at the moment " << d_restartsCounter << endl; + } } } + Assert(unenqueuedVariablesAreConsistent()); } -bool TheoryArith::entireStateIsConsistent(){ +bool TheoryArith::entireStateIsConsistent(const string& s){ typedef std::vector::const_iterator VarIter; bool result = true; 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() << "Assignment is not consistent for " << var << *i; + Warning() << s << ":" << "Assignment is not consistent for " << var << *i; if(d_tableau.isBasic(var)){ Warning() << " (basic)"; } @@ -2004,17 +2073,25 @@ bool TheoryArith::unenqueuedVariablesAreConsistent(){ bool result = true; 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_simplex.debugIsInCollectionQueue(var)){ + if(!d_partialModel.assignmentIsConsistent(var)){ + if(!d_simplex.debugIsInCollectionQueue(var)){ - d_partialModel.printModel(var); - Warning() << "Unenqueued var is not consistent for " << var << *i; - if(d_tableau.isBasic(var)){ - Warning() << " (basic)"; + d_partialModel.printModel(var); + Warning() << "Unenqueued var is not consistent for " << var << *i; + if(d_tableau.isBasic(var)){ + Warning() << " (basic)"; + } + Warning() << endl; + result = false; + } else { + d_partialModel.printModel(var); + Warning() << "Initial var is not consistent for " << var << *i; + if(d_tableau.isBasic(var)){ + Warning() << " (basic)"; + } + Warning() << endl; } - Warning() << endl; - result = false; - } + } } return result; } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index d3b0964cf..0431f543c 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -277,11 +277,23 @@ private: /** - * A copy of the tableau immediately after removing variables - * without bounds in presolve(). + * A copy of the tableau. + * This is equivalent to the original tableau if d_tableauSizeHasBeenModified + * is false. + * The set of basic and non-basic variables may differ from d_tableau. */ Tableau d_smallTableauCopy; + /** + * Returns true if all of the basic variables in the simplex queue of + * basic variables that violate their bounds in the current tableau + * are basic in d_smallTableauCopy. + * + * d_tableauSizeHasBeenModified must be false when calling this. + * Simplex's priority queue must be in collection mode. + */ + bool safeToReset() const; + /** This keeps track of difference equalities. Mostly for sharing. */ ArithCongruenceManager d_congruenceManager; @@ -463,7 +475,7 @@ private: * Debugging only routine! * Returns true iff every variable is consistent in the partial model. */ - bool entireStateIsConsistent(); + bool entireStateIsConsistent(const std::string& locationHint); bool unenqueuedVariablesAreConsistent(); bool isImpliedUpperBound(ArithVar var, Node exp); -- 2.30.2