delta_rational.cpp \
partial_model.h \
partial_model.cpp \
+ linear_equality.h \
+ linear_equality.cpp \
ordered_set.h \
arithvar_set.h \
tableau.h \
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);
typedef context::CDSet<ArithVar> CDArithVarSet;
+class ArithVarCallBack {
+public:
+ virtual void callback(ArithVar x) = 0;
+};
+
+
inline Node mkRationalNode(const Rational& q){
return NodeManager::currentNM()->mkConst<Rational>(q);
}
}
+ 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;
--- /dev/null
+/********************* */
+/*! \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<true>(ArithVar basic, NodeBuilder<>& output);
+template void LinearEqualityModule::explainNonbasics<false>(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<<endl;
+ sum = sum + (beta*coeff);
+ }
+ DeltaRational shouldBe = d_partialModel.getAssignment(basic);
+ Debug("paranoid:check_tableau") << "ending row" << sum
+ << "," << shouldBe << endl;
+
+ Assert(sum == shouldBe);
+ }
+}
+
+DeltaRational LinearEqualityModule::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;
+}
+
+/**
+ * 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 <bool upperBound>
+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 */
--- /dev/null
+/********************* */
+/*! \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 <bool upperBound>
+ void explainNonbasics(ArithVar basic, NodeBuilder<>& output);
+
+public:
+ void explainNonbasicsLowerBound(ArithVar basic, NodeBuilder<>& output){
+ explainNonbasics<false>(basic, output);
+ }
+ void explainNonbasicsUpperBound(ArithVar basic, NodeBuilder<>& output){
+ explainNonbasics<true>(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 */
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;
}
}
-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);
}
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;
}
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);
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) {
}
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),
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);
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);
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);
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();
Assert(d_queue.inCollectionMode());
- Debug("arith::updateInconsistentVars") << "end updateInconsistentVars() "
- << instance << endl;
+ Debug("arith::findModel") << "end findModel() " << instance << endl;
return possibleConflict;
}
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);
//corresponds to Check() in dM06
//template <SimplexDecisionProcedure::PreferenceFunction pf>
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;
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);
return Node::null();
}
-template <bool upperBound>
-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){
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<<endl;
- sum = sum + (beta*coeff);
- }
- DeltaRational shouldBe = d_partialModel.getAssignment(basic);
- Debug("paranoid:check_tableau") << "ending row" << sum
- << "," << shouldBe << endl;
-
- Assert(sum == shouldBe);
- }
-}
-
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief [[ Add one-line brief description here ]]
+ ** \brief This is an implementation of the Simplex Module for the Simplex for DPLL(T) decision procedure.
**
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** This implements the Simplex module for the Simpelx for DPLL(T) decision procedure.
+ ** See the Simplex for DPLL(T) technical report for more background.(citation?)
+ ** 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 is required to either produce a conflict or satisifying PartialModel.
+ ** Further, we require being told when a basic variable updates its value.
+ **
+ ** During the Simplex search we maintain a queue of variables.
+ ** The queue is required to contain all of the basic variables that voilate their bounds.
+ ** As elimination from the queue is more efficient to be done lazily,
+ ** we do not maintain that the queue of variables needs to be only basic variables or only variables that satisfy their bounds.
+ **
+ ** The simplex procedure roughly follows Alberto's thesis. (citation?)
+ ** There is one round of selecting using a hueristic pivoting rule. (See PreferenceFunction Documentation for the available options.)
+ ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that Leonardo invented this first.)
+ ** After this, Bland's pivot rule is invoked.
+ **
+ ** During this proccess, we periodically inspect the queue of variables to
+ ** 1) remove now extraneous extries,
+ ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the current queue hueristics, and
+ ** 3) detect multiple conflicts.
+ **
+ ** Conflicts are greedily slackened to use the weakest bounds that still produce the conflict.
+ **
+ ** Extra things tracked atm: (Subject to change at Tim's whims)
+ ** - A superset of all of the newly pivoted variables.
+ ** - A queue of additional conflicts that were discovered by Simplex.
+ ** These are theory valid and are currently turned into lemmas
**/
#include "theory/arith/tableau.h"
#include "theory/arith/partial_model.h"
#include "theory/arith/arith_prop_manager.h"
+#include "theory/arith/linear_equality.h"
#include "util/options.h"
class SimplexDecisionProcedure {
private:
+ /** Linear equality module. */
+ LinearEqualityModule& d_linEq;
+
/**
* Manages information about the assignment and upper and lower bounds on
* variables.
+ * Partial model matches that in LinearEqualityModule.
*/
ArithPartialModel& d_partialModel;
+ /**
+ * Stores the linear equalities used by Simplex.
+ * Tableau from the LinearEquality module.
+ */
Tableau& d_tableau;
+
+ /** Contains a superset of the basic variables in violation of their bounds. */
ArithPriorityQueue d_queue;
+ /** A link to the propagation manager. This is used to generate weaker conflicts. */
ArithPropManager& d_propManager;
+ /** Number of variables in the system. This is used for tuning heuristics. */
ArithVar d_numVariables;
std::queue<Node> 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
/**
* 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);
* 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);
/**
* 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);
*/
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 <bool upperBound>
- void explainNonbasics(ArithVar basic, NodeBuilder<>& output);
- void explainNonbasicsLowerBound(ArithVar basic, NodeBuilder<>& output){
- explainNonbasics<false>(basic, output);
- }
- void explainNonbasicsUpperBound(ArithVar basic, NodeBuilder<>& output){
- explainNonbasics<true>(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.
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.*/
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;
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();
};
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),
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),
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()
{}
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),
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);
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);
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();
}
//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);
}
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<false>(assertion, simpleKind);
- TNode right = getSide<true>(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<false>(assertion, simpleKind);
- TNode right = getSide<true>(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);
if(!possibleConflict.isNull()){
d_partialModel.revertAssignmentChanges();
Debug("arith::conflict") << "conflict " << possibleConflict << endl;
- d_simplex.clearUpdates();
+ clearUpdates();
d_out->conflict(possibleConflict);
return;
}
}
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);
}
}//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;
}
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()){
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;
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")) {
}
}
+
+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);
+ }
+}
#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"
*/
std::map<ArithVar, Node> d_removedRows;
+ /**
+ * List of all of the inequalities asserted in the current context.
+ */
+ context::CDSet<Node, NodeHashFunction> d_diseq;
+
/**
* Manages information about the assignment and upper and lower bounds on
* variables.
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<Node, NodeHashFunction> 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
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;
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.
*/
/** 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;
IntStat d_smallerSetToCurr;
TimerStat d_restartTimer;
+ TimerStat d_boundComputationTime;
+ IntStat d_boundComputations, d_boundPropagations;
+
Statistics();
~Statistics();
};
}
}
+ bool isZero() const {
+ return cln::zerop(d_value);
+ }
+
Rational abs() const {
if(sgn() < 0){
return -(*this);
return mpq_sgn(d_value.get_mpq_t());
}
+ bool isZero() const {
+ return sgn() == 0;
+ }
+
Rational abs() const {
if(sgn() < 0){
return -(*this);
projects / cvc5.git / commitdiff