diff options
author | Tim King <taking@cs.nyu.edu> | 2010-10-14 18:26:42 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-10-14 18:26:42 +0000 |
commit | bfdb4be24bfa474e6036a993e5afac16e77b4d2a (patch) | |
tree | 8fef3c3f29fa082ba1c3421a7de88555f49ff1d9 /src/theory/arith/partial_model.h | |
parent | 1e9fcef592fa5c841e1430446659c8d33fdcc3e2 (diff) |
Fixed computation of infinitesimals for arithmetic model generation.
Diffstat (limited to 'src/theory/arith/partial_model.h')
-rw-r--r-- | src/theory/arith/partial_model.h | 99 |
1 files changed, 14 insertions, 85 deletions
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<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: @@ -135,6 +51,8 @@ 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. @@ -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(). |