diff options
Diffstat (limited to 'src/theory/arith/linear_equality.h')
-rw-r--r-- | src/theory/arith/linear_equality.h | 629 |
1 files changed, 606 insertions, 23 deletions
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 14df8d819..8b9b888f2 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -27,36 +27,198 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H -#define __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H +#pragma once #include "theory/arith/delta_rational.h" #include "theory/arith/arithvar.h" #include "theory/arith/partial_model.h" -#include "theory/arith/matrix.h" -#include "theory/arith/constraint.h" +#include "theory/arith/tableau.h" +#include "theory/arith/constraint_forward.h" +#include "theory/arith/simplex_update.h" +#include "theory/arith/options.h" +#include "util/maybe.h" #include "util/statistics_registry.h" namespace CVC4 { namespace theory { namespace arith { +struct Border{ + // The constraint for the border + Constraint d_bound; + + // The change to the nonbasic to reach the border + DeltaRational d_diff; + + // Is reach this value fixing the constraint + // or is going past this value hurting the constraint + bool d_areFixing; + + // Entry into the tableau + const Tableau::Entry* d_entry; + + // Was this an upper bound or a lower bound? + bool d_upperbound; + + Border(): + d_bound(NullConstraint) // ignore the other values + {} + + Border(Constraint l, const DeltaRational& diff, bool areFixing, const Tableau::Entry* en, bool ub): + d_bound(l), d_diff(diff), d_areFixing(areFixing), d_entry(en), d_upperbound(ub) + {} + + Border(Constraint l, const DeltaRational& diff, bool areFixing, bool ub): + d_bound(l), d_diff(diff), d_areFixing(areFixing), d_entry(NULL), d_upperbound(ub) + {} + bool operator<(const Border& other) const{ + return d_diff < other.d_diff; + } + + /** d_lim is the nonbasic variable's own bound. */ + bool ownBorder() const { return d_entry == NULL; } + + bool isZero() const { return d_diff.sgn() == 0; } + static bool nonZero(const Border& b) { return !b.isZero(); } + + const Rational& getCoefficient() const { + Assert(!ownBorder()); + return d_entry->getCoefficient(); + } + void output(std::ostream& out) const; +}; + +inline std::ostream& operator<<(std::ostream& out, const Border& b){ + b.output(out); + return out; +} + +typedef std::vector<Border> BorderVec; + +class BorderHeap { + const int d_dir; + + class BorderHeapCmp { + private: + int d_nbDirection; + public: + BorderHeapCmp(int dir): d_nbDirection(dir){} + bool operator()(const Border& a, const Border& b) const{ + if(d_nbDirection > 0){ + // if nb is increasing, + // this needs to act like a max + // in order to have a min heap + return b < a; + }else{ + // if nb is decreasing, + // this needs to act like a min + // in order to have a max heap + return a < b; + } + } + }; + const BorderHeapCmp d_cmp; + + BorderVec d_vec; + + BorderVec::iterator d_begin; + + /** + * Once this is initialized the top of the heap will always + * be at d_end - 1 + */ + BorderVec::iterator d_end; + + int d_possibleFixes; + int d_numZeroes; + +public: + BorderHeap(int dir) + : d_dir(dir), d_cmp(dir), d_possibleFixes(0), d_numZeroes(0) + {} + + void push_back(const Border& b){ + d_vec.push_back(b); + if(b.d_areFixing){ + d_possibleFixes++; + } + if(b.d_diff.sgn() == 0){ + d_numZeroes++; + } + } + + int numZeroes() const { return d_numZeroes; } + int possibleFixes() const { return d_possibleFixes; } + int direction() const { return d_dir; } + + void make_heap(){ + d_begin = d_vec.begin(); + d_end = d_vec.end(); + std::make_heap(d_begin, d_end, d_cmp); + } + + void dropNonZeroes(){ + std::remove_if(d_vec.begin(), d_vec.end(), &Border::nonZero); + } + + const Border& top() const { + Assert(more()); + return *d_begin; + } + void pop_heap(){ + Assert(more()); + + std::pop_heap(d_begin, d_end, d_cmp); + --d_end; + } + + BorderVec::const_iterator end() const{ + return BorderVec::const_iterator(d_end); + } + BorderVec::const_iterator begin() const{ + return BorderVec::const_iterator(d_begin); + } + + inline bool more() const{ return d_begin != d_end; } + + inline bool empty() const{ return d_vec.empty(); } + + void clear(){ + d_possibleFixes = 0; + d_numZeroes = 0; + d_vec.clear(); + } +}; + + + + + class LinearEqualityModule { +public: + typedef ArithVar (LinearEqualityModule::*VarPreferenceFunction)(ArithVar, ArithVar) const; + + + typedef bool (LinearEqualityModule::*UpdatePreferenceFunction)(const UpdateInfo&, const UpdateInfo&) const; + private: /** * Manages information about the assignment and upper and lower bounds on the * variables. */ - ArithPartialModel& d_partialModel; + ArithVariables& d_variables; - /** - * Reference to the Tableau to operate upon. - */ + /** Reference to the Tableau to operate upon. */ Tableau& d_tableau; /** Called whenever the value of a basic variable is updated. */ - ArithVarCallBack& d_basicVariableUpdates; + BasicVarModelUpdateCallBack d_basicVariableUpdates; + + BorderHeap d_increasing; + BorderHeap d_decreasing; + Maybe<DeltaRational> d_upperBoundDifference; + Maybe<DeltaRational> d_lowerBoundDifference; public: @@ -64,15 +226,22 @@ public: * Initializes 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) - {} + LinearEqualityModule(ArithVariables& vars, Tableau& t, BoundCountingVector& boundTracking, BasicVarModelUpdateCallBack 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); + 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); + }else{ + updateUntracked(x_i,v); + } + } + void updateMany(const DenseMap<DeltaRational>& many); /** * Updates the value of a basic variable x_i to v, @@ -80,11 +249,12 @@ public: * Updates the assignment of the other basic variables accordingly. */ void pivotAndUpdate(ArithVar x_i, ArithVar x_j, const DeltaRational& v); + //void pivotAndUpdateAdj(ArithVar x_i, ArithVar x_j, const DeltaRational& v); - - ArithPartialModel& getPartialModel() const{ return d_partialModel; } + ArithVariables& getVariables() const{ return d_variables; } Tableau& getTableau() const{ return d_tableau; } + void forceNewBasis(const DenseSet& newBasis); bool hasBounds(ArithVar basic, bool upperBound); bool hasLowerBounds(ArithVar basic){ @@ -94,7 +264,180 @@ public: return hasBounds(basic, true); } + void startTrackingBoundCounts(); + void stopTrackingBoundCounts(); + + + void includeBoundCountChange(ArithVar nb, BoundCounts prev); + + void computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunction basic); + + + uint32_t updateProduct(const UpdateInfo& inf) const; + + inline bool minNonBasicVarOrder(const UpdateInfo& a, const UpdateInfo& b) const{ + return a.nonbasic() >= b.nonbasic(); + } + + /** + * Prefer the update that touch the fewest entries in the matrix. + * + * The intuition is that this operation will be cheaper. + * This strongly biases the system towards updates instead of pivots. + */ + inline bool minProduct(const UpdateInfo& a, const UpdateInfo& b) const{ + uint32_t aprod = updateProduct(a); + uint32_t bprod = updateProduct(b); + + if(aprod == bprod){ + return minNonBasicVarOrder(a,b); + }else{ + return aprod > bprod; + } + } + inline bool constrainedMin(const UpdateInfo& a, const UpdateInfo& b) const{ + if(a.describesPivot() && b.describesPivot()){ + bool aAtBounds = basicsAtBounds(a); + bool bAtBounds = basicsAtBounds(b); + if(aAtBounds != bAtBounds){ + return bAtBounds; + } + } + return minProduct(a,b); + } + + /** + * If both a and b are pivots, prefer the pivot with the leaving variables that has equal bounds. + * The intuition is that such variables will be less likely to lead to future problems. + */ + inline bool preferFrozen(const UpdateInfo& a, const UpdateInfo& b) const { + if(a.describesPivot() && b.describesPivot()){ + bool aFrozen = d_variables.boundsAreEqual(a.leaving()); + bool bFrozen = d_variables.boundsAreEqual(b.leaving()); + + if(aFrozen != bFrozen){ + return bFrozen; + } + } + return constrainedMin(a,b); + } + + /** + * Prefer pivots with entering variables that do not have bounds. + * The intuition is that such variables will be less likely to lead to future problems. + */ + bool preferNeitherBound(const UpdateInfo& a, const UpdateInfo& b) const { + if(d_variables.hasEitherBound(a.nonbasic()) == d_variables.hasEitherBound(b.nonbasic())){ + return preferFrozen(a,b); + }else{ + return d_variables.hasEitherBound(a.nonbasic()); + } + } + + // 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()); + Assert(b.describesPivot()); + if(a.nonbasic() == b.nonbasic()){ + bool aIsZero = a.nonbasicDelta().sgn() == 0; + bool bIsZero = b.nonbasicDelta().sgn() == 0; + + if((aIsZero || bIsZero) && (!aIsZero || !bIsZero)){ + return bIsZero; + }else{ + return a.leaving() >= b.leaving(); + } + }else{ + return a.nonbasic() > b.nonbasic(); + } + } + + template <bool heuristic> + bool preferWitness(const UpdateInfo& a, const UpdateInfo& b) const{ + WitnessImprovement aImp = a.getWitness(!heuristic); + WitnessImprovement bImp = b.getWitness(!heuristic); + + if(aImp == bImp){ + switch(aImp){ + case ConflictFound: + return preferNeitherBound(a,b); + case ErrorDropped: + if(a.errorsChange() == b.errorsChange()){ + return preferNeitherBound(a,b); + }else{ + return a.errorsChange() > b.errorsChange(); + } + case FocusImproved: + return preferNeitherBound(a,b); + case BlandsDegenerate: + Assert(a.describesPivot()); + Assert(b.describesPivot()); + Assert(a.focusDirection() == 0 && b.focusDirection() == 0); + return modifiedBlands(a,b); + case HeuristicDegenerate: + Assert(a.describesPivot()); + Assert(b.describesPivot()); + Assert(a.focusDirection() == 0 && b.focusDirection() == 0); + return preferNeitherBound(a,b); + case AntiProductive: + return minNonBasicVarOrder(a, b); + // Not valid responses + case Degenerate: + case FocusShrank: + Unreachable(); + } + Unreachable(); + }else{ + return aImp > bImp; + } + } + private: + typedef std::vector<const Tableau::Entry*> EntryPointerVector; + EntryPointerVector d_relevantErrorBuffer; + + //uint32_t computeUnconstrainedUpdate(ArithVar nb, int sgn, DeltaRational& am); + //uint32_t computedFixed(ArithVar nb, int sgn, const DeltaRational& am); + void computedFixed(UpdateInfo&); + + // RowIndex -> BoundCount + BoundCountingVector& d_boundTracking; + bool d_areTracking; + /** * Exports either the explanation of an upperbound or a lower bound * of the basic variable basic, using the non-basic variables in the row. @@ -104,11 +447,9 @@ private: public: void propagateNonbasicsLowerBound(ArithVar basic, Constraint c){ - Assert(c->isLowerBound()); propagateNonbasics<false>(basic, c); } void propagateNonbasicsUpperBound(ArithVar basic, Constraint c){ - Assert(c->isUpperBound()); propagateNonbasics<true>(basic, c); } @@ -128,42 +469,284 @@ public: return computeBound(basic, true); } + /** + * A PreferenceFunction takes a const ref to the SimplexDecisionProcedure, + * and 2 ArithVar variables and returns one of the ArithVar variables + * potentially using the internals of the SimplexDecisionProcedure. + */ + + ArithVar noPreference(ArithVar x, ArithVar y) const{ + return x; + } + + /** + * minVarOrder is a PreferenceFunction for selecting the smaller of the 2 + * ArithVars. This PreferenceFunction is used during the VarOrder stage of + * findModel. + */ + ArithVar minVarOrder(ArithVar x, ArithVar y) const; + + /** + * minColLength is a PreferenceFunction for selecting the variable with the + * smaller row count in the tableau. + * + * This is a heuristic rule and should not be used during the VarOrder + * stage of findModel. + */ + ArithVar minColLength(ArithVar x, ArithVar y) const; + + /** + * minRowLength is a PreferenceFunction for selecting the variable with the + * smaller row count in the tableau. + * + * This is a heuristic rule and should not be used during the VarOrder + * stage of findModel. + */ + ArithVar minRowLength(ArithVar x, ArithVar y) const; + + /** + * minBoundAndRowCount is a PreferenceFunction for preferring a variable + * without an asserted bound over variables with an asserted bound. + * If both have bounds or both do not have bounds, + * the rule falls back to minRowCount(...). + * + * This is a heuristic rule and should not be used during the VarOrder + * stage of findModel. + */ + ArithVar minBoundAndColLength(ArithVar x, ArithVar y) const; + + + template <bool above> + inline bool isAcceptableSlack(int sgn, ArithVar nonbasic) const { + return + ( above && sgn < 0 && d_variables.strictlyBelowUpperBound(nonbasic)) || + ( above && sgn > 0 && d_variables.strictlyAboveLowerBound(nonbasic)) || + (!above && sgn > 0 && d_variables.strictlyBelowUpperBound(nonbasic)) || + (!above && sgn < 0 && d_variables.strictlyAboveLowerBound(nonbasic)); + } + + /** + * Given the basic variable x_i, + * this function finds the smallest nonbasic variable x_j in the row of x_i + * in the tableau that can "take up the slack" to let x_i satisfy its bounds. + * This returns ARITHVAR_SENTINEL if none exists. + * + * More formally one of the following conditions must be satisfied: + * - lowerBound && a_ij < 0 && assignment(x_j) < upperbound(x_j) + * - lowerBound && a_ij > 0 && assignment(x_j) > lowerbound(x_j) + * - !lowerBound && a_ij > 0 && assignment(x_j) < upperbound(x_j) + * - !lowerBound && a_ij < 0 && assignment(x_j) > lowerbound(x_j) + * + */ + template <bool lowerBound> ArithVar selectSlack(ArithVar x_i, VarPreferenceFunction pf) const; + ArithVar selectSlackLowerBound(ArithVar x_i, VarPreferenceFunction pf) const { + return selectSlack<true>(x_i, pf); + } + ArithVar selectSlackUpperBound(ArithVar x_i, VarPreferenceFunction pf) const { + return selectSlack<false>(x_i, pf); + } + + const Tableau::Entry* selectSlackEntry(ArithVar x_i, bool above) const; + + inline bool basicIsTracked(ArithVar v) const { + return d_boundTracking.isKey(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 trackVariable(ArithVar x_i){ + // Assert(!basicIsTracked(x_i)); + // d_boundTracking.set(x_i,computeBoundCounts(x_i)); + // } + bool basicsAtBounds(const UpdateInfo& u) const; +private: + BoundCounts computeBoundCounts(ArithVar x_i) const; +public: + //BoundCounts cachingCountBounds(ArithVar x_i) const; + BoundCounts _countBounds(ArithVar x_i) const; + void trackingCoefficientChange(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn); + + void trackingSwap(ArithVar basic, ArithVar nb, int sgn); + + bool nonbasicsAtLowerBounds(ArithVar x_i) const; + bool nonbasicsAtUpperBounds(ArithVar x_i) const; + + ArithVar _anySlackLowerBound(ArithVar x_i) const { + return selectSlack<true>(x_i, &LinearEqualityModule::noPreference); + } + ArithVar _anySlackUpperBound(ArithVar x_i) const { + return selectSlack<false>(x_i, &LinearEqualityModule::noPreference); + } + +private: + class TrackingCallback : public CoefficientChangeCallback { + private: + LinearEqualityModule* d_linEq; + public: + TrackingCallback(LinearEqualityModule* le) : d_linEq(le) {} + 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); + } + bool canUseRow(RowIndex ridx) const { + ArithVar basic = d_linEq->getTableau().rowIndexToBasic(ridx); + return d_linEq->basicIsTracked(basic); + } + } d_trackCallback; + + /** + * Selects the constraint for the variable v on the row for basic + * with the weakest possible constraint that is consistent with the surplus + * surplus. + */ + Constraint weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, + const Rational& coeff, bool& anyWeakening, ArithVar basic) const; + +public: + /** + * Constructs a minimally weak conflict for the basic variable basicVar. + */ + Node minimallyWeakConflict(bool aboveUpper, ArithVar basicVar) const; + + /** + * Given a non-basic variable that is know to have a conflict on it, + * construct and return a conflict. + * Follows section 4.2 in the CAV06 paper. + */ + inline Node generateConflictAboveUpperBound(ArithVar conflictVar) const { + return minimallyWeakConflict(true, conflictVar); + } + + inline Node generateConflictBelowLowerBound(ArithVar conflictVar) const { + return minimallyWeakConflict(false, conflictVar); + } + private: DeltaRational computeBound(ArithVar basic, bool upperBound); public: + void substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult); + void directlyAddToCoefficient(ArithVar row, ArithVar col, const Rational& mult); + + /** * Checks to make sure the assignment is consistent with the tableau. * This code is for debugging. */ void debugCheckTableau(); + void debugCheckTracking(); + /** Debugging information for a pivot. */ void debugPivot(ArithVar x_i, ArithVar x_j); + /** Checks the tableau + partial model for consistency. */ + bool debugEntireLinEqIsConsistent(const std::string& s); + + + ArithVar minBy(const ArithVarVec& vec, VarPreferenceFunction pf) const; + /** - * + * Returns true if there would be a conflict on this row after a pivot + * and update using its basic variable and one of the non-basic variables on + * the row. */ - bool debugEntireLinEqIsConsistent(const std::string& s); + bool willBeInConflictAfterPivot(const Tableau::Entry& entry, const DeltaRational& nbDiff, bool bToUB) const; + UpdateInfo mkConflictUpdate(const Tableau::Entry& entry, bool ub) const; + /** + * Looks more an update for fcSimplex on the nonbasic variable nb with the focus coefficient. + */ + UpdateInfo speculativeUpdate(ArithVar nb, const Rational& focusCoeff, UpdatePreferenceFunction pref); + +private: + + /** + * Examines the effects of pivoting the entries column variable + * with the row's basic variable and setting the variable s.t. + * the basic variable is equal to one of its bounds. + * + * If ub, then the basic variable will be equal its upper bound. + * If not ub,then the basic variable will be equal its lower bound. + * + * Returns iff this row will be in conflict after the pivot. + * + * If this is false, add the bound to the relevant heap. + * If the bound is +/-infinity, this is ignored. + + * + * Returns true if this would be a conflict. + * If it returns false, this + */ + bool accumulateBorder(const Tableau::Entry& entry, bool ub); + + void handleBorders(UpdateInfo& selected, ArithVar nb, const Rational& focusCoeff, BorderHeap& heap, int minimumFixes, UpdatePreferenceFunction pref); + void pop_block(BorderHeap& heap, int& brokenInBlock, int& fixesRemaining, int& negErrorChange); + void clearSpeculative(); + Rational updateCoefficient(BorderVec::const_iterator startBlock, BorderVec::const_iterator endBlock); private: /** These fields are designed to be accessible to TheoryArith methods. */ class Statistics { public: IntStat d_statPivots, d_statUpdates; - TimerStat d_pivotTime; + TimerStat d_adjTime; + + IntStat d_weakeningAttempts, d_weakeningSuccesses, d_weakenings; + TimerStat d_weakenTime; Statistics(); ~Statistics(); }; - Statistics d_statistics; + mutable Statistics d_statistics; };/* class LinearEqualityModule */ +struct Cand { + ArithVar d_nb; + uint32_t d_penalty; + int d_sgn; + const Rational* d_coeff; + + Cand(ArithVar nb, uint32_t penalty, int s, const Rational* c) : + d_nb(nb), d_penalty(penalty), d_sgn(s), d_coeff(c){} +}; + + +class CompPenaltyColLength { +private: + LinearEqualityModule* d_mod; +public: + CompPenaltyColLength(LinearEqualityModule* mod): d_mod(mod){} + + bool operator()(const Cand& x, const Cand& y) const { + if(x.d_penalty == y.d_penalty || !options::havePenalties()){ + return x.d_nb == d_mod->minBoundAndColLength(x.d_nb,y.d_nb); + }else{ + return x.d_penalty < y.d_penalty; + } + } +}; + +class UpdateTrackingCallback : public BoundCountsCallback { +private: + LinearEqualityModule* d_mod; +public: + UpdateTrackingCallback(LinearEqualityModule* mod): d_mod(mod){} + void operator()(ArithVar v, BoundCounts bc){ + d_mod->includeBoundCountChange(v, bc); + } +}; + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__ARITH__LINEAR_EQUALITY_H */ |