Fix for bug 439. Delta computation now includes disequality information.

diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 73e7943b0752deb6f44333bee0050b2c8e29d52c..edba437ab2adda6577273fef5fc324cc1d018ee2 100644 (file)
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -289,9 +289,9 @@ void ArithPartialModel::deltaIsSmallerThan(const DeltaRational& l, const DeltaRa
   }
 }
 
-void ArithPartialModel::computeDelta(){
+void ArithPartialModel::computeDelta(const Rational& init){
   Assert(!d_deltaIsSafe);
-  d_delta = 1;
+  d_delta = init;
 
   for(ArithVar x = 0; x < d_mapSize; ++x){
     const DeltaRational& a = getAssignment(x);

diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 83e2a4f2baa07c9bdc9060fe100a6804bb9de419..bcc65b85d88b274dc8ac20db3a486b2c7a96a3a7 100644 (file)
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -175,16 +175,19 @@ public:
     return d_ubc[x] != NullConstraint;
   }
 
-  const Rational& getDelta(){
+  const Rational& getDelta(const Rational& init = Rational(1)){
+    Assert(init.sgn() > 0);
     if(!d_deltaIsSafe){
-      computeDelta();
+      computeDelta(init);
+    }else if(init < d_delta){
+      d_delta = init;
     }
     return d_delta;
   }
 
 private:
 
-  void computeDelta();
+  void computeDelta(const Rational& init);
   void deltaIsSmallerThan(const DeltaRational& l, const DeltaRational& u);
 
   /**

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 4ce1113a4c5cbb99c3a04acd8aa57f86c465d404..b342c9271bf19553c81bff97153bfe3b9f377ca8 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -2075,14 +2075,57 @@ DeltaRational TheoryArith::getDeltaValueWithNonlinear(TNode n, bool& failed) {
   }
 }
 
+Rational TheoryArith::safeDeltaValueForDisequality(){
+  Rational min(2);
+  context::CDQueue<Constraint>::const_iterator iter = d_diseqQueue.begin();
+  context::CDQueue<Constraint>::const_iterator iter_end = d_diseqQueue.end(); 
+
+  for(; iter != iter_end; ++iter){
+    Constraint curr = *iter;
+    
+    ArithVar lhsVar = curr->getVariable();
+
+    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);
+
+      if(d < min){
+        min = d;
+      }
+    }
+  }
+
+  Assert(min.sgn() > 0);
+  Rational belowMin = min/Rational(2);  
+  return belowMin;
+}
+
 void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){
   AlwaysAssert(d_qflraStatus ==  Result::SAT);
   //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints");
 
   Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl;
 
+
   // Delta lasts at least the duration of the function call
-  const Rational& delta = d_partialModel.getDelta();
+  const Rational init = safeDeltaValueForDisequality();
+  const Rational& delta = d_partialModel.getDelta(init);
   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 da4a80208fdb33e9c52812a946885e7fe4538c00..754fa6521d352d09502ba3bd3a285082467bb342 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -335,6 +335,7 @@ public:
   void propagate(Effort e);
   Node explain(TNode n);
 
+  Rational safeDeltaValueForDisequality();
   void collectModelInfo( TheoryModel* m, bool fullModel );
 
   void shutdown(){ }

diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am
index 289569b1ab4fae8e5b99bfcef3d8f4d4920ff28b..f4797a28771e82e5e76fb9633ad311c562516dfa 100644 (file)
--- a/test/regress/regress0/uflra/Makefile.am
+++ b/test/regress/regress0/uflra/Makefile.am
@@ -35,8 +35,8 @@ SMT_TESTS = \
        incorrect1.smt \
        incorrect1.delta01.smt \
        incorrect1.delta02.smt 
-       error1.smt
-
+       error1.smt \
+       neq-deltacomp.smt
 # Regression tests for SMT2 inputs
 SMT2_TESTS =
 

diff --git a/test/regress/regress0/uflra/neq-deltacomp.smt b/test/regress/regress0/uflra/neq-deltacomp.smt
index 4144fcb79907eba48289bb704ab14893aa3053a1..9185a18c82fc8dd92116585e458f676f5253d9f0 100644 (file)
--- a/test/regress/regress0/uflra/neq-deltacomp.smt
+++ b/test/regress/regress0/uflra/neq-deltacomp.smt
@@ -3,7 +3,7 @@
 :extrafuns ((v2 Real))
 :extrafuns ((v1 Real))
 :extrafuns ((v0 Real))
-:status unknown
+:status sat
 :formula
 (let (?n1 (~ v1))
 (flet ($n2 (>= ?n1 v0))