diff options
Diffstat (limited to 'src/theory/arith/partial_model.h')
-rw-r--r-- | src/theory/arith/partial_model.h | 56 |
1 files changed, 32 insertions, 24 deletions
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index d04d8dd8c..26f9a135b 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -60,12 +60,13 @@ typedef expr::Attribute<SafeAssignmentAttrID, * 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. +/* 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* + * 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 @@ -74,22 +75,23 @@ typedef context::CDMap<TNode, DeltaRational, TNodeHashFunction> CDDRationalMap; * 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*. + * 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. + * 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)) + * 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. */ @@ -117,18 +119,18 @@ private: partial_model::CDDRationalMap d_UpperBoundMap; + /** + * List contains all of the variables that have an unsafe assignment. + */ typedef std::vector<TNode> HistoryList; HistoryList d_history; - bool d_unsafeMode; - public: ArithPartialModel(context::Context* c): d_LowerBoundMap(c), d_UpperBoundMap(c), - d_history(), - d_unsafeMode(false) + d_history() { } void setLowerConstraint(TNode x, TNode constraint); @@ -138,23 +140,24 @@ public: + /* Initializes a variable to a safe value.*/ void initialize(TNode x, const DeltaRational& r); + /* Gets the last assignment to a variable that is known to be conistent. */ DeltaRational getSafeAssignment(TNode x) const; - bool isInUnsafeMode() { return d_unsafeMode; } - - void turnOnUnsafeMode(); - void turnOffUnsafeMode(); - + /* Reverts all variable assignments to their safe values. */ void revertAssignmentChanges(); - void commitAssignmentChanges(); + /* Commits all variables assignments as safe.*/ + void commitAssignmentChanges(); void setUpperBound(TNode x, const DeltaRational& r); void setLowerBound(TNode x, const DeltaRational& r); + + /* Sets an unsafe variable assignment */ void setAssignment(TNode x, const DeltaRational& r); /** Must know that the bound exists before calling this! */ @@ -182,6 +185,11 @@ public: void printModel(TNode x); private: + + /** + * This function implements the mostly identical: + * revertAssignmentChanges() and commitAssignmentChanges(). + */ void clearSafeAssignments(bool revert); }; |