diff options
author | Tim King <taking@cs.nyu.edu> | 2012-04-17 16:07:22 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-04-17 16:07:22 +0000 |
commit | ccd77233892ace44fd4852999e66534d1c2283ea (patch) | |
tree | a856cacd24508a5839fcdbe728583ff055b64e34 /src/theory/arith/simplex.h | |
parent | 9644b6e12fbd3b649daafa43c5400d272e27bfb4 (diff) |
Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Below is a highlight of the changes:
- This introduces a new normal form to arithmetic.
-- Equalities and disequalities are in solved form.
Roughly speaking this means: (= x (+ y z)) is in normal form.
(See the comments in normal_form.h for what this formally requires.)
-- The normal form for inequality atoms always uses GEQ and GT instead of GEQ and LEQ.
Integer atoms always use GEQ.
- Constraint was added to TheoryArith.
-- A constraint is a triple of (k x v) where:
--- k is the type of the constraint (either LowerBound, UpperBound, Equality or Disequality),
--- x is an ArithVar, and
--- v is a DeltaRational value.
-- Constraints are always attached to a ConstraintDatabase.
-- A Constraint has its negation in the ConstraintDatabase [at least for now].
-- Every constraint belongs to a set of constraints for each ArithVar sorted by the delta rational values.
-- This set can be iterated over and provides efficient access to other constraints for this variable.
-- A literal may be attached to a constraint.
-- Constraints with attached literals may be marked as being asserted to the theory (sat context dependent).
-- Constraints can be propagated.
-- Every constraint has a proof (sat context dependent).
-- Proofs can be explained for either conflicts or propagations (if the node was propagated). (These proofs may be different.)
-- Equalities and disequalities can be marked as being split (user context dependent)
- This removes and replaces:
-- src/theory/arith/arith_prop_manager.*
-- src/theory/arith/atom_database.*
-- src/theory/arith/ordered_set.h
- Added isZero(), isOne() and isNegativeOne() to Rational and Integer.
- Added operator+ to CDList::const_iterator.
- Added const_iterator to CDQueue.
- Changes to regression tests.
Diffstat (limited to 'src/theory/arith/simplex.h')
-rw-r--r-- | src/theory/arith/simplex.h | 52 |
1 files changed, 17 insertions, 35 deletions
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 39c0bc20b..4e5ba3d9e 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -56,11 +56,11 @@ #include "theory/arith/delta_rational.h" #include "theory/arith/tableau.h" #include "theory/arith/partial_model.h" -#include "theory/arith/arith_prop_manager.h" #include "theory/arith/linear_equality.h" -#include "util/options.h" +#include "context/cdlist.h" +#include "util/options.h" #include "util/stats.h" #include <queue> @@ -91,13 +91,11 @@ private: /** Contains a superset of the basic variables in violation of their bounds. */ ArithPriorityQueue d_queue; - /** A link to the propagation manager. This is used to generate weaker conflicts. */ - ArithPropManager& d_propManager; - /** Number of variables in the system. This is used for tuning heuristics. */ ArithVar d_numVariables; - std::queue<Node> d_delayedLemmas; + /** This is the call back channel for Simplex to report conflicts. */ + NodeCallBack& d_conflictChannel; /** Maps a variable to how many times they have been used as a pivot in the simplex search. */ ArithVarMultiset d_pivotsInRound; @@ -106,8 +104,7 @@ private: DeltaRational d_DELTA_ZERO; public: - SimplexDecisionProcedure(ArithPropManager& propManager, - LinearEqualityModule& linEq); + SimplexDecisionProcedure(LinearEqualityModule& linEq, NodeCallBack& conflictChannel); /** * This must be called when the value of a basic variable may now voilate one @@ -123,14 +120,15 @@ public: * This is done by a simplex search through the possible bases of the tableau. * * If all of the variables can be made consistent with their bounds - * Node::null() is returned. Otherwise a minimized conflict is returned. + * false is returned. Otherwise true is returned, and at least 1 conflict + * was reported on the conflictCallback passed to the Module. * * Tableau pivoting is performed so variables may switch from being basic to * nonbasic and vice versa. * * Corresponds to the "check()" procedure in [Cav06]. */ - Node findModel(); + bool findModel(); private: @@ -158,6 +156,7 @@ private: * during the VarOrder stage of findModel. */ static ArithVar minColLength(const SimplexDecisionProcedure& simp, ArithVar x, ArithVar y); + /** * minBoundAndRowCount is a PreferenceFunction for preferring a variable * without an asserted bound over variables with an asserted bound. @@ -173,11 +172,11 @@ private: private: - Node searchForFeasibleSolution(uint32_t maxIterations); + bool searchForFeasibleSolution(uint32_t maxIterations); enum SearchPeriod {BeforeDiffSearch, DuringDiffSearch, AfterDiffSearch, DuringVarOrderSearch, AfterVarOrderSearch}; - Node findConflictOnTheQueue(SearchPeriod period, bool returnFirst = true); + bool findConflictOnTheQueue(SearchPeriod period); /** @@ -217,29 +216,12 @@ private: public: void increaseMax() {d_numVariables++;} - /** Returns true if the simplex procedure has more delayed lemmas in its queue.*/ - bool hasMoreLemmas() const { - return !d_delayedLemmas.empty(); - } - /** Returns the next delayed lemmas on the queue.*/ - Node popLemma(){ - Assert(hasMoreLemmas()); - Node lemma = d_delayedLemmas.front(); - d_delayedLemmas.pop(); - return lemma; - } - private: - /** Adds a lemma to the queue. */ - void pushLemma(Node lemma){ - d_delayedLemmas.push(lemma); - ++(d_statistics.d_delayedConflicts); - } - /** Adds a conflict as a lemma to the queue. */ - void delayConflictAsLemma(Node conflict){ - Node negatedConflict = negateConjunctionAsClause(conflict); - pushLemma(negatedConflict); + /** Reports a conflict to on the output channel. */ + void reportConflict(Node conflict){ + d_conflictChannel(conflict); + ++(d_statistics.d_simplexConflicts); } template <bool above> @@ -259,7 +241,7 @@ private: Node checkBasicForConflict(ArithVar b); Node weakenConflict(bool aboveUpper, ArithVar basicVar); - TNode weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic); + Constraint weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic); @@ -280,7 +262,7 @@ private: TimerStat d_weakenTime; - IntStat d_delayedConflicts; + IntStat d_simplexConflicts; Statistics(); ~Statistics(); |