Fixes to getValue for TheoryArith.

diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index a0f0247bee8c056f27f778f4da0ddfd597749606..bee24aa39f49c959d23c57df3b24a3a0a8de30a5 100644 (file)
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -250,27 +250,34 @@ void ArithPartialModel::printModel(ArithVar x){
   }
 }
 
+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(){
   Assert(!d_deltaIsSafe);
-  d_deltaIsSafe = true;
   d_delta = 1;
 
   for(ArithVar x = 0; x < d_mapSize; ++x){
-    if(hasBounds(x)){
+    const DeltaRational& a = getAssignment(x);
+    if(!d_lowerConstraint[x].isNull()){
       const DeltaRational& l = getLowerBound(x);
+      deltaIsSmallerThan(l,a);
+    }
+    if(!d_upperConstraint[x].isNull()){
       const DeltaRational& u = getUpperBound(x);
-      // c + k\ep <= d + h\ep
-      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;
-        }
-      }
+      deltaIsSmallerThan(a,u);
     }
   }
+  d_deltaIsSafe = true;
 }

diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 256a6b931d7a001f5c2b175400aff4741c027252..518d59fbd6eac2378d78a813f8c7dc10696cd7a5 100644 (file)
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -147,6 +147,7 @@ public:
 private:
 
   void computeDelta();
+  void deltaIsSmallerThan(const DeltaRational& l, const DeltaRational& u);
 
   /**
    * This function implements the mostly identical:

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6cf0d94146823dcdaf74fa11df09f5ae17b58295..9458ab153332a18e78385f3122b6b56ffbc69f5e 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -193,7 +193,13 @@ void TheoryArith::preRegisterTerm(TNode n) {
     d_out->augmentingLemma(eagerSplit);
   }
 
-  if(isTheoryLeaf(n)){
+  bool isStrictlyVarList = n.getKind() == kind::MULT && VarList::isMember(n);
+
+  if(isStrictlyVarList){
+    d_out->setIncomplete();
+  }
+
+  if(isTheoryLeaf(n) || isStrictlyVarList){
     ArithVar varN = requestArithVar(n,false);
     setupInitialValue(varN);
   }
@@ -935,8 +941,14 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
 
   switch(n.getKind()) {
   case kind::VARIABLE: {
-    DeltaRational drat = d_partialModel.getAssignment(asArithVar(n));
+    ArithVar var = asArithVar(n);
+    if(d_tableau.isEjected(var)){
+      reinjectVariable(var);
+    }
+
+    DeltaRational drat = d_partialModel.getAssignment(var);
     const Rational& delta = d_partialModel.getDelta();
+    Debug("getValue") << n << " " << drat << " " << delta << endl;
     return nodeManager->
       mkConst( drat.getNoninfinitesimalPart() +
                drat.getInfinitesimalPart() * delta );