branches/arith-indexed-variables merged into the main trunk.

1 files changed, 284 insertions, 171 deletions

diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 18993c748..6f0ded9e5 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -28,267 +28,368 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 using namespace CVC4::theory::arith::partial_model;
 
-void ArithPartialModel::setUpperBound(TNode x, const DeltaRational& r){
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+void ArithPartialModel::setUpperBound(ArithVar x, const DeltaRational& r){
+  //Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
   Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl;
-  x.setAttribute(partial_model::HasHadABound(), true);
+  //x.setAttribute(partial_model::HasHadABound(), true);
+  d_hasHadABound[x] = true;
 
-  d_UpperBoundMap[x] = r;
+  d_upperBound.set(x,r);
 }
 
-void ArithPartialModel::setLowerBound(TNode x, const DeltaRational& r){
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-  Debug("partial_model") << "setLowerBound(" << x << "," << r << ")" << endl;
-  x.setAttribute(partial_model::HasHadABound(), true);
+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_LowerBoundMap[x] = r;
+//   d_LowerBoundMap[x] = r;
+  d_hasHadABound[x] = true;
+  d_lowerBound.set(x,r);
 }
 
-void ArithPartialModel::setAssignment(TNode 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);
+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]){
+    d_safeAssignment[x] = d_assignment[x];
+    d_hasSafeAssignment[x] = true;
     d_history.push_back(x);
   }
-
-  *curr = r;
-  Debug("partial_model") << "pm: updating the assignment to" << x
-                         << " now " << r <<endl;
+  d_assignment[x] = r;
 }
-void ArithPartialModel::setAssignment(TNode 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());
-
+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){
-    if(saved != NULL){
-      x.setAttribute(partial_model::SafeAssignment(), NULL);
-      delete saved;
-    }
+    d_hasSafeAssignment[x] = false;
   }else{
-    if(saved == NULL){
-      saved = new DeltaRational(safe);
-      x.setAttribute(partial_model::SafeAssignment(), saved);
-    }else{
-      *saved = safe;
+    d_safeAssignment[x] = safe;
+
+    if(!d_hasSafeAssignment[x]){
+      d_hasSafeAssignment[x] = true;
+      d_history.push_back(x);
     }
-    d_history.push_back(x);
   }
-  *curr = r;
+  d_assignment[x] = r;
+}
 
-  Debug("partial_model") << "pm: updating the assignment to" << x
-                         << " now " << r <<endl;
+bool ArithPartialModel::equalSizes(){
+  return d_mapSize == d_hasHadABound.size() &&
+    d_mapSize == d_hasSafeAssignment.size() &&
+    d_mapSize == d_assignment.size() &&
+    d_mapSize == d_safeAssignment.size() &&
+    d_mapSize == d_upperBound.size() &&
+    d_mapSize == d_lowerBound.size() &&
+    d_mapSize == d_upperConstraint.size() &&
+    d_mapSize == d_lowerConstraint.size();
 }
 
-void ArithPartialModel::initialize(TNode x, const DeltaRational& r){
-   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+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.hasAttribute(partial_model::Assignment()));
-   Assert(!x.hasAttribute(partial_model::SafeAssignment()));
+  Assert(x == d_mapSize);
+  Assert(equalSizes());
+  ++d_mapSize;
 
-   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;
+  d_hasHadABound.push_back( false );
+
+  d_hasSafeAssignment.push_back( false );
+  d_assignment.push_back( r );
+  d_safeAssignment.push_back( DeltaRational(0) );
+
+  d_upperBound.push_back( DeltaRational(0) );
+  d_lowerBound.push_back( DeltaRational(0) );
+
+  d_upperConstraint.push_back( TNode::null() );
+  d_lowerConstraint.push_back( TNode::null() );
 }
 
 /** Must know that the bound exists both calling this! */
