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/congruence_manager.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/congruence_manager.h')
-rw-r--r-- | src/theory/arith/congruence_manager.h | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 63a370f9a..1864bc89e 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -25,7 +25,8 @@ namespace arith { class ArithCongruenceManager { private: - context::CDMaybe<Node> d_conflict; + context::CDRaised d_inConflict; + NodeCallBack& d_raiseConflict; /** * The set of ArithVars equivalent to a pair of terms. @@ -101,17 +102,18 @@ private: eq::EqualityEngine d_ee; + void raiseConflict(Node conflict){ + Assert(!inConflict()); + Debug("arith::conflict") << "difference manager conflict " << conflict << std::endl; + d_inConflict.raise(); + d_raiseConflict(conflict); + } public: bool inConflict() const{ - return d_conflict.isSet(); + return d_inConflict.isRaised(); }; - Node conflict() const{ - Assert(inConflict()); - return d_conflict.get(); - } - bool hasMorePropagations() const { return !d_propagatations.empty(); } @@ -182,7 +184,7 @@ private: public: - ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack&, const ArithVarNodeMap&); + ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack& setLiteral, const ArithVarNodeMap&, NodeCallBack& raiseConflict); Node explain(TNode literal); void explain(TNode lit, NodeBuilder<>& out); |