From: Tim King Date: Thu, 14 Oct 2010 18:26:42 +0000 (+0000) Subject: Fixed computation of infinitesimals for arithmetic model generation. X-Git-Tag: cvc5-1.0.0~8800 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bfdb4be24bfa474e6036a993e5afac16e77b4d2a;p=cvc5.git Fixed computation of infinitesimals for arithmetic model generation. --- 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 <= 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; + } + } + } + } } diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index bec703369..256a6b931 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -34,90 +34,6 @@ namespace CVC4 { 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 Assignment; - - -// struct SafeAssignmentAttrID {}; -// typedef expr::Attribute 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 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 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 LowerConstraint; - -/** - * See the documentation for LowerConstraint. - */ -// struct UpperConstraintAttrID {}; -// typedef expr::CDAttribute UpperConstraint; - -// struct TheoryArithPropagatedID {}; -// typedef expr::CDAttribute TheoryArithPropagated; - -// struct HasHadABoundID {}; -// typedef expr::Attribute HasHadABound; - -}; /*namespace partial_model*/ - - - class ArithPartialModel { private: @@ -135,6 +51,8 @@ private: context::CDVector d_upperConstraint; context::CDVector d_lowerConstraint; + bool d_deltaIsSafe; + Rational d_delta; /** * List contains all of the variables that have an unsafe assignment. @@ -154,6 +72,8 @@ public: d_lowerBound(c, false), d_upperConstraint(c,false), d_lowerConstraint(c,false), + d_deltaIsSafe(false), + d_delta(-1,1), d_history() { } @@ -163,7 +83,6 @@ public: TNode getUpperConstraint(ArithVar x); - /* Initializes a variable to a safe value.*/ void initialize(ArithVar x, const DeltaRational& r); @@ -211,14 +130,24 @@ public: 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(). diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 4a783a6a4..6cf0d9414 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -936,10 +936,10 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { switch(n.getKind()) { case kind::VARIABLE: { DeltaRational drat = d_partialModel.getAssignment(asArithVar(n)); - // FIXME our infinitesimal is fixed here at 1e-06 + const Rational& delta = d_partialModel.getDelta(); return nodeManager-> mkConst( drat.getNoninfinitesimalPart() + - drat.getInfinitesimalPart() * Rational(1, 1000000) ); + drat.getInfinitesimalPart() * delta ); } case kind::EQUAL: // 2 args