Fixed computation of infinitesimals for arithmetic model generation.

3 files changed, 44 insertions, 278 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;
+        }
+      }
+    }
+  }
 }
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index bec703369..256a6b931 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -34,90 +34,6 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-namespace partial_model {
-// struct DeltaRationalCleanupStrategy{
-//   static void cleanup(DeltaRational* dq){
-//     Debug("arithgc") << "cleaning up  " << dq << "\n";
-//     if(dq != NULL){
-//       delete dq;
-//     }
-//   }
-// };
-
-
-// struct AssignmentAttrID {};
-// typedef expr::Attribute<AssignmentAttrID,
-//                         DeltaRational*,
-//                         DeltaRationalCleanupStrategy> Assignment;
-
-
-// struct SafeAssignmentAttrID {};
-// typedef expr::Attribute<SafeAssignmentAttrID,
-//                         DeltaRational*,
-//                         DeltaRationalCleanupStrategy> SafeAssignment;
-
-
-
-/**
- * This defines a context dependent delta rational map.
- * This is used to keep track of the current lower and upper bounds on
- * each variable.  This information is conext dependent.
- */
-//typedef context::CDMap<TNode, DeltaRational, TNodeHashFunction> CDDRationalMap;
-/* Side disucssion for why new tables are introduced instead of using the
- * attribute framework.
- * It comes down to that the obvious ways to use the current attribute
- * framework do not provide a terribly satisfying answer.
- * - Suppose the type of the attribute is CD and maps to type DeltaRational.
- *   Well it can't map to a DeltaRational, and it thus it will be a
- *   DeltaRational*
- *   However being context dependent means givening up cleanup functions.
- *   So this leaks memory.
- * - Suppose the type of the attribute is CD and the type mapped to
- *   was a Node wrapping a CONST_DELTA_RATIONAL.
- *   This was rejected for inefficiency, and uglyness.
- *   Inefficiency: Every lookup and comparison will require going through the
- *   massaging in between a node and the constant being wrapped. Every update
- *   requires going through the additional expense of creating at least 1 node.
- *   The Uglyness: If this was chosen it would also suggest using comparisons
- *   against DeltaRationals for the tracking the constraints for conflict
- *   analysis. This seems to invite misuse and introducing Nodes that should
- *   probably not escape arith.
- * - Suppose that the of the attribute was not CD and mapped to a
- *   CDO<DeltaRational*> or similarly a ContextObj that wraps a DeltaRational*.
- *   This is currently rejected just because this is difficult to get right,
- *   and maintain. However with enough effort this the best solution is
- *   probably of this form.
- */
-
-
-/**
- * This is the literal that was asserted in the current context to the theory
- * that asserted the tightest lower bound on a variable.
- * For example: for a variable x this could be the constraint
- *    (>= x 4) or (not (<= x 50))
- * Note the strong correspondence between this and LowerBoundMap.
- * This is used during conflict analysis.
- */
-// struct LowerConstraintAttrID {};
-// typedef expr::CDAttribute<LowerConstraintAttrID,TNode> LowerConstraint;
-
-/**
- * See the documentation for LowerConstraint.
- */
-// struct UpperConstraintAttrID {};
-// typedef expr::CDAttribute<UpperConstraintAttrID,TNode> UpperConstraint;
-
-// struct TheoryArithPropagatedID {};
-// typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated;
-
-// struct HasHadABoundID {};
-// typedef expr::Attribute<HasHadABoundID, bool> HasHadABound;
-
-}; /*namespace partial_model*/
-
-
-
 class ArithPartialModel {
 private:
 
@@ -135,6 +51,8 @@ private:
   context::CDVector<TNode> d_upperConstraint;
   context::CDVector<TNode> d_lowerConstraint;
 
+  bool d_deltaIsSafe;
+  Rational d_delta;
 
   /**
    * List contains all of the variables that have an unsafe assignment.
@@ -154,6 +72,8 @@ public:
     d_lowerBound(c, false),
     d_upperConstraint(c,false),
     d_lowerConstraint(c,false),
+    d_deltaIsSafe(false),
+    d_delta(-1,1),
     d_history()
   { }
 
@@ -163,7 +83,6 @@ public:
   TNode getUpperConstraint(ArithVar x);
 
 
-
   /* Initializes a variable to a safe value.*/
   void initialize(ArithVar x, const DeltaRational& r);
 
@@ -211,14 +130,24 @@ public:
 
   void printModel(ArithVar x);
 
+  /** returns true iff x has both a lower and upper bound. */
   bool hasBounds(ArithVar x);
 
   bool hasEverHadABound(ArithVar var){
     return d_hasHadABound[var];
   }
 
+  const Rational& getDelta(){
+    if(!d_deltaIsSafe){
+      computeDelta();
+    }
+    return d_delta;
+  }
+
 private:
 
+  void computeDelta();
+
   /**
    * This function implements the mostly identical:
    * revertAssignmentChanges() and commitAssignmentChanges().
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 4a783a6a4..6cf0d9414 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -936,10 +936,10 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
   switch(n.getKind()) {
   case kind::VARIABLE: {
     DeltaRational drat = d_partialModel.getAssignment(asArithVar(n));
-    // FIXME our infinitesimal is fixed here at 1e-06
+    const Rational& delta = d_partialModel.getDelta();
     return nodeManager->
       mkConst( drat.getNoninfinitesimalPart() +
-               drat.getInfinitesimalPart() * Rational(1, 1000000) );
+               drat.getInfinitesimalPart() * delta );
   }
 
   case kind::EQUAL: // 2 args