diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-06 17:06:07 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-06 17:06:07 +0000 |
commit | 9da04b35ddb44761285af21519023d88f3adf1b5 (patch) | |
tree | 80c0b3315544727012e5b904099bcd663b6be686 /src/theory/arith/partial_model.cpp | |
parent | bcf15fb3ff5ec39f50187c157cf1f36daecb4763 (diff) |
Some assorted fixes and local optimizations for theory arith.
Diffstat (limited to 'src/theory/arith/partial_model.cpp')
-rw-r--r-- | src/theory/arith/partial_model.cpp | 52 |
1 files changed, 17 insertions, 35 deletions
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index d4be75559..bb2864cf9 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -44,19 +44,16 @@ void ArithPartialModel::setLowerBound(TNode x, const DeltaRational& 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()); - if(d_unsafeMode){ - Assert(x.hasAttribute(partial_model::SafeAssignment())); - 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); - } + 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; @@ -99,14 +96,14 @@ DeltaRational ArithPartialModel::getLowerBound(TNode x) const{ DeltaRational ArithPartialModel::getSafeAssignment(TNode x) const{ Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - if(d_unsafeMode){ - Assert( x.hasAttribute(partial_model::SafeAssignment())); - DeltaRational* safeAssignment = x.getAttribute(partial_model::SafeAssignment()); - if(safeAssignment != NULL){ - return *safeAssignment; - } + Assert( x.hasAttribute(SafeAssignment())); + + DeltaRational* safeAssignment = x.getAttribute(SafeAssignment()); + if(safeAssignment != NULL){ + return *safeAssignment; + }else{ + return getAssignment(x); //The current assignment is safe. } - return getAssignment(x); } const DeltaRational& ArithPartialModel::getAssignment(TNode x) const{ @@ -238,34 +235,19 @@ bool ArithPartialModel::assignmentIsConsistent(TNode x){ return above_li && below_ui; } -void ArithPartialModel::turnOnUnsafeMode(){ - Assert(!d_unsafeMode); - Assert(d_history.empty()); - - d_unsafeMode = true; -} - -void ArithPartialModel::turnOffUnsafeMode(){ - Assert(d_unsafeMode); - Assert(d_history.empty()); - - d_unsafeMode = false; -} void ArithPartialModel::clearSafeAssignments(bool revert){ - Assert(d_unsafeMode); for(HistoryList::iterator i = d_history.begin(); i != d_history.end(); ++i){ TNode x = *i; - Assert(x.hasAttribute(partial_model::SafeAssignment())); + Assert(x.hasAttribute(SafeAssignment())); + Assert(x.hasAttribute(Assignment())); - DeltaRational* safeAssignment = x.getAttribute(partial_model::SafeAssignment()); + DeltaRational* safeAssignment = x.getAttribute(SafeAssignment()); if(revert){ - Assert(x.hasAttribute(partial_model::Assignment())); - - DeltaRational* assign = x.getAttribute(partial_model::Assignment()); + DeltaRational* assign = x.getAttribute(Assignment()); *assign = *safeAssignment; } x.setAttribute(partial_model::SafeAssignment(), NULL); |