diff options
Diffstat (limited to 'src/theory/arith/simplex.h')
-rw-r--r-- | src/theory/arith/simplex.h | 36 |
1 files changed, 5 insertions, 31 deletions
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index c5c4da661..9fed7dc0b 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -5,6 +5,7 @@ #define __CVC4__THEORY__ARITH__SIMPLEX_H #include "theory/arith/arith_utilities.h" +#include "theory/arith/arith_priority_queue.h" #include "theory/arith/arithvar_set.h" #include "theory/arith/delta_rational.h" #include "theory/arith/tableau.h" @@ -21,30 +22,7 @@ namespace arith { class SimplexDecisionProcedure { private: - typedef std::pair<ArithVar, DeltaRational> VarDRatPair; - struct VarDRatPairCompare{ - inline bool operator()(const VarDRatPair& a, const VarDRatPair& b){ - return a.second > b.second; - } - }; - typedef std::priority_queue<VarDRatPair, std::vector<VarDRatPair>, VarDRatPairCompare> GriggioPQueue; - - GriggioPQueue d_griggioRuleQueue; - - /** - * Priority Queue of the basic variables that may be inconsistent. - * - * This is required to contain at least 1 instance of every inconsistent - * basic variable. This is only required to be a superset though so its - * contents must be checked to still be basic and inconsistent. - * - * This is also required to agree with the row on variable order for termination. - * Effectively this means that this must be a min-heap. - */ - typedef std::priority_queue<ArithVar, vector<ArithVar>, std::greater<ArithVar> > PQueue; - - PQueue d_possiblyInconsistent; /** Stores system wide constants to avoid unnessecary reconstruction. */ const ArithConstants& d_constants; @@ -58,23 +36,21 @@ private: OutputChannel* d_out; Tableau& d_tableau; + ArithPriorityQueue d_queue; ArithVar d_numVariables; - bool d_pivotStage; - public: SimplexDecisionProcedure(const ArithConstants& constants, ArithPartialModel& pm, OutputChannel* out, Tableau& tableau) : - d_possiblyInconsistent(), d_constants(constants), d_partialModel(pm), d_out(out), d_tableau(tableau), - d_numVariables(0), - d_pivotStage(true) + d_queue(pm, tableau), + d_numVariables(0) {} void increaseMax() {d_numVariables++;} @@ -130,7 +106,7 @@ public: */ Node updateInconsistentVars(); private: - Node privateUpdateInconsistentVars(); + template <bool limitIterations> Node searchForFeasibleSolution(uint32_t maxIterations); Node selectInitialConflict(); @@ -182,8 +158,6 @@ public: DeltaRational computeRowValue(ArithVar x, bool useSafe); private: - /** Check to make sure all of the basic variables are within their bounds. */ - void checkBasicVariable(ArithVar basic); /** * Checks a basic variable, b, to see if it is in conflict. |