5 files changed, 153 insertions, 83 deletions

diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h
index 5982b7ac5..7cb6c6e99 100644
--- a/src/theory/arith/arithvar.h
+++ b/src/theory/arith/arithvar.h
@@ -60,6 +60,11 @@ public:
   virtual void operator()(Node n) = 0;
 };
 
+class RationalCallBack {
+public:
+  virtual Rational operator()() const = 0;
+};
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index edba437ab..0ffe67763 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -26,7 +26,7 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-ArithPartialModel::ArithPartialModel(context::Context* c)
+ArithPartialModel::ArithPartialModel(context::Context* c, RationalCallBack& deltaComputingFunc)
  : d_mapSize(0),
    d_hasSafeAssignment(),
    d_assignment(),
@@ -35,9 +35,20 @@ ArithPartialModel::ArithPartialModel(context::Context* c)
    d_lbc(c),
    d_deltaIsSafe(false),
    d_delta(-1,1),
+   d_deltaComputingFunc(deltaComputingFunc),
    d_history()
 { }
 
+
+const Rational& ArithPartialModel::getDelta(){
+  if(!d_deltaIsSafe){
+    Rational nextDelta = d_deltaComputingFunc();
+    setDelta(nextDelta);
+  }
+  Assert(d_deltaIsSafe);
+  return d_delta;
+}
+
 bool ArithPartialModel::boundsAreEqual(ArithVar x) const{
   if(hasLowerBound(x) && hasUpperBound(x)){
     return getUpperBound(x) == getLowerBound(x);
@@ -54,8 +65,7 @@ void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& r){
     d_hasSafeAssignment[x] = true;
     d_history.push_back(x);
   }
-
-  d_deltaIsSafe = false;
+  invalidateDelta();
   d_assignment[x] = r;
 }
 void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){
@@ -72,7 +82,7 @@ void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, con
     }
   }
 
-  d_deltaIsSafe = false;
+  invalidateDelta();
   d_assignment[x] = r;
 }
 
