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]){
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){
}
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;
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) {
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{
}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];
}
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];
}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){
}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){
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){
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){
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();
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;
+ }
+ }
+ }
+ }
}
namespace theory {
namespace arith {
-namespace partial_model {
-// struct DeltaRationalCleanupStrategy{
-// static void cleanup(DeltaRational* dq){
-// Debug("arithgc") << "cleaning up " << dq << "\n";
-// if(dq != NULL){
-// delete dq;
-// }
-// }
-// };
-
-
-// struct AssignmentAttrID {};
-// typedef expr::Attribute<AssignmentAttrID,
-// DeltaRational*,
-// DeltaRationalCleanupStrategy> Assignment;
-
-
-// struct SafeAssignmentAttrID {};
-// typedef expr::Attribute<SafeAssignmentAttrID,
-// DeltaRational*,
-// DeltaRationalCleanupStrategy> SafeAssignment;
-
-
-
-/**
- * This defines a context dependent delta rational map.
- * This is used to keep track of the current lower and upper bounds on
- * each variable. This information is conext dependent.
- */
-//typedef context::CDMap<TNode, DeltaRational, TNodeHashFunction> CDDRationalMap;
-/* Side disucssion for why new tables are introduced instead of using the
- * attribute framework.
- * It comes down to that the obvious ways to use the current attribute
- * framework do not provide a terribly satisfying answer.
- * - Suppose the type of the attribute is CD and maps to type DeltaRational.
- * Well it can't map to a DeltaRational, and it thus it will be a
- * DeltaRational*
- * However being context dependent means givening up cleanup functions.
- * So this leaks memory.
- * - Suppose the type of the attribute is CD and the type mapped to
- * was a Node wrapping a CONST_DELTA_RATIONAL.
- * This was rejected for inefficiency, and uglyness.
- * Inefficiency: Every lookup and comparison will require going through the
- * massaging in between a node and the constant being wrapped. Every update
- * requires going through the additional expense of creating at least 1 node.
- * The Uglyness: If this was chosen it would also suggest using comparisons
- * against DeltaRationals for the tracking the constraints for conflict
- * analysis. This seems to invite misuse and introducing Nodes that should
- * probably not escape arith.
- * - Suppose that the of the attribute was not CD and mapped to a
- * CDO<DeltaRational*> or similarly a ContextObj that wraps a DeltaRational*.
- * This is currently rejected just because this is difficult to get right,
- * and maintain. However with enough effort this the best solution is
- * probably of this form.
- */
-
-
-/**
- * This is the literal that was asserted in the current context to the theory
- * that asserted the tightest lower bound on a variable.
- * For example: for a variable x this could be the constraint
- * (>= x 4) or (not (<= x 50))
- * Note the strong correspondence between this and LowerBoundMap.
- * This is used during conflict analysis.
- */
-// struct LowerConstraintAttrID {};
-// typedef expr::CDAttribute<LowerConstraintAttrID,TNode> LowerConstraint;
-
-/**
- * See the documentation for LowerConstraint.
- */
-// struct UpperConstraintAttrID {};
-// typedef expr::CDAttribute<UpperConstraintAttrID,TNode> UpperConstraint;
-
-// struct TheoryArithPropagatedID {};
-// typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated;
-
-// struct HasHadABoundID {};
-// typedef expr::Attribute<HasHadABoundID, bool> HasHadABound;
-
-}; /*namespace partial_model*/
-
-
-
class ArithPartialModel {
private:
context::CDVector<TNode> d_upperConstraint;
context::CDVector<TNode> d_lowerConstraint;
+ bool d_deltaIsSafe;
+ Rational d_delta;
/**
* List contains all of the variables that have an unsafe assignment.
d_lowerBound(c, false),
d_upperConstraint(c,false),
d_lowerConstraint(c,false),
+ d_deltaIsSafe(false),
+ d_delta(-1,1),
d_history()
{ }
TNode getUpperConstraint(ArithVar x);
-
/* Initializes a variable to a safe value.*/
void initialize(ArithVar x, const DeltaRational& r);
void printModel(ArithVar x);
+ /** returns true iff x has both a lower and upper bound. */
bool hasBounds(ArithVar x);
bool hasEverHadABound(ArithVar var){
return d_hasHadABound[var];
}
+ const Rational& getDelta(){
+ if(!d_deltaIsSafe){
+ computeDelta();
+ }
+ return d_delta;
+ }
+
private:
+ void computeDelta();
+
/**
* This function implements the mostly identical:
* revertAssignmentChanges() and commitAssignmentChanges().
projects / cvc5.git / commitdiff