diff options
Diffstat (limited to 'src/theory/arith/partial_model.cpp')
-rw-r--r-- | src/theory/arith/partial_model.cpp | 219 |
1 files changed, 28 insertions, 191 deletions
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 6f0ded9e5..a0f0247be 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -26,43 +26,23 @@ using namespace std; using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::arith; -using namespace CVC4::theory::arith::partial_model; void ArithPartialModel::setUpperBound(ArithVar x, const DeltaRational& r){ - //Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); + d_deltaIsSafe = false; Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl; - //x.setAttribute(partial_model::HasHadABound(), true); d_hasHadABound[x] = true; - d_upperBound.set(x,r); } void ArithPartialModel::setLowerBound(ArithVar 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_deltaIsSafe = false; -// d_LowerBoundMap[x] = r; d_hasHadABound[x] = true; d_lowerBound.set(x,r); } void ArithPartialModel::setAssignment(ArithVar 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()); - -// 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; Debug("partial_model") << "pm: updating the assignment to" << x << " now " << r <<endl; if(!d_hasSafeAssignment[x]){ @@ -73,31 +53,6 @@ void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& r){ d_assignment[x] = r; } void ArithPartialModel::setAssignment(ArithVar 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; if(safe == r){ @@ -125,18 +80,6 @@ bool ArithPartialModel::equalSizes(){ } void ArithPartialModel::initialize(ArithVar x, const DeltaRational& r){ -// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - -// Assert(!x.hasAttribute(partial_model::Assignment())); -// Assert(!x.hasAttribute(partial_model::SafeAssignment())); - -// DeltaRational* c = new DeltaRational(r); -// x.setAttribute(partial_model::Assignment(), c); -// x.setAttribute(partial_model::SafeAssignment(), NULL); - -// Debug("partial_model") << "pm: constructing an assignment for " << x -// << " initially " << (*c) <<endl; - Assert(x == d_mapSize); Assert(equalSizes()); ++d_mapSize; @@ -161,13 +104,6 @@ const DeltaRational& ArithPartialModel::getUpperBound(ArithVar x) { Assert(!d_upperConstraint[x].isNull()); return d_upperBound[x]; - -// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - -// CDDRationalMap::iterator i = d_UpperBoundMap.find(x); -// Assert(i != d_UpperBoundMap.end()); - -// return DeltaRational((*i).second); } const DeltaRational& ArithPartialModel::getLowerBound(ArithVar x) { @@ -175,13 +111,6 @@ const DeltaRational& ArithPartialModel::getLowerBound(ArithVar x) { Assert(!d_lowerConstraint[x].isNull()); return d_lowerBound[x]; - -// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - -// CDDRationalMap::iterator i = d_LowerBoundMap.find(x); -// Assert(i != d_LowerBoundMap.end()); - -// return DeltaRational((*i).second); } const DeltaRational& ArithPartialModel::getSafeAssignment(ArithVar x) const{ @@ -191,23 +120,9 @@ const DeltaRational& ArithPartialModel::getSafeAssignment(ArithVar x) const{ }else{ return d_assignment[x]; } -// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); -// Assert( x.hasAttribute(SafeAssignment())); - -// DeltaRational* safeAssignment = x.getAttribute(SafeAssignment()); -// if(safeAssignment != NULL){ -// return *safeAssignment; -// }else{ -// return getAssignment(x); //The current assignment is safe. -// } } const DeltaRational& ArithPartialModel::getAssignment(ArithVar x) const{ -// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - -// DeltaRational* assign; -// AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign)); -// return *assign; Assert(inMaps(x)); return d_assignment[x]; } @@ -215,47 +130,27 @@ const DeltaRational& ArithPartialModel::getAssignment(ArithVar x) const{ void ArithPartialModel::setLowerConstraint(ArithVar x, TNode constraint){ -// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - Debug("partial_model") << "setLowerConstraint(" << x << ":" << constraint << ")" << endl; - -// x.setAttribute(partial_model::LowerConstraint(),constraint); - Assert(inMaps(x)); d_lowerConstraint.set(x,constraint); } void ArithPartialModel::setUpperConstraint(ArithVar x, TNode constraint){ -// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - Debug("partial_model") << "setUpperConstraint(" << x << ":" << constraint << ")" << endl; - -// x.setAttribute(partial_model::UpperConstraint(),constraint); Assert(inMaps(x)); d_upperConstraint.set(x, constraint); } TNode ArithPartialModel::getLowerConstraint(ArithVar x){ -// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - -// TNode ret; -// AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret)); -// return ret; - Assert(inMaps(x)); Assert(!d_lowerConstraint[x].isNull()); return d_lowerConstraint[x]; } TNode ArithPartialModel::getUpperConstraint(ArithVar x){ -// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - -// TNode ret; -// AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret)); -// return ret; Assert(inMaps(x)); Assert(!d_upperConstraint[x].isNull()); return d_upperConstraint[x]; @@ -274,20 +169,6 @@ bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool }else{ return c <= d_lowerBound[x]; } -// CDDRationalMap::iterator i = d_LowerBoundMap.find(x); -// if(i == d_LowerBoundMap.end()){ -// // l = -\intfy -// // ? c < -\infty |- _|_ -// return false; -// } - -// const DeltaRational& l = (*i).second; - -// if(strict){ -// return c < l; -// }else{ -// return c <= l; -// } } bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){ @@ -301,27 +182,10 @@ bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool }else{ return c >= d_upperBound[x]; } -// CDDRationalMap::iterator i = d_UpperBoundMap.find(x); -// if(i == d_UpperBoundMap.end()){ -// // u = -\intfy -// // ? u < -\infty |- _|_ -// return false; -// } -// const DeltaRational& u = (*i).second; - -// if(strict){ -// return c > u; -// }else{ -// return c >= u; -// } } bool ArithPartialModel::hasBounds(ArithVar x){ - return - !d_lowerConstraint[x].isNull() || !d_upperConstraint[x].isNull(); - // return -// d_UpperBoundMap.find(x) != d_UpperBoundMap.end() || -// d_LowerBoundMap.find(x) != d_LowerBoundMap.end(); + return !d_lowerConstraint[x].isNull() || !d_upperConstraint[x].isNull(); } bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x){ @@ -330,16 +194,6 @@ bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x){ return true; } return d_assignment[x] < d_upperBound[x]; -// DeltaRational* assign; -// AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign)); - -// CDDRationalMap::iterator i = d_UpperBoundMap.find(x); -// if(i == d_UpperBoundMap.end()){// u = \infty -// return true; -// } - -// const DeltaRational& u = (*i).second; -// return (*assign) < u; } bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){ @@ -348,17 +202,6 @@ bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){ return true; } return d_lowerBound[x] < d_assignment[x]; - -// DeltaRational* assign; -// AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign)); - -// CDDRationalMap::iterator i = d_LowerBoundMap.find(x); -// if(i == d_LowerBoundMap.end()){// l = \infty -// return true; -// } - -// const DeltaRational& l = (*i).second; -// return l < *assign; } bool ArithPartialModel::assignmentIsConsistent(ArithVar x){ @@ -379,17 +222,6 @@ void ArithPartialModel::clearSafeAssignments(bool revert){ if(revert){ d_assignment[x] = d_safeAssignment[x]; } -// Assert(x.hasAttribute(SafeAssignment())); -// Assert(x.hasAttribute(Assignment())); - -// DeltaRational* safeAssignment = x.getAttribute(SafeAssignment()); - -// if(revert){ -// DeltaRational* assign = x.getAttribute(Assignment()); -// *assign = *safeAssignment; -// } -// x.setAttribute(partial_model::SafeAssignment(), NULL); -// delete safeAssignment; } d_history.clear(); @@ -416,24 +248,29 @@ void ArithPartialModel::printModel(ArithVar x){ Debug("model") << getUpperBound(x) << " "; Debug("model") << getUpperConstraint(x) << " "; } -// Debug("model") << "model" << x << ":"<< getAssignment(x) << " "; - -// CDDRationalMap::iterator i = d_LowerBoundMap.find(x); -// if(i != d_LowerBoundMap.end()){ -// DeltaRational l = (*i).second; -// Debug("model") << l << " "; -// Debug("model") << getLowerConstraint(x) << " "; -// }else{ -// Debug("model") << "no lb "; -// } - -// i = d_UpperBoundMap.find(x); -// if(i != d_UpperBoundMap.end()){ -// DeltaRational u = (*i).second; -// Debug("model") << u << " "; -// Debug("model") << getUpperConstraint(x) << " "; -// }else{ -// Debug("model") << "no ub "; -// } -// Debug("model") << endl; +} + +void ArithPartialModel::computeDelta(){ + Assert(!d_deltaIsSafe); + d_deltaIsSafe = true; + d_delta = 1; + + for(ArithVar x = 0; x < d_mapSize; ++x){ + if(hasBounds(x)){ + const DeltaRational& l = getLowerBound(x); + const DeltaRational& u = getUpperBound(x); + // c + k\ep <= d + h\ep + const Rational& c = l.getNoninfinitesimalPart(); + const Rational& k = l.getInfinitesimalPart(); + const Rational& d = u.getNoninfinitesimalPart(); + const Rational& h = u.getInfinitesimalPart(); + + if(c < d && k > h){ + Rational ep = (d-c)/(k-h); + if(ep < d_delta){ + d_delta = ep; + } + } + } + } } |