diff options
Diffstat (limited to 'src/theory/arith/partial_model.h')
| -rw-r--r-- | src/theory/arith/partial_model.h | 372 |
1 files changed, 93 insertions, 279 deletions
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index a0f35f9db..5a0b662f8 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -1,9 +1,11 @@ -#include "context/cdlist.h" #include "context/context.h" +#include "context/cdmap.h" #include "theory/arith/delta_rational.h" +#include "expr/attribute.h" #include "expr/node.h" +#include <deque> #ifndef __CVC4__THEORY__ARITH__PARTIAL_MODEL_H #define __CVC4__THEORY__ARITH__PARTIAL_MODEL_H @@ -12,8 +14,6 @@ namespace CVC4 { namespace theory { namespace arith { -typedef CVC4::context::CDList<TNode> BoundsList; - namespace partial_model { struct DeltaRationalCleanupStrategy{ static void cleanup(DeltaRational* dq){ @@ -22,316 +22,130 @@ struct DeltaRationalCleanupStrategy{ } }; -struct AssignmentAttrID; -typedef expr::Attribute<AssignmentAttrID,DeltaRational*,DeltaRationalCleanupStrategy> Assignment; - -// TODO should have a cleanup see bug #110 -struct LowerBoundAttrID; -typedef expr::CDAttribute<LowerBoundAttrID,DeltaRational*> LowerBound; - -// TODO should have a cleanup see bug #110 -struct UpperBoundAttrID; -typedef expr::CDAttribute<UpperBoundAttrID,DeltaRational*> UpperBound; - -struct LowerConstraintAttrID; -typedef expr::CDAttribute<LowerConstraintAttrID,TNode> LowerConstraint; - -struct UpperConstraintAttrID; -typedef expr::CDAttribute<UpperConstraintAttrID,TNode> UpperConstraint; - -typedef CVC4::context::CDList<TNode> BoundsList; - -struct BoundsListCleanupStrategy{ - static void cleanup(BoundsList* bl){ - Debug("arithgc") << "cleaning up " << bl << "\n"; - bl->deleteSelf(); - } -}; - - -/** Unique name to use for constructing ECAttr. */ -struct BoundsListID; +struct AssignmentAttrID {}; +typedef expr::Attribute<AssignmentAttrID, + DeltaRational*, + DeltaRationalCleanupStrategy> Assignment; /** - * BoundsListAttr is the attribute that maps a node to atoms . + * 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 + * 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. */ -typedef expr::Attribute<BoundsListID, - BoundsList*, - BoundsListCleanupStrategy> BoundsListAttr; - -}; /*namespace partial_model*/ -struct TheoryArithPropagatedID; -typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated; /** - * Validates that a node constraint has the following form: - * constraint: x |><| c - * where |><| is either <, <=, ==, >=, LT and c is a constant rational. + * 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. */ -bool validateConstraint(TNode constraint){ - using namespace CVC4::kind; - switch(constraint.getKind()){ - case LT:case LEQ: case EQUAL: case GEQ: case GT: break; - default: return false; - } - - if(constraint[0].getMetaKind() != metakind::VARIABLE) return false; - return constraint[1].getKind() == CONST_RATIONAL; -} - -void addBound(TNode constraint){ - Assert(validateConstraint(constraint)); - TNode x = constraint[0]; - - BoundsList* bl; - if(!x.getAttribute(partial_model::BoundsListAttr(), bl)){ - //TODO - context::Context* context = NULL; - bl = new (true) BoundsList(context); - x.setAttribute(partial_model::BoundsListAttr(), bl); - } - bl->push_back(constraint); -} - -inline int deltaCoeff(Kind k){ - switch(k){ - case kind::LT: - return -1; - case kind::GT: - return 1; - default: - return 0; - } -} - +struct LowerConstraintAttrID {}; +typedef expr::CDAttribute<LowerConstraintAttrID,TNode> LowerConstraint; -inline bool negateBoundPropogation(CVC4::Kind k, bool isLowerBound){ - /* !isLowerBound - * [x <= u && u < c] \=> x < c - * [x <= u && u < c] \=> x <= c - * [x <= u && u < c] \=> !(x == c) - * [x <= u && u < c] \=> !(x >= c) - * [x <= u && u < c] \=> !(x > c) - */ - /* isLowerBound - * [x >= l && l > c] \=> x > c - * [x >= l && l > c] \=> x >= c - * [x >= l && l > c] \=> !(x == c) - * [x >= l && l > c] \=> !(x <= c) - * [x >= l && l > c] \=> !(x < c) - */ - using namespace CVC4::kind; - switch(k){ - case LT: - case LEQ: - return isLowerBound; - case EQUAL: - return true; - case GEQ: - case GT: - return !isLowerBound; - default: - Unreachable(); - return false; - } -} +/** + * See the documentation for LowerConstraint. + */ +struct UpperConstraintAttrID {}; +typedef expr::CDAttribute<UpperConstraintAttrID,TNode> UpperConstraint; -void propogateBound(TNode constraint, OutputChannel& oc, bool isLower){ - constraint.setAttribute(TheoryArithPropagated(),true); - bool neg = negateBoundPropogation(constraint.getKind(), isLower); - if(neg){ - oc.propagate(constraint.notNode(),false); - }else{ - oc.propagate(constraint,false); - } -} - -void propagateBoundConstraints(TNode x, OutputChannel& oc){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - - DeltaRational* l; - DeltaRational* u; - bool hasLowerBound = x.getAttribute(partial_model::LowerBound(), l); - bool hasUpperBound = x.getAttribute(partial_model::UpperBound(), u); - - if(!(hasLowerBound || hasUpperBound)) return; - BoundsList* bl; - - if(!x.getAttribute(partial_model::BoundsListAttr(), bl)) return; - - for(BoundsList::const_iterator iter = bl->begin(); iter != bl->end(); ++iter){ - TNode constraint = *iter; - if(constraint.hasAttribute(TheoryArithPropagated())){ - continue; - } - //TODO improve efficiency Rational& - Rational c = constraint[1].getConst<Rational>(); - Rational k(Integer(deltaCoeff(constraint.getKind()))); - DeltaRational ec(c, k); - if(hasUpperBound && (*u) < ec ){ - propogateBound(constraint, oc, false); - } - if(hasLowerBound && (*l) > ec ){ - propogateBound(constraint, oc, true); - } - } -} - -void setUpperBound(TNode x, DeltaRational& r){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - DeltaRational* c; - if(x.getAttribute(partial_model::UpperBound(), c)){ - *c = r; - }else{ - c = new DeltaRational(r); - x.setAttribute(partial_model::UpperBound(), c); - } -} - -void setLowerBound(TNode x, DeltaRational& r){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - DeltaRational* c; - if(x.getAttribute(partial_model::LowerBound(), c)){ - *c = r; - }else{ - c = new DeltaRational(r); - x.setAttribute(partial_model::LowerBound(), c); - } -} -void setAssignment(TNode x, DeltaRational& r){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - DeltaRational* c; - if(x.getAttribute(partial_model::Assignment(), c)){ - *c = r; - }else{ - c = new DeltaRational(r); - x.setAttribute(partial_model::Assignment(), c); - } -} +}; /*namespace partial_model*/ -/** Must know that the bound exists both calling this! */ -DeltaRational getUpperBound(TNode x){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - DeltaRational* assign; - AlwaysAssert(x.getAttribute(partial_model::UpperBound(),assign)); - return *assign; -} +struct TheoryArithPropagatedID {}; +typedef expr::CDAttribute<TheoryArithPropagatedID, bool> TheoryArithPropagated; -DeltaRational getLowerBound(TNode x){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); - DeltaRational* assign; - AlwaysAssert(x.getAttribute(partial_model::LowerBound(),assign)); - return *assign; -} +class ArithPartialModel { +private: + partial_model::CDDRationalMap d_LowerBoundMap; + partial_model::CDDRationalMap d_UpperBoundMap; -DeltaRational getAssignment(TNode x){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); + typedef std::pair<TNode, DeltaRational> HistoryPair; + typedef std::deque< HistoryPair > HistoryStack; - DeltaRational* assign; - AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign)); - return *assign; -} + HistoryStack d_history; -void setLowerConstraint(TNode constraint){ - TNode x = constraint[0]; - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); + bool d_savingAssignments; - x.setAttribute(partial_model::LowerConstraint(),constraint); -} +public: -void setUpperConstraint(TNode constraint){ - TNode x = constraint[0]; - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); + ArithPartialModel(context::Context* c): + d_LowerBoundMap(c), + d_UpperBoundMap(c), + d_history(), + d_savingAssignments(false) + { } - x.setAttribute(partial_model::UpperConstraint(),constraint); -} -TNode getLowerConstraint(TNode x){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); + void setLowerConstraint(TNode x, TNode constraint); + void setUpperConstraint(TNode x, TNode constraint); + TNode getLowerConstraint(TNode x); + TNode getUpperConstraint(TNode x); - TNode ret; - AlwaysAssert(x.getAttribute(partial_model::LowerConstraint(),ret)); - return ret; -} -TNode getUpperConstraint(TNode x){ - Assert(x.getMetaKind() == CVC4::kind::metakind::VARIABLE); + void beginRecordingAssignments(); - TNode ret; - AlwaysAssert(x.getAttribute(partial_model::UpperConstraint(),ret)); - return ret; -} + /* */ + void stopRecordingAssignments(bool revert); -/** - * x <= l - * ? c < l - */ -bool belowLowerBound(TNode x, DeltaRational& c, bool strict){ - DeltaRational* l; - if(!x.getAttribute(partial_model::LowerBound(), l)){ - // l = -\intfy - // ? c < -\infty |- _|_ - return false; - } - if(strict){ - return c < *l; - }else{ - return c <= *l; - } -} + void setUpperBound(TNode x, const DeltaRational& r); + void setLowerBound(TNode x, const DeltaRational& r); + void setAssignment(TNode x, const DeltaRational& r); -/** - * x <= u - * ? c < u - */ -bool aboveUpperBound(TNode x, DeltaRational& c, bool strict){ - DeltaRational* u; - if(!x.getAttribute(partial_model::UpperBound(), u)){ - // c = \intfy - // ? c > \infty |- _|_ - return false; - } + /** Must know that the bound exists before calling this! */ + DeltaRational getUpperBound(TNode x) const; + DeltaRational getLowerBound(TNode x) const; + DeltaRational getAssignment(TNode x) const; - if(strict){ - return c > *u; - }else{ - return c >= *u; - } -} -bool strictlyBelowUpperBound(TNode x){ - DeltaRational* assign; - AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign)); + /** + * x <= l + * ? c < l + */ + bool belowLowerBound(TNode x, DeltaRational& c, bool strict); - DeltaRational* u; - if(!x.getAttribute(partial_model::UpperBound(), u)){ // u = \infty - return true; - } - return *assign < *u; -} + /** + * x <= u + * ? c < u + */ + bool aboveUpperBound(TNode x, DeltaRational& c, bool strict); -bool strictlyAboveLowerBound(TNode x){ - DeltaRational* assign; - AlwaysAssert(x.getAttribute(partial_model::Assignment(),assign)); + bool strictlyBelowUpperBound(TNode x); + bool strictlyAboveLowerBound(TNode x); + bool assignmentIsConsistent(TNode x); +}; - DeltaRational* l; - if(!x.getAttribute(partial_model::LowerBound(), l)){ // l = -\infty - return true; - } - return *l < *assign; -} -bool assignmentIsConsistent(TNode x){ - DeltaRational beta = getAssignment(x); - //l_i <= beta(x_i) <= u_i - return !aboveUpperBound(x,beta, true) && !belowLowerBound(x,beta,true); -} }; /* namesapce arith */ }; /* namespace theory */ |