From: Tim King Date: Tue, 28 Feb 2012 21:26:35 +0000 (+0000) Subject: This commit merges in branches/arithmetic/internalbb up to revision 2831. This is... X-Git-Tag: cvc5-1.0.0~8297 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eefe0b63e564320eb135eb66d6c02c9dc6e9e8de;p=cvc5.git This commit merges in branches/arithmetic/internalbb up to revision 2831. This is a significant refactoring of code. - r2820 -- Refactors Simplex so that it does significantly fewer functions. -- Adds the LinearEqualityModule for handling update and pivotAndUpdate and other utility functions that require access to both the tableau and partial model. -- Some of the code for propagation has moved to TheoryArith. -r2826 -- Small changes to documentation and removes the no longer implemented deduceLowerBound() and deduceUpperBound(). - r2827 -- Adds isZero() to Rational. Adds cmp to DeltaRational. - r2831 -- Refactored comparison to upper and lower in the partial model to use DeltaRational::cmp. -- Refactored AssertUpper and AssertLower in TheoryArith to include functionality that has weaseled into TheoryArith::assertionCases. --- diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 4ca8aff0b..7934140a0 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -25,6 +25,8 @@ libarith_la_SOURCES = \ delta_rational.cpp \ partial_model.h \ partial_model.cpp \ + linear_equality.h \ + linear_equality.cpp \ ordered_set.h \ arithvar_set.h \ tableau.h \ diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp index e74a250a3..bd2939df9 100644 --- a/src/theory/arith/arith_priority_queue.cpp +++ b/src/theory/arith/arith_priority_queue.cpp @@ -118,7 +118,7 @@ ArithVar ArithPriorityQueue::dequeueInconsistentBasicVariable(){ ArithPriorityQueue::VarDRatPair ArithPriorityQueue::computeDiff(ArithVar basic){ Assert(basicAndInconsistent(basic)); const DeltaRational& beta = d_partialModel.getAssignment(basic); - DeltaRational diff = d_partialModel.belowLowerBound(basic,beta,true) ? + DeltaRational diff = d_partialModel.strictlyLessThanLowerBound(basic,beta) ? d_partialModel.getLowerBound(basic) - beta: beta - d_partialModel.getUpperBound(basic); diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 0168ee043..07387c977 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -51,6 +51,12 @@ typedef context::CDSet CDNodeSet; typedef context::CDSet CDArithVarSet; +class ArithVarCallBack { +public: + virtual void callback(ArithVar x) = 0; +}; + + inline Node mkRationalNode(const Rational& q){ return NodeManager::currentNM()->mkConst(q); diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 682d13720..c004a681f 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -63,6 +63,15 @@ public: } } + int cmp(const DeltaRational& other) const{ + int cmp = c.cmp(other.c); + if(cmp == 0){ + return k.cmp(other.k); + }else{ + return cmp; + } + } + DeltaRational operator+(const DeltaRational& other) const{ CVC4::Rational tmpC = c+other.c; CVC4::Rational tmpK = k+other.k; diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp new file mode 100644 index 000000000..c84e61285 --- /dev/null +++ b/src/theory/arith/linear_equality.cpp @@ -0,0 +1,302 @@ +/********************* */ +/*! \file simplex.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This implements the LinearEqualityModule. + ** + ** This implements the LinearEqualityModule. + **/ + + +#include "theory/arith/linear_equality.h" + +using namespace std; + +namespace CVC4 { +namespace theory { +namespace arith { + +/* Explicitly instatiate this function. */ +template void LinearEqualityModule::explainNonbasics(ArithVar basic, NodeBuilder<>& output); +template void LinearEqualityModule::explainNonbasics(ArithVar basic, NodeBuilder<>& output); + +LinearEqualityModule::Statistics::Statistics(): + d_statPivots("theory::arith::pivots",0), + d_statUpdates("theory::arith::updates",0), + d_pivotTime("theory::arith::pivotTime") +{ + StatisticsRegistry::registerStat(&d_statPivots); + StatisticsRegistry::registerStat(&d_statUpdates); + + StatisticsRegistry::registerStat(&d_pivotTime); +} + +LinearEqualityModule::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_statPivots); + StatisticsRegistry::unregisterStat(&d_statUpdates); + StatisticsRegistry::unregisterStat(&d_pivotTime); +} + +void LinearEqualityModule::update(ArithVar x_i, const DeltaRational& v){ + Assert(!d_tableau.isBasic(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; + + //Assert(matchingSets(d_tableau, x_i)); + Tableau::ColIterator basicIter = d_tableau.colIterator(x_i); + for(; !basicIter.atEnd(); ++basicIter){ + const TableauEntry& entry = *basicIter; + Assert(entry.getColVar() == x_i); + + ArithVar x_j = entry.getRowVar(); + //ReducedRowVector& row_j = d_tableau.lookup(x_j); + + //const Rational& a_ji = row_j.lookup(x_i); + const Rational& a_ji = entry.getCoefficient(); + + const DeltaRational& assignment = d_partialModel.getAssignment(x_j); + DeltaRational nAssignment = assignment+(diff * a_ji); + d_partialModel.setAssignment(x_j, nAssignment); + + d_basicVariableUpdates.callback(x_j); + } + + d_partialModel.setAssignment(x_i, v); + + Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_i)); + //double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_i)); + + //(d_statistics.d_avgNumRowsNotContainingOnUpdate).addEntry(difference); + if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); } +} + +void LinearEqualityModule::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){ + Assert(x_i != x_j); + + TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime); + + if(Debug.isOn("arith::simplex:row")){ debugPivot(x_i, x_j); } + + const TableauEntry& entry_ij = d_tableau.findEntry(x_i, x_j); + Assert(!entry_ij.blank()); + + + const Rational& a_ij = entry_ij.getCoefficient(); + + + 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); + + + //Assert(matchingSets(d_tableau, x_j)); + for(Tableau::ColIterator iter = d_tableau.colIterator(x_j); !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + Assert(entry.getColVar() == x_j); + ArithVar x_k = entry.getRowVar(); + if(x_k != x_i ){ + const Rational& a_kj = entry.getCoefficient(); + DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj); + d_partialModel.setAssignment(x_k, nextAssignment); + + d_basicVariableUpdates.callback(x_k); + } + } + + // Pivots + ++(d_statistics.d_statPivots); + + Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_j)); + //double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_j)); + //(d_statistics.d_avgNumRowsNotContainingOnPivot).addEntry(difference); + d_tableau.pivot(x_i, x_j); + + d_basicVariableUpdates.callback(x_j); + + if(Debug.isOn("tableau")){ + d_tableau.printTableau(); + } +} + + +void LinearEqualityModule::debugPivot(ArithVar x_i, ArithVar x_j){ + Debug("arith::pivot") << "debugPivot("<< x_i <<"|->"<< x_j << ")" << endl; + + for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + + ArithVar var = entry.getColVar(); + const Rational& coeff = entry.getCoefficient(); + DeltaRational beta = d_partialModel.getAssignment(var); + Debug("arith::pivot") << var << beta << coeff; + if(d_partialModel.hasLowerBound(var)){ + Debug("arith::pivot") << "(lb " << d_partialModel.getLowerBound(var) << ")"; + } + if(d_partialModel.hasUpperBound(var)){ + Debug("arith::pivot") << "(up " << d_partialModel.getUpperBound(var) << ")"; + } + Debug("arith::pivot") << endl; + } + Debug("arith::pivot") << "end row"<< endl; +} + +/** + * This check is quite expensive. + * It should be wrapped in a Debug.isOn() guard. + * if(Debug.isOn("paranoid:check_tableau")){ + * checkTableau(); + * } + */ +void LinearEqualityModule::debugCheckTableau(){ + ArithVarSet::const_iterator basicIter = d_tableau.beginBasic(); + ArithVarSet::const_iterator endIter = d_tableau.endBasic(); + for(; basicIter != endIter; ++basicIter){ + ArithVar basic = *basicIter; + DeltaRational sum; + Debug("paranoid:check_tableau") << "starting row" << basic << endl; + Tableau::RowIterator nonbasicIter = d_tableau.rowIterator(basic); + for(; !nonbasicIter.atEnd(); ++nonbasicIter){ + const TableauEntry& entry = *nonbasicIter; + ArithVar nonbasic = entry.getColVar(); + if(basic == nonbasic) continue; + + const Rational& coeff = entry.getCoefficient(); + DeltaRational beta = d_partialModel.getAssignment(nonbasic); + Debug("paranoid:check_tableau") << nonbasic << beta << coeff< 0) : (sgn < 0); + + const DeltaRational& bound = ub ? + d_partialModel.getUpperBound(nonbasic): + d_partialModel.getLowerBound(nonbasic); + + DeltaRational diff = bound * coeff; + sum = sum + diff; + } + return sum; +} + +/** + * Computes the value of a basic variable using the current assignment. + */ +DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe){ + Assert(d_tableau.isBasic(x)); + DeltaRational sum(0); + + for(Tableau::RowIterator i = d_tableau.rowIterator(x); !i.atEnd(); ++i){ + const TableauEntry& entry = (*i); + ArithVar nonbasic = entry.getColVar(); + if(nonbasic == x) continue; + const Rational& coeff = entry.getCoefficient(); + + const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe); + sum = sum + (assignment * coeff); + } + return sum; +} + +bool LinearEqualityModule::hasBounds(ArithVar basic, bool upperBound){ + for(Tableau::RowIterator iter = d_tableau.rowIterator(basic); !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + + ArithVar var = entry.getColVar(); + if(var == basic) continue; + int sgn = entry.getCoefficient().sgn(); + if(upperBound){ + if( (sgn < 0 && !d_partialModel.hasLowerBound(var)) || + (sgn > 0 && !d_partialModel.hasUpperBound(var))){ + return false; + } + }else{ + if( (sgn < 0 && !d_partialModel.hasUpperBound(var)) || + (sgn > 0 && !d_partialModel.hasLowerBound(var))){ + return false; + } + } + } + return true; +} + +template +void LinearEqualityModule::explainNonbasics(ArithVar basic, NodeBuilder<>& output){ + Assert(d_tableau.isBasic(basic)); + + Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics(" + << basic <<") start" << endl; + + + Tableau::RowIterator iter = d_tableau.rowIterator(basic); + for(; !iter.atEnd(); ++iter){ + const TableauEntry& entry = *iter; + ArithVar nonbasic = entry.getColVar(); + if(nonbasic == basic) continue; + + const Rational& a_ij = entry.getCoefficient(); + TNode bound = TNode::null(); + + int sgn = a_ij.sgn(); + Assert(sgn != 0); + if(upperBound){ + if(sgn < 0){ + bound = d_partialModel.getLowerConstraint(nonbasic); + }else{ + Assert(sgn > 0); + bound = d_partialModel.getUpperConstraint(nonbasic); + } + }else{ + if(sgn < 0){ + bound = d_partialModel.getUpperConstraint(nonbasic); + }else{ + Assert(sgn > 0); + bound = d_partialModel.getLowerConstraint(nonbasic); + } + } + Assert(!bound.isNull()); + Debug("arith::explainNonbasics") << "\t" << nonbasic << " " << sgn << " " << bound + << endl; + output << bound; + } + Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics(" + << basic << ") done" << endl; +} + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h new file mode 100644 index 000000000..aa8a49238 --- /dev/null +++ b/src/theory/arith/linear_equality.h @@ -0,0 +1,163 @@ +/********************* */ +/*! \file linear_equality.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief This module maintains the relationship between a Tableau and PartialModel. + ** + ** This shares with the theory a Tableau, and a PartialModel that: + ** - satisfies the equalities in the Tableau, and + ** - the assignment for the non-basic variables satisfies their bounds. + ** This maintains the relationship needed by the SimplexDecisionProcedure. + ** + ** In the language of Simplex for DPLL(T), this provides: + ** - update() + ** - pivotAndUpdate() + ** + ** This class also provides utility functions that require + ** using both the Tableau and PartialModel. + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H +#define __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H + +#include "theory/arith/delta_rational.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/partial_model.h" +#include "theory/arith/tableau.h" + +#include "util/stats.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +class LinearEqualityModule { +private: + /** + * Manages information about the assignment and upper and lower bounds on the + * variables. + */ + ArithPartialModel& d_partialModel; + + /** + * Reference to the Tableau to operate upon. + */ + Tableau& d_tableau; + + /** Called whenever the value of a basic variable is updated. */ + ArithVarCallBack& d_basicVariableUpdates; + +public: + + /** + * Initailizes a LinearEqualityModule with a partial model, a tableau, + * and a callback function for when basic variables update their values. + */ + LinearEqualityModule(ArithPartialModel& pm, Tableau& t, ArithVarCallBack& f): + d_partialModel(pm), d_tableau(t), d_basicVariableUpdates(f) + {} + + /** + * 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); + + + ArithPartialModel& getPartialModel() const{ return d_partialModel; } + Tableau& getTableau() const{ return d_tableau; } + + + bool hasBounds(ArithVar basic, bool upperBound); + bool hasLowerBounds(ArithVar basic){ + return hasBounds(basic, false); + } + bool hasUpperBounds(ArithVar basic){ + return hasBounds(basic, true); + } + +private: + /** + * Exports either the explanation of an upperbound or a lower bound + * of the basic variable basic, using the non-basic variables in the row. + */ + template + void explainNonbasics(ArithVar basic, NodeBuilder<>& output); + +public: + void explainNonbasicsLowerBound(ArithVar basic, NodeBuilder<>& output){ + explainNonbasics(basic, output); + } + void explainNonbasicsUpperBound(ArithVar basic, NodeBuilder<>& output){ + explainNonbasics(basic, output); + } + + /** + * 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); + + inline DeltaRational computeLowerBound(ArithVar basic){ + return computeBound(basic, false); + } + inline DeltaRational computeUpperBound(ArithVar basic){ + return computeBound(basic, true); + } + +private: + DeltaRational computeBound(ArithVar basic, bool upperBound); + +public: + /** + * Checks to make sure the assignment is consistent with the tableau. + * This code is for debugging. + */ + void debugCheckTableau(); + + /** Debugging information for a pivot. */ + void debugPivot(ArithVar x_i, ArithVar x_j); + + +private: + /** These fields are designed to be accessable to TheoryArith methods. */ + class Statistics { + public: + IntStat d_statPivots, d_statUpdates; + + TimerStat d_pivotTime; + + Statistics(); + ~Statistics(); + }; + Statistics d_statistics; + +};/* class LinearEqualityModule */ + +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H */ diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 4a126ec55..f113c4d34 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -209,21 +209,52 @@ TNode ArithPartialModel::getUpperConstraint(ArithVar x){ return d_upperConstraint[x]; } - - -bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){ +int ArithPartialModel::cmpToLowerBound(ArithVar x, const DeltaRational& c){ if(!hasLowerBound(x)){ // l = -\intfy // ? c < -\infty |- _|_ - return false; + return 1; + }else{ + return c.cmp(d_lowerBound[x]); } - if(strict){ - return c < d_lowerBound[x]; +} + +int ArithPartialModel::cmpToUpperBound(ArithVar x, const DeltaRational& c){ + if(!hasUpperBound(x)){ + //u = \intfy + // ? c > \infty |- _|_ + return -1; }else{ - return c <= d_lowerBound[x]; + return c.cmp(d_upperBound[x]); } } +// bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){ +// if(!hasLowerBound(x)){ +// // l = -\intfy +// // ? c < -\infty |- _|_ +// return false; +// } +// if(strict){ +// return c < d_lowerBound[x]; +// }else{ +// return c <= d_lowerBound[x]; +// } +// } + +// bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){ +// if(!hasUpperBound(x)){ +// // u = \intfy +// // ? c > \infty |- _|_ +// return false; +// } +// if(strict){ +// return c > d_upperBound[x]; +// }else{ +// return c >= d_upperBound[x]; +// } +// } + bool ArithPartialModel::equalsLowerBound(ArithVar x, const DeltaRational& c){ if(!hasLowerBound(x)){ return false; @@ -239,18 +270,6 @@ bool ArithPartialModel::equalsUpperBound(ArithVar x, const DeltaRational& c){ } } -bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){ - if(!hasUpperBound(x)){ - // u = \intfy - // ? c > \infty |- _|_ - return false; - } - if(strict){ - return c > d_upperBound[x]; - }else{ - return c >= d_upperBound[x]; - } -} bool ArithPartialModel::hasEitherBound(ArithVar x){ return hasLowerBound(x) || hasUpperBound(x); } @@ -271,35 +290,35 @@ bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){ return d_lowerBound[x] < d_assignment[x]; } -/** - * x <= u - * ? c < u - */ -bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x, const DeltaRational& c){ - Assert(inMaps(x)); - if(!hasUpperBound(x)){ // u = \infty - return true; - } - return c < d_upperBound[x]; -} - -/** - * x <= u - * ? c < u - */ -bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x, const DeltaRational& c){ - Assert(inMaps(x)); - if(!hasLowerBound(x)){ // l = -\infty - return true; - } - return d_lowerBound[x] < c; -} +// /** +// * x <= u +// * ? c < u +// */ +// bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x, const DeltaRational& c){ +// Assert(inMaps(x)); +// if(!hasUpperBound(x)){ // u = \infty +// return true; +// } +// return c < d_upperBound[x]; +// } + +// /** +// * x <= u +// * ? c < u +// */ +// bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x, const DeltaRational& c){ +// Assert(inMaps(x)); +// if(!hasLowerBound(x)){ // l = -\infty +// return true; +// } +// return d_lowerBound[x] < c; +// } bool ArithPartialModel::assignmentIsConsistent(ArithVar x){ const DeltaRational& beta = getAssignment(x); //l_i <= beta(x_i) <= u_i - return !belowLowerBound(x,beta,true) && !aboveUpperBound(x,beta,true); + return cmpToLowerBound(x,beta) >= 0 && cmpToUpperBound(x,beta) <= 0; } diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index cf0fc7d4e..d9fa51d8d 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -132,33 +132,52 @@ public: const DeltaRational& getAssignment(ArithVar x) const; + bool equalsLowerBound(ArithVar x, const DeltaRational& c); + bool equalsUpperBound(ArithVar x, const DeltaRational& c); /** - * x >= l - * ? c < l + * If lowerbound > - \infty: + * return getAssignment(x).cmp(getLowerBound(x)) + * If lowerbound = - \infty: + * return 1 */ - bool belowLowerBound(ArithVar x, const DeltaRational& c, bool strict); + int cmpToLowerBound(ArithVar x, const DeltaRational& c); - /** - * x <= u - * ? c > u - */ - bool aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict); + inline bool strictlyLessThanLowerBound(ArithVar x, const DeltaRational& c){ + return cmpToLowerBound(x, c) < 0; + } + inline bool lessThanLowerBound(ArithVar x, const DeltaRational& c){ + return cmpToLowerBound(x, c) <= 0; + } - bool equalsLowerBound(ArithVar x, const DeltaRational& c); - bool equalsUpperBound(ArithVar x, const DeltaRational& c); + inline bool strictlyGreaterThanLowerBound(ArithVar x, const DeltaRational& c){ + return cmpToLowerBound(x, c) > 0; + } /** - * x <= u - * ? c < u + * If upperbound < \infty: + * return getAssignment(x).cmp(getUpperBound(x)) + * If upperbound = \infty: + * return -1 */ - bool strictlyBelowUpperBound(ArithVar x, const DeltaRational& c); + int cmpToUpperBound(ArithVar x, const DeltaRational& c); + + inline bool strictlyLessThanUpperBound(ArithVar x, const DeltaRational& c){ + return cmpToUpperBound(x, c) < 0; + } + + inline bool lessThanUpperBound(ArithVar x, const DeltaRational& c){ + return cmpToUpperBound(x, c) <= 0; + } + + inline bool strictlyGreaterThanUpperBound(ArithVar x, const DeltaRational& c){ + return cmpToUpperBound(x, c) > 0; + } + + inline bool greaterThanUpperBound(ArithVar x, const DeltaRational& c){ + return cmpToUpperBound(x, c) >= 0; + } - /** - * x <= u - * ? c < u - */ - bool strictlyAboveLowerBound(ArithVar x, const DeltaRational& c); bool strictlyBelowUpperBound(ArithVar x); bool strictlyAboveLowerBound(ArithVar x); diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 6f8d02642..7fce748dc 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -34,16 +34,15 @@ static const bool CHECK_AFTER_PIVOT = true; static const uint32_t VARORDER_CHECK_PERIOD = 200; SimplexDecisionProcedure::SimplexDecisionProcedure(ArithPropManager& propManager, - ArithPartialModel& pm, - Tableau& tableau) : - d_partialModel(pm), - d_tableau(tableau), - d_queue(pm, tableau), + LinearEqualityModule& linEq) : + d_linEq(linEq), + d_partialModel(d_linEq.getPartialModel()), + d_tableau(d_linEq.getTableau()), + d_queue(d_partialModel, d_tableau), d_propManager(propManager), d_numVariables(0), d_delayedLemmas(), d_pivotsInRound(), - d_ZERO(0), d_DELTA_ZERO(0,0) { switch(Options::ArithPivotRule rule = Options::current()->pivotRule) { @@ -62,10 +61,6 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(ArithPropManager& propManager } 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), d_findConflictOnTheQueueTime("theory::arith::findConflictOnTheQueueTime"), d_attemptBeforeDiffSearch("theory::arith::qi::BeforeDiffSearch::attempt",0), @@ -82,18 +77,8 @@ SimplexDecisionProcedure::Statistics::Statistics(): d_weakeningSuccesses("theory::arith::weakening::success",0), d_weakenings("theory::arith::weakening::total",0), d_weakenTime("theory::arith::weakening::time"), - d_boundComputationTime("theory::arith::bound::time"), - d_boundComputations("theory::arith::bound::boundComputations",0), - d_boundPropagations("theory::arith::bound::boundPropagations",0), - d_delayedConflicts("theory::arith::delayedConflicts",0), - d_pivotTime("theory::arith::pivotTime"), - d_avgNumRowsNotContainingOnUpdate("theory::arith::avgNumRowsNotContainingOnUpdate"), - d_avgNumRowsNotContainingOnPivot("theory::arith::avgNumRowsNotContainingOnPivot") + d_delayedConflicts("theory::arith::delayedConflicts",0) { - StatisticsRegistry::registerStat(&d_statPivots); - StatisticsRegistry::registerStat(&d_statUpdates); - StatisticsRegistry::registerStat(&d_statAssertUpperConflicts); - StatisticsRegistry::registerStat(&d_statAssertLowerConflicts); StatisticsRegistry::registerStat(&d_statUpdateConflicts); StatisticsRegistry::registerStat(&d_findConflictOnTheQueueTime); @@ -114,23 +99,10 @@ SimplexDecisionProcedure::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_weakenings); StatisticsRegistry::registerStat(&d_weakenTime); - StatisticsRegistry::registerStat(&d_boundComputationTime); - StatisticsRegistry::registerStat(&d_boundComputations); - StatisticsRegistry::registerStat(&d_boundPropagations); - StatisticsRegistry::registerStat(&d_delayedConflicts); - - StatisticsRegistry::registerStat(&d_pivotTime); - - StatisticsRegistry::registerStat(&d_avgNumRowsNotContainingOnUpdate); - StatisticsRegistry::registerStat(&d_avgNumRowsNotContainingOnPivot); } SimplexDecisionProcedure::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_findConflictOnTheQueueTime); @@ -151,356 +123,14 @@ SimplexDecisionProcedure::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_weakenings); StatisticsRegistry::unregisterStat(&d_weakenTime); - StatisticsRegistry::unregisterStat(&d_boundComputationTime); - StatisticsRegistry::unregisterStat(&d_boundComputations); - StatisticsRegistry::unregisterStat(&d_boundPropagations); - StatisticsRegistry::unregisterStat(&d_delayedConflicts); - StatisticsRegistry::unregisterStat(&d_pivotTime); - - StatisticsRegistry::unregisterStat(&d_avgNumRowsNotContainingOnUpdate); - StatisticsRegistry::unregisterStat(&d_avgNumRowsNotContainingOnPivot); -} - -/* procedure AssertLower( x_i >= c_i ) */ -Node SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){ - Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl; - - if(d_partialModel.belowLowerBound(x_i, c_i, true)){ - return Node::null(); - } - - 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 conflict; - } - - d_partialModel.setLowerConstraint(x_i,original); - d_partialModel.setLowerBound(x_i, c_i); - - d_updatedBounds.softAdd(x_i); - - if(!d_tableau.isBasic(x_i)){ - if(d_partialModel.getAssignment(x_i) < c_i){ - update(x_i, c_i); - } - }else{ - d_queue.enqueueIfInconsistent(x_i); - } - - if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } - - return Node::null(); -} - -/* procedure AssertUpper( x_i <= c_i) */ -Node SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){ - - Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; - - if(d_partialModel.aboveUpperBound(x_i, c_i, true) ){ // \upperbound(x_i) <= c_i - return Node::null(); //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); - return conflict; - } - - d_partialModel.setUpperConstraint(x_i,original); - d_partialModel.setUpperBound(x_i, c_i); - - d_updatedBounds.softAdd(x_i); - - if(!d_tableau.isBasic(x_i)){ - if(d_partialModel.getAssignment(x_i) > c_i){ - update(x_i, c_i); - } - }else{ - d_queue.enqueueIfInconsistent(x_i); - } - - if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } - - return Node::null(); -} - - -/* procedure AssertLower( x_i == c_i ) */ -Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode original){ - - Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl; - - // 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 Node::null(); //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); - Debug("arith") << "AssertLower conflict " << conflict << endl; - return conflict; - } - - 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; - return conflict; - } - - 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_updatedBounds.softAdd(x_i); - - if(!d_tableau.isBasic(x_i)){ - if(!(d_partialModel.getAssignment(x_i) == c_i)){ - update(x_i, c_i); - } - }else{ - d_queue.enqueueIfInconsistent(x_i); - } - return Node::null(); -} - -void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){ - Assert(!d_tableau.isBasic(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; - - //Assert(matchingSets(d_tableau, x_i)); - Tableau::ColIterator basicIter = d_tableau.colIterator(x_i); - for(; !basicIter.atEnd(); ++basicIter){ - const TableauEntry& entry = *basicIter; - Assert(entry.getColVar() == x_i); - - ArithVar x_j = entry.getRowVar(); - //ReducedRowVector& row_j = d_tableau.lookup(x_j); - - //const Rational& a_ji = row_j.lookup(x_i); - const Rational& a_ji = entry.getCoefficient(); - - const DeltaRational& assignment = d_partialModel.getAssignment(x_j); - DeltaRational nAssignment = assignment+(diff * a_ji); - d_partialModel.setAssignment(x_j, nAssignment); - - d_queue.enqueueIfInconsistent(x_j); - } - - d_partialModel.setAssignment(x_i, v); - - Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_i)); - double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_i)); - - (d_statistics.d_avgNumRowsNotContainingOnUpdate).addEntry(difference); - if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); } -} - - -bool SimplexDecisionProcedure::propagateCandidateBound(ArithVar basic, bool upperBound){ - - DeltaRational bound = upperBound ? - computeUpperBound(basic): - computeLowerBound(basic); - - if((upperBound && d_partialModel.strictlyBelowUpperBound(basic, bound)) || - (!upperBound && d_partialModel.strictlyAboveLowerBound(basic, bound))){ - Node bestImplied = upperBound ? - d_propManager.getBestImpliedUpperBound(basic, bound): - d_propManager.getBestImpliedLowerBound(basic, bound); - - if(!bestImplied.isNull()){ - bool asserted = d_propManager.isAsserted(bestImplied); - bool propagated = d_propManager.isPropagated(bestImplied); - if( !asserted && !propagated){ - - NodeBuilder<> nb(kind::AND); - if(upperBound){ - explainNonbasicsUpperBound(basic, nb); - }else{ - explainNonbasicsLowerBound(basic, nb); - } - Node explanation = nb; - d_propManager.propagate(bestImplied, explanation, false); - return true; - }else{ - Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl; - } - } - } - return false; -} - - -bool SimplexDecisionProcedure::hasBounds(ArithVar basic, bool upperBound){ - for(Tableau::RowIterator iter = d_tableau.rowIterator(basic); !iter.atEnd(); ++iter){ - const TableauEntry& entry = *iter; - - ArithVar var = entry.getColVar(); - if(var == basic) continue; - int sgn = entry.getCoefficient().sgn(); - if(upperBound){ - if( (sgn < 0 && !d_partialModel.hasLowerBound(var)) || - (sgn > 0 && !d_partialModel.hasUpperBound(var))){ - return false; - } - }else{ - if( (sgn < 0 && !d_partialModel.hasUpperBound(var)) || - (sgn > 0 && !d_partialModel.hasLowerBound(var))){ - return false; - } - } - } - return true; } -void SimplexDecisionProcedure::propagateCandidate(ArithVar basic){ - bool success = false; - if(d_partialModel.strictlyAboveLowerBound(basic) && hasLowerBounds(basic)){ - ++d_statistics.d_boundComputations; - success |= propagateCandidateLowerBound(basic); - } - if(d_partialModel.strictlyBelowUpperBound(basic) && hasUpperBounds(basic)){ - ++d_statistics.d_boundComputations; - success |= propagateCandidateUpperBound(basic); - } - if(success){ - ++d_statistics.d_boundPropagations; - } -} - -void SimplexDecisionProcedure::propagateCandidates(){ - TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime); - Assert(d_candidateBasics.empty()); - if(d_updatedBounds.empty()){ return; } - PermissiveBackArithVarSet::const_iterator i = d_updatedBounds.begin(); - PermissiveBackArithVarSet::const_iterator end = d_updatedBounds.end(); - for(; i != end; ++i){ - ArithVar var = *i; - if(d_tableau.isBasic(var) && - d_tableau.getRowLength(var) <= Options::current()->arithPropagateMaxLength){ - d_candidateBasics.softAdd(var); - }else{ - Tableau::ColIterator basicIter = d_tableau.colIterator(var); - for(; !basicIter.atEnd(); ++basicIter){ - const TableauEntry& entry = *basicIter; - ArithVar rowVar = entry.getRowVar(); - Assert(entry.getColVar() == var); - Assert(d_tableau.isBasic(rowVar)); - if(d_tableau.getRowLength(rowVar) <= Options::current()->arithPropagateMaxLength){ - d_candidateBasics.softAdd(rowVar); - } - } - } - } - d_updatedBounds.purge(); - - while(!d_candidateBasics.empty()){ - ArithVar candidate = d_candidateBasics.pop_back(); - Assert(d_tableau.isBasic(candidate)); - propagateCandidate(candidate); - } -} -void SimplexDecisionProcedure::debugPivotSimplex(ArithVar x_i, ArithVar x_j){ - Debug("arith::simplex:row") << "debugRowSimplex(" - << x_i << "|->" << x_j - << ")" << endl; - for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){ - const TableauEntry& entry = *iter; - - ArithVar var = entry.getColVar(); - const Rational& coeff = entry.getCoefficient(); - DeltaRational beta = d_partialModel.getAssignment(var); - Debug("arith::simplex:row") << var << beta << coeff; - if(d_partialModel.hasLowerBound(var)){ - Debug("arith::simplex:row") << "(lb " << d_partialModel.getLowerBound(var) << ")"; - } - if(d_partialModel.hasUpperBound(var)){ - Debug("arith::simplex:row") << "(up " << d_partialModel.getUpperBound(var) << ")"; - } - Debug("arith::simplex:row") << endl; - } - Debug("arith::simplex:row") << "end row"<< endl; -} - -void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){ - Assert(x_i != x_j); - - TimerStat::CodeTimer codeTimer(d_statistics.d_pivotTime); - - if(Debug.isOn("arith::simplex:row")){ debugPivotSimplex(x_i, x_j); } - - const TableauEntry& entry_ij = d_tableau.findEntry(x_i, x_j); - Assert(!entry_ij.blank()); - - - const Rational& a_ij = entry_ij.getCoefficient(); - - - 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); - - - //Assert(matchingSets(d_tableau, x_j)); - for(Tableau::ColIterator iter = d_tableau.colIterator(x_j); !iter.atEnd(); ++iter){ - const TableauEntry& entry = *iter; - Assert(entry.getColVar() == x_j); - ArithVar x_k = entry.getRowVar(); - if(x_k != x_i ){ - const Rational& a_kj = entry.getCoefficient(); - DeltaRational nextAssignment = d_partialModel.getAssignment(x_k) + (theta * a_kj); - d_partialModel.setAssignment(x_k, nextAssignment); - - d_queue.enqueueIfInconsistent(x_k); - } - } - - // Pivots - ++(d_statistics.d_statPivots); - - Assert(d_tableau.getNumRows() >= d_tableau.getRowLength(x_j)); - double difference = ((double)d_tableau.getNumRows()) - ((double) d_tableau.getRowLength(x_j)); - (d_statistics.d_avgNumRowsNotContainingOnPivot).addEntry(difference); - d_tableau.pivot(x_i, x_j); - - - d_queue.enqueueIfInconsistent(x_j); - - if(Debug.isOn("tableau")){ - d_tableau.printTableau(); - } -} ArithVar SimplexDecisionProcedure::minVarOrder(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y){ Assert(x != ARITHVAR_SENTINEL); @@ -615,15 +245,14 @@ Node SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type, bool re return firstConflict; } -Node SimplexDecisionProcedure::updateInconsistentVars(){ +Node SimplexDecisionProcedure::findModel(){ if(d_queue.empty()){ return Node::null(); } static CVC4_THREADLOCAL(unsigned int) instance = 0; instance = instance + 1; - Debug("arith::updateInconsistentVars") << "begin updateInconsistentVars() " - << instance << endl; + Debug("arith::findModel") << "begin findModel()" << instance << endl; d_queue.transitionToDifferenceMode(); @@ -678,8 +307,7 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){ Assert(d_queue.inCollectionMode()); - Debug("arith::updateInconsistentVars") << "end updateInconsistentVars() " - << instance << endl; + Debug("arith::findModel") << "end findModel() " << instance << endl; return possibleConflict; } @@ -689,12 +317,12 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ Assert(d_tableau.isBasic(basic)); const DeltaRational& beta = d_partialModel.getAssignment(basic); - if(d_partialModel.belowLowerBound(basic, beta, true)){ + if(d_partialModel.strictlyLessThanLowerBound(basic, beta)){ ArithVar x_j = selectSlackUpperBound(basic); if(x_j == ARITHVAR_SENTINEL ){ return generateConflictBelowLowerBound(basic); } - }else if(d_partialModel.aboveUpperBound(basic, beta, true)){ + }else if(d_partialModel.strictlyGreaterThanUpperBound(basic, beta)){ ArithVar x_j = selectSlackLowerBound(basic); if(x_j == ARITHVAR_SENTINEL ){ return generateConflictAboveUpperBound(basic); @@ -706,11 +334,11 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){ //corresponds to Check() in dM06 //template Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){ - Debug("arith") << "updateInconsistentVars" << endl; + Debug("arith") << "searchForFeasibleSolution" << endl; Assert(remainingIterations > 0); while(remainingIterations > 0){ - if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); } + if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); } ArithVar x_i = d_queue.dequeueInconsistentBasicVariable(); Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl; @@ -737,23 +365,23 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera DeltaRational beta_i = d_partialModel.getAssignment(x_i); ArithVar x_j = ARITHVAR_SENTINEL; - if(d_partialModel.belowLowerBound(x_i, beta_i, true)){ + if(d_partialModel.strictlyLessThanLowerBound(x_i, beta_i)){ x_j = selectSlackUpperBound(x_i, pf); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); return generateConflictBelowLowerBound(x_i); //unsat } DeltaRational l_i = d_partialModel.getLowerBound(x_i); - pivotAndUpdate(x_i, x_j, l_i); + d_linEq.pivotAndUpdate(x_i, x_j, l_i); - }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){ + }else if(d_partialModel.strictlyGreaterThanUpperBound(x_i, beta_i)){ x_j = selectSlackLowerBound(x_i, pf); if(x_j == ARITHVAR_SENTINEL ){ ++(d_statistics.d_statUpdateConflicts); return generateConflictAboveUpperBound(x_i); //unsat } DeltaRational u_i = d_partialModel.getUpperBound(x_i); - pivotAndUpdate(x_i, x_j, u_i); + d_linEq.pivotAndUpdate(x_i, x_j, u_i); } Assert(x_j != ARITHVAR_SENTINEL); @@ -770,49 +398,6 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera return Node::null(); } -template -void SimplexDecisionProcedure::explainNonbasics(ArithVar basic, NodeBuilder<>& output){ - Assert(d_tableau.isBasic(basic)); - - Debug("arith::explainNonbasics") << "SimplexDecisionProcedure::explainNonbasics(" - << basic <<") start" << endl; - - - Tableau::RowIterator iter = d_tableau.rowIterator(basic); - for(; !iter.atEnd(); ++iter){ - const TableauEntry& entry = *iter; - ArithVar nonbasic = entry.getColVar(); - if(nonbasic == basic) continue; - - const Rational& a_ij = entry.getCoefficient(); - Assert(a_ij != d_ZERO); - TNode bound = TNode::null(); - - int sgn = a_ij.sgn(); - Assert(sgn != 0); - if(upperBound){ - if(sgn < 0){ - bound = d_partialModel.getLowerConstraint(nonbasic); - }else{ - Assert(sgn > 0); - bound = d_partialModel.getUpperConstraint(nonbasic); - } - }else{ - if(sgn < 0){ - bound = d_partialModel.getUpperConstraint(nonbasic); - }else{ - Assert(sgn > 0); - bound = d_partialModel.getLowerConstraint(nonbasic); - } - } - Assert(!bound.isNull()); - Debug("arith::explainNonbasics") << "\t" << nonbasic << " " << sgn << " " << bound - << endl; - output << bound; - } - Debug("arith::explainNonbasics") << "SimplexDecisionProcedure::explainNonbasics(" - << basic << ") done" << endl; -} TNode SimplexDecisionProcedure::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic){ @@ -912,75 +497,3 @@ Node SimplexDecisionProcedure::generateConflictBelowLowerBound(ArithVar conflict return weakenConflict(false, conflictVar); } -/** - * Computes the value of a basic variable using the current assignment. - */ -DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe){ - Assert(d_tableau.isBasic(x)); - DeltaRational sum(0); - - for(Tableau::RowIterator i = d_tableau.rowIterator(x); !i.atEnd(); ++i){ - const TableauEntry& entry = (*i); - ArithVar nonbasic = entry.getColVar(); - if(nonbasic == x) continue; - const Rational& coeff = entry.getCoefficient(); - - const DeltaRational& assignment = d_partialModel.getAssignment(nonbasic, useSafe); - sum = sum + (assignment * coeff); - } - return sum; -} - -DeltaRational SimplexDecisionProcedure::computeBound(ArithVar basic, bool upperBound){ - DeltaRational sum(0,0); - for(Tableau::RowIterator i = d_tableau.rowIterator(basic); !i.atEnd(); ++i){ - const TableauEntry& entry = (*i); - ArithVar nonbasic = entry.getColVar(); - if(nonbasic == basic) continue; - const Rational& coeff = entry.getCoefficient(); - int sgn = coeff.sgn(); - bool ub = upperBound ? (sgn > 0) : (sgn < 0); - - const DeltaRational& bound = ub ? - d_partialModel.getUpperBound(nonbasic): - d_partialModel.getLowerBound(nonbasic); - - DeltaRational diff = bound * coeff; - sum = sum + diff; - } - return sum; -} - -/** - * This check is quite expensive. - * It should be wrapped in a Debug.isOn() guard. - * if(Debug.isOn("paranoid:check_tableau")){ - * checkTableau(); - * } - */ -void SimplexDecisionProcedure::debugCheckTableau(){ - ArithVarSet::const_iterator basicIter = d_tableau.beginBasic(); - ArithVarSet::const_iterator endIter = d_tableau.endBasic(); - for(; basicIter != endIter; ++basicIter){ - ArithVar basic = *basicIter; - DeltaRational sum; - Debug("paranoid:check_tableau") << "starting row" << basic << endl; - Tableau::RowIterator nonbasicIter = d_tableau.rowIterator(basic); - for(; !nonbasicIter.atEnd(); ++nonbasicIter){ - const TableauEntry& entry = *nonbasicIter; - ArithVar nonbasic = entry.getColVar(); - if(basic == nonbasic) continue; - - const Rational& coeff = entry.getCoefficient(); - DeltaRational beta = d_partialModel.getAssignment(nonbasic); - Debug("paranoid:check_tableau") << nonbasic << beta << coeff< d_delayedLemmas; - PermissiveBackArithVarSet d_updatedBounds; - PermissiveBackArithVarSet d_candidateBasics; - + /** Maps a variable to how many times they have been used as a pivot in the simplex search. */ ArithVarMultiset d_pivotsInRound; - Rational d_ZERO; + /** Stores to the DeltaRational constant 0. */ DeltaRational d_DELTA_ZERO; public: SimplexDecisionProcedure(ArithPropManager& propManager, - ArithPartialModel& pm, - Tableau& tableau); + LinearEqualityModule& linEq); + /** + * This must be called when the value of a basic variable may now voilate one + * of its bounds. + */ + void updateBasic(ArithVar x){ + d_queue.enqueueIfInconsistent(x); + } /** - * 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. + * Tries to update the assignments of variables such that all of the + * assignments are consistent with their bounds. + * This is done by a simplex search through the possible bases of the tableau. * - * orig must be a literal in the SAT solver so that it can be used for - * conflict analysis. + * If all of the variables can be made consistent with their bounds + * Node::null() is returned. Otherwise a minimized conflict is returned. * - * x is the variable getting the new bound, - * c is the value of the new bound. + * Tableau pivoting is performed so variables may switch from being basic to + * nonbasic and vice versa. * - * If this new bound is in conflict with the other bound, - * a node describing this conflict is returned. - * If this new bound is not in conflict, Node::null() is returned. + * Corresponds to the "check()" procedure in [Cav06]. */ - Node AssertLower(ArithVar x, const DeltaRational& c, TNode orig); - Node AssertUpper(ArithVar x, const DeltaRational& c, TNode orig); - Node AssertEquality(ArithVar x, const DeltaRational& c, TNode orig); + Node findModel(); 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); - -private: /** * A PreferenceFunction takes a const ref to the SimplexDecisionProcedure, * and 2 ArithVar variables and returns one of the ArithVar variables potentially @@ -119,7 +146,7 @@ private: /** * minVarOrder is a PreferenceFunction for selecting the smaller of the 2 ArithVars. * This PreferenceFunction is used during the VarOrder stage of - * updateInconsistentVars. + * findModel. */ static ArithVar minVarOrder(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y); @@ -128,7 +155,7 @@ private: * row count in the tableau. * * This is a hueristic rule and should not be used - * during the VarOrder stage of updateInconsistentVars. + * during the VarOrder stage of findModel. */ static ArithVar minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y); /** @@ -138,27 +165,13 @@ private: * the rule falls back to minRowCount(...). * * This is a hueristic rule and should not be used - * during the VarOrder stage of updateInconsistentVars. + * during the VarOrder stage of findModel. */ static ArithVar minBoundAndRowCount(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y); -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 searchForFeasibleSolution(uint32_t maxIterations); @@ -193,23 +206,6 @@ private: */ ArithVar selectSmallestInconsistentVar(); - - /** - * Exports either the explanation of an upperbound or a lower bound - * of the basic variable basic, using the non-basic variables in the row. - */ - template - void explainNonbasics(ArithVar basic, NodeBuilder<>& output); - void explainNonbasicsLowerBound(ArithVar basic, NodeBuilder<>& output){ - explainNonbasics(basic, output); - } - void explainNonbasicsUpperBound(ArithVar basic, NodeBuilder<>& output){ - explainNonbasics(basic, output); - } - - Node deduceUpperBound(ArithVar basicVar); - Node deduceLowerBound(ArithVar basicVar); - /** * Given a non-basic variable that is know to not be updatable * to a consistent value, construct and return a conflict. @@ -219,29 +215,6 @@ private: Node generateConflictBelowLowerBound(ArithVar conflictVar); public: - /** - * Checks to make sure the assignment is consistent with the tableau. - * This code is for debugging. - */ - void debugCheckTableau(); - void debugPivotSimplex(ArithVar x_i, ArithVar x_j); - - - /** - * 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); - - bool hasAnyUpdates() { return !d_updatedBounds.empty(); } - void clearUpdates(){ - d_updatedBounds.purge(); - } - void propagateCandidates(); - void increaseMax() {d_numVariables++;} /** Returns true if the simplex procedure has more delayed lemmas in its queue.*/ @@ -288,39 +261,11 @@ private: Node weakenConflict(bool aboveUpper, ArithVar basicVar); TNode weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic); - void propagateCandidate(ArithVar basic); - bool propagateCandidateBound(ArithVar basic, bool upperBound); - - inline bool propagateCandidateLowerBound(ArithVar basic){ - return propagateCandidateBound(basic, false); - } - inline bool propagateCandidateUpperBound(ArithVar basic){ - return propagateCandidateBound(basic, true); - } - - bool hasBounds(ArithVar basic, bool upperBound); - bool hasLowerBounds(ArithVar basic){ - return hasBounds(basic, false); - } - bool hasUpperBounds(ArithVar basic){ - return hasBounds(basic, true); - } - DeltaRational computeBound(ArithVar basic, bool upperBound); - - inline DeltaRational computeLowerBound(ArithVar basic){ - return computeBound(basic, false); - } - inline DeltaRational computeUpperBound(ArithVar basic){ - return computeBound(basic, true); - } /** These fields are designed to be accessable to TheoryArith methods. */ class Statistics { public: - IntStat d_statPivots, d_statUpdates; - - IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts; IntStat d_statUpdateConflicts; TimerStat d_findConflictOnTheQueueTime; @@ -334,16 +279,9 @@ private: IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings; TimerStat d_weakenTime; - TimerStat d_boundComputationTime; - IntStat d_boundComputations, d_boundPropagations; IntStat d_delayedConflicts; - TimerStat d_pivotTime; - - AverageStat d_avgNumRowsNotContainingOnUpdate; - AverageStat d_avgNumRowsNotContainingOnPivot; - Statistics(); ~Statistics(); }; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index b10fc964d..1137ca7b7 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -56,6 +56,7 @@ using namespace CVC4::theory::arith; static const uint32_t RESET_START = 2; + TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) : Theory(THEORY_ARITH, c, u, out, valuation), d_hasDoneWorkSinceCut(false), @@ -65,9 +66,10 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_constantIntegerVariables(c), d_CivIterator(c,0), d_varsInDioSolver(c), - d_partialModel(c, d_differenceManager), d_diseq(c), + d_partialModel(c, d_differenceManager), d_tableau(), + d_linEq(d_partialModel, d_tableau, d_basicVarModelUpdateCallBack), d_diosolver(c), d_pbSubstitutions(u), d_restartsCounter(0), @@ -77,7 +79,8 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_atomDatabase(c, out), d_propManager(c, d_arithvarNodeMap, d_atomDatabase, valuation), d_differenceManager(c, d_propManager), - d_simplex(d_propManager, d_partialModel, d_tableau), + d_simplex(d_propManager, d_linEq), + d_basicVarModelUpdateCallBack(d_simplex), d_DELTA_ZERO(0), d_statistics() {} @@ -85,6 +88,8 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha TheoryArith::~TheoryArith(){} TheoryArith::Statistics::Statistics(): + d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0), + d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0), d_statUserVariables("theory::arith::UserVariables", 0), d_statSlackVariables("theory::arith::SlackVariables", 0), d_statDisequalitySplits("theory::arith::DisequalitySplits", 0), @@ -97,8 +102,14 @@ TheoryArith::Statistics::Statistics(): d_initialTableauSize("theory::arith::initialTableauSize", 0), d_currSetToSmaller("theory::arith::currSetToSmaller", 0), d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0), - d_restartTimer("theory::arith::restartTimer") + d_restartTimer("theory::arith::restartTimer"), + d_boundComputationTime("theory::arith::bound::time"), + d_boundComputations("theory::arith::bound::boundComputations",0), + d_boundPropagations("theory::arith::bound::boundPropagations",0) { + StatisticsRegistry::registerStat(&d_statAssertUpperConflicts); + StatisticsRegistry::registerStat(&d_statAssertLowerConflicts); + StatisticsRegistry::registerStat(&d_statUserVariables); StatisticsRegistry::registerStat(&d_statSlackVariables); StatisticsRegistry::registerStat(&d_statDisequalitySplits); @@ -115,9 +126,16 @@ TheoryArith::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_currSetToSmaller); StatisticsRegistry::registerStat(&d_smallerSetToCurr); StatisticsRegistry::registerStat(&d_restartTimer); + + StatisticsRegistry::registerStat(&d_boundComputationTime); + StatisticsRegistry::registerStat(&d_boundComputations); + StatisticsRegistry::registerStat(&d_boundPropagations); } TheoryArith::Statistics::~Statistics(){ + StatisticsRegistry::unregisterStat(&d_statAssertUpperConflicts); + StatisticsRegistry::unregisterStat(&d_statAssertLowerConflicts); + StatisticsRegistry::unregisterStat(&d_statUserVariables); StatisticsRegistry::unregisterStat(&d_statSlackVariables); StatisticsRegistry::unregisterStat(&d_statDisequalitySplits); @@ -134,6 +152,186 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_currSetToSmaller); StatisticsRegistry::unregisterStat(&d_smallerSetToCurr); StatisticsRegistry::unregisterStat(&d_restartTimer); + + StatisticsRegistry::unregisterStat(&d_boundComputationTime); + StatisticsRegistry::unregisterStat(&d_boundComputations); + StatisticsRegistry::unregisterStat(&d_boundPropagations); +} + +/* procedure AssertLower( x_i >= c_i ) */ +Node TheoryArith::AssertLower(ArithVar x_i, DeltaRational& c_i, TNode original){ + Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl; + + if(isInteger(x_i)){ + c_i = DeltaRational(c_i.ceiling()); + } + + //TODO Relax to less than? + if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){ + return Node::null(); + } + + int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i); + if(cmpToUB > 0){ // c_i < \lowerbound(x_i) + 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 conflict; + }else if(cmpToUB == 0){ + if(isInteger(x_i)){ + d_constantIntegerVariables.push_back(x_i); + } + //check to make sure x_i != c_i has not been asserted + Node left = d_arithvarNodeMap.asNode(x_i); + + // if lowerbound and upperbound are equal, then the infinitesimal must be 0 + Assert(c_i.getInfinitesimalPart().isZero()); + Node right = mkRationalNode(c_i.getNoninfinitesimalPart()); + + Node diseq = left.eqNode(right).notNode(); + if (d_diseq.find(diseq) != d_diseq.end()) { + Node lb = d_partialModel.getLowerConstraint(x_i); + return disequalityConflict(diseq, lb , original); + } + } + + d_partialModel.setLowerConstraint(x_i,original); + d_partialModel.setLowerBound(x_i, c_i); + + d_updatedBounds.softAdd(x_i); + + if(!d_tableau.isBasic(x_i)){ + if(d_partialModel.getAssignment(x_i) < c_i){ + d_linEq.update(x_i, c_i); + } + }else{ + d_simplex.updateBasic(x_i); + } + + if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } + + return Node::null(); +} + +/* procedure AssertUpper( x_i <= c_i) */ +Node TheoryArith::AssertUpper(ArithVar x_i, DeltaRational& c_i, TNode original){ + Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; + + if(isInteger(x_i)){ + c_i = DeltaRational(c_i.floor()); + } + + Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl; + + if(d_partialModel.strictlyGreaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i + return Node::null(); //sat + } + + // cmpToLb = \lowerbound(x_i).cmp(c_i) + int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i); + if( cmpToLB < 0 ){ // \upperbound(x_i) < \lowerbound(x_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); + return conflict; + }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i) + if(isInteger(x_i)){ + d_constantIntegerVariables.push_back(x_i); + } + + //check to make sure x_i != c_i has not been asserted + Node left = d_arithvarNodeMap.asNode(x_i); + + // if lowerbound and upperbound are equal, then the infinitesimal must be 0 + Assert(c_i.getInfinitesimalPart().isZero()); + Node right = mkRationalNode(c_i.getNoninfinitesimalPart()); + + Node diseq = left.eqNode(right).notNode(); + if (d_diseq.find(diseq) != d_diseq.end()) { + Node lb = d_partialModel.getLowerConstraint(x_i); + return disequalityConflict(diseq, lb , original); + } + } + + d_partialModel.setUpperConstraint(x_i,original); + d_partialModel.setUpperBound(x_i, c_i); + + d_updatedBounds.softAdd(x_i); + + if(!d_tableau.isBasic(x_i)){ + if(d_partialModel.getAssignment(x_i) > c_i){ + d_linEq.update(x_i, c_i); + } + }else{ + d_simplex.updateBasic(x_i); + } + + if(Debug.isOn("model")) { d_partialModel.printModel(x_i); } + + return Node::null(); +} + + +/* procedure AssertLower( x_i == c_i ) */ +Node TheoryArith::AssertEquality(ArithVar x_i, DeltaRational& c_i, TNode original){ + + Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl; + + int cmpToLB = d_partialModel.cmpToLowerBound(x_i, c_i); + int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_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(cmpToUB >= 0 && cmpToLB <= 0){ + return Node::null(); //sat + } + + if(cmpToUB > 0){ + Node ubc = d_partialModel.getUpperConstraint(x_i); + Node conflict = NodeManager::currentNM()->mkNode(AND, ubc, original); + Debug("arith") << "AssertLower conflict " << conflict << endl; + return conflict; + } + + if(cmpToLB < 0){ + Node lbc = d_partialModel.getLowerConstraint(x_i); + Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original); + Debug("arith") << "AssertUpper conflict " << conflict << endl; + return conflict; + } + + Assert(cmpToUB <= 0); + Assert(cmpToLB >= 0); + Assert(cmpToUB < 0 || cmpToLB > 0); + + + if(isInteger(x_i)){ + d_constantIntegerVariables.push_back(x_i); + } + + // Don't bother to check whether x_i != c_i is in d_diseq + // The a and (not a) should never be on the fact queue + + 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_updatedBounds.softAdd(x_i); + + if(!d_tableau.isBasic(x_i)){ + if(!(d_partialModel.getAssignment(x_i) == c_i)){ + d_linEq.update(x_i, c_i); + } + }else{ + d_simplex.updateBasic(x_i); + } + return Node::null(); } @@ -482,8 +680,8 @@ void TheoryArith::setupInitialValue(ArithVar x){ //This can go away if the tableau creation is done at preregister //time instead of register - DeltaRational safeAssignment = d_simplex.computeRowValue(x, true); - DeltaRational assignment = d_simplex.computeRowValue(x, false); + DeltaRational safeAssignment = d_linEq.computeRowValue(x, true); + DeltaRational assignment = d_linEq.computeRowValue(x, false); d_partialModel.initialize(x,safeAssignment); d_partialModel.setAssignment(x,assignment); } @@ -634,69 +832,33 @@ Node TheoryArith::assertionCases(TNode assertion){ ArithVar x_i = determineLeftVariable(assertion, simpleKind); DeltaRational c_i = determineRightConstant(assertion, simpleKind); - bool tightened = false; + // bool tightened = false; - //If the variable is an integer tighen the constraint. - if(isInteger(x_i)){ - if(simpleKind == LT){ - tightened = true; - c_i = DeltaRational(c_i.floor()); - }else if(simpleKind == GT){ - tightened = true; - c_i = DeltaRational(c_i.ceiling()); - } - } + // //If the variable is an integer tighen the constraint. + // if(isInteger(x_i)){ + // if(simpleKind == LT){ + // tightened = true; + // c_i = DeltaRational(c_i.floor()); + // }else if(simpleKind == GT){ + // tightened = true; + // c_i = DeltaRational(c_i.ceiling()); + // } + // } Debug("arith::assertions") << "arith assertion @" << getContext()->getLevel() <<"(" << assertion - << " \\-> " - << x_i<<" "<< simpleKind <<" "<< c_i << ")" << std::endl; + << " \\-> " + << x_i<<" "<< simpleKind <<" "<< c_i << ")" << std::endl; switch(simpleKind){ case LEQ: case LT: - if(simpleKind == LEQ || (simpleKind == LT && tightened)){ - if (d_partialModel.hasLowerBound(x_i) && d_partialModel.getLowerBound(x_i) == c_i) { - //If equal - TNode left = getSide(assertion, simpleKind); - TNode right = getSide(assertion, simpleKind); - - Node diseq = left.eqNode(right).notNode(); - if (d_diseq.find(diseq) != d_diseq.end()) { - Node lb = d_partialModel.getLowerConstraint(x_i); - return disequalityConflict(diseq, lb , assertion); - } - - if(isInteger(x_i)){ - d_constantIntegerVariables.push_back(x_i); - } - } - } - return d_simplex.AssertUpper(x_i, c_i, assertion); + return AssertUpper(x_i, c_i, assertion); case GEQ: case GT: - if(simpleKind == GEQ || (simpleKind == GT && tightened)){ - if (d_partialModel.hasUpperBound(x_i) && d_partialModel.getUpperBound(x_i) == c_i) { - //If equal - TNode left = getSide(assertion, simpleKind); - TNode right = getSide(assertion, simpleKind); - - Node diseq = left.eqNode(right).notNode(); - if (d_diseq.find(diseq) != d_diseq.end()) { - Node ub = d_partialModel.getUpperConstraint(x_i); - return disequalityConflict(diseq, assertion, ub); - } - if(isInteger(x_i)){ - d_constantIntegerVariables.push_back(x_i); - } - } - } - return d_simplex.AssertLower(x_i, c_i, assertion); + return AssertLower(x_i, c_i, assertion); case EQUAL: - if(isInteger(x_i)){ - d_constantIntegerVariables.push_back(x_i); - } - return d_simplex.AssertEquality(x_i, c_i, assertion); + return AssertEquality(x_i, c_i, assertion); case DISTINCT: { d_diseq.insert(assertion); @@ -760,7 +922,7 @@ void TheoryArith::check(Effort effortLevel){ if(!possibleConflict.isNull()){ d_partialModel.revertAssignmentChanges(); Debug("arith::conflict") << "conflict " << possibleConflict << endl; - d_simplex.clearUpdates(); + clearUpdates(); d_out->conflict(possibleConflict); return; } @@ -771,10 +933,10 @@ void TheoryArith::check(Effort effortLevel){ } bool emmittedConflictOrSplit = false; - Node possibleConflict = d_simplex.updateInconsistentVars(); + Node possibleConflict = d_simplex.findModel(); if(possibleConflict != Node::null()){ d_partialModel.revertAssignmentChanges(); - d_simplex.clearUpdates(); + clearUpdates(); Debug("arith::conflict") << "conflict " << possibleConflict << endl; d_out->conflict(possibleConflict); @@ -818,7 +980,7 @@ void TheoryArith::check(Effort effortLevel){ } }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel() - if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); } + if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); } if(Debug.isOn("arith::print_model")) { debugPrintModel(); } Debug("arith") << "TheoryArith::check end" << std::endl; } @@ -958,10 +1120,10 @@ Node flattenAnd(Node n){ void TheoryArith::propagate(Effort e) { if(quickCheckOrMore(e)){ bool propagated = false; - if(Options::current()->arithPropagation && d_simplex.hasAnyUpdates()){ - d_simplex.propagateCandidates(); + if(Options::current()->arithPropagation && hasAnyUpdates()){ + propagateCandidates(); }else{ - d_simplex.clearUpdates(); + clearUpdates(); } while(d_propManager.hasMorePropagations()){ @@ -1106,7 +1268,7 @@ void TheoryArith::notifyEq(TNode lhs, TNode rhs) { void TheoryArith::notifyRestart(){ TimerStat::CodeTimer codeTimer(d_statistics.d_restartTimer); - if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); } + if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); } ++d_restartsCounter; @@ -1225,7 +1387,7 @@ void TheoryArith::presolve(){ d_statistics.d_initialTableauSize.setData(d_tableau.size()); - if(Debug.isOn("paranoid:check_tableau")){ d_simplex.debugCheckTableau(); } + if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); } static CVC4_THREADLOCAL(unsigned) callCount = 0; if(Debug.isOn("arith::presolve")) { @@ -1245,3 +1407,87 @@ EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) { } } + +bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){ + ++d_statistics.d_boundComputations; + + DeltaRational bound = upperBound ? + d_linEq.computeUpperBound(basic): + d_linEq.computeLowerBound(basic); + + if((upperBound && d_partialModel.strictlyLessThanUpperBound(basic, bound)) || + (!upperBound && d_partialModel.strictlyGreaterThanLowerBound(basic, bound))){ + Node bestImplied = upperBound ? + d_propManager.getBestImpliedUpperBound(basic, bound): + d_propManager.getBestImpliedLowerBound(basic, bound); + + if(!bestImplied.isNull()){ + bool asserted = d_propManager.isAsserted(bestImplied); + bool propagated = d_propManager.isPropagated(bestImplied); + if( !asserted && !propagated){ + + NodeBuilder<> nb(kind::AND); + if(upperBound){ + d_linEq.explainNonbasicsUpperBound(basic, nb); + }else{ + d_linEq.explainNonbasicsLowerBound(basic, nb); + } + Node explanation = nb; + d_propManager.propagate(bestImplied, explanation, false); + return true; + }else{ + Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl; + } + } + } + return false; +} + +void TheoryArith::propagateCandidate(ArithVar basic){ + bool success = false; + if(d_partialModel.strictlyAboveLowerBound(basic) && d_linEq.hasLowerBounds(basic)){ + success |= propagateCandidateLowerBound(basic); + } + if(d_partialModel.strictlyBelowUpperBound(basic) && d_linEq.hasUpperBounds(basic)){ + success |= propagateCandidateUpperBound(basic); + } + if(success){ + ++d_statistics.d_boundPropagations; + } +} + +void TheoryArith::propagateCandidates(){ + TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime); + + Assert(d_candidateBasics.empty()); + + if(d_updatedBounds.empty()){ return; } + + PermissiveBackArithVarSet::const_iterator i = d_updatedBounds.begin(); + PermissiveBackArithVarSet::const_iterator end = d_updatedBounds.end(); + for(; i != end; ++i){ + ArithVar var = *i; + if(d_tableau.isBasic(var) && + d_tableau.getRowLength(var) <= Options::current()->arithPropagateMaxLength){ + d_candidateBasics.softAdd(var); + }else{ + Tableau::ColIterator basicIter = d_tableau.colIterator(var); + for(; !basicIter.atEnd(); ++basicIter){ + const TableauEntry& entry = *basicIter; + ArithVar rowVar = entry.getRowVar(); + Assert(entry.getColVar() == var); + Assert(d_tableau.isBasic(rowVar)); + if(d_tableau.getRowLength(rowVar) <= Options::current()->arithPropagateMaxLength){ + d_candidateBasics.softAdd(rowVar); + } + } + } + } + d_updatedBounds.purge(); + + while(!d_candidateBasics.empty()){ + ArithVar candidate = d_candidateBasics.pop_back(); + Assert(d_tableau.isBasic(candidate)); + propagateCandidate(candidate); + } +} diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index c19a20ead..f364885c2 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -32,6 +32,7 @@ #include "theory/arith/tableau.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/partial_model.h" +#include "theory/arith/linear_equality.h" #include "theory/arith/atom_database.h" #include "theory/arith/simplex.h" #include "theory/arith/arith_static_learner.h" @@ -179,6 +180,11 @@ private: */ std::map d_removedRows; + /** + * List of all of the inequalities asserted in the current context. + */ + context::CDSet d_diseq; + /** * Manages information about the assignment and upper and lower bounds on * variables. @@ -186,14 +192,14 @@ private: ArithPartialModel d_partialModel; /** - * List of all of the inequalities asserted in the current context. + * The tableau for all of the constraints seen thus far in the system. */ - context::CDSet d_diseq; + Tableau d_tableau; /** - * The tableau for all of the constraints seen thus far in the system. + * Maintains the relationship between the PartialModel and the Tableau. */ - Tableau d_tableau; + LinearEqualityModule d_linEq; /** * A Diophantine equation solver. Accesses the tableau and partial @@ -279,6 +285,23 @@ public: void addSharedTerm(TNode n); private: + + class BasicVarModelUpdateCallBack : public ArithVarCallBack{ + private: + SimplexDecisionProcedure& d_simplex; + + public: + BasicVarModelUpdateCallBack(SimplexDecisionProcedure& s): + d_simplex(s) + {} + + void callback(ArithVar x){ + d_simplex.updateBasic(x); + } + }; + + BasicVarModelUpdateCallBack d_basicVarModelUpdateCallBack; + /** The constant zero. */ DeltaRational d_DELTA_ZERO; @@ -330,6 +353,45 @@ private: void setupSlack(TNode left); + /** + * 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. + * + * orig must be a literal in the SAT solver so that it can be used for + * conflict analysis. + * + * x is the variable getting the new bound, + * c is the value of the new bound. + * + * If this new bound is in conflict with the other bound, + * a node describing this conflict is returned. + * If this new bound is not in conflict, Node::null() is returned. + */ + Node AssertLower(ArithVar x, DeltaRational& c, TNode orig); + Node AssertUpper(ArithVar x, DeltaRational& c, TNode orig); + Node AssertEquality(ArithVar x, DeltaRational& c, TNode orig); + + /** Tracks the bounds that were updated in the current round. */ + PermissiveBackArithVarSet d_updatedBounds; + + /** Tracks the basic variables where propagatation might be possible. */ + PermissiveBackArithVarSet d_candidateBasics; + + bool hasAnyUpdates() { return !d_updatedBounds.empty(); } + void clearUpdates(){ d_updatedBounds.purge(); } + + void propagateCandidates(); + void propagateCandidate(ArithVar basic); + bool propagateCandidateBound(ArithVar basic, bool upperBound); + + inline bool propagateCandidateLowerBound(ArithVar basic){ + return propagateCandidateBound(basic, false); + } + inline bool propagateCandidateUpperBound(ArithVar basic){ + return propagateCandidateBound(basic, true); + } + /** * Performs a check to see if it is definitely true that setup can be avoided. */ @@ -383,6 +445,8 @@ private: /** These fields are designed to be accessable to TheoryArith methods. */ class Statistics { public: + IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts; + IntStat d_statUserVariables, d_statSlackVariables; IntStat d_statDisequalitySplits; IntStat d_statDisequalityConflicts; @@ -399,6 +463,9 @@ private: IntStat d_smallerSetToCurr; TimerStat d_restartTimer; + TimerStat d_boundComputationTime; + IntStat d_boundComputations, d_boundPropagations; + Statistics(); ~Statistics(); }; diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index 885e6b628..69eede0d6 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -192,6 +192,10 @@ public: } } + bool isZero() const { + return cln::zerop(d_value); + } + Rational abs() const { if(sgn() < 0){ return -(*this); diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 4635ce881..751c8f137 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -169,6 +169,10 @@ public: return mpq_sgn(d_value.get_mpq_t()); } + bool isZero() const { + return sgn() == 0; + } + Rational abs() const { if(sgn() < 0){ return -(*this);