From 8b5686a7dd0b559356e9e3bf76be93ad9c726085 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Sat, 10 Nov 2012 19:01:49 +0000
Subject: [PATCH] Fix for bug 439. Delta computation now includes disequality
 information.

---
 src/theory/arith/partial_model.cpp            |  4 +-
 src/theory/arith/partial_model.h              |  9 ++--
 src/theory/arith/theory_arith.cpp             | 45 ++++++++++++++++++-
 src/theory/arith/theory_arith.h               |  1 +
 test/regress/regress0/uflra/Makefile.am       |  4 +-
 test/regress/regress0/uflra/neq-deltacomp.smt |  2 +-
 6 files changed, 56 insertions(+), 9 deletions(-)

diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 73e7943b0..edba437ab 100644
--- 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 83e2a4f2b..bcc65b85d 100644
--- 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 4ce1113a4..b342c9271 100644
--- 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 da4a80208..754fa6521 100644
--- 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 289569b1a..f4797a287 100644
--- 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 4144fcb79..9185a18c8 100644
--- 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))
-- 
2.30.2