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/theory_arith.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/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 754fa6521..9c2ca7d45 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -322,6 +322,17 @@ private: Node axiomIteForTotalIntDivision(Node int_div_like); + class DeltaComputeCallback : public RationalCallBack { + private: + const TheoryArith* d_ta; + public: + DeltaComputeCallback(const TheoryArith* ta) : d_ta(ta){} + + Rational operator()() const{ + return d_ta->deltaValueForTotalOrder(); + } + } d_deltaComputeCallback; + public: TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); virtual ~TheoryArith(); @@ -335,7 +346,7 @@ public: void propagate(Effort e); Node explain(TNode n); - Rational safeDeltaValueForDisequality(); + Rational deltaValueForTotalOrder() const; void collectModelInfo( TheoryModel* m, bool fullModel ); void shutdown(){ } |