diff options
Diffstat (limited to 'src/theory/arith/partial_model.cpp')
-rw-r--r-- | src/theory/arith/partial_model.cpp | 455 |
1 files changed, 284 insertions, 171 deletions
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 18993c748..6f0ded9e5 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -28,267 +28,368 @@ using namespace CVC4::theory; using namespace CVC4::theory::arith; using namespace CVC4::theory::arith::partial_model; -void ArithPartialModel::setUpperBound(TNode x, const DeltaRational& r){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); +void ArithPartialModel::setUpperBound(ArithVar x, const DeltaRational& r){ + //Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); Debug("partial_model") << "setUpperBound(" << x << "," << r << ")" << endl; - x.setAttribute(partial_model::HasHadABound(), true); + //x.setAttribute(partial_model::HasHadABound(), true); + d_hasHadABound[x] = true; - d_UpperBoundMap[x] = r; + d_upperBound.set(x,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); +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_LowerBoundMap[x] = r; +// d_LowerBoundMap[x] = r; + d_hasHadABound[x] = true; + d_lowerBound.set(x,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()); - - DeltaRational* saved = x.getAttribute(partial_model::SafeAssignment()); - if(saved == NULL){ - saved = new DeltaRational(*curr); - x.setAttribute(partial_model::SafeAssignment(), saved); +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]){ + d_safeAssignment[x] = d_assignment[x]; + d_hasSafeAssignment[x] = true; d_history.push_back(x); } - - *curr = r; - Debug("partial_model") << "pm: updating the assignment to" << x - << " now " << r <<endl; + d_assignment[x] = r; } -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()); - +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){ - if(saved != NULL){ - x.setAttribute(partial_model::SafeAssignment(), NULL); - delete saved; - } + d_hasSafeAssignment[x] = false; }else{ - if(saved == NULL){ - saved = new DeltaRational(safe); - x.setAttribute(partial_model::SafeAssignment(), saved); - }else{ - *saved = safe; + d_safeAssignment[x] = safe; + + if(!d_hasSafeAssignment[x]){ + d_hasSafeAssignment[x] = true; + d_history.push_back(x); } - d_history.push_back(x); } - *curr = r; + d_assignment[x] = r; +} - Debug("partial_model") << "pm: updating the assignment to" << x - << " now " << r <<endl; +bool ArithPartialModel::equalSizes(){ + return d_mapSize == d_hasHadABound.size() && + d_mapSize == d_hasSafeAssignment.size() && + d_mapSize == d_assignment.size() && + d_mapSize == d_safeAssignment.size() && + d_mapSize == d_upperBound.size() && + d_mapSize == d_lowerBound.size() && + d_mapSize == d_upperConstraint.size() && + d_mapSize == d_lowerConstraint.size(); } -void ArithPartialModel::initialize(TNode x, const DeltaRational& r){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); +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.hasAttribute(partial_model::Assignment())); - Assert(!x.hasAttribute(partial_model::SafeAssignment())); + Assert(x == d_mapSize); + Assert(equalSizes()); + ++d_mapSize; - 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; + d_hasHadABound.push_back( false ); + + d_hasSafeAssignment.push_back( false ); + d_assignment.push_back( r ); + d_safeAssignment.push_back( DeltaRational(0) ); + + d_upperBound.push_back( DeltaRational(0) ); + d_lowerBound.push_back( DeltaRational(0) ); + + d_upperConstraint.push_back( TNode::null() ); + d_lowerConstraint.push_back( TNode::null() ); } /** Must know that the bound exists both calling this! */ -DeltaRational ArithPartialModel::getUpperBound(TNode x) const { - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); +const DeltaRational& ArithPartialModel::getUpperBound(ArithVar x) { + Assert(inMaps(x)); + Assert(!d_upperConstraint[x].isNull()); - CDDRationalMap::iterator i = d_UpperBoundMap.find(x); - Assert(i != d_UpperBoundMap.end()); + return d_upperBound[x]; - return DeltaRational((*i).second); +// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); + +// CDDRationalMap::iterator i = d_UpperBoundMap.find(x); +// Assert(i != d_UpperBoundMap.end()); + +// return DeltaRational((*i).second); } -DeltaRational ArithPartialModel::getLowerBound(TNode x) const{ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); +const DeltaRational& ArithPartialModel::getLowerBound(ArithVar x) { + Assert(inMaps(x)); + Assert(!d_lowerConstraint[x].isNull()); - CDDRationalMap::iterator i = d_LowerBoundMap.find(x); - Assert(i != d_LowerBoundMap.end()); + return d_lowerBound[x]; - return DeltaRational((*i).second); -} +// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); -DeltaRational ArithPartialModel::getSafeAssignment(TNode x) const{ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - Assert( x.hasAttribute(SafeAssignment())); +// CDDRationalMap::iterator i = d_LowerBoundMap.find(x); +// Assert(i != d_LowerBoundMap.end()); - DeltaRational* safeAssignment = x.getAttribute(SafeAssignment()); - if(safeAssignment != NULL){ - return *safeAssignment; +// return DeltaRational((*i).second); +} + +const DeltaRational& ArithPartialModel::getSafeAssignment(ArithVar x) const{ + Assert(inMaps(x)); + if(d_hasSafeAssignment[x]){ + return d_safeAssignment[x]; }else{ - return getAssignment(x); //The current assignment is safe. + 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(TNode x) const{ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); +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; +// DeltaRational* assign; +// AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign)); +// return *assign; + Assert(inMaps(x)); + return d_assignment[x]; } -void ArithPartialModel::setLowerConstraint(TNode x, TNode constraint){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); +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); -} +// x.setAttribute(partial_model::LowerConstraint(),constraint); -void ArithPartialModel::setUpperConstraint(TNode x, TNode constraint){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); + Assert(inMaps(x)); + d_lowerConstraint.set(x,constraint); - Debug("partial_model") << "setUpperConstraint(" - << x << ":" << constraint << ")" << endl; - - x.setAttribute(partial_model::UpperConstraint(),constraint); } -TNode ArithPartialModel::getLowerConstraint(TNode x){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - - TNode ret; - AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret)); - return ret; -} +void ArithPartialModel::setUpperConstraint(ArithVar x, TNode constraint){ +// Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); -TNode ArithPartialModel::getUpperConstraint(TNode x){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); + Debug("partial_model") << "setUpperConstraint(" + << x << ":" << constraint << ")" << endl; - TNode ret; - AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret)); - return ret; +// x.setAttribute(partial_model::UpperConstraint(),constraint); + Assert(inMaps(x)); + d_upperConstraint.set(x, constraint); } -// TNode CVC4::theory::arith::getLowerConstraint(TNode x){ +TNode ArithPartialModel::getLowerConstraint(ArithVar x){ // Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); // TNode ret; // AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret)); // return ret; -// } -// TNode CVC4::theory::arith::getUpperConstraint(TNode x){ + 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]; +} -bool ArithPartialModel::belowLowerBound(TNode x, const DeltaRational& c, bool strict){ - CDDRationalMap::iterator i = d_LowerBoundMap.find(x); - if(i == d_LowerBoundMap.end()){ + +bool ArithPartialModel::belowLowerBound(ArithVar x, const DeltaRational& c, bool strict){ + if(d_lowerConstraint[x].isNull()){ // l = -\intfy // ? c < -\infty |- _|_ return false; } - - const DeltaRational& l = (*i).second; - if(strict){ - return c < l; + return c < d_lowerBound[x]; }else{ - return c <= l; + 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(TNode x, const DeltaRational& c, bool strict){ - CDDRationalMap::iterator i = d_UpperBoundMap.find(x); - if(i == d_UpperBoundMap.end()){ - // u = -\intfy - // ? u < -\infty |- _|_ +bool ArithPartialModel::aboveUpperBound(ArithVar x, const DeltaRational& c, bool strict){ + if(d_upperConstraint[x].isNull()){ + // u = \intfy + // ? c > \infty |- _|_ return false; } - const DeltaRational& u = (*i).second; - if(strict){ - return c > u; + return c > d_upperBound[x]; }else{ - return c >= u; + 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(TNode x){ +bool ArithPartialModel::hasBounds(ArithVar x){ return - d_UpperBoundMap.find(x) != d_UpperBoundMap.end() || - d_LowerBoundMap.find(x) != d_LowerBoundMap.end(); + !d_lowerConstraint[x].isNull() || !d_upperConstraint[x].isNull(); + // 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)); - - CDDRationalMap::iterator i = d_UpperBoundMap.find(x); - if(i == d_UpperBoundMap.end()){// u = \infty +bool ArithPartialModel::strictlyBelowUpperBound(ArithVar x){ + Assert(inMaps(x)); + if(d_upperConstraint[x].isNull()){ // u = \infty return true; } + return d_assignment[x] < d_upperBound[x]; +// DeltaRational* assign; +// AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign)); - const DeltaRational& u = (*i).second; - return (*assign) < u; -} +// CDDRationalMap::iterator i = d_UpperBoundMap.find(x); +// if(i == d_UpperBoundMap.end()){// u = \infty +// return true; +// } -bool ArithPartialModel::strictlyAboveLowerBound(TNode x){ - DeltaRational* assign; - AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign)); +// const DeltaRational& u = (*i).second; +// return (*assign) < u; +} - CDDRationalMap::iterator i = d_LowerBoundMap.find(x); - if(i == d_LowerBoundMap.end()){// l = \infty +bool ArithPartialModel::strictlyAboveLowerBound(ArithVar x){ + Assert(inMaps(x)); + if(d_lowerConstraint[x].isNull()){ // l = -\infty return true; } + return d_lowerBound[x] < d_assignment[x]; + +// DeltaRational* assign; +// AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign)); - const DeltaRational& l = (*i).second; - return l < *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(TNode x){ +bool ArithPartialModel::assignmentIsConsistent(ArithVar x){ const DeltaRational& beta = getAssignment(x); - bool above_li = !belowLowerBound(x,beta,true); - bool below_ui = !aboveUpperBound(x,beta,true); - //l_i <= beta(x_i) <= u_i - return above_li && below_ui; + return !belowLowerBound(x,beta,true) && !aboveUpperBound(x,beta,true); } void ArithPartialModel::clearSafeAssignments(bool revert){ for(HistoryList::iterator i = d_history.begin(); i != d_history.end(); ++i){ - TNode x = *i; - - Assert(x.hasAttribute(SafeAssignment())); - Assert(x.hasAttribute(Assignment())); - - DeltaRational* safeAssignment = x.getAttribute(SafeAssignment()); + ArithVar x = *i; + Assert(d_hasSafeAssignment[x]); + d_hasSafeAssignment[x] = false; if(revert){ - DeltaRational* assign = x.getAttribute(Assignment()); - *assign = *safeAssignment; + d_assignment[x] = d_safeAssignment[x]; } - x.setAttribute(partial_model::SafeAssignment(), NULL); - delete safeAssignment; +// 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(); @@ -301,26 +402,38 @@ void ArithPartialModel::commitAssignmentChanges(){ clearSafeAssignments(false); } -void ArithPartialModel::printModel(TNode x){ - +void ArithPartialModel::printModel(ArithVar 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{ + if(d_lowerConstraint[x].isNull()){ 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") << getLowerBound(x) << " "; + Debug("model") << getLowerConstraint(x) << " "; + } + if(d_upperConstraint[x].isNull()){ Debug("model") << "no ub "; + }else{ + Debug("model") << getUpperBound(x) << " "; + Debug("model") << getUpperConstraint(x) << " "; } - Debug("model") << endl; +// 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; } |