@@ -93,7 +103,7 @@ void ArithPartialModel::initialize(ArithVar x, const DeltaRational& r){
   d_hasSafeAssignment.push_back( false );
   // Is wirth mentioning that this is not strictly necessary, but this maintains the internal invariant
   // that when d_assignment is set this gets set.
-  d_deltaIsSafe = false;
+  invalidateDelta();
   d_assignment.push_back( r );
   d_safeAssignment.push_back( DeltaRational(0) );
 
@@ -149,7 +159,7 @@ void ArithPartialModel::setLowerBoundConstraint(Constraint c){
   Assert(inMaps(x));
   Assert(greaterThanLowerBound(x, c->getValue()));
 
-  d_deltaIsSafe = false;
+  invalidateDelta();
   d_lbc.set(x, c);
 }
 
@@ -163,7 +173,7 @@ void ArithPartialModel::setUpperBoundConstraint(Constraint c){
   Assert(inMaps(x));
   Assert(lessThanUpperBound(x, c->getValue()));
 
-  d_deltaIsSafe = false;
+  invalidateDelta();
   d_ubc.set(x, c);
 }
 
@@ -245,7 +255,7 @@ void ArithPartialModel::clearSafeAssignments(bool revert){
   }
 
   if(revert && !d_history.empty()){
-    d_deltaIsSafe = false;
+    invalidateDelta();
   }
 
   d_history.clear();
@@ -275,37 +285,37 @@ void ArithPartialModel::printModel(ArithVar x){
   Debug("model") << endl;
 }
 
-void ArithPartialModel::deltaIsSmallerThan(const DeltaRational& l, const DeltaRational& u){
-  const Rational& c = l.getNoninfinitesimalPart();
-  const Rational& k = l.getInfinitesimalPart();
-  const Rational& d = u.getNoninfinitesimalPart();
-  const Rational& h = u.getInfinitesimalPart();
-
-  if(c < d && k > h){
-    Rational ep = (d-c)/(k-h);
-    if(ep < d_delta){
-      d_delta = ep;
-    }
-  }
-}
-
-void ArithPartialModel::computeDelta(const Rational& init){
-  Assert(!d_deltaIsSafe);
-  d_delta = init;
-
-  for(ArithVar x = 0; x < d_mapSize; ++x){
-    const DeltaRational& a = getAssignment(x);
-    if(hasLowerBound(x)){
-      const DeltaRational& l = getLowerBound(x);
-      deltaIsSmallerThan(l,a);
-    }
-    if(hasUpperBound(x)){
-      const DeltaRational& u = getUpperBound(x);
-      deltaIsSmallerThan(a,u);
-    }
-  }
-  d_deltaIsSafe = true;
-}
+// void ArithPartialModel::deltaIsSmallerThan(const DeltaRational& l, const DeltaRational& u){
+//   const Rational& c = l.getNoninfinitesimalPart();
+//   const Rational& k = l.getInfinitesimalPart();
+//   const Rational& d = u.getNoninfinitesimalPart();
+//   const Rational& h = u.getInfinitesimalPart();
+
+//   if(c < d && k > h){
+//     Rational ep = (d-c)/(k-h);
+//     if(ep < d_delta){
+//       d_delta = ep;
+//     }
+//   }
+// }
+
+// void ArithPartialModel::computeDelta(const Rational& init){
+//   Assert(!d_deltaIsSafe);
+//   d_delta = init;
+
+//   for(ArithVar x = 0; x < d_mapSize; ++x){
+//     const DeltaRational& a = getAssignment(x);
+//     if(hasLowerBound(x)){
+//       const DeltaRational& l = getLowerBound(x);
+//       deltaIsSmallerThan(l,a);
+//     }
+//     if(hasUpperBound(x)){
+//       const DeltaRational& u = getUpperBound(x);
+//       deltaIsSmallerThan(a,u);
+//     }
+//   }
+//   d_deltaIsSafe = true;
+// }
 
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
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:
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index b342c9271..e23262137 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -28,6 +28,7 @@
 #include "util/boolean_simplification.h"
 #include "util/dense_map.h"
 
+#include "smt/logic_exception.h"
 
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/delta_rational.h"
@@ -68,7 +69,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_diseqQueue(c, false),
   d_currentPropagationList(),
   d_learnedBounds(c),
-  d_partialModel(c),
+  d_partialModel(c, d_deltaComputeCallback),
   d_tableau(),
   d_linEq(d_partialModel, d_tableau, d_basicVarModelUpdateCallBack),
   d_diosolver(c),
@@ -81,6 +82,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap, d_raiseConflict),
   d_simplex(d_linEq, d_raiseConflict),
   d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager, d_raiseConflict),
+  d_deltaComputeCallback(this),
   d_basicVarModelUpdateCallBack(d_simplex),
   d_DELTA_ZERO(0),
   d_statistics()
@@ -664,6 +666,7 @@ bool TheoryArith::AssertDisequality(Constraint constraint){
   }else{
     Debug("eq") << "push back" << constraint << endl;
     d_diseqQueue.push(constraint);
+    d_partialModel.invalidateDelta();
   }
   return false;
 
