diff options
Diffstat (limited to 'src/theory/arith/partial_model.cpp')
-rw-r--r-- | src/theory/arith/partial_model.cpp | 549 |
1 files changed, 407 insertions, 142 deletions
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 6bbaa1e5e..695d9df25 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -19,6 +19,7 @@ #include "theory/arith/partial_model.h" #include "util/output.h" #include "theory/arith/constraint.h" +#include "theory/arith/normal_form.h" using namespace std; @@ -26,21 +27,164 @@ namespace CVC4 { namespace theory { namespace arith { -ArithPartialModel::ArithPartialModel(context::Context* c, RationalCallBack& deltaComputingFunc) - : d_mapSize(0), - d_hasSafeAssignment(), - d_assignment(), +ArithVariables::ArithVariables(context::Context* c, DeltaComputeCallback deltaComputingFunc) + : d_vars(), d_safeAssignment(), - d_ubc(c), - d_lbc(c), + d_numberOfVariables(0), + d_pool(), + d_released(), + d_releasedIterator(d_released.begin()), + d_nodeToArithVarMap(), + d_lbRevertHistory(c, true, LowerBoundCleanUp(this)), + d_ubRevertHistory(c, true, UpperBoundCleanUp(this)), d_deltaIsSafe(false), d_delta(-1,1), d_deltaComputingFunc(deltaComputingFunc), - d_history() + d_enqueueingBoundCounts(true) { } +ArithVariables::VarInfo::VarInfo() + : d_var(ARITHVAR_SENTINEL), + d_assignment(0), + d_lb(NullConstraint), + d_ub(NullConstraint), + d_cmpAssignmentLB(1), + d_cmpAssignmentUB(-1), + d_pushCount(0), + d_node(Node::null()), + d_slack(false) +{ } + +void ArithVariables::VarInfo::initialize(ArithVar v, Node n, bool slack){ + Assert(!initialized()); + Assert(d_lb == NullConstraint); + Assert(d_ub == NullConstraint); + Assert(d_cmpAssignmentLB > 0); + Assert(d_cmpAssignmentUB < 0); + d_var = v; + d_node = n; + d_slack = slack; + + if(d_slack){ + //The type computation is not quite accurate for Rationals that are + //integral. + //We'll use the isIntegral check from the polynomial package instead. + Polynomial p = Polynomial::parsePolynomial(n); + d_type = p.isIntegral() ? ATInteger : ATReal; + }else{ + d_type = nodeToArithType(n); + } + + Assert(initialized()); +} +void ArithVariables::VarInfo::uninitialize(){ + d_var = ARITHVAR_SENTINEL; + d_node = Node::null(); +} + +bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundCounts & prev){ + Assert(initialized()); + d_assignment = a; + int cmpUB = (d_ub == NullConstraint) ? -1 : + d_assignment.cmp(d_ub->getValue()); + + int cmpLB = (d_lb == NullConstraint) ? 1 : + d_assignment.cmp(d_lb->getValue()); + + bool lbChanged = cmpLB != d_cmpAssignmentLB && + (cmpLB == 0 || d_cmpAssignmentLB == 0); + bool ubChanged = cmpUB != d_cmpAssignmentUB && + (cmpUB == 0 || d_cmpAssignmentUB == 0); + + if(lbChanged || ubChanged){ + prev = boundCounts(); + } + + d_cmpAssignmentUB = cmpUB; + d_cmpAssignmentLB = cmpLB; + return lbChanged || ubChanged; +} + +void ArithVariables::releaseArithVar(ArithVar v){ + VarInfo& vi = d_vars.get(v); + vi.uninitialize(); + + if(d_safeAssignment.isKey(v)){ + d_safeAssignment.remove(v); + } + if(vi.canBeReclaimed()){ + d_pool.push_back(v); + }else{ + d_released.push_back(v); + } +} + +bool ArithVariables::VarInfo::setUpperBound(Constraint ub, BoundCounts& prev){ + Assert(initialized()); + d_ub = ub; + int cmpUB = (d_ub == NullConstraint) ? -1 : d_assignment.cmp(d_ub->getValue()); + bool ubChanged = cmpUB != d_cmpAssignmentUB && + (cmpUB == 0 || d_cmpAssignmentUB == 0); + if(ubChanged){ + prev = boundCounts(); + } + d_cmpAssignmentUB = cmpUB; + return ubChanged; +} -const Rational& ArithPartialModel::getDelta(){ +bool ArithVariables::VarInfo::setLowerBound(Constraint lb, BoundCounts& prev){ + Assert(initialized()); + d_lb = lb; + int cmpLB = (d_lb == NullConstraint) ? 1 : d_assignment.cmp(d_lb->getValue()); + + bool lbChanged = cmpLB != d_cmpAssignmentLB && + (cmpLB == 0 || d_cmpAssignmentLB == 0); + if(lbChanged){ + prev = boundCounts(); + } + d_cmpAssignmentLB = cmpLB; + return lbChanged; +} + +void ArithVariables::attemptToReclaimReleased(){ + std::list<ArithVar>::iterator i_end = d_released.end(); + for(int iter = 0; iter < 20 && d_releasedIterator != i_end; ++d_releasedIterator){ + ArithVar v = *d_releasedIterator; + VarInfo& vi = d_vars.get(v); + if(vi.canBeReclaimed()){ + d_pool.push_back(v); + std::list<ArithVar>::iterator curr = d_releasedIterator; + ++d_releasedIterator; + d_released.erase(curr); + }else{ + ++d_releasedIterator; + } + } + if(d_releasedIterator == i_end){ + d_releasedIterator = d_released.begin(); + } +} + +ArithVar ArithVariables::allocateVariable(){ + if(d_pool.empty()){ + attemptToReclaimReleased(); + } + bool reclaim = !d_pool.empty(); + + ArithVar varX; + if(reclaim){ + varX = d_pool.back(); + d_pool.pop_back(); + }else{ + varX = d_numberOfVariables; + ++d_numberOfVariables; + } + d_vars.set(varX, VarInfo()); + return varX; +} + + +const Rational& ArithVariables::getDelta(){ if(!d_deltaIsSafe){ Rational nextDelta = d_deltaComputingFunc(); setDelta(nextDelta); @@ -49,7 +193,7 @@ const Rational& ArithPartialModel::getDelta(){ return d_delta; } -bool ArithPartialModel::boundsAreEqual(ArithVar x) const{ +bool ArithVariables::boundsAreEqual(ArithVar x) const{ if(hasLowerBound(x) && hasUpperBound(x)){ return getUpperBound(x) == getLowerBound(x); }else{ @@ -57,102 +201,108 @@ bool ArithPartialModel::boundsAreEqual(ArithVar x) const{ } } -void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& 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); +void ArithVariables::setAssignment(ArithVar x, const DeltaRational& r){ + Debug("partial_model") << "pm: updating the assignment to" << x + << " now " << r <<endl; + VarInfo& vi = d_vars.get(x); + if(!d_safeAssignment.isKey(x)){ + d_safeAssignment.set(x, vi.d_assignment); } invalidateDelta(); - d_assignment[x] = r; + + BoundCounts prev; + if(vi.setAssignment(r, prev)){ + addToBoundQueue(x, prev); + } } -void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){ - Debug("partial_model") << "pm: updating the assignment to" << x - << " now " << r <<endl; + +void ArithVariables::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){ + Debug("partial_model") << "pm: updating the assignment to" << x + << " now " << r <<endl; if(safe == r){ - if(d_hasSafeAssignment[x]){ - d_safeAssignment[x] = safe; + if(d_safeAssignment.isKey(x)){ + d_safeAssignment.remove(x); } }else{ - d_safeAssignment[x] = safe; - - if(!d_hasSafeAssignment[x]){ - d_hasSafeAssignment[x] = true; - d_history.push_back(x); - } + d_safeAssignment.set(x, safe); } invalidateDelta(); - d_assignment[x] = r; + VarInfo& vi = d_vars.get(x); + BoundCounts prev; + if(vi.setAssignment(r, prev)){ + addToBoundQueue(x, prev); + } } -bool ArithPartialModel::equalSizes(){ - return - d_mapSize == d_hasSafeAssignment.size() && - d_mapSize == d_assignment.size() && - d_mapSize == d_safeAssignment.size() && - d_mapSize == d_ubc.size() && - d_mapSize == d_lbc.size(); +void ArithVariables::initialize(ArithVar x, Node n, bool slack){ + VarInfo& vi = d_vars.get(x); + vi.initialize(x, n, slack); + d_nodeToArithVarMap[n] = x; } -void ArithPartialModel::initialize(ArithVar x, const DeltaRational& r){ - Assert(x == d_mapSize); - Assert(equalSizes()); - ++d_mapSize; +ArithVar ArithVariables::allocate(Node n, bool slack){ + ArithVar v = allocateVariable(); + initialize(v, n, slack); + return v; +} - 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. - invalidateDelta(); - d_assignment.push_back( r ); - d_safeAssignment.push_back( DeltaRational(0) ); +// void ArithVariables::initialize(ArithVar x, const DeltaRational& r){ +// Assert(x == d_mapSize); +// Assert(equalSizes()); +// ++d_mapSize; - d_ubc.push_back(NullConstraint); - d_lbc.push_back(NullConstraint); -} +// // Is worth mentioning that this is not strictly necessary, but this maintains the internal invariant +// // that when d_assignment is set this gets set. +// invalidateDelta(); +// d_assignment.push_back( r ); + +// d_boundRel.push_back(BetweenBounds); + +// d_ubc.push_back(NullConstraint); +// d_lbc.push_back(NullConstraint); +// } /** Must know that the bound exists both calling this! */ -const DeltaRational& ArithPartialModel::getUpperBound(ArithVar x) const { +const DeltaRational& ArithVariables::getUpperBound(ArithVar x) const { Assert(inMaps(x)); Assert(hasUpperBound(x)); return getUpperBoundConstraint(x)->getValue(); } -const DeltaRational& ArithPartialModel::getLowerBound(ArithVar x) const { +const DeltaRational& ArithVariables::getLowerBound(ArithVar x) const { Assert(inMaps(x)); Assert(hasLowerBound(x)); return getLowerBoundConstraint(x)->getValue(); } -const DeltaRational& ArithPartialModel::getSafeAssignment(ArithVar x) const{ +const DeltaRational& ArithVariables::getSafeAssignment(ArithVar x) const{ Assert(inMaps(x)); - if(d_hasSafeAssignment[x]){ + if(d_safeAssignment.isKey(x)){ return d_safeAssignment[x]; }else{ - return d_assignment[x]; + return d_vars[x].d_assignment; } } -const DeltaRational& ArithPartialModel::getAssignment(ArithVar x, bool safe) const{ +const DeltaRational& ArithVariables::getAssignment(ArithVar x, bool safe) const{ Assert(inMaps(x)); - if(safe && d_hasSafeAssignment[x]){ + if(safe && d_safeAssignment.isKey(x)){ return d_safeAssignment[x]; }else{ - return d_assignment[x]; + return d_vars[x].d_assignment; } } -const DeltaRational& ArithPartialModel::getAssignment(ArithVar x) const{ +const DeltaRational& ArithVariables::getAssignment(ArithVar x) const{ Assert(inMaps(x)); - return d_assignment[x]; + return d_vars[x].d_assignment; } -void ArithPartialModel::setLowerBoundConstraint(Constraint c){ +void ArithVariables::setLowerBoundConstraint(Constraint c){ AssertArgument(c != NullConstraint, "Cannot set a lower bound to NullConstraint."); AssertArgument(c->isEquality() || c->isLowerBound(), "Constraint type must be set to an equality or UpperBound."); @@ -162,10 +312,15 @@ void ArithPartialModel::setLowerBoundConstraint(Constraint c){ Assert(greaterThanLowerBound(x, c->getValue())); invalidateDelta(); - d_lbc.set(x, c); + VarInfo& vi = d_vars.get(x); + pushLowerBound(vi); + BoundCounts prev; + if(vi.setLowerBound(c, prev)){ + addToBoundQueue(x, prev); + } } -void ArithPartialModel::setUpperBoundConstraint(Constraint c){ +void ArithVariables::setUpperBoundConstraint(Constraint c){ AssertArgument(c != NullConstraint, "Cannot set a upper bound to NullConstraint."); AssertArgument(c->isEquality() || c->isUpperBound(), "Constraint type must be set to an equality or UpperBound."); @@ -176,29 +331,40 @@ void ArithPartialModel::setUpperBoundConstraint(Constraint c){ Assert(lessThanUpperBound(x, c->getValue())); invalidateDelta(); - d_ubc.set(x, c); + VarInfo& vi = d_vars.get(x); + pushUpperBound(vi); + BoundCounts prev; + if(vi.setUpperBound(c, prev)){ + addToBoundQueue(x, prev); + } } -void ArithPartialModel::forceRelaxLowerBound(ArithVar v){ - AssertArgument(inMaps(v), "Calling forceRelaxLowerBound on a variable that is not properly setup."); - AssertArgument(hasLowerBound(v), "Calling forceRelaxLowerBound on a variable without a lowerbound."); +// void ArithVariables::forceRelaxLowerBound(ArithVar v){ +// AssertArgument(inMaps(v), "Calling forceRelaxLowerBound on a variable that is not properly setup."); +// AssertArgument(hasLowerBound(v), "Calling forceRelaxLowerBound on a variable without a lowerbound."); - Debug("partial_model") << "forceRelaxLowerBound(" << v << ") dropping :" << getLowerBoundConstraint(v) << endl; +// Debug("partial_model") << "forceRelaxLowerBound(" << v << ") dropping :" << getLowerBoundConstraint(v) << endl; - d_lbc.set(v, NullConstraint); -} +// invalidateDelta(); +// VarInfo& vi = d_vars.get(v); +// pushLowerBound(vi); +// vi.setLowerBound(NullConstraint); +// } -void ArithPartialModel::forceRelaxUpperBound(ArithVar v){ - AssertArgument(inMaps(v), "Calling forceRelaxUpperBound on a variable that is not properly setup."); - AssertArgument(hasUpperBound(v), "Calling forceRelaxUpperBound on a variable without an upper bound."); +// void ArithVariables::forceRelaxUpperBound(ArithVar v){ +// AssertArgument(inMaps(v), "Calling forceRelaxUpperBound on a variable that is not properly setup."); +// AssertArgument(hasUpperBound(v), "Calling forceRelaxUpperBound on a variable without an upper bound."); - Debug("partial_model") << "forceRelaxUpperBound(" << v << ") dropping :" << getUpperBoundConstraint(v) << endl; +// Debug("partial_model") << "forceRelaxUpperBound(" << v << ") dropping :" << getUpperBoundConstraint(v) << endl; - d_ubc.set(v, NullConstraint); -} +// invalidateDelta(); +// VarInfo& vi = d_vars.get(v); +// pushUpperBound(vi); +// vi.setUpperBound(NullConstraint); +// } -int ArithPartialModel::cmpToLowerBound(ArithVar x, const DeltaRational& c) const{ +int ArithVariables::cmpToLowerBound(ArithVar x, const DeltaRational& c) const{ if(!hasLowerBound(x)){ // l = -\intfy // ? c < -\infty |- _|_ @@ -208,7 +374,7 @@ int ArithPartialModel::cmpToLowerBound(ArithVar x, const DeltaRational& c) const } } -int ArithPartialModel::cmpToUpperBound(ArithVar x, const DeltaRational& c) const{ +int ArithVariables::cmpToUpperBound(ArithVar x, const DeltaRational& c) const{ if(!hasUpperBound(x)){ //u = \intfy // ? c > \infty |- _|_ @@ -218,14 +384,14 @@ int ArithPartialModel::cmpToUpperBound(ArithVar x, const DeltaRational& c) const } } -bool ArithPartialModel::equalsLowerBound(ArithVar x, const DeltaRational& c){ +bool ArithVariables::equalsLowerBound(ArithVar x, const DeltaRational& c){ if(!hasLowerBound(x)){ return false; }else{ return c == getLowerBound(x); } } -bool ArithPartialModel::equalsUpperBound(ArithVar x, const DeltaRational& c){ +bool ArithVariables::equalsUpperBound(ArithVar x, const DeltaRational& c){ if(!hasUpperBound(x)){ return false; }else{ @@ -233,111 +399,210 @@ bool ArithPartialModel::equalsUpperBound(ArithVar x, const DeltaRational& c){ } } -bool ArithPartialModel::hasEitherBound(ArithVar x) const{ +bool ArithVariables::hasEitherBound(ArithVar x) const{ return hasLowerBound(x) || hasUpperBound(x); } -bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x) const{ - Assert(inMaps(x)); - if(!hasUpperBound(x)){ // u = \infty - return true; - }else{ - return d_assignment[x] < getUpperBound(x); - } +bool ArithVariables::strictlyBelowUpperBound(ArithVar x) const{ + return d_vars[x].d_cmpAssignmentUB < 0; + // if(!hasUpperBound(x)){ // u = \infty + // return true; + // }else{ + // return d_assignment[x] < getUpperBound(x); + // } } -bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x) const{ - Assert(inMaps(x)); - if(!hasLowerBound(x)){ // l = -\infty - return true; - }else{ - return getLowerBound(x) < d_assignment[x]; - } +bool ArithVariables::strictlyAboveLowerBound(ArithVar x) const{ + return d_vars[x].d_cmpAssignmentLB > 0; + // if(!hasLowerBound(x)){ // l = -\infty + // return true; + // }else{ + // return getLowerBound(x) < d_assignment[x]; + // } } -bool ArithPartialModel::assignmentIsConsistent(ArithVar x) const{ - const DeltaRational& beta = getAssignment(x); +bool ArithVariables::assignmentIsConsistent(ArithVar x) const{ + return + d_vars[x].d_cmpAssignmentLB >= 0 && + d_vars[x].d_cmpAssignmentUB <= 0; + // const DeltaRational& beta = getAssignment(x); - //l_i <= beta(x_i) <= u_i - return greaterThanLowerBound(x,beta) && lessThanUpperBound(x,beta); + // //l_i <= beta(x_i) <= u_i + // return greaterThanLowerBound(x,beta) && lessThanUpperBound(x,beta); } -void ArithPartialModel::clearSafeAssignments(bool revert){ +void ArithVariables::clearSafeAssignments(bool revert){ - for(HistoryList::iterator i = d_history.begin(); i != d_history.end(); ++i){ - ArithVar x = *i; - Assert(d_hasSafeAssignment[x]); - d_hasSafeAssignment[x] = false; + if(revert && !d_safeAssignment.empty()){ + invalidateDelta(); + } + while(!d_safeAssignment.empty()){ + ArithVar atBack = d_safeAssignment.back(); if(revert){ - d_assignment[x] = d_safeAssignment[x]; + VarInfo& vi = d_vars.get(atBack); + BoundCounts prev; + if(vi.setAssignment(d_safeAssignment[atBack], prev)){ + addToBoundQueue(atBack, prev); + } } + d_safeAssignment.pop_back(); } - - if(revert && !d_history.empty()){ - invalidateDelta(); - } - - d_history.clear(); } -void ArithPartialModel::revertAssignmentChanges(){ +void ArithVariables::revertAssignmentChanges(){ clearSafeAssignments(true); } -void ArithPartialModel::commitAssignmentChanges(){ +void ArithVariables::commitAssignmentChanges(){ clearSafeAssignments(false); } -void ArithPartialModel::printModel(ArithVar x){ - Debug("model") << "model" << x << ":"<< getAssignment(x) << " "; +void ArithVariables::printEntireModel(std::ostream& out) const{ + out << "---Printing Model ---" << std::endl; + for(var_iterator i = var_begin(), iend = var_end(); i != iend; ++i){ + printModel(*i, out); + } + out << "---Done Model ---" << std::endl; +} + +void ArithVariables::printModel(ArithVar x, std::ostream& out) const{ + out << "model" << x << ": " + << asNode(x) << " " + << getAssignment(x) << " "; if(!hasLowerBound(x)){ - Debug("model") << "no lb "; + out << "no lb "; }else{ - Debug("model") << getLowerBound(x) << " "; - Debug("model") << getLowerBoundConstraint(x) << " "; + out << getLowerBound(x) << " "; + out << getLowerBoundConstraint(x) << " "; } if(!hasUpperBound(x)){ - Debug("model") << "no ub "; + out << "no ub "; }else{ - Debug("model") << getUpperBound(x) << " "; - Debug("model") << getUpperBoundConstraint(x) << " "; + out << getUpperBound(x) << " "; + out << getUpperBoundConstraint(x) << " "; } - Debug("model") << endl; + out << endl; } -// void ArithPartialModel::deltaIsSmallerThan(const DeltaRational& l, const DeltaRational& u){ -// const Rational& c = l.getNoninfinitesimalPart(); -// const Rational& k = l.getInfinitesimalPart(); -// const Rational& d = u.getNoninfinitesimalPart(); -// const Rational& h = u.getInfinitesimalPart(); +void ArithVariables::printModel(ArithVar x) const{ + printModel(x, Debug("model")); +} -// if(c < d && k > h){ -// Rational ep = (d-c)/(k-h); -// if(ep < d_delta){ -// d_delta = ep; +// BoundRelationship ArithVariables::boundRelationship(Constraint lb, const DeltaRational& d, Constraint ub){ +// if(lb == NullConstraint && ub == NullConstraint){ +// return BetweenBounds; +// }else if(lb == NullConstraint){ +// int cmp = d.cmp(ub->getValue()); +// return (cmp < 0) ? BetweenBounds : +// (cmp == 0 ? AtUpperBound : AboveUpperBound); +// }else if(ub == NullConstraint){ +// int cmp = d.cmp(lb->getValue()); +// return (cmp > 0) ? BetweenBounds : +// (cmp == 0 ? AtLowerBound : BelowLowerBound); +// }else{ +// Assert(lb->getValue() <= ub->getValue()); +// int cmpToLB = d.cmp(lb->getValue()); +// if(cmpToLB < 0){ +// return BelowLowerBound; +// }else if(cmpToLB == 0){ +// return (d == ub->getValue()) ? AtBothBounds : AtLowerBound; +// }else{ +// // d > 0 +// int cmpToUB = d.cmp(ub->getValue()); +// return (cmpToUB > 0) ? BetweenBounds : +// (cmpToUB == 0 ? AtLowerBound : BelowLowerBound); // } // } // } -// void ArithPartialModel::computeDelta(const Rational& init){ -// Assert(!d_deltaIsSafe); -// d_delta = init; +void ArithVariables::pushUpperBound(VarInfo& vi){ + ++vi.d_pushCount; + d_ubRevertHistory.push_back(make_pair(vi.d_var, vi.d_ub)); +} +void ArithVariables::pushLowerBound(VarInfo& vi){ + ++vi.d_pushCount; + d_lbRevertHistory.push_back(make_pair(vi.d_var, vi.d_lb)); +} + +void ArithVariables::popUpperBound(AVCPair* c){ + ArithVar x = c->first; + VarInfo& vi = d_vars.get(x); + BoundCounts prev; + if(vi.setUpperBound(c->second, prev)){ + addToBoundQueue(x, prev); + } + --vi.d_pushCount; +} + +void ArithVariables::popLowerBound(AVCPair* c){ + ArithVar x = c->first; + VarInfo& vi = d_vars.get(x); + BoundCounts prev; + if(vi.setLowerBound(c->second, prev)){ + addToBoundQueue(x, prev); + } + --vi.d_pushCount; +} -// for(ArithVar x = 0; x < d_mapSize; ++x){ -// const DeltaRational& a = getAssignment(x); -// if(hasLowerBound(x)){ -// const DeltaRational& l = getLowerBound(x); -// deltaIsSmallerThan(l,a); +/* To ensure that the final deallocation stuff works, + * we need to ensure that we need to not reference any of the other vectors + */ +// void ArithVariables::relaxUpperBound(Constraint curr, Constraint afterPop){ +// BoundRelation next = Undefined; +// switch(d_boundRel[x]){ +// case BelowLowerBound: +// case BetweenBounds: +// case AtLowerBound: +// return; // do nothing +// case AtUpperBound: +// if(afterPop != NullConstraint +// && curr->getValue() == afterPop->getValue()){ +// next = AtUpperBound; +// }else{ +// next = BetweenBounds; +// } +// break; +// case AtBothBounds: +// if(afterPop != NullConstraint +// && curr->getValue() == afterPop->getValue()){ +// next = AtUpperBound; +// }else{ +// next = AtLowerBound; // } -// if(hasUpperBound(x)){ -// const DeltaRational& u = getUpperBound(x); -// deltaIsSmallerThan(a,u); +// break; +// case AboveUpperBound: +// if(afterPop == NullConstraint){ +// next = BetweenBounds; +// }else{ +// int cmp = d_assignment[x].cmp(afterPop->getValue()); +// next = (cmp < 0) ? BetweenBounds : +// (cmp == 0) ? AtUpperBound : AboveUpperBound; // } +// break; +// default: +// Unreachable(); // } -// d_deltaIsSafe = true; +// d_boundRel[x] = next; // } + + +// void ArithVariables::relaxLowerBound(Constraint curr, Constraint afterPop){ +// // TODO this can be optimized using the automata induced by d_boundRel and +// // the knowledge that lb <= ub +// ArithVar x = curr->getVariable(); +// d_boundRel[x] = boundRelationship(afterPop, d_assignment[x], d_ubc[x]); +// } + +void ArithVariables::LowerBoundCleanUp::operator()(AVCPair* p){ + d_pm->popLowerBound(p); +} + +void ArithVariables::UpperBoundCleanUp::operator()(AVCPair* p){ + d_pm->popUpperBound(p); +} + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |