This commit merges the decaying-rows branch into the main trunk.

1 files changed, 36 insertions, 0 deletions

diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index e7e3f8bc2..bd2d5d61e 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -32,6 +32,7 @@ void ArithPartialModel::setUpperBound(TNode x, const DeltaRational& r){
   Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
 
   Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl;
+  x.setAttribute(partial_model::HasHadABound(), true);
 
   d_UpperBoundMap[x] = r;
 }
@@ -39,6 +40,8 @@ void ArithPartialModel::setUpperBound(TNode x, const DeltaRational& 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);
+
   d_LowerBoundMap[x] = r;
 }
 
@@ -60,6 +63,33 @@ void ArithPartialModel::setAssignment(TNode x, const DeltaRational& r){
   Debug("partial_model") << "pm: updating the assignment to" << x
                          << " now " << r <<endl;
 }
+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());
+
+  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;
+}
 
 void ArithPartialModel::initialize(TNode x, const DeltaRational& r){
    Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE);
@@ -200,6 +230,12 @@ bool ArithPartialModel::aboveUpperBound(TNode x, const DeltaRational& c, bool st
   }
 }
 
+bool ArithPartialModel::hasBounds(TNode x){
+  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));