diff options
author | Tim King <taking@cs.nyu.edu> | 2012-10-26 21:14:58 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-10-26 21:14:58 +0000 |
commit | 4ba0d73db87df39dd1f3d943ff5415b9f104d3e1 (patch) | |
tree | 49d12dad281cf171207bbf6d9503cab89b63aabe /src/theory/arith | |
parent | 080d8353c6d0704885c2e491122c8e337542b0e8 (diff) |
Fix for bug 430. d_delta in PartialModel was never being computed. (Delta remained at its initial non-sensical value of -1.) There was a problem with guarding d_delta with d_deltaIsSafe in PartialModel.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/partial_model.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 7e4a2daad..73e7943b0 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -91,6 +91,9 @@ void ArithPartialModel::initialize(ArithVar x, const DeltaRational& r){ ++d_mapSize; d_hasSafeAssignment.push_back( false ); + // Is wirth mentioning that this is not strictly necessary, but this maintains the internal invariant + // that when d_assignment is set this gets set. + d_deltaIsSafe = false; d_assignment.push_back( r ); d_safeAssignment.push_back( DeltaRational(0) ); @@ -146,6 +149,7 @@ void ArithPartialModel::setLowerBoundConstraint(Constraint c){ Assert(inMaps(x)); Assert(greaterThanLowerBound(x, c->getValue())); + d_deltaIsSafe = false; d_lbc.set(x, c); } @@ -159,6 +163,7 @@ void ArithPartialModel::setUpperBoundConstraint(Constraint c){ Assert(inMaps(x)); Assert(lessThanUpperBound(x, c->getValue())); + d_deltaIsSafe = false; d_ubc.set(x, c); } @@ -240,7 +245,7 @@ void ArithPartialModel::clearSafeAssignments(bool revert){ } if(revert && !d_history.empty()){ - d_deltaIsSafe = true; + d_deltaIsSafe = false; } d_history.clear(); |