summaryrefslogtreecommitdiff
path: root/src/theory/arith/linear_equality.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/linear_equality.h')
-rw-r--r--src/theory/arith/linear_equality.h105
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);
}
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback