diff options
Diffstat (limited to 'src/theory/arith/linear_equality.h')
-rw-r--r-- | src/theory/arith/linear_equality.h | 105 |
1 files changed, 41 insertions, 64 deletions
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 8b9b888f2..bc653fdad 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -192,9 +192,6 @@ public: }; - - - class LinearEqualityModule { public: typedef ArithVar (LinearEqualityModule::*VarPreferenceFunction)(ArithVar, ArithVar) const; @@ -226,14 +223,12 @@ public: * 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); @@ -241,6 +236,17 @@ public: 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); /** @@ -268,7 +274,7 @@ public: void stopTrackingBoundCounts(); - void includeBoundCountChange(ArithVar nb, BoundCounts prev); + void includeBoundUpdate(ArithVar nb, const BoundsInfo& prev); void computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunction basic); @@ -334,40 +340,6 @@ public: } } - // 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()); @@ -434,8 +406,10 @@ private: //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; /** @@ -548,31 +522,34 @@ public: 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; @@ -593,8 +570,8 @@ private: 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); @@ -737,13 +714,13 @@ public: } }; -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); } }; |