diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-29 22:01:30 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-29 22:01:30 +0000 |
commit | b1200db566d19132a3f0861eeef35f3c0aaa0a08 (patch) | |
tree | 9d7855232f833230ca5d92cb8948e5b894dff197 /src/theory/arith/partial_model.cpp | |
parent | 200a0b748085004595a948fdea7c73a5ab45bdcf (diff) |
This commit merges the decaying-rows branch into the main trunk.
Diffstat (limited to 'src/theory/arith/partial_model.cpp')
-rw-r--r-- | src/theory/arith/partial_model.cpp | 36 |
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)); |