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.

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(){ }