Fixed computation of infinitesimals for arithmetic model generation.

1 files changed, 28 insertions, 191 deletions

diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 6f0ded9e5..a0f0247be 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -26,43 +26,23 @@ using namespace std;
 using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
-using namespace CVC4::theory::arith::partial_model;
 
 void ArithPartialModel::setUpperBound(ArithVar x, const DeltaRational& r){
-  //Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+  d_deltaIsSafe = false;
 
   Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl;
-  //x.setAttribute(partial_model::HasHadABound(), true);
   d_hasHadABound[x] = true;
-
   d_upperBound.set(x,r);
 }
 
 void ArithPartialModel::setLowerBound(ArithVar x, const DeltaRational& r){
-  //Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-  // Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl;
-//   x.setAttribute(partial_model::HasHadABound(), true);
+  d_deltaIsSafe = false;
 
-//   d_LowerBoundMap[x] = r;
   d_hasHadABound[x] = true;
   d_lowerBound.set(x,r);
 }
 
 void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& r){
-  //Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-  //Assert(x.hasAttribute(partial_model::Assignment()));
-  //Assert(x.hasAttribute(partial_model::SafeAssignment()));
-
-//   DeltaRational* curr = x.getAttribute(partial_model::Assignment());
-
-//   DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment());
-//   if(saved == NULL){
-//     saved = new DeltaRational(*curr);
-//     x.setAttribute(partial_model::SafeAssignment(), saved);
-//     d_history.push_back(x);
-//   }
-
-//   *curr = r;
    Debug("partial_model") << "pm: updating the assignment to" << x
                           << " now " << r <<endl;
   if(!d_hasSafeAssignment[x]){
@@ -73,31 +53,6 @@ void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& r){
   d_assignment[x] = r;
 }
 void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){
-  // Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-//   Assert(x.hasAttribute(partial_model::Assignment()));
-//   Assert(x.hasAttribute(partial_model::SafeAssignment()));
-
-//   DeltaRational* curr = x.getAttribute(partial_model::Assignment());
-//   DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment());
-
-
-
-//   if(safe == r){
-//     if(saved != NULL){
-//       x.setAttribute(partial_model::SafeAssignment(), NULL);
-//       delete saved;
-//     }
-//   }else{
-//     if(saved == NULL){
-//       saved = new DeltaRational(safe);
-//       x.setAttribute(partial_model::SafeAssignment(), saved);
-//     }else{
-//       *saved = safe;
-//     }
-//     d_history.push_back(x);
-//   }
-//   *curr = r;
-
    Debug("partial_model") << "pm: updating the assignment to" << x
                           << " now " << r <<endl;
   if(safe == r){
@@ -125,18 +80,6 @@ bool ArithPartialModel::equalSizes(){
 }
 
 void ArithPartialModel::initialize(ArithVar x, const DeltaRational& r){
-//    Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
-//    Assert(!x.hasAttribute(partial_model::Assignment()));
-//    Assert(!x.hasAttribute(partial_model::SafeAssignment()));
-
-//    DeltaRational* c = new DeltaRational(r);
-//    x.setAttribute(partial_model::Assignment(), c);
-//    x.setAttribute(partial_model::SafeAssignment(), NULL);
-
-//    Debug("partial_model") << "pm: constructing an assignment for " << x
-//                           << " initially " << (*c) <<endl;
-
   Assert(x == d_mapSize);
   Assert(equalSizes());
   ++d_mapSize;
@@ -161,13 +104,6 @@ const DeltaRational& ArithPartialModel::getUpperBound(ArithVar x) {
   Assert(!d_upperConstraint[x].isNull());
 
   return d_upperBound[x];
-
-//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
-//   CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
-//   Assert(i != d_UpperBoundMap.end());
-
-//   return DeltaRational((*i).second);
 }
 
 const DeltaRational& ArithPartialModel::getLowerBound(ArithVar x) {
@@ -175,13 +111,6 @@ const DeltaRational& ArithPartialModel::getLowerBound(ArithVar x) {
   Assert(!d_lowerConstraint[x].isNull());
 
   return d_lowerBound[x];
-
-//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
-//   CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
-//   Assert(i != d_LowerBoundMap.end());
-
-//   return DeltaRational((*i).second);
 }
 
 const DeltaRational& ArithPartialModel::getSafeAssignment(ArithVar x) const{
@@ -191,23 +120,9 @@ const DeltaRational& ArithPartialModel::getSafeAssignment(ArithVar x) const{
   }else{
     return d_assignment[x];
   }
-//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-//   Assert( x.hasAttribute(SafeAssignment()));
-
-//   DeltaRational* safeAssignment = x.getAttribute(SafeAssignment());
-//   if(safeAssignment != NULL){
-//     return *safeAssignment;
-//   }else{
-//     return getAssignment(x); //The current assignment is safe.
-//   }
 }
 
 const DeltaRational& ArithPartialModel::getAssignment(ArithVar x) const{
-//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
-//   DeltaRational* assign;
-//   AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
-//   return *assign;
   Assert(inMaps(x));
   return d_assignment[x];
 }
@@ -215,47 +130,27 @@ const DeltaRational& ArithPartialModel::getAssignment(ArithVar x) const{
 
 
 void ArithPartialModel::setLowerConstraint(ArithVar x, TNode constraint){
-//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
   Debug("partial_model") << "setLowerConstraint("
                          << x << ":" << constraint << ")" << endl;
-
-//   x.setAttribute(partial_model::LowerConstraint(),constraint);
-
   Assert(inMaps(x));
   d_lowerConstraint.set(x,constraint);
 
 }
 
 void ArithPartialModel::setUpperConstraint(ArithVar x, TNode constraint){
-//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
   Debug("partial_model") << "setUpperConstraint("
                          << x << ":" << constraint << ")" << endl;
-
-//   x.setAttribute(partial_model::UpperConstraint(),constraint);
   Assert(inMaps(x));
   d_upperConstraint.set(x, constraint);
 }
 
 TNode ArithPartialModel::getLowerConstraint(ArithVar x){
-//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
-//   TNode ret;
-//   AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret));
-//   return ret;
-
   Assert(inMaps(x));
   Assert(!d_lowerConstraint[x].isNull());
   return d_lowerConstraint[x];
 }
 
 TNode ArithPartialModel::getUpperConstraint(ArithVar x){
-//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
-//   TNode ret;
-//   AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret));
-//   return ret;
   Assert(inMaps(x));
   Assert(!d_upperConstraint[x].isNull());
   return d_upperConstraint[x];
@@ -274,20 +169,6 @@ bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool
   }else{
     return c <= d_lowerBound[x];
   }
-//   CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
-//   if(i == d_LowerBoundMap.end()){
-//     // l = -\intfy
-//     // ? c < -\infty |-  _|_
-//     return false;
-//   }
-
-//   const DeltaRational& l = (*i).second;
-
-//   if(strict){
-//     return c < l;
-//   }else{
-//     return c <= l;
-//   }
 }
 
 bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){
@@ -301,27 +182,10 @@ bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool
   }else{
     return c >= d_upperBound[x];
   }
-//   CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
-//   if(i == d_UpperBoundMap.end()){
-//     // u = -\intfy
-//     // ? u < -\infty |-  _|_
-//     return false;
-//   }
-//   const DeltaRational& u = (*i).second;
-
-//   if(strict){
-//     return c > u;
-//   }else{
-//     return c >= u;
-//   }
 }
 
 bool ArithPartialModel::hasBounds(ArithVar x){
-  return
-    !d_lowerConstraint[x].isNull() || !d_upperConstraint[x].isNull();
-  // return
-//     d_UpperBoundMap.find(x) != d_UpperBoundMap.end() ||
-//     d_LowerBoundMap.find(x) != d_LowerBoundMap.end();
+  return !d_lowerConstraint[x].isNull() || !d_upperConstraint[x].isNull();
 }
 
 bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x){
@@ -330,16 +194,6 @@ bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x){
     return true;
   }
   return d_assignment[x] < d_upperBound[x];
-//   DeltaRational* assign;
-//   AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
-
-//   CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
-//   if(i == d_UpperBoundMap.end()){// u = \infty
-//     return true;
-//   }
-
-//   const DeltaRational& u = (*i).second;
-//   return (*assign) < u;
 }
 
 bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){
@@ -348,17 +202,6 @@ bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){
     return true;
   }
   return  d_lowerBound[x] < d_assignment[x];