@@ -854,6 +857,10 @@ void TheoryArith::setupVariableList(const VarList& vl){
   if(!vl.singleton()){
     // vl is the product of at least 2 variables
     // vl : (* v1 v2 ...)
+    if(getLogicInfo().isLinear()){
+      throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
+    }
+
     d_out->setIncomplete();
     d_nlIncomplete = true;
 
@@ -885,6 +892,11 @@ void TheoryArith::cautiousSetupPolynomial(const Polynomial& p){
 
 void TheoryArith::setupDivLike(const Variable& v){
   Assert(v.isDivLike());
+
+  if(getLogicInfo().isLinear()){
+    throw LogicException("Non-linear term was asserted to arithmetic in a linear logic.");
+  }
+
   Node vnode = v.getNode();
   Assert(isSetup(vnode)); // Otherwise there is some invariant breaking recursion
   Polynomial m = Polynomial::parsePolynomial(vnode[0]);
@@ -2075,44 +2087,74 @@ DeltaRational TheoryArith::getDeltaValueWithNonlinear(TNode n, bool& failed) {
   }
 }
 
-Rational TheoryArith::safeDeltaValueForDisequality(){
+Rational TheoryArith::deltaValueForTotalOrder() const{
   Rational min(2);
-  context::CDQueue<Constraint>::const_iterator iter = d_diseqQueue.begin();
-  context::CDQueue<Constraint>::const_iterator iter_end = d_diseqQueue.end(); 
+  std::set<DeltaRational> relevantDeltaValues;
+  context::CDQueue<Constraint>::const_iterator qiter = d_diseqQueue.begin();
+  context::CDQueue<Constraint>::const_iterator qiter_end = d_diseqQueue.end();
 
-  for(; iter != iter_end; ++iter){
-    Constraint curr = *iter;
-    
-    ArithVar lhsVar = curr->getVariable();
+  for(; qiter != qiter_end; ++qiter){
+    Constraint curr = *qiter;
 
-    const DeltaRational& lhsValue = d_partialModel.getAssignment(lhsVar);
     const DeltaRational& rhsValue = curr->getValue();
-    DeltaRational diff = lhsValue - rhsValue;
-    Assert(diff.sgn() != 0);
-
-    // diff != 0
-    // dinf * delta + dmajor != 0
-    // dinf * delta != -dmajor
-    const Rational& dinf = diff.getInfinitesimalPart();
-    const Rational& dmaj = diff.getNoninfinitesimalPart();
-    if(dinf.isZero()){
-      Assert(!dmaj.isZero());
-    }else if(dmaj.isZero()){
-      Assert(!dinf.isZero());
-    }else{
-      // delta != - dmajor / dinf
-      // if 0 < delta < abs(dmajor/dinf), then 
-      Rational d = (dmaj/dinf).abs();
-      Assert(d.sgn() > 0);
+    relevantDeltaValues.insert(rhsValue);
+  }
+
+  for(ArithVar v = 0; v < d_variables.size(); ++v){
+    const DeltaRational& value = d_partialModel.getAssignment(v);
+    relevantDeltaValues.insert(value);
+    if( d_partialModel.hasLowerBound(v)){
+      const DeltaRational& lb = d_partialModel.getLowerBound(v);
+      relevantDeltaValues.insert(lb);
+    }
+    if( d_partialModel.hasUpperBound(v)){
+      const DeltaRational& ub = d_partialModel.getUpperBound(v);
+      relevantDeltaValues.insert(ub);
+    }
+  }
+
+  if(relevantDeltaValues.size() >= 2){
+    std::set<DeltaRational>::const_iterator iter = relevantDeltaValues.begin();
+    std::set<DeltaRational>::const_iterator iter_end = relevantDeltaValues.end();
+    DeltaRational prev = *iter;
+    ++iter;
+    for(; iter != iter_end; ++iter){
+      const DeltaRational& curr = *iter;
+
+      Assert(prev < curr);
+
+      const Rational& pinf = prev.getInfinitesimalPart();
+      const Rational& cinf = curr.getInfinitesimalPart();
 
-      if(d < min){
-        min = d;
+      const Rational& pmaj = prev.getNoninfinitesimalPart();
+      const Rational& cmaj = curr.getNoninfinitesimalPart();
+
+      if(pmaj == cmaj){
+        Assert(pinf < cinf);
+        // any value of delta preserves the order
+      }else if(pinf == cinf){
+        Assert(pmaj < cmaj);
+        // any value of delta preserves the order
+      }else{
+        Assert(pinf != cinf && pmaj != cmaj);
+        Rational denDiffAbs = (cinf - pinf).abs();
+
+        Rational numDiff = (cmaj - pmaj);
+        Assert(numDiff.sgn() >= 0);
+        Assert(denDiffAbs.sgn() > 0);
+        Rational ratio = numDiff / denDiffAbs;
+        Assert(ratio.sgn() > 0);
+
+        if(ratio < min){
+          min = ratio;
+        }
       }
+      prev = curr;
     }
   }
 
   Assert(min.sgn() > 0);
-  Rational belowMin = min/Rational(2);  
+  Rational belowMin = min/Rational(2);
   return belowMin;
 }
 
@@ -2124,8 +2166,7 @@ void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){
 
 
   // Delta lasts at least the duration of the function call
-  const Rational init = safeDeltaValueForDisequality();
-  const Rational& delta = d_partialModel.getDelta(init);
+  const Rational& delta = d_partialModel.getDelta();
   std::hash_set<TNode, TNodeHashFunction> shared = currentlySharedTerms();
 
   // TODO:
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(){ }