From 7d4a5842ea4f53fe2e05f336c9342db9b94a31f1 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 29 Oct 2010 00:45:10 +0000 Subject: [PATCH] Factors out the QF_LRA decision procedure from TheoryArith and puts this into its own class SimplexDecisionProcedure. Implements about 1/2 of the pivoting rule from Alberto's thesis (section2.5.3). --- src/theory/arith/Makefile.am | 2 + src/theory/arith/simplex.cpp | 549 ++++++++++++++++++++++++++++++ src/theory/arith/simplex.h | 211 ++++++++++++ src/theory/arith/theory_arith.cpp | 531 +---------------------------- src/theory/arith/theory_arith.h | 100 +----- 5 files changed, 781 insertions(+), 612 deletions(-) create mode 100644 src/theory/arith/simplex.cpp create mode 100644 src/theory/arith/simplex.h diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 907c8820f..7d78b1e6c 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -21,6 +21,8 @@ libarith_la_SOURCES = \ arithvar_dense_set.h \ tableau.h \ tableau.cpp \ + simplex.h \ + simplex.cpp \ row_vector.h \ row_vector.cpp \ arith_propagator.h \ diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp new file mode 100644 index 000000000..be2b87252 --- /dev/null +++ b/src/theory/arith/simplex.cpp @@ -0,0 +1,549 @@ + +#include "theory/arith/simplex.h" + +using namespace std; + +using namespace CVC4; +using namespace CVC4::kind; + +using namespace CVC4::theory; +using namespace CVC4::theory::arith; + +const static uint64_t ACTIVITY_THRESHOLD = 100; + +SimplexDecisionProcedure::Statistics::Statistics(): + d_statPivots("theory::arith::pivots",0), + d_statUpdates("theory::arith::updates",0), + d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0), + d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0), + d_statUpdateConflicts("theory::arith::UpdateConflicts", 0) +{ + StatisticsRegistry::registerStat(&d_statPivots); + StatisticsRegistry::registerStat(&d_statUpdates); + StatisticsRegistry::registerStat(&d_statAssertUpperConflicts); + StatisticsRegistry::registerStat(&d_statAssertLowerConflicts); + StatisticsRegistry::registerStat(&d_statUpdateConflicts); +} + +SimplexDecisionProcedure::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_statPivots); + StatisticsRegistry::unregisterStat(&d_statUpdates); + StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts); + StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts); + StatisticsRegistry::unregisterStat(&d_statUpdateConflicts); +} + + +void SimplexDecisionProcedure::ejectInactiveVariables(){ + Debug("decay") << "begin ejectInactiveVariables()" << endl; + for(ArithVar variable = 0, end = d_numVariables; variable != end; ++variable){ + + if(shouldEject(variable)){ + if(d_basicManager.isMember(variable)){ + Debug("decay") << "ejecting basic " << variable << endl;; + d_tableau.ejectBasic(variable); + } + } + } +} + +void SimplexDecisionProcedure::reinjectVariable(ArithVar x){ + d_tableau.reinjectBasic(x); + + + DeltaRational safeAssignment = computeRowValue(x, true); + DeltaRational assignment = computeRowValue(x, false); + d_partialModel.setAssignment(x,safeAssignment,assignment); +} + +bool SimplexDecisionProcedure::shouldEject(ArithVar var){ + if(d_partialModel.hasEitherBound(var)){ + return false; + }else if(d_tableau.isEjected(var)) { + return false; + }else if(!d_partialModel.hasEverHadABound(var)){ + return true; + }else if(d_activityMonitor[var] >= ACTIVITY_THRESHOLD){ + return true; + } + return false; +} + +/* procedure AssertLower( x_i >= c_i ) */ +bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){ + Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl; + + if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ + reinjectVariable(x_i); + } + + if(d_partialModel.belowLowerBound(x_i, c_i, false)){ + return false; //sat + } + if(d_partialModel.aboveUpperBound(x_i, c_i, true)){ + Node ubc = d_partialModel.getUpperConstraint(x_i); + Node conflict = NodeManager::currentNM()->mkNode(AND, ubc, original); + d_out->conflict(conflict); + Debug("arith") << "AssertLower conflict " << conflict << endl; + ++(d_statistics.d_statAssertLowerConflicts); + return true; + } + + d_partialModel.setLowerConstraint(x_i,original); + d_partialModel.setLowerBound(x_i, c_i); + d_activityMonitor[x_i] = 0; + + if(!d_basicManager.isMember(x_i)){ + if(d_partialModel.getAssignment(x_i) < c_i){ + update(x_i, c_i); + } + }else{ + checkBasicVariable(x_i); + } + + return false; +} + +/* procedure AssertUpper( x_i <= c_i) */ +bool SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){ + + Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; + if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ + reinjectVariable(x_i); + } + + if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i + return false; //sat + } + if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i + Node lbc = d_partialModel.getLowerConstraint(x_i); + Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); + Debug("arith") << "AssertUpper conflict " << conflict << endl; + ++(d_statistics.d_statAssertUpperConflicts); + d_out->conflict(conflict); + return true; + } + + d_partialModel.setUpperConstraint(x_i,original); + d_partialModel.setUpperBound(x_i, c_i); + + d_activityMonitor[x_i] = 0; + + if(!d_basicManager.isMember(x_i)){ + if(d_partialModel.getAssignment(x_i) > c_i){ + update(x_i, c_i); + } + }else{ + checkBasicVariable(x_i); + } + d_partialModel.printModel(x_i); + return false; +} + + +/* procedure AssertLower( x_i == c_i ) */ +bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode original){ + + Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl; + + if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ + reinjectVariable(x_i); + } + + // u_i <= c_i <= l_i + // This can happen if both c_i <= x_i and x_i <= c_i are in the system. + if(d_partialModel.belowLowerBound(x_i, c_i, false) && + d_partialModel.aboveUpperBound(x_i, c_i, false)){ + return false; //sat + } + + if(d_partialModel.aboveUpperBound(x_i, c_i, true)){ + Node ubc = d_partialModel.getUpperConstraint(x_i); + Node conflict = NodeManager::currentNM()->mkNode(AND, ubc, original); + d_out->conflict(conflict); + Debug("arith") << "AssertLower conflict " << conflict << endl; + return true; + } + + if(d_partialModel.belowLowerBound(x_i, c_i, true)){ + Node lbc = d_partialModel.getLowerConstraint(x_i); + Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); + Debug("arith") << "AssertUpper conflict " << conflict << endl; + d_out->conflict(conflict); + return true; + } + + d_partialModel.setLowerConstraint(x_i,original); + d_partialModel.setLowerBound(x_i, c_i); + + d_partialModel.setUpperConstraint(x_i,original); + d_partialModel.setUpperBound(x_i, c_i); + d_activityMonitor[x_i] = 0; + + if(!d_basicManager.isMember(x_i)){ + if(!(d_partialModel.getAssignment(x_i) == c_i)){ + update(x_i, c_i); + } + }else{ + checkBasicVariable(x_i); + } + + return false; +} + +void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ + Assert(!d_basicManager.isMember(x_i)); + DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i); + ++(d_statistics.d_statUpdates); + + Debug("arith") <<"update " << x_i << ": " + << assignment_x_i << "|-> " << v << endl; + DeltaRational diff = v - assignment_x_i; + + for(ArithVarSet::iterator basicIter = d_tableau.begin(); + basicIter != d_tableau.end(); + ++basicIter){ + ArithVar x_j = *basicIter; + ReducedRowVector* row_j = d_tableau.lookup(x_j); + + if(row_j->has(x_i)){ + const Rational& a_ji = row_j->lookup(x_i); + + const DeltaRational& assignment = d_partialModel.getAssignment(x_j); + DeltaRational nAssignment = assignment+(diff * a_ji); + d_partialModel.setAssignment(x_j, nAssignment); + + d_activityMonitor[x_j] += 1; + + checkBasicVariable(x_j); + } + } + + d_partialModel.setAssignment(x_i, v); + + if(Debug.isOn("paranoid:check_tableau")){ + checkTableau(); + } +} + +void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){ + Assert(x_i != x_j); + + ReducedRowVector* row_i = d_tableau.lookup(x_i); + const Rational& a_ij = row_i->lookup(x_j); + + + const DeltaRational& betaX_i = d_partialModel.getAssignment(x_i); + + Rational inv_aij = a_ij.inverse(); + DeltaRational theta = (v - betaX_i)*inv_aij; + + d_partialModel.setAssignment(x_i, v); + + + DeltaRational tmp = d_partialModel.getAssignment(x_j) + theta; + d_partialModel.setAssignment(x_j, tmp); + + for(ArithVarSet::iterator basicIter = d_tableau.begin(); + basicIter != d_tableau.end(); + ++basicIter){ + ArithVar x_k = *basicIter; + ReducedRowVector* row_k = d_tableau.lookup(x_k); + + if(x_k != x_i && row_k->has(x_j)){ + const 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_activityMonitor[x_j] += 1; + + checkBasicVariable(x_k); + } + } + + ++(d_statistics.d_statPivots); + d_tableau.pivot(x_i, x_j); + + checkBasicVariable(x_j); + + if(Debug.isOn("tableau")){ + d_tableau.printTableau(); + } +} + +ArithVar SimplexDecisionProcedure::selectSmallestInconsistentVar(){ + Debug("arith_update") << "selectSmallestInconsistentVar()" << endl; + Debug("arith_update") << "possiblyInconsistent.size()" + << d_possiblyInconsistent.size() << endl; + + if(d_pivotStage){ + while(!d_griggioRuleQueue.empty()){ + ArithVar var = d_griggioRuleQueue.top().first; + Debug("arith_update") << "possiblyInconsistentGriggio var" << var << endl; + if(d_basicManager.isMember(var)){ + if(!d_partialModel.assignmentIsConsistent(var)){ + return var; + } + } + d_griggioRuleQueue.pop(); + } + }else{ + while(!d_possiblyInconsistent.empty()){ + ArithVar var = d_possiblyInconsistent.top(); + Debug("arith_update") << "possiblyInconsistent var" << var << endl; + if(d_basicManager.isMember(var)){ + if(!d_partialModel.assignmentIsConsistent(var)){ + return var; + } + } + d_possiblyInconsistent.pop(); + } + } + return ARITHVAR_SENTINEL; +} + +template +ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){ + ReducedRowVector* row_i = d_tableau.lookup(x_i); + + for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); + nbi != end; ++nbi){ + ArithVar nonbasic = getArithVar(*nbi); + if(nonbasic == x_i) continue; + + const Rational& a_ij = nbi->second; + int cmp = a_ij.cmp(d_constants.d_ZERO); + if(above){ // beta(x_i) > u_i + if( cmp < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){ + return nonbasic; + }else if( cmp > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){ + return nonbasic; + } + }else{ //beta(x_i) < l_i + if(cmp > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){ + return nonbasic; + }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){ + return nonbasic; + } + } + } + return ARITHVAR_SENTINEL; +} + +Node SimplexDecisionProcedure::updateInconsistentVars(){ + d_pivotStage = true; + return privateUpdateInconsistentVars(); +} + +//corresponds to Check() in dM06 +Node SimplexDecisionProcedure::privateUpdateInconsistentVars(){ + Assert(d_pivotStage || d_griggioRuleQueue.empty()); + + Debug("arith") << "updateInconsistentVars" << endl; + + uint32_t iteratationNum = 0; + static const int EJECT_FREQUENCY = 10; + + while(!d_pivotStage || iteratationNum <= d_numVariables){ + if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } + + ArithVar x_i = selectSmallestInconsistentVar(); + Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl; + if(x_i == ARITHVAR_SENTINEL){ + Debug("arith_update") << "No inconsistent variables" << endl; + return Node::null(); //sat + } + + ++iteratationNum; + if(iteratationNum % EJECT_FREQUENCY == 0) + ejectInactiveVariables(); + + DeltaRational beta_i = d_partialModel.getAssignment(x_i); + + if(d_partialModel.belowLowerBound(x_i, beta_i, true)){ + DeltaRational l_i = d_partialModel.getLowerBound(x_i); + ArithVar x_j = selectSlackBelow(x_i); + if(x_j == ARITHVAR_SENTINEL ){ + ++(d_statistics.d_statUpdateConflicts); + return generateConflictBelow(x_i); //unsat + } + 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); + ArithVar x_j = selectSlackAbove(x_i); + if(x_j == ARITHVAR_SENTINEL ){ + ++(d_statistics.d_statUpdateConflicts); + return generateConflictAbove(x_i); //unsat + } + pivotAndUpdate(x_i, x_j, u_i); + } + } + + if(d_pivotStage && iteratationNum >= d_numVariables){ + while(!d_griggioRuleQueue.empty()){ + ArithVar var = d_griggioRuleQueue.top().first; + if(d_basicManager.isMember(var)){ + d_possiblyInconsistent.push(var); + } + d_griggioRuleQueue.pop(); + } + d_pivotStage = false; + return updateInconsistentVars(); + } + + Unreachable(); +} + + +Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ + + ReducedRowVector* row_i = d_tableau.lookup(conflictVar); + + NodeBuilder<> nb(kind::AND); + TNode bound = d_partialModel.getUpperConstraint(conflictVar); + + Debug("arith") << "generateConflictAbove " + << "conflictVar " << conflictVar + << " " << d_partialModel.getAssignment(conflictVar) + << " " << bound << endl; + + nb << bound; + + for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); + nbi != end; ++nbi){ + ArithVar nonbasic = getArithVar(*nbi); + if(nonbasic == conflictVar) continue; + + const Rational& a_ij = nbi->second; + + Assert(a_ij != d_constants.d_ZERO); + + if(a_ij < d_constants.d_ZERO){ + bound = d_partialModel.getUpperConstraint(nonbasic); + Debug("arith") << "below 0 " << nonbasic << " " + << d_partialModel.getAssignment(nonbasic) + << " " << bound << endl; + nb << bound; + }else{ + bound = d_partialModel.getLowerConstraint(nonbasic); + Debug("arith") << " above 0 " << nonbasic << " " + << d_partialModel.getAssignment(nonbasic) + << " " << bound << endl; + nb << bound; + } + } + Node conflict = nb; + return conflict; +} + +Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ + ReducedRowVector* row_i = d_tableau.lookup(conflictVar); + + NodeBuilder<> nb(kind::AND); + TNode bound = d_partialModel.getLowerConstraint(conflictVar); + + Debug("arith") << "generateConflictBelow " + << "conflictVar " << conflictVar + << d_partialModel.getAssignment(conflictVar) << " " + << " " << bound << endl; + nb << bound; + + for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); nbi != end; ++nbi){ + ArithVar nonbasic = getArithVar(*nbi); + if(nonbasic != conflictVar) continue; + + const Rational& a_ij = nbi->second; + + Assert(a_ij != d_constants.d_ZERO); + + if(a_ij < d_constants.d_ZERO){ + TNode bound = d_partialModel.getLowerConstraint(nonbasic); + Debug("arith") << "Lower "<< nonbasic << " " + << d_partialModel.getAssignment(nonbasic) << " " + << bound << endl; + + nb << bound; + }else{ + TNode bound = d_partialModel.getUpperConstraint(nonbasic); + Debug("arith") << "Upper "<< nonbasic << " " + << d_partialModel.getAssignment(nonbasic) << " " + << bound << endl; + + nb << bound; + } + } + Node conflict (nb.constructNode()); + return conflict; +} + +/** + * Computes the value of a basic variable using the current assignment. + */ +DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe){ + Assert(d_basicManager.isMember(x)); + DeltaRational sum = d_constants.d_ZERO_DELTA; + + ReducedRowVector* row = d_tableau.lookup(x); + for(ReducedRowVector::NonZeroIterator i = row->beginNonZero(), end = row->endNonZero(); + i != end;++i){ + ArithVar nonbasic = getArithVar(*i); + if(nonbasic == row->basic()) continue; + const Rational& coeff = getCoefficient(*i); + + const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe); + sum = sum + (assignment * coeff); + } + return sum; +} + + +void SimplexDecisionProcedure::checkBasicVariable(ArithVar basic){ + Assert(d_basicManager.isMember(basic)); + if(!d_partialModel.assignmentIsConsistent(basic)){ + if(d_pivotStage){ + const DeltaRational& beta = d_partialModel.getAssignment(basic); + DeltaRational diff = d_partialModel.belowLowerBound(basic,beta,true) ? + d_partialModel.getLowerBound(basic) - beta: + beta - d_partialModel.getUpperBound(basic); + d_griggioRuleQueue.push(make_pair(basic,diff)); + }else{ + d_possiblyInconsistent.push(basic); + } + } +} + +/** + * This check is quite expensive. + * It should be wrapped in a Debug.isOn() guard. + * if(Debug.isOn("paranoid:check_tableau")){ + * checkTableau(); + * } + */ +void SimplexDecisionProcedure::checkTableau(){ + + for(ArithVarSet::iterator basicIter = d_tableau.begin(); + basicIter != d_tableau.end(); ++basicIter){ + ArithVar basic = *basicIter; + ReducedRowVector* row_k = d_tableau.lookup(basic); + DeltaRational sum; + Debug("paranoid:check_tableau") << "starting row" << basic << endl; + for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k->beginNonZero(); + nonbasicIter != row_k->endNonZero(); + ++nonbasicIter){ + ArithVar nonbasic = nonbasicIter->first; + if(basic == nonbasic) continue; + + const Rational& coeff = nonbasicIter->second; + DeltaRational beta = d_partialModel.getAssignment(nonbasic); + Debug("paranoid:check_tableau") << nonbasic << beta << coeff< + +namespace CVC4 { +namespace theory { +namespace arith { + +class SimplexDecisionProcedure { +private: + typedef std::pair VarDRatPair; + + struct VarDRatPairCompare{ + inline bool operator()(const VarDRatPair& a, const VarDRatPair& b){ + return a.second > b.second; + } + }; + + std::priority_queue, VarDRatPairCompare> d_griggioRuleQueue; + + /** + * Priority Queue of the basic variables that may be inconsistent. + * + * This is required to contain at least 1 instance of every inconsistent + * basic variable. This is only required to be a superset though so its + * contents must be checked to still be basic and inconsistent. + */ + std::priority_queue d_possiblyInconsistent; + + /** Stores system wide constants to avoid unnessecary reconstruction. */ + const ArithConstants& d_constants; + + /** + * Manages information about the assignment and upper and lower bounds on + * variables. + */ + ArithPartialModel& d_partialModel; + + ArithVarDenseSet& d_basicManager; + ActivityMonitor& d_activityMonitor; + + OutputChannel* d_out; + + + Tableau& d_tableau; + + ArithVar d_numVariables; + + bool d_pivotStage; + +public: + SimplexDecisionProcedure(const ArithConstants& constants, + ArithPartialModel& pm, + ArithVarDenseSet& bm, + OutputChannel* out, + ActivityMonitor& am, + Tableau& tableau) : + d_possiblyInconsistent(), + d_constants(constants), + d_partialModel(pm), + d_basicManager(bm), + d_activityMonitor(am), + d_out(out), + d_tableau(tableau), + d_numVariables(0) + {} + + void increaseMax() {d_numVariables++;} + + /** + * Assert*(n, orig) takes an bound n that is implied by orig. + * and asserts that as a new bound if it is tighter than the current bound + * and updates the value of a basic variable if needed. + * If this new bound is in conflict with the other bound, + * a conflict is created and asserted to the output channel. + * + * orig must be an atom in the SAT solver so that it can be used for + * conflict analysis. + * + * n is of the form (x =?= c) where x is a variable, + * c is a constant and =?= is either LT, LEQ, EQ, GEQ, or GT. + * + * returns true if a conflict was asserted. + */ + bool AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode orig); + bool AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig); + bool AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode orig); + +private: + /** + * Updates the assignment of a nonbasic variable x_i to v. + * Also updates the assignment of basic variables accordingly. + */ + void update(ArithVar x_i, const DeltaRational& v); + + /** + * Updates the value of a basic variable x_i to v, + * and then pivots x_i with the nonbasic variable in its row x_j. + * Updates the assignment of the other basic variables accordingly. + */ + void pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v); + +public: + /** + * Tries to update the assignments of variables such that all of the + * assignments are consistent with their bounds. + * + * This is done by searching through the tableau. + * If all of the variables can be made consistent with their bounds + * Node::null() is returned. Otherwise a minimized conflict is returned. + * + * If a conflict is found, changes to the assignments need to be reverted. + * + * Tableau pivoting is performed so variables may switch from being basic to + * nonbasic and vice versa. + * + * Corresponds to the "check()" procedure in [Cav06]. + */ + Node updateInconsistentVars(); +private: + Node privateUpdateInconsistentVars(); + +private: + /** + * Given the basic variable x_i, + * this function finds the smallest nonbasic variable x_j in the row of x_i + * in the tableau that can "take up the slack" to let x_i satisfy its bounds. + * This returns TNode::null() if none exists. + * + * More formally one of the following conditions must be satisfied: + * - above && a_ij < 0 && assignment(x_j) < upperbound(x_j) + * - above && a_ij > 0 && assignment(x_j) > lowerbound(x_j) + * - !above && a_ij > 0 && assignment(x_j) < upperbound(x_j) + * - !above && a_ij < 0 && assignment(x_j) > lowerbound(x_j) + */ + template ArithVar selectSlack(ArithVar x_i); + + ArithVar selectSlackBelow(ArithVar x_i) { return selectSlack(x_i); } + ArithVar selectSlackAbove(ArithVar x_i) { return selectSlack(x_i); } + /** + * Returns the smallest basic variable whose assignment is not consistent + * with its upper and lower bounds. + */ + ArithVar selectSmallestInconsistentVar(); + + /** + * Given a non-basic variable that is know to not be updatable + * to a consistent value, construct and return a conflict. + * Follows section 4.2 in the CAV06 paper. + */ + Node generateConflictAbove(ArithVar conflictVar); + Node generateConflictBelow(ArithVar conflictVar); + +public: + /** Checks to make sure the assignment is consistent with the tableau. */ + void checkTableau(); + +private: + bool shouldEject(ArithVar var); + void ejectInactiveVariables(); + +public: + void reinjectVariable(ArithVar x); + + /** + * Computes the value of a basic variable using the assignments + * of the values of the variables in the basic variable's row tableau. + * This can compute the value using either: + * - the the current assignment (useSafe=false) or + * - the safe assignment (useSafe = true). + */ + DeltaRational computeRowValue(ArithVar x, bool useSafe); + +private: + /** Check to make sure all of the basic variables are within their bounds. */ + void checkBasicVariable(ArithVar basic); + + + /** These fields are designed to be accessable to TheoryArith methods. */ + class Statistics { + public: + IntStat d_statPivots, d_statUpdates, d_statAssertUpperConflicts; + IntStat d_statAssertLowerConflicts, d_statUpdateConflicts; + + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; + +};/* class SimplexDecisionProcedure */ + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__SIMPLEX_H */ + diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 6efffa21c..e691788fa 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -53,8 +53,6 @@ using namespace CVC4::theory::arith; struct SlackAttrID; typedef expr::Attribute Slack; -const static uint64_t ACTIVITY_THRESHOLD = 100; - TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) : Theory(id, c, out), d_constants(NodeManager::currentNM()), @@ -65,58 +63,27 @@ TheoryArith::TheoryArith(int id, context::Context* c, OutputChannel& out) : d_tableau(d_activityMonitor, d_basicManager), d_rewriter(&d_constants), d_propagator(c), + d_simplex(d_constants, d_partialModel, d_basicManager, d_out, d_activityMonitor, d_tableau), d_statistics() {} -TheoryArith::~TheoryArith(){ - for(vector::iterator i=d_variables.begin(); i!= d_variables.end(); ++i){ - Node var = *i; - Debug("arithgc") << var << endl; - } -} +TheoryArith::~TheoryArith(){} TheoryArith::Statistics::Statistics(): - d_statPivots("theory::arith::pivots",0), - d_statUpdates("theory::arith::updates",0), - d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0), - d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0), - d_statUpdateConflicts("theory::arith::UpdateConflicts", 0), d_statUserVariables("theory::arith::UserVariables", 0), d_statSlackVariables("theory::arith::SlackVariables", 0) { - StatisticsRegistry::registerStat(&d_statPivots); - StatisticsRegistry::registerStat(&d_statUpdates); - StatisticsRegistry::registerStat(&d_statAssertUpperConflicts); - StatisticsRegistry::registerStat(&d_statAssertLowerConflicts); - StatisticsRegistry::registerStat(&d_statUpdateConflicts); StatisticsRegistry::registerStat(&d_statUserVariables); StatisticsRegistry::registerStat(&d_statSlackVariables); } TheoryArith::Statistics::~Statistics(){ - StatisticsRegistry::unregisterStat(&d_statPivots); - StatisticsRegistry::unregisterStat(&d_statUpdates); - StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts); - StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts); - StatisticsRegistry::unregisterStat(&d_statUpdateConflicts); StatisticsRegistry::unregisterStat(&d_statUserVariables); StatisticsRegistry::unregisterStat(&d_statSlackVariables); } -bool TheoryArith::shouldEject(ArithVar var){ - if(d_partialModel.hasEitherBound(var)){ - return false; - }else if(d_tableau.isEjected(var)) { - return false; - }else if(!d_partialModel.hasEverHadABound(var)){ - return true; - }else if(d_activityMonitor[var] >= ACTIVITY_THRESHOLD){ - return true; - } - return false; -} ArithVar TheoryArith::findBasicRow(ArithVar variable){ for(ArithVarSet::iterator basicIter = d_tableau.begin(); @@ -132,28 +99,6 @@ ArithVar TheoryArith::findBasicRow(ArithVar variable){ return ARITHVAR_SENTINEL; } -void TheoryArith::ejectInactiveVariables(){ - Debug("decay") << "begin ejectInactiveVariables()" << endl; - for(ArithVar variable = 0, end = d_variables.size(); variable != end; ++variable){ - //TNode var = *i; - //ArithVar variable = asArithVar(var); - if(shouldEject(variable)){ - if(d_basicManager.isMember(variable)){ - Debug("decay") << "ejecting basic " << variable << endl;; - d_tableau.ejectBasic(variable); - } - } - } -} - -void TheoryArith::reinjectVariable(ArithVar x){ - d_tableau.reinjectBasic(x); - - - DeltaRational safeAssignment = computeRowValue(x, true); - DeltaRational assignment = computeRowValue(x, false); - d_partialModel.setAssignment(x,safeAssignment,assignment); -} void TheoryArith::preRegisterTerm(TNode n) { Debug("arith_preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl; @@ -206,13 +151,6 @@ void TheoryArith::preRegisterTerm(TNode n) { -void TheoryArith::checkBasicVariable(ArithVar basic){ - Assert(d_basicManager.isMember(basic)); - if(!d_partialModel.assignmentIsConsistent(basic)){ - d_possiblyInconsistent.push(basic); - } -} - bool TheoryArith::isTheoryLeaf(TNode x) const{ return x.getMetaKind() == kind::metakind::VARIABLE; } @@ -224,6 +162,8 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){ ArithVar varX = d_variables.size(); d_variables.push_back(Node(x)); + d_simplex.increaseMax(); + setArithVar(x,varX); Assert(varX == d_activityMonitor.size()); @@ -288,12 +228,15 @@ void TheoryArith::setupInitialValue(ArithVar x){ //This can go away if the tableau creation is done at preregister //time instead of register - DeltaRational safeAssignment = computeRowValue(x, true); - DeltaRational assignment = computeRowValue(x, false); + DeltaRational safeAssignment = d_simplex.computeRowValue(x, true); + DeltaRational assignment = d_simplex.computeRowValue(x, false); d_partialModel.initialize(x,safeAssignment); d_partialModel.setAssignment(x,assignment); - checkBasicVariable(x); + + //d_simplex.checkBasicVariable(x); + //Conciously violating unneeded check + //Strictly speaking checking x is unnessecary as it cannot have an upper or //lower bound. This is done to strongly enforce the notion that basic //variables should not be changed without begin checked. @@ -302,27 +245,6 @@ void TheoryArith::setupInitialValue(ArithVar x){ Debug("arithgc") << "setupVariable("<beginNonZero(), end = row->endNonZero(); - i != end;++i){ - ArithVar nonbasic = getArithVar(*i); - if(nonbasic == row->basic()) continue; - const Rational& coeff = getCoefficient(*i); - - const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe); - sum = sum + (assignment * coeff); - } - return sum; -} - - RewriteResponse TheoryArith::preRewrite(TNode n, bool topLevel) { return d_rewriter.preRewrite(n); } @@ -331,390 +253,6 @@ void TheoryArith::registerTerm(TNode tn){ Debug("arith") << "registerTerm(" << tn << ")" << endl; } -/* procedure AssertUpper( x_i <= c_i) */ -bool TheoryArith::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){ - - Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; - if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ - reinjectVariable(x_i); - } - - if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i - return false; //sat - } - if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i - Node lbc = d_partialModel.getLowerConstraint(x_i); - Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); - Debug("arith") << "AssertUpper conflict " << conflict << endl; - ++(d_statistics.d_statAssertUpperConflicts); - d_out->conflict(conflict); - return true; - } - - d_partialModel.setUpperConstraint(x_i,original); - d_partialModel.setUpperBound(x_i, c_i); - - d_activityMonitor[x_i] = 0; - - if(!d_basicManager.isMember(x_i)){ - if(d_partialModel.getAssignment(x_i) > c_i){ - update(x_i, c_i); - } - }else{ - checkBasicVariable(x_i); - } - d_partialModel.printModel(x_i); - return false; -} - -/* procedure AssertLower( x_i >= c_i ) */ -bool TheoryArith::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){ - Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl; - - if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ - reinjectVariable(x_i); - } - - if(d_partialModel.belowLowerBound(x_i, c_i, false)){ - return false; //sat - } - if(d_partialModel.aboveUpperBound(x_i, c_i, true)){ - Node ubc = d_partialModel.getUpperConstraint(x_i); - Node conflict = NodeManager::currentNM()->mkNode(AND, ubc, original); - d_out->conflict(conflict); - Debug("arith") << "AssertLower conflict " << conflict << endl; - ++(d_statistics.d_statAssertLowerConflicts); - return true; - } - - d_partialModel.setLowerConstraint(x_i,original); - d_partialModel.setLowerBound(x_i, c_i); - d_activityMonitor[x_i] = 0; - - if(!d_basicManager.isMember(x_i)){ - if(d_partialModel.getAssignment(x_i) < c_i){ - update(x_i, c_i); - } - }else{ - checkBasicVariable(x_i); - } - - return false; -} - -/* procedure AssertLower( x_i == c_i ) */ -bool TheoryArith::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode original){ - - Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl; - - if(d_basicManager.isMember(x_i) && d_tableau.isEjected(x_i)){ - reinjectVariable(x_i); - } - - // u_i <= c_i <= l_i - // This can happen if both c_i <= x_i and x_i <= c_i are in the system. - if(d_partialModel.belowLowerBound(x_i, c_i, false) && - d_partialModel.aboveUpperBound(x_i, c_i, false)){ - return false; //sat - } - - if(d_partialModel.aboveUpperBound(x_i, c_i, true)){ - Node ubc = d_partialModel.getUpperConstraint(x_i); - Node conflict = NodeManager::currentNM()->mkNode(AND, ubc, original); - d_out->conflict(conflict); - Debug("arith") << "AssertLower conflict " << conflict << endl; - return true; - } - - if(d_partialModel.belowLowerBound(x_i, c_i, true)){ - Node lbc = d_partialModel.getLowerConstraint(x_i); - Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); - Debug("arith") << "AssertUpper conflict " << conflict << endl; - d_out->conflict(conflict); - return true; - } - - d_partialModel.setLowerConstraint(x_i,original); - d_partialModel.setLowerBound(x_i, c_i); - - d_partialModel.setUpperConstraint(x_i,original); - d_partialModel.setUpperBound(x_i, c_i); - d_activityMonitor[x_i] = 0; - - if(!d_basicManager.isMember(x_i)){ - if(!(d_partialModel.getAssignment(x_i) == c_i)){ - update(x_i, c_i); - } - }else{ - checkBasicVariable(x_i); - } - - return false; -} -void TheoryArith::update(ArithVar x_i, const DeltaRational& v){ - Assert(!d_basicManager.isMember(x_i)); - DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i); - ++(d_statistics.d_statUpdates); - - Debug("arith") <<"update " << x_i << ": " - << assignment_x_i << "|-> " << v << endl; - DeltaRational diff = v - assignment_x_i; - - for(ArithVarSet::iterator basicIter = d_tableau.begin(); - basicIter != d_tableau.end(); - ++basicIter){ - ArithVar x_j = *basicIter; - ReducedRowVector* row_j = d_tableau.lookup(x_j); - - if(row_j->has(x_i)){ - const Rational& a_ji = row_j->lookup(x_i); - - const DeltaRational& assignment = d_partialModel.getAssignment(x_j); - DeltaRational nAssignment = assignment+(diff * a_ji); - d_partialModel.setAssignment(x_j, nAssignment); - - d_activityMonitor[x_j] += 1; - - checkBasicVariable(x_j); - } - } - - d_partialModel.setAssignment(x_i, v); - - if(Debug.isOn("paranoid:check_tableau")){ - checkTableau(); - } -} - -void TheoryArith::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){ - Assert(x_i != x_j); - - ReducedRowVector* row_i = d_tableau.lookup(x_i); - const Rational& a_ij = row_i->lookup(x_j); - - - const DeltaRational& betaX_i = d_partialModel.getAssignment(x_i); - - Rational inv_aij = a_ij.inverse(); - DeltaRational theta = (v - betaX_i)*inv_aij; - - d_partialModel.setAssignment(x_i, v); - - - DeltaRational tmp = d_partialModel.getAssignment(x_j) + theta; - d_partialModel.setAssignment(x_j, tmp); - - for(ArithVarSet::iterator basicIter = d_tableau.begin(); - basicIter != d_tableau.end(); - ++basicIter){ - ArithVar x_k = *basicIter; - ReducedRowVector* row_k = d_tableau.lookup(x_k); - - if(x_k != x_i && row_k->has(x_j)){ - const 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_activityMonitor[x_j] += 1; - - checkBasicVariable(x_k); - } - } - - ++(d_statistics.d_statPivots); - d_tableau.pivot(x_i, x_j); - - checkBasicVariable(x_j); - - if(Debug.isOn("tableau")){ - d_tableau.printTableau(); - } -} - -ArithVar TheoryArith::selectSmallestInconsistentVar(){ - Debug("arith_update") << "selectSmallestInconsistentVar()" << endl; - Debug("arith_update") << "possiblyInconsistent.size()" - << d_possiblyInconsistent.size() << endl; - - while(!d_possiblyInconsistent.empty()){ - ArithVar var = d_possiblyInconsistent.top(); - Debug("arith_update") << "possiblyInconsistent var" << var << endl; - if(d_basicManager.isMember(var)){ - if(!d_partialModel.assignmentIsConsistent(var)){ - return var; - } - } - d_possiblyInconsistent.pop(); - } - - if(Debug.isOn("paranoid:variables")){ - for(ArithVarSet::iterator basicIter = d_tableau.begin(); - basicIter != d_tableau.end(); - ++basicIter){ - - ArithVar basic = *basicIter; - Assert(d_partialModel.assignmentIsConsistent(basic)); - if(!d_partialModel.assignmentIsConsistent(basic)){ - return basic; - } - } - } - - return ARITHVAR_SENTINEL; -} - -template -ArithVar TheoryArith::selectSlack(ArithVar x_i){ - ReducedRowVector* row_i = d_tableau.lookup(x_i); - - for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); - nbi != end; ++nbi){ - ArithVar nonbasic = getArithVar(*nbi); - if(nonbasic == x_i) continue; - - const Rational& a_ij = nbi->second; - int cmp = a_ij.cmp(d_constants.d_ZERO); - if(above){ // beta(x_i) > u_i - if( cmp < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){ - return nonbasic; - }else if( cmp > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){ - return nonbasic; - } - }else{ //beta(x_i) < l_i - if(cmp > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){ - return nonbasic; - }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){ - return nonbasic; - } - } - } - return ARITHVAR_SENTINEL; -} - - -Node TheoryArith::updateInconsistentVars(){ //corresponds to Check() in dM06 - Debug("arith") << "updateInconsistentVars" << endl; - - static int iteratationNum = 0; - static const int EJECT_FREQUENCY = 10; - while(true){ - if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } - - ArithVar x_i = selectSmallestInconsistentVar(); - Debug("arith_update") << "selectSmallestInconsistentVar()=" << x_i << endl; - if(x_i == ARITHVAR_SENTINEL){ - Debug("arith_update") << "No inconsistent variables" << endl; - return Node::null(); //sat - } - - ++iteratationNum; - if(iteratationNum % EJECT_FREQUENCY == 0) - ejectInactiveVariables(); - - DeltaRational beta_i = d_partialModel.getAssignment(x_i); - - if(d_partialModel.belowLowerBound(x_i, beta_i, true)){ - DeltaRational l_i = d_partialModel.getLowerBound(x_i); - ArithVar x_j = selectSlackBelow(x_i); - if(x_j == ARITHVAR_SENTINEL ){ - ++(d_statistics.d_statUpdateConflicts); - return generateConflictBelow(x_i); //unsat - } - 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); - ArithVar x_j = selectSlackAbove(x_i); - if(x_j == ARITHVAR_SENTINEL ){ - ++(d_statistics.d_statUpdateConflicts); - return generateConflictAbove(x_i); //unsat - } - pivotAndUpdate(x_i, x_j, u_i); - } - } -} - -Node TheoryArith::generateConflictAbove(ArithVar conflictVar){ - - ReducedRowVector* row_i = d_tableau.lookup(conflictVar); - - NodeBuilder<> nb(kind::AND); - TNode bound = d_partialModel.getUpperConstraint(conflictVar); - - Debug("arith") << "generateConflictAbove " - << "conflictVar " << conflictVar - << " " << d_partialModel.getAssignment(conflictVar) - << " " << bound << endl; - - nb << bound; - - for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); - nbi != end; ++nbi){ - ArithVar nonbasic = getArithVar(*nbi); - if(nonbasic == conflictVar) continue; - - const Rational& a_ij = nbi->second; - - Assert(a_ij != d_constants.d_ZERO); - - if(a_ij < d_constants.d_ZERO){ - bound = d_partialModel.getUpperConstraint(nonbasic); - Debug("arith") << "below 0 " << nonbasic << " " - << d_partialModel.getAssignment(nonbasic) - << " " << bound << endl; - nb << bound; - }else{ - bound = d_partialModel.getLowerConstraint(nonbasic); - Debug("arith") << " above 0 " << nonbasic << " " - << d_partialModel.getAssignment(nonbasic) - << " " << bound << endl; - nb << bound; - } - } - Node conflict = nb; - return conflict; -} - -Node TheoryArith::generateConflictBelow(ArithVar conflictVar){ - ReducedRowVector* row_i = d_tableau.lookup(conflictVar); - - NodeBuilder<> nb(kind::AND); - TNode bound = d_partialModel.getLowerConstraint(conflictVar); - - Debug("arith") << "generateConflictBelow " - << "conflictVar " << conflictVar - << d_partialModel.getAssignment(conflictVar) << " " - << " " << bound << endl; - nb << bound; - - for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero(); nbi != end; ++nbi){ - ArithVar nonbasic = getArithVar(*nbi); - if(nonbasic != conflictVar) continue; - - const Rational& a_ij = nbi->second; - - Assert(a_ij != d_constants.d_ZERO); - - if(a_ij < d_constants.d_ZERO){ - TNode bound = d_partialModel.getLowerConstraint(nonbasic); - Debug("arith") << "Lower "<< nonbasic << " " - << d_partialModel.getAssignment(nonbasic) << " " - << bound << endl; - - nb << bound; - }else{ - TNode bound = d_partialModel.getUpperConstraint(nonbasic); - Debug("arith") << "Upper "<< nonbasic << " " - << d_partialModel.getAssignment(nonbasic) << " " - << bound << endl; - - nb << bound; - } - } - Node conflict (nb.constructNode()); - return conflict; -} - template TNode getSide(TNode assertion, Kind simpleKind){ switch(simpleKind){ @@ -766,12 +304,12 @@ bool TheoryArith::assertionCases(TNode assertion){ switch(simpKind){ case LEQ: case LT: - return AssertUpper(x_i, c_i, assertion); + return d_simplex.AssertUpper(x_i, c_i, assertion); case GT: case GEQ: - return AssertLower(x_i, c_i, assertion); + return d_simplex.AssertLower(x_i, c_i, assertion); case EQUAL: - return AssertEquality(x_i, c_i, assertion); + return d_simplex.AssertEquality(x_i, c_i, assertion); case DISTINCT: d_diseq.push_back(assertion); return false; @@ -798,9 +336,9 @@ void TheoryArith::check(Effort level){ } //TODO This must be done everytime for the time being - if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } + if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); } - Node possibleConflict = updateInconsistentVars(); + Node possibleConflict = d_simplex.updateInconsistentVars(); if(possibleConflict != Node::null()){ d_partialModel.revertAssignmentChanges(); @@ -814,7 +352,7 @@ void TheoryArith::check(Effort level){ }else{ d_partialModel.commitAssignmentChanges(); } - if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } + if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); } Debug("arith") << "TheoryArith::check end" << std::endl; @@ -843,41 +381,6 @@ void TheoryArith::check(Effort level){ } } -/** - * This check is quite expensive. - * It should be wrapped in a Debug.isOn() guard. - * if(Debug.isOn("paranoid:check_tableau")){ - * checkTableau(); - * } - */ -void TheoryArith::checkTableau(){ - - for(ArithVarSet::iterator basicIter = d_tableau.begin(); - basicIter != d_tableau.end(); ++basicIter){ - ArithVar basic = *basicIter; - ReducedRowVector* row_k = d_tableau.lookup(basic); - DeltaRational sum; - Debug("paranoid:check_tableau") << "starting row" << basic << endl; - for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k->beginNonZero(); - nonbasicIter != row_k->endNonZero(); - ++nonbasicIter){ - ArithVar nonbasic = nonbasicIter->first; - if(basic == nonbasic) continue; - - const Rational& coeff = nonbasicIter->second; - DeltaRational beta = d_partialModel.getAssignment(nonbasic); - Debug("paranoid:check_tableau") << nonbasic << beta << coeff<" @@ -904,7 +407,7 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { case kind::VARIABLE: { ArithVar var = asArithVar(n); if(d_tableau.isEjected(var)){ - reinjectVariable(var); + d_simplex.reinjectVariable(var); } DeltaRational drat = d_partialModel.getAssignment(var); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 5395327c0..af52da444 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -33,6 +33,7 @@ #include "theory/arith/arith_rewriter.h" #include "theory/arith/partial_model.h" #include "theory/arith/arith_propagator.h" +#include "theory/arith/simplex.h" #include "util/stats.h" @@ -98,6 +99,7 @@ private: ArithRewriter d_rewriter; ArithUnatePropagator d_propagator; + SimplexDecisionProcedure d_simplex; public: TheoryArith(int id, context::Context* c, OutputChannel& out); @@ -137,90 +139,9 @@ private: bool isTheoryLeaf(TNode x) const; - /** - * Assert*(n, orig) takes an bound n that is implied by orig. - * and asserts that as a new bound if it is tighter than the current bound - * and updates the value of a basic variable if needed. - * If this new bound is in conflict with the other bound, - * a conflict is created and asserted to the output channel. - * - * orig must be an atom in the SAT solver so that it can be used for - * conflict analysis. - * - * n is of the form (x =?= c) where x is a variable, - * c is a constant and =?= is either LT, LEQ, EQ, GEQ, or GT. - * - * returns true if a conflict was asserted. - */ - bool AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode orig); - bool AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig); - bool AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode orig); - ArithVar determineLeftVariable(TNode assertion, Kind simpleKind); - /** - * Updates the assignment of a nonbasic variable x_i to v. - * Also updates the assignment of basic variables accordingly. - */ - void update(ArithVar x_i, const DeltaRational& v); - - /** - * Updates the value of a basic variable x_i to v, - * and then pivots x_i with the nonbasic variable in its row x_j. - * Updates the assignment of the other basic variables accordingly. - */ - void pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v); - - /** - * Tries to update the assignments of variables such that all of the - * assignments are consistent with their bounds. - * - * This is done by searching through the tableau. - * If all of the variables can be made consistent with their bounds - * Node::null() is returned. Otherwise a minimized conflict is returned. - * - * If a conflict is found, changes to the assignments need to be reverted. - * - * Tableau pivoting is performed so variables may switch from being basic to - * nonbasic and vice versa. - * - * Corresponds to the "check()" procedure in [Cav06]. - */ - Node updateInconsistentVars(); - - /** - * Given the basic variable x_i, - * this function finds the smallest nonbasic variable x_j in the row of x_i - * in the tableau that can "take up the slack" to let x_i satisfy its bounds. - * This returns TNode::null() if none exists. - * - * More formally one of the following conditions must be satisfied: - * - above && a_ij < 0 && assignment(x_j) < upperbound(x_j) - * - above && a_ij > 0 && assignment(x_j) > lowerbound(x_j) - * - !above && a_ij > 0 && assignment(x_j) < upperbound(x_j) - * - !above && a_ij < 0 && assignment(x_j) > lowerbound(x_j) - */ - template ArithVar selectSlack(ArithVar x_i); - - ArithVar selectSlackBelow(ArithVar x_i) { return selectSlack(x_i); } - ArithVar selectSlackAbove(ArithVar x_i) { return selectSlack(x_i); } - - /** - * Returns the smallest basic variable whose assignment is not consistent - * with its upper and lower bounds. - */ - ArithVar selectSmallestInconsistentVar(); - - /** - * Given a non-basic variable that is know to not be updatable - * to a consistent value, construct and return a conflict. - * Follows section 4.2 in the CAV06 paper. - */ - Node generateConflictAbove(ArithVar conflictVar); - Node generateConflictBelow(ArithVar conflictVar); - - /** * This requests a new unique ArithVar value for x. * This also does initial (not context dependent) set up for a variable, @@ -234,20 +155,8 @@ private: /** Initial (not context dependent) sets up for a new slack variable.*/ void setupSlack(TNode left); - /** - * Computes the value of a basic variable using the assignments - * of the values of the variables in the basic variable's row tableau. - * This can compute the value using either: - * - the the current assignment (useSafe=false) or - * - the safe assignment (useSafe = true). - */ - DeltaRational computeRowValue(ArithVar x, bool useSafe); - /** Checks to make sure the assignment is consistent with the tableau. */ - void checkTableau(); - /** Check to make sure all of the basic variables are within their bounds. */ - void checkBasicVariable(ArithVar basic); /** * Handles the case splitting for check() for a new assertion. @@ -256,9 +165,6 @@ private: bool assertionCases(TNode assertion); ArithVar findBasicRow(ArithVar variable); - bool shouldEject(ArithVar var); - void ejectInactiveVariables(); - void reinjectVariable(ArithVar x); void asVectors(Polynomial& p, std::vector& coeffs, @@ -268,8 +174,6 @@ private: /** These fields are designed to be accessable to TheoryArith methods. */ class Statistics { public: - IntStat d_statPivots, d_statUpdates, d_statAssertUpperConflicts; - IntStat d_statAssertLowerConflicts, d_statUpdateConflicts; IntStat d_statUserVariables, d_statSlackVariables; Statistics(); -- 2.30.2