-
-//   DeltaRational* assign;
-//   AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
-
-//   CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
-//   if(i == d_LowerBoundMap.end()){// l = \infty
-//     return true;
-//   }
-
-//   const DeltaRational& l = (*i).second;
-//   return l < *assign;
 }
 
 bool ArithPartialModel::assignmentIsConsistent(ArithVar x){
@@ -379,17 +222,6 @@ void ArithPartialModel::clearSafeAssignments(bool revert){
     if(revert){
       d_assignment[x] = d_safeAssignment[x];
     }
-//     Assert(x.hasAttribute(SafeAssignment()));
-//     Assert(x.hasAttribute(Assignment()));
-
-//     DeltaRational* safeAssignment = x.getAttribute(SafeAssignment());
-
-//     if(revert){
-//       DeltaRational* assign = x.getAttribute(Assignment());
-//       *assign = *safeAssignment;
-//     }
-//     x.setAttribute(partial_model::SafeAssignment(), NULL);
-//     delete safeAssignment;
   }
 
   d_history.clear();
@@ -416,24 +248,29 @@ void ArithPartialModel::printModel(ArithVar x){
     Debug("model") << getUpperBound(x) << " ";
     Debug("model") << getUpperConstraint(x) << " ";
   }
-//   Debug("model") << "model" << x << ":"<< getAssignment(x) << " ";
-
-//   CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
-//   if(i != d_LowerBoundMap.end()){
-//     DeltaRational l = (*i).second;
-//     Debug("model") << l << " ";
-//     Debug("model") << getLowerConstraint(x) << " ";
-//   }else{
-//     Debug("model") << "no lb ";
-//   }
-
-//   i = d_UpperBoundMap.find(x);
-//   if(i != d_UpperBoundMap.end()){
-//     DeltaRational u = (*i).second;
-//     Debug("model") << u << " ";
-//     Debug("model") << getUpperConstraint(x) << " ";
-//   }else{
-//     Debug("model") << "no ub ";
-//   }
-//   Debug("model") << endl;
+}
+
+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& l = getLowerBound(x);
+      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;
+        }
+      }
+    }
+  }
 }