-DeltaRational ArithPartialModel::getUpperBound(TNode x) const {
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+const DeltaRational& ArithPartialModel::getUpperBound(ArithVar x) {
+  Assert(inMaps(x));
+  Assert(!d_upperConstraint[x].isNull());
 
-  CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
-  Assert(i != d_UpperBoundMap.end());
+  return d_upperBound[x];
 
-  return DeltaRational((*i).second);
+//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+
+//   CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
+//   Assert(i != d_UpperBoundMap.end());
+
+//   return DeltaRational((*i).second);
 }
 
-DeltaRational ArithPartialModel::getLowerBound(TNode x) const{
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+const DeltaRational& ArithPartialModel::getLowerBound(ArithVar x) {
+  Assert(inMaps(x));
+  Assert(!d_lowerConstraint[x].isNull());
 
-  CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
-  Assert(i != d_LowerBoundMap.end());
+  return d_lowerBound[x];
 
-  return DeltaRational((*i).second);
-}
+//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
-DeltaRational ArithPartialModel::getSafeAssignment(TNode x) const{
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-  Assert( x.hasAttribute(SafeAssignment()));
+//   CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
+//   Assert(i != d_LowerBoundMap.end());
 
-  DeltaRational* safeAssignment = x.getAttribute(SafeAssignment());
-  if(safeAssignment != NULL){
-    return *safeAssignment;
+//   return DeltaRational((*i).second);
+}
+
+const DeltaRational& ArithPartialModel::getSafeAssignment(ArithVar x) const{
+  Assert(inMaps(x));
+  if(d_hasSafeAssignment[x]){
+    return d_safeAssignment[x];
   }else{
-    return getAssignment(x); //The current assignment is safe.
+    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(TNode x) const{
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+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;
+//   DeltaRational* assign;
+//   AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+//   return *assign;
+  Assert(inMaps(x));
+  return d_assignment[x];
 }
 
 
 
-void ArithPartialModel::setLowerConstraint(TNode x, TNode constraint){
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+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);
-}
+//   x.setAttribute(partial_model::LowerConstraint(),constraint);
 
-void ArithPartialModel::setUpperConstraint(TNode x, TNode constraint){
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+  Assert(inMaps(x));
+  d_lowerConstraint.set(x,constraint);
 
-  Debug("partial_model") << "setUpperConstraint("
-                         << x << ":" << constraint << ")" << endl;
-
-  x.setAttribute(partial_model::UpperConstraint(),constraint);
 }
 
-TNode ArithPartialModel::getLowerConstraint(TNode x){
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
-
-  TNode ret;
-  AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret));
-  return ret;
-}
+void ArithPartialModel::setUpperConstraint(ArithVar x, TNode constraint){
+//   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
-TNode ArithPartialModel::getUpperConstraint(TNode x){
-  Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
+  Debug("partial_model") << "setUpperConstraint("
+                         << x << ":" << constraint << ")" << endl;
 
-  TNode ret;
-  AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret));
-  return ret;
+//   x.setAttribute(partial_model::UpperConstraint(),constraint);
+  Assert(inMaps(x));
+  d_upperConstraint.set(x, constraint);
 }
 
-// TNode CVC4::theory::arith::getLowerConstraint(TNode x){
+TNode ArithPartialModel::getLowerConstraint(ArithVar x){
 //   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
 //   TNode ret;
 //   AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret));
 //   return ret;
-// }
 
-// TNode CVC4::theory::arith::getUpperConstraint(TNode x){
+  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];
+}
 
 
-bool ArithPartialModel::belowLowerBound(TNode x, const DeltaRational& c, bool strict){
-  CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
-  if(i == d_LowerBoundMap.end()){
+
+bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){
+  if(d_lowerConstraint[x].isNull()){
     // l = -\intfy
     // ? c < -\infty |-  _|_
     return false;
   }
-
-  const DeltaRational& l = (*i).second;
-
   if(strict){
-    return c < l;
+    return c < d_lowerBound[x];
   }else{
-    return c <= l;
+    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(TNode x, const DeltaRational& c, bool strict){
-  CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
-  if(i == d_UpperBoundMap.end()){
-    // u = -\intfy
-    // ? u < -\infty |-  _|_
+bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){
+  if(d_upperConstraint[x].isNull()){
+    // u = \intfy
+    // ? c > \infty |-  _|_
     return false;
   }
-  const DeltaRational& u = (*i).second;
-
   if(strict){
-    return c > u;
+    return c > d_upperBound[x];
   }else{
-    return c >= u;
+    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(TNode x){
+bool ArithPartialModel::hasBounds(ArithVar x){
   return
-    d_UpperBoundMap.find(x) != d_UpperBoundMap.end() ||
-    d_LowerBoundMap.find(x) != d_LowerBoundMap.end();
+    !d_lowerConstraint[x].isNull() || !d_upperConstraint[x].isNull();
+  // return
+//     d_UpperBoundMap.find(x) != d_UpperBoundMap.end() ||
+//     d_LowerBoundMap.find(x) != d_LowerBoundMap.end();
 }
 
-bool ArithPartialModel::strictlyBelowUpperBound(TNode x){
-  DeltaRational* assign;
-  AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
-
-  CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
-  if(i == d_UpperBoundMap.end()){// u = \infty
+bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x){
+  Assert(inMaps(x));
+  if(d_upperConstraint[x].isNull()){ // u = \infty
     return true;
   }
+  return d_assignment[x] < d_upperBound[x];
+//   DeltaRational* assign;
+//   AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
 
-  const DeltaRational& u = (*i).second;
-  return (*assign) < u;
-}
+//   CDDRationalMap::iterator i = d_UpperBoundMap.find(x);
+//   if(i == d_UpperBoundMap.end()){// u = \infty
+//     return true;
+//   }
 
-bool ArithPartialModel::strictlyAboveLowerBound(TNode x){
-  DeltaRational* assign;
-  AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
+//   const DeltaRational& u = (*i).second;
+//   return (*assign) < u;
+}
 
-  CDDRationalMap::iterator i = d_LowerBoundMap.find(x);
-  if(i == d_LowerBoundMap.end()){// l = \infty
+bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){
+  Assert(inMaps(x));
+  if(d_lowerConstraint[x].isNull()){ // l = -\infty
     return true;
   }
+  return  d_lowerBound[x] < d_assignment[x];
+
+//   DeltaRational* assign;
+//   AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign));
 
-  const DeltaRational& l = (*i).second;
-  return l < *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(TNode x){
+bool ArithPartialModel::assignmentIsConsistent(ArithVar x){
   const DeltaRational& beta = getAssignment(x);
 
-  bool above_li = !belowLowerBound(x,beta,true);
-  bool below_ui = !aboveUpperBound(x,beta,true);
-
   //l_i <= beta(x_i) <= u_i
-  return  above_li && below_ui;
+  return  !belowLowerBound(x,beta,true) && !aboveUpperBound(x,beta,true);
 }
 
 
 void ArithPartialModel::clearSafeAssignments(bool revert){
 
   for(HistoryList::iterator i = d_history.begin(); i != d_history.end(); ++i){
-    TNode x = *i;
-
-    Assert(x.hasAttribute(SafeAssignment()));
-    Assert(x.hasAttribute(Assignment()));
-
-    DeltaRational* safeAssignment = x.getAttribute(SafeAssignment());
+    ArithVar x = *i;
+    Assert(d_hasSafeAssignment[x]);
+    d_hasSafeAssignment[x] = false;
 
     if(revert){
-      DeltaRational* assign = x.getAttribute(Assignment());
-      *assign = *safeAssignment;
+      d_assignment[x] = d_safeAssignment[x];
     }
-    x.setAttribute(partial_model::SafeAssignment(), NULL);
-    delete safeAssignment;
+//     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();
@@ -301,26 +402,38 @@ void ArithPartialModel::commitAssignmentChanges(){
   clearSafeAssignments(false);
 }
 
-void ArithPartialModel::printModel(TNode x){
-
+void ArithPartialModel::printModel(ArithVar 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{
+  if(d_lowerConstraint[x].isNull()){
     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") << getLowerBound(x) << " ";
+    Debug("model") << getLowerConstraint(x) << " ";
+  }
+  if(d_upperConstraint[x].isNull()){
     Debug("model") << "no ub ";
+  }else{
+    Debug("model") << getUpperBound(x) << " ";
+    Debug("model") << getUpperConstraint(x) << " ";
   }
-  Debug("model") << endl;
+//   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;
 }