diff options
author | Tim King <taking@cs.nyu.edu> | 2012-02-28 21:26:35 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-02-28 21:26:35 +0000 |
commit | eefe0b63e564320eb135eb66d6c02c9dc6e9e8de (patch) | |
tree | 14d9643427fadab3e1c064d5528fa02e46f6bef7 /src/theory/arith/theory_arith.h | |
parent | 9450e5841a08db3a9529c25e03fc5cea16a8f1f5 (diff) |
This commit merges in branches/arithmetic/internalbb up to revision 2831. This is a significant refactoring of code.
- r2820
-- Refactors Simplex so that it does significantly fewer functions.
-- Adds the LinearEqualityModule for handling update and pivotAndUpdate and other utility functions that require access to both the tableau and partial model.
-- Some of the code for propagation has moved to TheoryArith.
-r2826
-- Small changes to documentation and removes the no longer implemented deduceLowerBound() and deduceUpperBound().
- r2827
-- Adds isZero() to Rational. Adds cmp to DeltaRational.
- r2831
-- Refactored comparison to upper and lower in the partial model to use DeltaRational::cmp.
-- Refactored AssertUpper and AssertLower in TheoryArith to include functionality that has weaseled into TheoryArith::assertionCases.
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 75 |
1 files changed, 71 insertions, 4 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index c19a20ead..f364885c2 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -32,6 +32,7 @@ #include "theory/arith/tableau.h" #include "theory/arith/arith_rewriter.h" #include "theory/arith/partial_model.h" +#include "theory/arith/linear_equality.h" #include "theory/arith/atom_database.h" #include "theory/arith/simplex.h" #include "theory/arith/arith_static_learner.h" @@ -180,20 +181,25 @@ private: std::map<ArithVar, Node> d_removedRows; /** + * List of all of the inequalities asserted in the current context. + */ + context::CDSet<Node, NodeHashFunction> d_diseq; + + /** * Manages information about the assignment and upper and lower bounds on * variables. */ ArithPartialModel d_partialModel; /** - * List of all of the inequalities asserted in the current context. + * The tableau for all of the constraints seen thus far in the system. */ - context::CDSet<Node, NodeHashFunction> d_diseq; + Tableau d_tableau; /** - * The tableau for all of the constraints seen thus far in the system. + * Maintains the relationship between the PartialModel and the Tableau. */ - Tableau d_tableau; + LinearEqualityModule d_linEq; /** * A Diophantine equation solver. Accesses the tableau and partial @@ -279,6 +285,23 @@ public: void addSharedTerm(TNode n); private: + + class BasicVarModelUpdateCallBack : public ArithVarCallBack{ + private: + SimplexDecisionProcedure& d_simplex; + + public: + BasicVarModelUpdateCallBack(SimplexDecisionProcedure& s): + d_simplex(s) + {} + + void callback(ArithVar x){ + d_simplex.updateBasic(x); + } + }; + + BasicVarModelUpdateCallBack d_basicVarModelUpdateCallBack; + /** The constant zero. */ DeltaRational d_DELTA_ZERO; @@ -331,6 +354,45 @@ private: /** + * Assert*(n, orig) takes an bound n that is implied by orig. + * and asserts that as a new bound if it is tighter than the current bound + * and updates the value of a basic variable if needed. + * + * orig must be a literal in the SAT solver so that it can be used for + * conflict analysis. + * + * x is the variable getting the new bound, + * c is the value of the new bound. + * + * If this new bound is in conflict with the other bound, + * a node describing this conflict is returned. + * If this new bound is not in conflict, Node::null() is returned. + */ + Node AssertLower(ArithVar x, DeltaRational& c, TNode orig); + Node AssertUpper(ArithVar x, DeltaRational& c, TNode orig); + Node AssertEquality(ArithVar x, DeltaRational& c, TNode orig); + + /** Tracks the bounds that were updated in the current round. */ + PermissiveBackArithVarSet d_updatedBounds; + + /** Tracks the basic variables where propagatation might be possible. */ + PermissiveBackArithVarSet d_candidateBasics; + + bool hasAnyUpdates() { return !d_updatedBounds.empty(); } + void clearUpdates(){ d_updatedBounds.purge(); } + + void propagateCandidates(); + void propagateCandidate(ArithVar basic); + bool propagateCandidateBound(ArithVar basic, bool upperBound); + + inline bool propagateCandidateLowerBound(ArithVar basic){ + return propagateCandidateBound(basic, false); + } + inline bool propagateCandidateUpperBound(ArithVar basic){ + return propagateCandidateBound(basic, true); + } + + /** * Performs a check to see if it is definitely true that setup can be avoided. */ bool canSafelyAvoidEqualitySetup(TNode equality); @@ -383,6 +445,8 @@ private: /** These fields are designed to be accessable to TheoryArith methods. */ class Statistics { public: + IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts; + IntStat d_statUserVariables, d_statSlackVariables; IntStat d_statDisequalitySplits; IntStat d_statDisequalityConflicts; @@ -399,6 +463,9 @@ private: IntStat d_smallerSetToCurr; TimerStat d_restartTimer; + TimerStat d_boundComputationTime; + IntStat d_boundComputations, d_boundPropagations; + Statistics(); ~Statistics(); }; |