diff options
author | Tim King <taking@cs.nyu.edu> | 2012-06-13 20:37:43 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-06-13 20:37:43 +0000 |
commit | d0b33af0cf910ca7adb0357dad13e7e88baedebc (patch) | |
tree | fc9c1fae8b7c4e9a26656e81314800852996e2f6 /src/theory/arith/theory_arith.h | |
parent | 6acb8e96739df11859d3bca8a9e67bdaff5600c6 (diff) |
- Added a loop to internally assert constraints that are marked as true.
- Changes how CongruenceManager reports conflicts.
- ConstraintDatabase can now detect and raise conflicts when doing unate propagation.
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 26 |
1 files changed, 19 insertions, 7 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 1f0120387..e23a9a943 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -184,6 +184,8 @@ private: */ std::deque<Constraint> d_currentPropagationList; + context::CDQueue<Constraint> d_learnedBounds; + /** * Manages information about the assignment and upper and lower bounds on * variables. @@ -245,8 +247,17 @@ private: void operator()(Node n){ d_list.push_back(n); } - }; - PushCallBack d_conflictCallBack; + } d_raiseConflict; + + /** Returns true iff a conflict has been raised. */ + inline bool inConflict() const { + return !d_conflicts.empty(); + } + /** + * Outputs the contents of d_conflicts onto d_out. + * Must be inConflict(). + */ + void outputConflicts(); /** @@ -386,10 +397,10 @@ private: * a node describing this conflict is returned. * If this new bound is not in conflict, Node::null() is returned. */ - Node AssertLower(Constraint constraint); - Node AssertUpper(Constraint constraint); - Node AssertEquality(Constraint constraint); - Node AssertDisequality(Constraint constraint); + bool AssertLower(Constraint constraint); + bool AssertUpper(Constraint constraint); + bool AssertEquality(Constraint constraint); + bool AssertDisequality(Constraint constraint); /** Tracks the bounds that were updated in the current round. */ DenseSet d_updatedBounds; @@ -423,7 +434,8 @@ private: * Returns a conflict if one was found. * Returns Node::null if no conflict was found. */ - Node assertionCases(TNode assertion); + Constraint constraintFromFactQueue(); + bool assertionCases(Constraint c); /** * Returns the basic variable with the shorted row containg a non-basic variable. |