diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-12 22:54:35 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-12 22:54:35 +0000 |
commit | 8c325a4bf6888e33fb8fdc1e071a8aab4aa20b6f (patch) | |
tree | 0132d93da953d48f57b0b0ed125c6de19c2c6e29 /src/theory/arith/partial_model.h | |
parent | 069feb82d76d10bbeebcf93a00d85b7caedb2d36 (diff) |
Delta is now generated in arithmetic to keep consistent the total order of DeltaRational values for lowerbounds, upperbounds, assignments and disequalities. Throws LogicException when a non-linear term is asserted and the the LogicInfo isLinear() disagrees.
Diffstat (limited to 'src/theory/arith/partial_model.h')
-rw-r--r-- | src/theory/arith/partial_model.h | 27 |
1 files changed, 15 insertions, 12 deletions
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index bcc65b85d..49cfd44a1 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -50,8 +50,12 @@ private: context::CDVector<Constraint> d_ubc; context::CDVector<Constraint> d_lbc; + // This is true when setDelta() is called, until invalidateDelta is called bool d_deltaIsSafe; + // Cache of a value of delta to ensure a total order. Rational d_delta; + // Function to call if the value of delta needs to be recomputed. + RationalCallBack& d_deltaComputingFunc; /** * List contains all of the variables that have an unsafe assignment. @@ -62,7 +66,7 @@ private: public: - ArithPartialModel(context::Context* c); + ArithPartialModel(context::Context* c, RationalCallBack& deltaComputation); void setLowerBoundConstraint(Constraint lb); void setUpperBoundConstraint(Constraint ub); @@ -175,20 +179,19 @@ public: return d_ubc[x] != NullConstraint; } - const Rational& getDelta(const Rational& init = Rational(1)){ - Assert(init.sgn() > 0); - if(!d_deltaIsSafe){ - computeDelta(init); - }else if(init < d_delta){ - d_delta = init; - } - return d_delta; + const Rational& getDelta(); + + inline void invalidateDelta() { + d_deltaIsSafe = false; } -private: + void setDelta(const Rational& d){ + d_delta = d; + d_deltaIsSafe = true; + } - void computeDelta(const Rational& init); - void deltaIsSmallerThan(const DeltaRational& l, const DeltaRational& u); + +private: /** * This function implements the mostly identical: |