arithvar.h \
arithvar.cpp \
bound_counts.h \
+ bound_counts.cpp \
arith_rewriter.h \
arith_rewriter.cpp \
arith_static_learner.h \
--- /dev/null
+#include "theory/arith/bound_counts.h"
+#include "theory/arith/tableau.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const {
+ RowIndex ridx = d_tab->basicToRowIndex(basic);
+ Assert(d_bc->isKey(ridx));
+ return (*d_bc)[ridx];
+}
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
namespace theory {
namespace arith {
-/**
- * x = \sum_{a < 0} a_i i + \sum_{b > 0} b_j j
- *
- * AtUpperBound = {assignment(i) = lb(i)} \cup {assignment(j) = ub(j)}
- * AtLowerBound = {assignment(i) = ub(i)} \cup {assignment(j) = lb(j)}
- */
class BoundCounts {
private:
- uint32_t d_atLowerBounds;
- uint32_t d_atUpperBounds;
+ uint32_t d_lowerBoundCount;
+ uint32_t d_upperBoundCount;
public:
- BoundCounts() : d_atLowerBounds(0), d_atUpperBounds(0) {}
+ BoundCounts() : d_lowerBoundCount(0), d_upperBoundCount(0) {}
BoundCounts(uint32_t lbs, uint32_t ubs)
- : d_atLowerBounds(lbs), d_atUpperBounds(ubs) {}
+ : d_lowerBoundCount(lbs), d_upperBoundCount(ubs) {}
bool operator==(BoundCounts bc) const {
- return d_atLowerBounds == bc.d_atLowerBounds
- && d_atUpperBounds == bc.d_atUpperBounds;
+ return d_lowerBoundCount == bc.d_lowerBoundCount
+ && d_upperBoundCount == bc.d_upperBoundCount;
}
bool operator!=(BoundCounts bc) const {
- return d_atLowerBounds != bc.d_atLowerBounds
- || d_atUpperBounds != bc.d_atUpperBounds;
+ return d_lowerBoundCount != bc.d_lowerBoundCount
+ || d_upperBoundCount != bc.d_upperBoundCount;
}
- inline bool isZero() const{ return d_atLowerBounds == 0 && d_atUpperBounds == 0; }
- inline uint32_t atLowerBounds() const{
- return d_atLowerBounds;
+ /** This is not a total order! */
+ bool operator>=(BoundCounts bc) const {
+ return d_lowerBoundCount >= bc.d_lowerBoundCount &&
+ d_upperBoundCount >= bc.d_upperBoundCount;
}
- inline uint32_t atUpperBounds() const{
- return d_atUpperBounds;
+
+ inline bool isZero() const{ return d_lowerBoundCount == 0 && d_upperBoundCount == 0; }
+ inline uint32_t lowerBoundCount() const{
+ return d_lowerBoundCount;
+ }
+ inline uint32_t upperBoundCount() const{
+ return d_upperBoundCount;
}
inline BoundCounts operator+(BoundCounts bc) const{
- return BoundCounts(d_atLowerBounds + bc.d_atLowerBounds,
- d_atUpperBounds + bc.d_atUpperBounds);
+ return BoundCounts(d_lowerBoundCount + bc.d_lowerBoundCount,
+ d_upperBoundCount + bc.d_upperBoundCount);
}
inline BoundCounts operator-(BoundCounts bc) const {
- Assert(d_atLowerBounds >= bc.d_atLowerBounds);
- Assert(d_atUpperBounds >= bc.d_atUpperBounds);
- return BoundCounts(d_atLowerBounds - bc.d_atLowerBounds,
- d_atUpperBounds - bc.d_atUpperBounds);
+ Assert( *this >= bc );
+ return BoundCounts(d_lowerBoundCount - bc.d_lowerBoundCount,
+ d_upperBoundCount - bc.d_upperBoundCount);
+ }
+
+
+ inline BoundCounts& operator+=(BoundCounts bc) {
+ d_upperBoundCount += bc.d_upperBoundCount;
+ d_lowerBoundCount += bc.d_lowerBoundCount;
+ return *this;
+ }
+
+ inline BoundCounts& operator-=(BoundCounts bc) {
+ Assert(d_lowerBoundCount >= bc.d_lowerBoundCount);
+ Assert(d_upperBoundCount >= bc.d_upperBoundCount);
+ d_upperBoundCount -= bc.d_upperBoundCount;
+ d_lowerBoundCount -= bc.d_lowerBoundCount;
+
+ return *this;
+ }
+
+ /** Based on the sign coefficient a variable is multiplied by,
+ * the effects the bound counts either has no effect (sgn == 0),
+ * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
+ */
+ inline BoundCounts multiplyBySgn(int sgn) const{
+ if(sgn > 0){
+ return *this;
+ }else if(sgn == 0){
+ return BoundCounts(0,0);
+ }else{
+ return BoundCounts(d_upperBoundCount, d_lowerBoundCount);
+ }
}
inline void addInChange(int sgn, BoundCounts before, BoundCounts after){
- Assert(before != after);
- if(sgn < 0){
- Assert(d_atUpperBounds >= before.d_atLowerBounds);
- Assert(d_atLowerBounds >= before.d_atUpperBounds);
- d_atUpperBounds += after.d_atLowerBounds - before.d_atLowerBounds;
- d_atLowerBounds += after.d_atUpperBounds - before.d_atUpperBounds;
+ if(before == after){
+ return;
+ }else if(sgn < 0){
+ Assert(d_upperBoundCount >= before.d_lowerBoundCount);
+ Assert(d_lowerBoundCount >= before.d_upperBoundCount);
+ d_upperBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
+ d_lowerBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
}else if(sgn > 0){
- Assert(d_atUpperBounds >= before.d_atUpperBounds);
- Assert(d_atLowerBounds >= before.d_atLowerBounds);
- d_atUpperBounds += after.d_atUpperBounds - before.d_atUpperBounds;
- d_atLowerBounds += after.d_atLowerBounds - before.d_atLowerBounds;
+ Assert(d_upperBoundCount >= before.d_upperBoundCount);
+ Assert(d_lowerBoundCount >= before.d_lowerBoundCount);
+ d_upperBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
+ d_lowerBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
}
}
Assert(!bc.isZero());
if(before < 0){
- d_atUpperBounds -= bc.d_atLowerBounds;
- d_atLowerBounds -= bc.d_atUpperBounds;
+ d_upperBoundCount -= bc.d_lowerBoundCount;
+ d_lowerBoundCount -= bc.d_upperBoundCount;
}else if(before > 0){
- d_atUpperBounds -= bc.d_atUpperBounds;
- d_atLowerBounds -= bc.d_atLowerBounds;
+ d_upperBoundCount -= bc.d_upperBoundCount;
+ d_lowerBoundCount -= bc.d_lowerBoundCount;
}
if(after < 0){
- d_atUpperBounds += bc.d_atLowerBounds;
- d_atLowerBounds += bc.d_atUpperBounds;
+ d_upperBoundCount += bc.d_lowerBoundCount;
+ d_lowerBoundCount += bc.d_upperBoundCount;
}else if(after > 0){
- d_atUpperBounds += bc.d_atUpperBounds;
- d_atLowerBounds += bc.d_atLowerBounds;
+ d_upperBoundCount += bc.d_upperBoundCount;
+ d_lowerBoundCount += bc.d_lowerBoundCount;
}
}
+};
- inline BoundCounts& operator+=(BoundCounts bc) {
- d_atUpperBounds += bc.d_atUpperBounds;
- d_atLowerBounds += bc.d_atLowerBounds;
- return *this;
+class BoundsInfo {
+private:
+
+ /**
+ * x = \sum_{a < 0} a_i i + \sum_{b > 0} b_j j
+ *
+ * AtUpperBound = {assignment(i) = lb(i)} \cup {assignment(j) = ub(j)}
+ * AtLowerBound = {assignment(i) = ub(i)} \cup {assignment(j) = lb(j)}
+ */
+ BoundCounts d_atBounds;
+
+ /** This is for counting how many upper and lower bounds a row has. */
+ BoundCounts d_hasBounds;
+
+public:
+ BoundsInfo() : d_atBounds(), d_hasBounds() {}
+ BoundsInfo(BoundCounts atBounds, BoundCounts hasBounds)
+ : d_atBounds(atBounds), d_hasBounds(hasBounds) {}
+
+ BoundCounts atBounds() const { return d_atBounds; }
+ BoundCounts hasBounds() const { return d_hasBounds; }
+
+ /** This corresponds to adding in another variable to the row. */
+ inline BoundsInfo operator+(const BoundsInfo& bc) const{
+ return BoundsInfo(d_atBounds + bc.d_atBounds,
+ d_hasBounds + bc.d_hasBounds);
+ }
+ /** This corresponds to removing a variable from the row. */
+ inline BoundsInfo operator-(const BoundsInfo& bc) const {
+ Assert(*this >= bc);
+ return BoundsInfo(d_atBounds - bc.d_atBounds,
+ d_hasBounds - bc.d_hasBounds);
}
- inline BoundCounts& operator-=(BoundCounts bc) {
- Assert(d_atLowerBounds >= bc.d_atLowerBounds);
- Assert(d_atUpperBounds >= bc.d_atUpperBounds);
- d_atUpperBounds -= bc.d_atUpperBounds;
- d_atLowerBounds -= bc.d_atLowerBounds;
+ inline BoundsInfo& operator+=(const BoundsInfo& bc) {
+ d_atBounds += bc.d_atBounds;
+ d_hasBounds += bc.d_hasBounds;
+ return (*this);
+ }
- return *this;
+ /** Based on the sign coefficient a variable is multiplied by,
+ * the effects the bound counts either has no effect (sgn == 0),
+ * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
+ */
+ inline BoundsInfo multiplyBySgn(int sgn) const{
+ return BoundsInfo(d_atBounds.multiplyBySgn(sgn), d_hasBounds.multiplyBySgn(sgn));
}
- inline BoundCounts multiplyBySgn(int sgn) const{
- if(sgn > 0){
- return *this;
- }else if(sgn == 0){
- return BoundCounts(0,0);
- }else{
- return BoundCounts(d_atUpperBounds, d_atLowerBounds);
- }
+ bool operator==(const BoundsInfo& other) const{
+ return d_atBounds == other.d_atBounds && d_hasBounds == other.d_hasBounds;
+ }
+ bool operator!=(const BoundsInfo& other) const{
+ return !(*this == other);
+ }
+ /** This is not a total order! */
+ bool operator>=(const BoundsInfo& other) const{
+ return d_atBounds >= other.d_atBounds && d_hasBounds >= other.d_hasBounds;
+ }
+ void addInChange(int sgn, const BoundsInfo& before, const BoundsInfo& after){
+ addInAtBoundChange(sgn, before.d_atBounds, after.d_atBounds);
+ addInHasBoundChange(sgn, before.d_hasBounds, after.d_hasBounds);
+ }
+ void addInAtBoundChange(int sgn, BoundCounts before, BoundCounts after){
+ d_atBounds.addInChange(sgn, before, after);
+ }
+ void addInHasBoundChange(int sgn, BoundCounts before, BoundCounts after){
+ d_hasBounds.addInChange(sgn, before, after);
+ }
+
+ inline void addInSgn(const BoundsInfo& bc, int before, int after){
+ if(!bc.d_atBounds.isZero()){ d_atBounds.addInSgn(bc.d_atBounds, before, after);}
+ if(!bc.d_hasBounds.isZero()){ d_hasBounds.addInSgn(bc.d_hasBounds, before, after);}
}
};
-typedef DenseMap<BoundCounts> BoundCountingVector;
+/** This is intended to map each row to its relevant bound information. */
+typedef DenseMap<BoundsInfo> BoundInfoMap;
+
+class Tableau;
class BoundCountingLookup {
private:
- BoundCountingVector* d_bc;
+ BoundInfoMap* d_bc;
+ Tableau* d_tab;
public:
- BoundCountingLookup(BoundCountingVector* bc) : d_bc(bc) {}
- BoundCounts boundCounts(ArithVar v) const {
- Assert(d_bc->isKey(v));
- return (*d_bc)[v];
+ BoundCountingLookup(BoundInfoMap* bc, Tableau* tab) : d_bc(bc), d_tab(tab) {}
+ const BoundsInfo& boundsInfo(ArithVar basic) const;
+ BoundCounts atBounds(ArithVar basic) const{
+ return boundsInfo(basic).atBounds();
+ }
+ BoundCounts hasBounds(ArithVar basic) const {
+ return boundsInfo(basic).hasBounds();
}
};
inline std::ostream& operator<<(std::ostream& os, const BoundCounts& bc){
- os << "[bc " << bc.atLowerBounds() << ", "
- << bc.atUpperBounds() << "]";
+ os << "[bc " << bc.lowerBoundCount() << ", " << bc.upperBoundCount() << "]";
return os;
}
-class BoundCountsCallback {
+inline std::ostream& operator<<(std::ostream& os, const BoundsInfo& inf){
+ os << "[bi : @ " << inf.atBounds() << ", " << inf.hasBounds() << "]";
+ return os;
+}
+class BoundUpdateCallback {
public:
- virtual void operator()(ArithVar v, BoundCounts bc) = 0;
+ virtual void operator()(ArithVar v, const BoundsInfo& up) = 0;
};
}/* CVC4::theory::arith namespace */
uint32_t sumMetric(ArithVar a) const{
Assert(inError(a));
- BoundCounts bcs = d_boundLookup.boundCounts(a);
- uint32_t count = getSgn(a) > 0 ? bcs.atUpperBounds() : bcs.atLowerBounds();
+ BoundCounts bcs = d_boundLookup.atBounds(a);
+ uint32_t count = getSgn(a) > 0 ? bcs.upperBoundCount() : bcs.lowerBoundCount();
uint32_t length = d_tableauSizes.getRowLength(a);
Debug("arith::selectPrimalUpdate")
<< "selectPrimalUpdate " << instance << endl
<< basic << " " << d_tableau.basicRowLength(basic)
- << " " << d_linEq._countBounds(basic) << endl;
+ << " " << d_linEq.debugBasicAtBoundCount(basic) << endl;
static const int s_maxCandidatesAfterImprove = 3;
bool isFocus = basic == d_focusErrorVar;
int dir = !d_variables.assignmentIsConsistent(updated) ?
d_errorSet.getSgn(updated) : 0;
Debug("updateAndSignal") << " dir " << dir;
- Debug("updateAndSignal") << " _countBounds " << d_linEq._countBounds(updated) << endl;
+ Debug("updateAndSignal") << " debugBasicAtBoundCount " << d_linEq.debugBasicAtBoundCount(updated) << endl;
}
bool debugUpdatedBasic(const UpdateInfo& selected, ArithVar updated){
ArithVar leaving = selected.leaving();
ss << "leaving " << leaving
<< " " << d_tableau.basicRowLength(leaving)
- << " " << d_linEq._countBounds(leaving)
+ << " " << d_linEq.debugBasicAtBoundCount(leaving)
<< endl;
}
if(degenerate(w) && selected.describesPivot()){
<< "degenerate " << leaving
<< ", atBounds " << d_linEq.basicsAtBounds(selected)
<< ", len " << d_tableau.basicRowLength(leaving)
- << ", bc " << d_linEq._countBounds(leaving)
+ << ", bc " << d_linEq.debugBasicAtBoundCount(leaving)
<< endl;
}
}
template ArithVar LinearEqualityModule::selectSlack<true>(ArithVar x_i, VarPreferenceFunction pf) const;
template ArithVar LinearEqualityModule::selectSlack<false>(ArithVar x_i, VarPreferenceFunction pf) const;
-// template bool LinearEqualityModule::preferNonDegenerate<true>(const UpdateInfo& a, const UpdateInfo& b) const;
-// template bool LinearEqualityModule::preferNonDegenerate<false>(const UpdateInfo& a, const UpdateInfo& b) const;
-
-// template bool LinearEqualityModule::preferErrorsFixed<true>(const UpdateInfo& a, const UpdateInfo& b) const;
-// template bool LinearEqualityModule::preferErrorsFixed<false>(const UpdateInfo& a, const UpdateInfo& b) const;
-
template bool LinearEqualityModule::preferWitness<true>(const UpdateInfo& a, const UpdateInfo& b) const;
template bool LinearEqualityModule::preferWitness<false>(const UpdateInfo& a, const UpdateInfo& b) const;
<< "}";
}
-LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, BoundCountingVector& boundTracking, BasicVarModelUpdateCallBack f):
+LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, BoundInfoMap& boundsTracking, BasicVarModelUpdateCallBack f):
d_variables(vars),
d_tableau(t),
d_basicVariableUpdates(f),
d_increasing(1),
d_decreasing(-1),
d_relevantErrorBuffer(),
- d_boundTracking(boundTracking),
+ d_btracking(boundsTracking),
d_areTracking(false),
d_trackCallback(this)
{}
StatisticsRegistry::unregisterStat(&d_weakenings);
StatisticsRegistry::unregisterStat(&d_weakenTime);
}
-void LinearEqualityModule::includeBoundCountChange(ArithVar nb, BoundCounts prev){
- if(d_tableau.isBasic(nb)){
- return;
- }
- Assert(!d_tableau.isBasic(nb));
+void LinearEqualityModule::includeBoundUpdate(ArithVar v, const BoundsInfo& prev){
Assert(!d_areTracking);
- BoundCounts curr = d_variables.boundCounts(nb);
+ BoundsInfo curr = d_variables.boundsInfo(v);
Assert(prev != curr);
- Tableau::ColIterator basicIter = d_tableau.colIterator(nb);
+ Tableau::ColIterator basicIter = d_tableau.colIterator(v);
for(; !basicIter.atEnd(); ++basicIter){
const Tableau::Entry& entry = *basicIter;
- Assert(entry.getColVar() == nb);
+ Assert(entry.getColVar() == v);
int a_ijSgn = entry.getCoefficient().sgn();
- ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex());
-
- BoundCounts& counts = d_boundTracking.get(basic);
- Debug("includeBoundCountChange") << basic << " " << counts << " to " ;
- counts -= prev.multiplyBySgn(a_ijSgn);
- counts += curr.multiplyBySgn(a_ijSgn);
- Debug("includeBoundCountChange") << counts << " " << a_ijSgn << std::endl;
+ RowIndex ridx = entry.getRowIndex();
+ BoundsInfo& counts = d_btracking.get(ridx);
+ Debug("includeBoundUpdate") << d_tableau.rowIndexToBasic(ridx) << " " << counts << " to " ;
+ counts.addInChange(a_ijSgn, prev, curr);
+ Debug("includeBoundUpdate") << counts << " " << a_ijSgn << std::endl;
}
- d_boundTracking.set(nb, curr);
}
void LinearEqualityModule::updateMany(const DenseMap<DeltaRational>& many){
<< d_variables.getAssignment(x_i) << "|-> " << v << endl;
- BoundCounts before = d_variables.boundCounts(x_i);
+ BoundCounts before = d_variables.atBoundCounts(x_i);
d_variables.setAssignment(x_i, v);
- BoundCounts after = d_variables.boundCounts(x_i);
+ BoundCounts after = d_variables.atBoundCounts(x_i);
bool anyChange = before != after;
const Tableau::Entry& entry = *colIter;
Assert(entry.getColVar() == x_i);
- ArithVar x_j = d_tableau.rowIndexToBasic(entry.getRowIndex());
+ RowIndex ridx = entry.getRowIndex();
+ ArithVar x_j = d_tableau.rowIndexToBasic(ridx);
const Rational& a_ji = entry.getCoefficient();
const DeltaRational& assignment = d_variables.getAssignment(x_j);
DeltaRational nAssignment = assignment+(diff * a_ji);
Debug("update") << x_j << " " << a_ji << assignment << " -> " << nAssignment << endl;
+ BoundCounts xjBefore = d_variables.atBoundCounts(x_j);
d_variables.setAssignment(x_j, nAssignment);
+ BoundCounts xjAfter = d_variables.atBoundCounts(x_j);
- if(anyChange && basicIsTracked(x_j)){
- BoundCounts& next_bc_k = d_boundTracking.get(x_j);
- next_bc_k.addInChange(a_ji.sgn(), before, after);
+ Assert(rowIndexIsTracked(ridx));
+ BoundsInfo& next_bc_k = d_btracking.get(ridx);
+ if(anyChange){
+ next_bc_k.addInAtBoundChange(a_ji.sgn(), before, after);
+ }
+ if(xjBefore != xjAfter){
+ next_bc_k.addInAtBoundChange(-1, xjBefore, xjAfter);
}
d_basicVariableUpdates(x_j);
ArithVar var = entry.getColVar();
const Rational& coeff = entry.getCoefficient();
DeltaRational beta = d_variables.getAssignment(var);
- Debug("arith::tracking") << var << " " << d_variables.boundCounts(var)
+ Debug("arith::tracking") << var << " " << d_variables.boundsInfo(var)
<< " " << beta << coeff;
if(d_variables.hasLowerBound(var)){
Debug("arith::tracking") << "(lb " << d_variables.getLowerBound(var) << ")";
Debug("arith::tracking") << "end row"<< endl;
if(basicIsTracked(basic)){
- BoundCounts computed = computeBoundCounts(basic);
+ RowIndex ridx = d_tableau.basicToRowIndex(basic);
+ BoundsInfo computed = computeRowBoundInfo(ridx, false);
Debug("arith::tracking")
<< "computed " << computed
- << " tracking " << d_boundTracking[basic] << endl;
- Assert(computed == d_boundTracking[basic]);
+ << " tracking " << d_btracking[ridx] << endl;
+ Assert(computed == d_btracking[ridx]);
}
}
}
-void LinearEqualityModule::trackVariable(ArithVar x_i){
- Assert(!basicIsTracked(x_i));
- BoundCounts counts(0,0);
-
- for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd(); ++iter){
- const Tableau::Entry& entry = *iter;
- ArithVar nonbasic = entry.getColVar();
- if(nonbasic == x_i) continue;
-
- const Rational& a_ij = entry.getCoefficient();
- counts += (d_variables.oldBoundCounts(nonbasic)).multiplyBySgn(a_ij.sgn());
- }
- d_boundTracking.set(x_i, counts);
+void LinearEqualityModule::trackRowIndex(RowIndex ridx){
+ Assert(!rowIndexIsTracked(ridx));
+ BoundsInfo bi = computeRowBoundInfo(ridx, true);
+ d_btracking.set(ridx, bi);
}
-BoundCounts LinearEqualityModule::computeBoundCounts(ArithVar x_i) const{
- BoundCounts counts(0,0);
+BoundsInfo LinearEqualityModule::computeRowBoundInfo(RowIndex ridx, bool inQueue) const{
+ BoundsInfo bi;
- for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd(); ++iter){
+ for(Tableau::RowIterator iter = d_tableau.getRow(ridx).begin(); !iter.atEnd(); ++iter){
const Tableau::Entry& entry = *iter;
- ArithVar nonbasic = entry.getColVar();
- if(nonbasic == x_i) continue;
-
+ ArithVar v = entry.getColVar();
const Rational& a_ij = entry.getCoefficient();
- counts += (d_variables.boundCounts(nonbasic)).multiplyBySgn(a_ij.sgn());
+ bi += (d_variables.selectBoundsInfo(v, inQueue)).multiplyBySgn(a_ij.sgn());
}
-
- return counts;
+ return bi;
}
-// BoundCounts LinearEqualityModule::cachingCountBounds(ArithVar x_i) const{
-// if(d_boundTracking.isKey(x_i)){
-// return d_boundTracking[x_i];
-// }else{
-// return computeBoundCounts(x_i);
-// }
-// }
-BoundCounts LinearEqualityModule::_countBounds(ArithVar x_i) const {
- Assert(d_boundTracking.isKey(x_i));
- return d_boundTracking[x_i];
+BoundCounts LinearEqualityModule::debugBasicAtBoundCount(ArithVar x_i) const {
+ return d_btracking[d_tableau.basicToRowIndex(x_i)].atBounds();
}
-// BoundCounts LinearEqualityModule::countBounds(ArithVar x_i){
-// if(d_boundTracking.isKey(x_i)){
-// return d_boundTracking[x_i];
-// }else{
-// BoundCounts bc = computeBoundCounts(x_i);
-// if(d_areTracking){
-// d_boundTracking.set(x_i,bc);
-// }
-// return bc;
-// }
-// }
-
+/**
+ * If the pivot described in u were performed,
+ * then the row would qualify as being either at the minimum/maximum
+ * to the non-basics being at their bounds.
+ * The minimum/maximum is determined by the direction the non-basic is changing.
+ */
bool LinearEqualityModule::basicsAtBounds(const UpdateInfo& u) const {
Assert(u.describesPivot());
int toLB = (c->getType() == LowerBound ||
c->getType() == Equality) ? 1 : 0;
+ RowIndex ridx = d_tableau.basicToRowIndex(basic);
- BoundCounts bcs = d_boundTracking[basic];
+ BoundCounts bcs = d_btracking[ridx].atBounds();
// x = c*n + \sum d*m
- // n = 1/c * x + -1/c * (\sum d*m)
- BoundCounts nonb = bcs - d_variables.boundCounts(nonbasic).multiplyBySgn(coeffSgn);
+ // 0 = -x + c*n + \sum d*m
+ // n = 1/c * x + -1/c * (\sum d*m)
+ BoundCounts nonb = bcs - d_variables.atBoundCounts(nonbasic).multiplyBySgn(coeffSgn);
+ nonb.addInChange(-1, d_variables.atBoundCounts(basic), BoundCounts(toLB, toUB));
nonb = nonb.multiplyBySgn(-coeffSgn);
- nonb += BoundCounts(toLB, toUB).multiplyBySgn(coeffSgn);
uint32_t length = d_tableau.basicRowLength(basic);
Debug("basicsAtBounds")
<< "bcs " << bcs
<< "nonb " << nonb
<< "length " << length << endl;
-
+ // nonb has nb excluded.
if(nbdir < 0){
- return bcs.atLowerBounds() + 1 == length;
+ return nonb.lowerBoundCount() + 1 == length;
}else{
Assert(nbdir > 0);
- return bcs.atUpperBounds() + 1 == length;
+ return nonb.upperBoundCount() + 1 == length;
}
}
bool LinearEqualityModule::nonbasicsAtLowerBounds(ArithVar basic) const {
Assert(basicIsTracked(basic));
- BoundCounts bcs = d_boundTracking[basic];
+ RowIndex ridx = d_tableau.basicToRowIndex(basic);
+
+ BoundCounts bcs = d_btracking[ridx].atBounds();
uint32_t length = d_tableau.basicRowLength(basic);
- return bcs.atLowerBounds() + 1 == length;
+ // return true if excluding the basic is every element is at its "lowerbound"
+ // The psuedo code is:
+ // bcs -= basic.count(basic, basic's sgn)
+ // return bcs.lowerBoundCount() + 1 == length
+ // As basic's sign is always -1, we can pull out the pieces of the count:
+ // bcs.lowerBoundCount() - basic.atUpperBoundInd() + 1 == length
+ // basic.atUpperBoundInd() is either 0 or 1
+ uint32_t lbc = bcs.lowerBoundCount();
+ return (lbc == length) ||
+ (lbc + 1 == length && d_variables.cmpAssignmentUpperBound(basic) != 0);
}
bool LinearEqualityModule::nonbasicsAtUpperBounds(ArithVar basic) const {
Assert(basicIsTracked(basic));
- BoundCounts bcs = d_boundTracking[basic];
+ RowIndex ridx = d_tableau.basicToRowIndex(basic);
+ BoundCounts bcs = d_btracking[ridx].atBounds();
uint32_t length = d_tableau.basicRowLength(basic);
+ uint32_t ubc = bcs.upperBoundCount();
+ // See the comment for nonbasicsAtLowerBounds()
- return bcs.atUpperBounds() + 1 == length;
+ return (ubc == length) ||
+ (ubc + 1 == length && d_variables.cmpAssignmentLowerBound(basic) != 0);
}
-void LinearEqualityModule::trackingSwap(ArithVar basic, ArithVar nb, int nbSgn) {
- Assert(basicIsTracked(basic));
-
- // z = a*x + \sum b*y
- // x = (1/a) z + \sum (-1/a)*b*y
- // basicCount(z) = bc(a*x) + bc(\sum b y)
- // basicCount(x) = bc(z/a) + bc(\sum -b/a * y)
-
- // sgn(1/a) = sgn(a)
- // bc(a*x) = bc(x).multiply(sgn(a))
- // bc(z/a) = bc(z).multiply(sgn(a))
- // bc(\sum -b/a * y) = bc(\sum b y).multiplyBySgn(-sgn(a))
- // bc(\sum b y) = basicCount(z) - bc(a*x)
- // basicCount(x) =
- // = bc(z).multiply(sgn(a)) + (basicCount(z) - bc(a*x)).multiplyBySgn(-sgn(a))
-
- BoundCounts bc = d_boundTracking[basic];
- bc -= (d_variables.boundCounts(nb)).multiplyBySgn(nbSgn);
- bc = bc.multiplyBySgn(-nbSgn);
- bc += d_variables.boundCounts(basic).multiplyBySgn(nbSgn);
- d_boundTracking.set(nb, bc);
- d_boundTracking.remove(basic);
+void LinearEqualityModule::trackingMultiplyRow(RowIndex ridx, int sgn) {
+ Assert(rowIndexIsTracked(ridx));
+ Assert(sgn != 0);
+ if(sgn < 0){
+ BoundsInfo& bi = d_btracking.get(ridx);
+ bi = bi.multiplyBySgn(sgn);
+ }
}
void LinearEqualityModule::trackingCoefficientChange(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn){
Assert(oldSgn != currSgn);
- BoundCounts nb_bc = d_variables.boundCounts(nb);
+ BoundsInfo nb_inf = d_variables.boundsInfo(nb);
- if(!nb_bc.isZero()){
- ArithVar basic = d_tableau.rowIndexToBasic(ridx);
- Assert(basicIsTracked(basic));
+ Assert(rowIndexIsTracked(ridx));
- BoundCounts& basic_bc = d_boundTracking.get(basic);
- basic_bc.addInSgn(nb_bc, oldSgn, currSgn);
- }
+ BoundsInfo& row_bi = d_btracking.get(ridx);
+ row_bi.addInSgn(nb_inf, oldSgn, currSgn);
}
void LinearEqualityModule::computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunction pref){
Assert(sgn != 0);
Assert(!d_tableau.isBasic(nb));
- //inf.setErrorsChange(0);
- //inf.setlimiting = NullConstraint;
-
// Error variables moving in the correct direction
Assert(d_relevantErrorBuffer.empty());
// Assume past this point, nb will be in error if this pivot is done
ArithVar nb = entry.getColVar();
- ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex());
- Assert(basicIsTracked(basic));
+ RowIndex ridx = entry.getRowIndex();
+ ArithVar basic = d_tableau.rowIndexToBasic(ridx);
+ Assert(rowIndexIsTracked(ridx));
int coeffSgn = entry.getCoefficient().sgn();
// 2) -a * x = -y + \sum b * z
// 3) x = (-1/a) * ( -y + \sum b * z)
- Assert(basicIsTracked(basic));
- BoundCounts bc = d_boundTracking[basic];
+ BoundCounts bc = d_btracking[ridx].atBounds();
// 1) y = a * x + \sum b * z
// Get bc(\sum b * z)
- BoundCounts sumOnly = bc - d_variables.boundCounts(nb).multiplyBySgn(coeffSgn);
+ BoundCounts sumOnly = bc - d_variables.atBoundCounts(nb).multiplyBySgn(coeffSgn);
// y's bounds in the proposed model
int yWillBeAtUb = (bToUB || d_variables.boundsAreEqual(basic)) ? 1 : 0;
// 2) -a * x = -y + \sum b * z
// Get bc(-y + \sum b * z)
- BoundCounts withNegY = sumOnly + ysBounds.multiplyBySgn(-1);
+ sumOnly.addInChange(-1, d_variables.atBoundCounts(basic), ysBounds);
// 3) x = (-1/a) * ( -y + \sum b * z)
// Get bc((-1/a) * ( -y + \sum b * z))
- BoundCounts xsBoundsAfterPivot = withNegY.multiplyBySgn(-coeffSgn);
+ BoundCounts xsBoundsAfterPivot = sumOnly.multiplyBySgn(-coeffSgn);
uint32_t length = d_tableau.basicRowLength(basic);
if(nbSgn > 0){
// Only check for the upper bound being violated
- return xsBoundsAfterPivot.atLowerBounds() + 1 == length;
+ return xsBoundsAfterPivot.lowerBoundCount() + 1 == length;
}else{
// Only check for the lower bound being violated
- return xsBoundsAfterPivot.atUpperBounds() + 1 == length;
+ return xsBoundsAfterPivot.upperBoundCount() + 1 == length;
}
}
};
-
-
-
class LinearEqualityModule {
public:
typedef ArithVar (LinearEqualityModule::*VarPreferenceFunction)(ArithVar, ArithVar) const;
* Initializes a LinearEqualityModule with a partial model, a tableau,
* and a callback function for when basic variables update their values.
*/
- LinearEqualityModule(ArithVariables& vars, Tableau& t, BoundCountingVector& boundTracking, BasicVarModelUpdateCallBack f);
+ LinearEqualityModule(ArithVariables& vars, Tableau& t, BoundInfoMap& boundTracking, BasicVarModelUpdateCallBack f);
/**
* Updates the assignment of a nonbasic variable x_i to v.
* Also updates the assignment of basic variables accordingly.
*/
- void updateUntracked(ArithVar x_i, const DeltaRational& v);
- void updateTracked(ArithVar x_i, const DeltaRational& v);
void update(ArithVar x_i, const DeltaRational& v){
if(d_areTracking){
updateTracked(x_i,v);
updateUntracked(x_i,v);
}
}
+
+ /** Specialization of update if the module is not tracking yet (for Assert*). */
+ void updateUntracked(ArithVar x_i, const DeltaRational& v);
+
+ /** Specialization of update if the module is not tracking yet (for Simplex). */
+ void updateTracked(ArithVar x_i, const DeltaRational& v);
+
+ /**
+ * Updates every non-basic to reflect the assignment in many.
+ * For use with ApproximateSimplex.
+ */
void updateMany(const DenseMap<DeltaRational>& many);
/**
void stopTrackingBoundCounts();
- void includeBoundCountChange(ArithVar nb, BoundCounts prev);
+ void includeBoundUpdate(ArithVar nb, const BoundsInfo& prev);
void computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunction basic);
}
}
- // template<bool heuristic>
- // bool preferNonDegenerate(const UpdateInfo& a, const UpdateInfo& b) const{
- // if(a.focusDirection() == b.focusDirection()){
- // if(heuristic){
- // return preferNeitherBound(a,b);
- // }else{
- // return minNonBasicVarOrder(a,b);
- // }
- // }else{
- // return a.focusDirection() < b.focusDirection();
- // }
- // }
-
- // template <bool heuristic>
- // bool preferErrorsFixed(const UpdateInfo& a, const UpdateInfo& b) const{
- // if( a.errorsChange() == b.errorsChange() ){
- // return preferNonDegenerate<heuristic>(a,b);
- // }else{
- // return a.errorsChange() > b.errorsChange();
- // }
- // }
-
- // template <bool heuristic>
- // bool preferConflictFound(const UpdateInfo& a, const UpdateInfo& b) const{
- // if(a.d_foundConflict && b.d_foundConflict){
- // // if both are true, determinize the preference
- // return minNonBasicVarOrder(a,b);
- // }else if( a.d_foundConflict || b.d_foundConflict ){
- // return b.d_foundConflict;
- // }else{
- // return preferErrorsFixed<heuristic>(a,b);
- // }
- // }
-
bool modifiedBlands(const UpdateInfo& a, const UpdateInfo& b) const {
Assert(a.focusDirection() == 0 && b.focusDirection() == 0);
Assert(a.describesPivot());
//uint32_t computedFixed(ArithVar nb, int sgn, const DeltaRational& am);
void computedFixed(UpdateInfo&);
- // RowIndex -> BoundCount
- BoundCountingVector& d_boundTracking;
+ /**
+ * This maps each row index to its relevant bounds info.
+ * This tracks the */
+ BoundInfoMap& d_btracking;
bool d_areTracking;
/**
const Tableau::Entry* selectSlackEntry(ArithVar x_i, bool above) const;
+ inline bool rowIndexIsTracked(RowIndex ridx) const {
+ return d_btracking.isKey(ridx);
+ }
inline bool basicIsTracked(ArithVar v) const {
- return d_boundTracking.isKey(v);
+ return rowIndexIsTracked(d_tableau.basicToRowIndex(v));
}
- void trackVariable(ArithVar x_i);
-
- void maybeRemoveTracking(ArithVar v){
- Assert(!d_tableau.isBasic(v));
- if(d_boundTracking.isKey(v)){
- d_boundTracking.remove(v);
- }
+ void trackRowIndex(RowIndex ridx);
+ void stopTrackingRowIndex(RowIndex ridx){
+ Assert(rowIndexIsTracked(ridx));
+ d_btracking.remove(ridx);
}
- // void trackVariable(ArithVar x_i){
- // Assert(!basicIsTracked(x_i));
- // d_boundTracking.set(x_i,computeBoundCounts(x_i));
- // }
+ /**
+ * If the pivot described in u were performed,
+ * then the row would qualify as being either at the minimum/maximum
+ * to the non-basics being at their bounds.
+ * The minimum/maximum is determined by the direction the non-basic is changing.
+ */
bool basicsAtBounds(const UpdateInfo& u) const;
private:
- BoundCounts computeBoundCounts(ArithVar x_i) const;
+ //BoundCounts computeBasicAtBoundCounts(ArithVar x_i) const;
+ //BoundCounts computeRowAtBoundCounts(RowIndex ridx) const;
+ BoundsInfo computeRowBoundInfo(RowIndex ridx, bool inQueue) const;
public:
//BoundCounts cachingCountBounds(ArithVar x_i) const;
- BoundCounts _countBounds(ArithVar x_i) const;
+ BoundCounts debugBasicAtBoundCount(ArithVar x_i) const;
void trackingCoefficientChange(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn);
-
- void trackingSwap(ArithVar basic, ArithVar nb, int sgn);
+ void trackingMultiplyRow(RowIndex ridx, int sgn);
bool nonbasicsAtLowerBounds(ArithVar x_i) const;
bool nonbasicsAtUpperBounds(ArithVar x_i) const;
void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn){
d_linEq->trackingCoefficientChange(ridx, nb, oldSgn, currSgn);
}
- void swap(ArithVar basic, ArithVar nb, int oldNbSgn){
- d_linEq->trackingSwap(basic, nb, oldNbSgn);
+ void multiplyRow(RowIndex ridx, int sgn){
+ d_linEq->trackingMultiplyRow(ridx, sgn);
}
bool canUseRow(RowIndex ridx) const {
ArithVar basic = d_linEq->getTableau().rowIndexToBasic(ridx);
}
};
-class UpdateTrackingCallback : public BoundCountsCallback {
+class UpdateTrackingCallback : public BoundUpdateCallback {
private:
LinearEqualityModule* d_mod;
public:
UpdateTrackingCallback(LinearEqualityModule* mod): d_mod(mod){}
- void operator()(ArithVar v, BoundCounts bc){
- d_mod->includeBoundCountChange(v, bc);
+ void operator()(ArithVar v, const BoundsInfo& bi){
+ d_mod->includeBoundUpdate(v, bi);
}
};
namespace arith {
void NoEffectCCCB::update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) {}
-void NoEffectCCCB::swap(ArithVar basic, ArithVar nb, int nbSgn){}
+void NoEffectCCCB::multiplyRow(RowIndex ridx, int sgn){}
bool NoEffectCCCB::canUseRow(RowIndex ridx) const { return false; }
}/* CVC4::theory::arith namespace */
class CoefficientChangeCallback {
public:
- virtual void update(RowIndex basic, ArithVar nb, int oldSgn, int currSgn) = 0;
- virtual void swap(ArithVar basic, ArithVar nb, int nbSgn) = 0;
+ virtual void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) = 0;
+ virtual void multiplyRow(RowIndex ridx, int Sgn) = 0;
virtual bool canUseRow(RowIndex ridx) const = 0;
};
class NoEffectCCCB : public CoefficientChangeCallback {
public:
void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn);
- void swap(ArithVar basic, ArithVar nb, int nbSgn);
+ void multiplyRow(RowIndex ridx, int Sgn);
bool canUseRow(RowIndex ridx) const;
};
d_released(),
d_releasedIterator(d_released.begin()),
d_nodeToArithVarMap(),
+ d_boundsQueue(),
+ d_enqueueingBoundCounts(true),
d_lbRevertHistory(c, true, LowerBoundCleanUp(this)),
d_ubRevertHistory(c, true, UpperBoundCleanUp(this)),
d_deltaIsSafe(false),
d_delta(-1,1),
- d_deltaComputingFunc(deltaComputingFunc),
- d_enqueueingBoundCounts(true)
+ d_deltaComputingFunc(deltaComputingFunc)
{ }
ArithVariables::VarInfo::VarInfo()
d_slack(false)
{ }
+bool ArithVariables::VarInfo::initialized() const {
+ return d_var != ARITHVAR_SENTINEL;
+}
+
void ArithVariables::VarInfo::initialize(ArithVar v, Node n, bool slack){
Assert(!initialized());
Assert(d_lb == NullConstraint);
d_node = Node::null();
}
-bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundCounts & prev){
+bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundsInfo& prev){
Assert(initialized());
d_assignment = a;
int cmpUB = (d_ub == NullConstraint) ? -1 :
(cmpUB == 0 || d_cmpAssignmentUB == 0);
if(lbChanged || ubChanged){
- prev = boundCounts();
+ prev = boundsInfo();
}
d_cmpAssignmentUB = cmpUB;
}
}
-bool ArithVariables::VarInfo::setUpperBound(Constraint ub, BoundCounts& prev){
+bool ArithVariables::VarInfo::setUpperBound(Constraint ub, BoundsInfo& prev){
Assert(initialized());
- d_ub = ub;
- int cmpUB = (d_ub == NullConstraint) ? -1 : d_assignment.cmp(d_ub->getValue());
- bool ubChanged = cmpUB != d_cmpAssignmentUB &&
- (cmpUB == 0 || d_cmpAssignmentUB == 0);
+ bool wasNull = d_ub == NullConstraint;
+ bool isNull = ub == NullConstraint;
+
+ int cmpUB = isNull ? -1 : d_assignment.cmp(ub->getValue());
+ bool ubChanged = (wasNull != isNull) ||
+ (cmpUB != d_cmpAssignmentUB && (cmpUB == 0 || d_cmpAssignmentUB == 0));
if(ubChanged){
- prev = boundCounts();
+ prev = boundsInfo();
}
+ d_ub = ub;
d_cmpAssignmentUB = cmpUB;
return ubChanged;
}
-bool ArithVariables::VarInfo::setLowerBound(Constraint lb, BoundCounts& prev){
+bool ArithVariables::VarInfo::setLowerBound(Constraint lb, BoundsInfo& prev){
Assert(initialized());
- d_lb = lb;
- int cmpLB = (d_lb == NullConstraint) ? 1 : d_assignment.cmp(d_lb->getValue());
+ bool wasNull = d_lb == NullConstraint;
+ bool isNull = lb == NullConstraint;
- bool lbChanged = cmpLB != d_cmpAssignmentLB &&
- (cmpLB == 0 || d_cmpAssignmentLB == 0);
+ int cmpLB = isNull ? 1 : d_assignment.cmp(lb->getValue());
+
+ bool lbChanged = (wasNull != isNull) ||
+ (cmpLB != d_cmpAssignmentLB && (cmpLB == 0 || d_cmpAssignmentLB == 0));
if(lbChanged){
- prev = boundCounts();
+ prev = boundsInfo();
}
+ d_lb = lb;
d_cmpAssignmentLB = cmpLB;
return lbChanged;
}
+BoundCounts ArithVariables::VarInfo::atBoundCounts() const {
+ uint32_t lbIndc = (d_cmpAssignmentLB == 0) ? 1 : 0;
+ uint32_t ubIndc = (d_cmpAssignmentUB == 0) ? 1 : 0;
+ return BoundCounts(lbIndc, ubIndc);
+}
+
+BoundCounts ArithVariables::VarInfo::hasBoundCounts() const {
+ uint32_t lbIndc = (d_lb != NullConstraint) ? 1 : 0;
+ uint32_t ubIndc = (d_ub != NullConstraint) ? 1 : 0;
+ return BoundCounts(lbIndc, ubIndc);
+}
+
+BoundsInfo ArithVariables::VarInfo::boundsInfo() const{
+ return BoundsInfo(atBoundCounts(), hasBoundCounts());
+}
+
+bool ArithVariables::VarInfo::canBeReclaimed() const{
+ return d_pushCount == 0;
+}
+
void ArithVariables::attemptToReclaimReleased(){
std::list<ArithVar>::iterator i_end = d_released.end();
for(int iter = 0; iter < 20 && d_releasedIterator != i_end; ++d_releasedIterator){
attemptToReclaimReleased();
}
bool reclaim = !d_pool.empty();
-
+
ArithVar varX;
if(reclaim){
varX = d_pool.back();
}
invalidateDelta();
- BoundCounts prev;
+ BoundsInfo prev;
if(vi.setAssignment(r, prev)){
addToBoundQueue(x, prev);
}
invalidateDelta();
VarInfo& vi = d_vars.get(x);
- BoundCounts prev;
+ BoundsInfo prev;
if(vi.setAssignment(r, prev)){
addToBoundQueue(x, prev);
}
invalidateDelta();
VarInfo& vi = d_vars.get(x);
pushLowerBound(vi);
- BoundCounts prev;
+ BoundsInfo prev;
if(vi.setLowerBound(c, prev)){
addToBoundQueue(x, prev);
}
invalidateDelta();
VarInfo& vi = d_vars.get(x);
pushUpperBound(vi);
- BoundCounts prev;
+ BoundsInfo prev;
if(vi.setUpperBound(c, prev)){
addToBoundQueue(x, prev);
}
}
-// void ArithVariables::forceRelaxLowerBound(ArithVar v){
-// AssertArgument(inMaps(v), "Calling forceRelaxLowerBound on a variable that is not properly setup.");
-// AssertArgument(hasLowerBound(v), "Calling forceRelaxLowerBound on a variable without a lowerbound.");
-
-// Debug("partial_model") << "forceRelaxLowerBound(" << v << ") dropping :" << getLowerBoundConstraint(v) << endl;
-
-// invalidateDelta();
-// VarInfo& vi = d_vars.get(v);
-// pushLowerBound(vi);
-// vi.setLowerBound(NullConstraint);
-// }
-
-
-// void ArithVariables::forceRelaxUpperBound(ArithVar v){
-// AssertArgument(inMaps(v), "Calling forceRelaxUpperBound on a variable that is not properly setup.");
-// AssertArgument(hasUpperBound(v), "Calling forceRelaxUpperBound on a variable without an upper bound.");
-
-// Debug("partial_model") << "forceRelaxUpperBound(" << v << ") dropping :" << getUpperBoundConstraint(v) << endl;
-
-// invalidateDelta();
-// VarInfo& vi = d_vars.get(v);
-// pushUpperBound(vi);
-// vi.setUpperBound(NullConstraint);
-// }
-
int ArithVariables::cmpToLowerBound(ArithVar x, const DeltaRational& c) const{
if(!hasLowerBound(x)){
// l = -\intfy
bool ArithVariables::strictlyBelowUpperBound(ArithVar x) const{
return d_vars[x].d_cmpAssignmentUB < 0;
- // if(!hasUpperBound(x)){ // u = \infty
- // return true;
- // }else{
- // return d_assignment[x] < getUpperBound(x);
- // }
}
bool ArithVariables::strictlyAboveLowerBound(ArithVar x) const{
return d_vars[x].d_cmpAssignmentLB > 0;
- // if(!hasLowerBound(x)){ // l = -\infty
- // return true;
- // }else{
- // return getLowerBound(x) < d_assignment[x];
- // }
}
bool ArithVariables::assignmentIsConsistent(ArithVar x) const{
return
d_vars[x].d_cmpAssignmentLB >= 0 &&
d_vars[x].d_cmpAssignmentUB <= 0;
- // const DeltaRational& beta = getAssignment(x);
-
- // //l_i <= beta(x_i) <= u_i
- // return greaterThanLowerBound(x,beta) && lessThanUpperBound(x,beta);
}
ArithVar atBack = d_safeAssignment.back();
if(revert){
VarInfo& vi = d_vars.get(atBack);
- BoundCounts prev;
+ BoundsInfo prev;
if(vi.setAssignment(d_safeAssignment[atBack], prev)){
addToBoundQueue(atBack, prev);
}
printModel(x, Debug("model"));
}
-// BoundRelationship ArithVariables::boundRelationship(Constraint lb, const DeltaRational& d, Constraint ub){
-// if(lb == NullConstraint && ub == NullConstraint){
-// return BetweenBounds;
-// }else if(lb == NullConstraint){
-// int cmp = d.cmp(ub->getValue());
-// return (cmp < 0) ? BetweenBounds :
-// (cmp == 0 ? AtUpperBound : AboveUpperBound);
-// }else if(ub == NullConstraint){
-// int cmp = d.cmp(lb->getValue());
-// return (cmp > 0) ? BetweenBounds :
-// (cmp == 0 ? AtLowerBound : BelowLowerBound);
-// }else{
-// Assert(lb->getValue() <= ub->getValue());
-// int cmpToLB = d.cmp(lb->getValue());
-// if(cmpToLB < 0){
-// return BelowLowerBound;
-// }else if(cmpToLB == 0){
-// return (d == ub->getValue()) ? AtBothBounds : AtLowerBound;
-// }else{
-// // d > 0
-// int cmpToUB = d.cmp(ub->getValue());
-// return (cmpToUB > 0) ? BetweenBounds :
-// (cmpToUB == 0 ? AtLowerBound : BelowLowerBound);
-// }
-// }
-// }
-
void ArithVariables::pushUpperBound(VarInfo& vi){
++vi.d_pushCount;
d_ubRevertHistory.push_back(make_pair(vi.d_var, vi.d_ub));
void ArithVariables::popUpperBound(AVCPair* c){
ArithVar x = c->first;
VarInfo& vi = d_vars.get(x);
- BoundCounts prev;
+ BoundsInfo prev;
if(vi.setUpperBound(c->second, prev)){
addToBoundQueue(x, prev);
}
void ArithVariables::popLowerBound(AVCPair* c){
ArithVar x = c->first;
VarInfo& vi = d_vars.get(x);
- BoundCounts prev;
+ BoundsInfo prev;
if(vi.setLowerBound(c->second, prev)){
addToBoundQueue(x, prev);
}
--vi.d_pushCount;
}
-/* To ensure that the final deallocation stuff works,
- * we need to ensure that we need to not reference any of the other vectors
- */
-// void ArithVariables::relaxUpperBound(Constraint curr, Constraint afterPop){
-// BoundRelation next = Undefined;
-// switch(d_boundRel[x]){
-// case BelowLowerBound:
-// case BetweenBounds:
-// case AtLowerBound:
-// return; // do nothing
-// case AtUpperBound:
-// if(afterPop != NullConstraint
-// && curr->getValue() == afterPop->getValue()){
-// next = AtUpperBound;
-// }else{
-// next = BetweenBounds;
-// }
-// break;
-// case AtBothBounds:
-// if(afterPop != NullConstraint
-// && curr->getValue() == afterPop->getValue()){
-// next = AtUpperBound;
-// }else{
-// next = AtLowerBound;
-// }
-// break;
-// case AboveUpperBound:
-// if(afterPop == NullConstraint){
-// next = BetweenBounds;
-// }else{
-// int cmp = d_assignment[x].cmp(afterPop->getValue());
-// next = (cmp < 0) ? BetweenBounds :
-// (cmp == 0) ? AtUpperBound : AboveUpperBound;
-// }
-// break;
-// default:
-// Unreachable();
-// }
-// d_boundRel[x] = next;
-// }
-
+void ArithVariables::addToBoundQueue(ArithVar v, const BoundsInfo& prev){
+ if(d_enqueueingBoundCounts && !d_boundsQueue.isKey(v)){
+ d_boundsQueue.set(v, prev);
+ }
+}
+BoundsInfo ArithVariables::selectBoundsInfo(ArithVar v, bool old) const {
+ if(old && d_boundsQueue.isKey(v)){
+ return d_boundsQueue[v];
+ }else{
+ return boundsInfo(v);
+ }
+}
-// void ArithVariables::relaxLowerBound(Constraint curr, Constraint afterPop){
-// // TODO this can be optimized using the automata induced by d_boundRel and
-// // the knowledge that lb <= ub
-// ArithVar x = curr->getVariable();
-// d_boundRel[x] = boundRelationship(afterPop, d_assignment[x], d_ubc[x]);
-// }
+void ArithVariables::processBoundsQueue(BoundUpdateCallback& changed){
+ while(!d_boundsQueue.empty()){
+ ArithVar v = d_boundsQueue.back();
+ BoundsInfo prev = d_boundsQueue[v];
+ d_boundsQueue.pop_back();
+ BoundsInfo curr = boundsInfo(v);
+ if(prev != curr){
+ changed(v, prev);
+ }
+ }
+}
void ArithVariables::LowerBoundCleanUp::operator()(AVCPair* p){
d_pm->popLowerBound(p);
class ArithVariables {
private:
+
class VarInfo {
friend class ArithVariables;
ArithVar d_var;
public:
VarInfo();
- bool setAssignment(const DeltaRational& r, BoundCounts& prev);
- bool setLowerBound(Constraint c, BoundCounts& prev);
- bool setUpperBound(Constraint c, BoundCounts& prev);
+ bool setAssignment(const DeltaRational& r, BoundsInfo& prev);
+ bool setLowerBound(Constraint c, BoundsInfo& prev);
+ bool setUpperBound(Constraint c, BoundsInfo& prev);
- bool initialized() const {
- return d_var != ARITHVAR_SENTINEL;
- }
+ /** Returns true if this VarInfo has been initialized. */
+ bool initialized() const;
+
+ /**
+ * Initializes the VarInfo with the ArithVar index it is associated with,
+ * the node that the variable represents, and whether it is a slack variable.
+ */
void initialize(ArithVar v, Node n, bool slack);
+ /** Uninitializes the VarInfo. */
void uninitialize();
- bool canBeReclaimed() const{
- return d_pushCount == 0;
- }
+ bool canBeReclaimed() const;
- BoundCounts boundCounts() const {
- uint32_t lbIndc = (d_cmpAssignmentLB == 0) ? 1 : 0;
- uint32_t ubIndc = (d_cmpAssignmentUB == 0) ? 1 : 0;
- return BoundCounts(lbIndc, ubIndc);
- }
+ /** Indicator variables for if the assignment is equal to the upper and lower bounds. */
+ BoundCounts atBoundCounts() const;
+
+ /** Combination of indicator variables for whether it has upper and lower bounds. */
+ BoundCounts hasBoundCounts() const;
+
+ /** Stores both atBoundCounts() and hasBoundCounts(). */
+ BoundsInfo boundsInfo() const;
};
- //Maps from ArithVar -> VarInfo
+ /**Maps from ArithVar -> VarInfo */
typedef DenseMap<VarInfo> VarInfoVec;
+ /** This maps an ArithVar to its Variable information.*/
VarInfoVec d_vars;
// Partial Map from Arithvar -> PreviousAssignment
// Inverse of d_vars[x].d_node
NodeToArithVarMap d_nodeToArithVarMap;
- DenseMap<BoundCounts> d_atBoundsQueue;
+
+ /** The queue of constraints where the assignment is at the bound.*/
+ DenseMap<BoundsInfo> d_boundsQueue;
+
+ /**
+ * If this is true, record the incoming changes to the bound information.
+ * If this is false, the responsibility of recording the changes is LinearEqualities's.
+ */
+ bool d_enqueueingBoundCounts;
public:
// Function to call if the value of delta needs to be recomputed.
DeltaComputeCallback d_deltaComputingFunc;
- bool d_enqueueingBoundCounts;
public:
return d_vars[x].d_lb;
}
- /**
- * This forces the lower bound for a variable to be relaxed in the current context.
- * This is done by forcing the lower bound to be NullConstraint.
- * This is an expert only operation! (See primal simplex for an example.)
- */
- //void forceRelaxLowerBound(ArithVar x);
-
- /**
- * This forces the upper bound for a variable to be relaxed in the current context.
- * This is done by forcing the upper bound to be NullConstraint.
- * This is an expert only operation! (See primal simplex for an example.)
- */
- //void forceRelaxUpperBound(ArithVar x);
-
/* Initializes a variable to a safe value.*/
- //void initialize(ArithVar x, const DeltaRational& r);
void initialize(ArithVar x, Node n, bool slack);
ArithVar allocate(Node n, bool slack = false);
return d_vars[x].d_cmpAssignmentUB;
}
- inline BoundCounts boundCounts(ArithVar x) const {
- return d_vars[x].boundCounts();
+ inline BoundCounts atBoundCounts(ArithVar x) const {
+ return d_vars[x].atBoundCounts();
+ }
+ inline BoundCounts hasBoundCounts(ArithVar x) const {
+ return d_vars[x].hasBoundCounts();
+ }
+ inline BoundsInfo boundsInfo(ArithVar x) const{
+ return d_vars[x].boundsInfo();
}
bool strictlyBelowUpperBound(ArithVar x) const;
d_deltaIsSafe = true;
}
- // inline bool initialized(ArithVar x) const {
- // return d_vars[x].initialized();
- // }
-
- void addToBoundQueue(ArithVar v, BoundCounts prev){
- if(d_enqueueingBoundCounts && !d_atBoundsQueue.isKey(v)){
- d_atBoundsQueue.set(v, prev);
- }
- }
+ void startQueueingBoundCounts(){ d_enqueueingBoundCounts = true; }
+ void stopQueueingBoundCounts(){ d_enqueueingBoundCounts = false; }
+ void addToBoundQueue(ArithVar v, const BoundsInfo& prev);
- BoundCounts oldBoundCounts(ArithVar v) const {
- if(d_atBoundsQueue.isKey(v)){
- return d_atBoundsQueue[v];
- }else{
- return boundCounts(v);
- }
- }
+ BoundsInfo selectBoundsInfo(ArithVar v, bool old) const;
- void startQueueingAtBoundQueue(){ d_enqueueingBoundCounts = true; }
- void stopQueueingAtBoundQueue(){ d_enqueueingBoundCounts = false; }
-
- void processAtBoundQueue(BoundCountsCallback& changed){
- while(!d_atBoundsQueue.empty()){
- ArithVar v = d_atBoundsQueue.back();
- BoundCounts prev = d_atBoundsQueue[v];
- d_atBoundsQueue.pop_back();
- BoundCounts curr = boundCounts(v);
- if(prev != curr){
- changed(v, prev);
- }
- }
- }
+ void processBoundsQueue(BoundUpdateCallback& changed);
void printEntireModel(std::ostream& out) const;
worthwhile = proposal.errorsChange() < 0 ||
(proposal.focusDirection() > 0 &&
- d_variables.boundCounts(curr).isZero() &&
+ d_variables.atBoundCounts(curr).isZero() &&
!proposal.describesPivot());
Debug("pu::refined")
if(worthwhile){
Debug("pu") << d_variables.getAssignment(d_focusErrorVar) << endl;
- BoundCounts before = d_variables.boundCounts(curr);
+ BoundCounts before = d_variables.atBoundCounts(curr);
DeltaRational newAssignment =
d_variables.getAssignment(curr) + proposal.nonbasicDelta();
d_linEq.updateTracked(curr, newAssignment);
- BoundCounts after = d_variables.boundCounts(curr);
+ BoundCounts after = d_variables.atBoundCounts(curr);
++d_statistics.d_pureUpdates;
++boundImprovements;
Assert(tmp != ARITHVAR_SENTINEL);
Assert(d_tableau.isBasic(tmp));
+ RowIndex ri = d_tableau.basicToRowIndex(tmp);
+ d_linEq.stopTrackingRowIndex(ri);
d_tableau.removeBasicRow(tmp);
releaseVariable(tmp);
}
DeltaRational newAssignment = d_linEq.computeRowValue(inf, false);
d_variables.setAssignment(inf, newAssignment);
- d_linEq.trackVariable(inf);
+ //d_linEq.trackVariable(inf);
+ d_linEq.trackRowIndex(d_tableau.basicToRowIndex(inf));
- Debug("Inf") << inf << " " << newAssignment << endl;
+ Debug("constructInfeasiblityFunction") << inf << " " << newAssignment << endl;
return inf;
}
Debug("soi::selectPrimalUpdate")
<< "selectPrimalUpdate " << instance << endl
<< d_soiVar << " " << d_tableau.basicRowLength(d_soiVar)
- << " " << d_linEq._countBounds(d_soiVar) << endl;
+ << " " << d_linEq.debugBasicAtBoundCount(d_soiVar) << endl;
typedef std::vector<Cand> CandVector;
CandVector candidates;
int dir = !d_variables.assignmentIsConsistent(updated) ?
d_errorSet.getSgn(updated) : 0;
Debug("updateAndSignal") << " dir " << dir;
- Debug("updateAndSignal") << " _countBounds " << d_linEq._countBounds(updated) << endl;
+ Debug("updateAndSignal") << " debugBasicAtBoundCount " << d_linEq.debugBasicAtBoundCount(updated) << endl;
}
ArithVar leaving = selected.leaving();
ss << "leaving " << leaving
<< " " << d_tableau.basicRowLength(leaving)
- << " " << d_linEq._countBounds(leaving)
+ << " " << d_linEq.debugBasicAtBoundCount(leaving)
<< endl;
}
if(degenerate(w) && selected.describesPivot()){
<< "degenerate " << leaving
<< ", atBounds " << d_linEq.basicsAtBounds(selected)
<< ", len " << d_tableau.basicRowLength(leaving)
- << ", bc " << d_linEq._countBounds(leaving)
+ << ", bc " << d_linEq.debugBasicAtBoundCount(leaving)
<< endl;
}
}
d_basic2RowIndex.set(basicNew, rid);
d_rowIndex2basic.set(rid, basicNew);
- cb.swap(basicOld, basicNew, a_rs_sgn);
+ cb.multiplyRow(rid, -a_rs_sgn);
}
TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
d_containing(containing),
d_nlIncomplete( false),
- d_boundTracking(),
+ d_rowTracking(),
d_constraintDatabase(c, u, d_partialModel, d_congruenceManager, RaiseConflict(*this)),
d_qflraStatus(Result::SAT_UNKNOWN),
d_unknownsInARow(0),
d_currentPropagationList(),
d_learnedBounds(c),
d_partialModel(c, DeltaComputeCallback(*this)),
- d_errorSet(d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(&d_boundTracking)),
+ d_errorSet(d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(&d_rowTracking, &d_tableau)),
d_tableau(),
- d_linEq(d_partialModel, d_tableau, d_boundTracking, BasicVarModelUpdateCallBack(*this)),
+ d_linEq(d_partialModel, d_tableau, d_rowTracking, BasicVarModelUpdateCallBack(*this)),
d_diosolver(c),
d_restartsCounter(0),
d_tableauSizeHasBeenModified(false),
ArithVar varSlack = requestArithVar(polyNode, true);
d_tableau.addRow(varSlack, coefficients, variables);
setupBasicValue(varSlack);
- d_linEq.trackVariable(varSlack);
+ d_linEq.trackRowIndex(d_tableau.basicToRowIndex(varSlack));
//Add differences to the difference manager
Polynomial::iterator i = poly.begin(), end = poly.end();
d_constraintDatabase.removeVariable(v);
d_partialModel.releaseArithVar(v);
- d_linEq.maybeRemoveTracking(v);
}
ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool slack){
bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
Assert(d_qflraStatus != Result::SAT);
- d_partialModel.stopQueueingAtBoundQueue();
+ d_partialModel.stopQueueingBoundCounts();
UpdateTrackingCallback utcb(&d_linEq);
- d_partialModel.processAtBoundQueue(utcb);
+ d_partialModel.processBoundsQueue(utcb);
d_linEq.startTrackingBoundCounts();
bool noPivotLimit = Theory::fullEffort(effortLevel) ||
// TODO Save zeroes with no conflicts
d_linEq.stopTrackingBoundCounts();
- d_partialModel.startQueueingAtBoundQueue();
+ d_partialModel.startQueueingBoundCounts();
return emmittedConflictOrSplit;
}
if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
++d_restartsCounter;
-#warning "removing restart"
- // return;
-
- // uint32_t currSize = d_tableau.size();
- // uint32_t copySize = d_smallTableauCopy.size();
-
- // Debug("arith::reset") << "resetting" << d_restartsCounter << endl;
- // Debug("arith::reset") << "curr " << currSize << " copy " << copySize << endl;
- // Debug("arith::reset") << "tableauSizeHasBeenModified " << d_tableauSizeHasBeenModified << endl;
-
- // if(d_tableauSizeHasBeenModified){
- // Debug("arith::reset") << "row has been added must copy " << d_restartsCounter << endl;
- // d_smallTableauCopy = d_tableau;
- // d_tableauSizeHasBeenModified = false;
- // }else if( d_restartsCounter >= RESET_START){
- // if(copySize >= currSize * 1.1 ){
- // Debug("arith::reset") << "size has shrunk " << d_restartsCounter << endl;
- // ++d_statistics.d_smallerSetToCurr;
- // d_smallTableauCopy = d_tableau;
- // }else if(d_tableauResetDensity * copySize <= currSize){
- // d_errorSet.popAllSignals();
- // if(safeToReset()){
- // Debug("arith::reset") << "resetting " << d_restartsCounter << endl;
- // ++d_statistics.d_currSetToSmaller;
- // d_tableau = d_smallTableauCopy;
- // }else{
- // Debug("arith::reset") << "not safe to reset at the moment " << d_restartsCounter << endl;
- // }
- // }
- // }
- // Assert(unenqueuedVariablesAreConsistent());
}
bool TheoryArithPrivate::entireStateIsConsistent(const string& s){
//d_learnedBounds.push(bestImplied);
return true;
}
+ cout << "failed " << basic << " " << bound << assertedToTheTheory << " " <<
+ canBePropagated << " " << hasProof << endl;
+ d_partialModel.printModel(basic, cout);
}
+ }else{
+ cout << "false " << bound << " ";
+ d_partialModel.printModel(basic, cout);
}
return false;
}
}
}
+void TheoryArithPrivate::propagateCandidatesNew(){
+ /* Four criteria must be met for progagation on a variable to happen using a row:
+ * 0: A new bound has to have been added to the row.
+ * 1: The hasBoundsCount for the row must be "full" or be full minus one variable
+ * (This is O(1) to check, but requires book keeping.)
+ * 2: The current assignment must be strictly smaller/greater than the current bound.
+ * assign(x) < upper(x)
+ * (This is O(1) to compute.)
+ * 3: There is a bound that is strictly smaller/greater than the current assignment.
+ * assign(x) < c for some x <= c literal
+ * (This is O(log n) to compute.)
+ * 4: The implied bound on x is strictly smaller/greater than the current bound.
+ * (This is O(n) to compute.)
+ */
+}
+
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
// TODO A better would be:
//context::CDO<bool> d_nlIncomplete;
- BoundCountingVector d_boundTracking;
+ BoundInfoMap d_rowTracking;
/**
* The constraint database associated with the theory.
void revertOutOfConflict();
+ void propagateCandidatesNew();
+
void propagateCandidates();
void propagateCandidate(ArithVar basic);
bool propagateCandidateBound(ArithVar basic, bool upperBound);
projects / cvc5.git / commitdiff