diff options
author | Tim King <taking@cs.nyu.edu> | 2014-03-07 18:00:37 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2014-03-07 18:00:52 -0500 |
commit | 9ccdea06edbc72e3ecd282e9e015f6fc4b2e7173 (patch) | |
tree | cde6138cb9ab6ef0b7c15edf42e3e8cc53637002 /src/theory/arith/congruence_manager.h | |
parent | 42be934ef4d4430944ae9074c7202a7d130c75bb (diff) |
Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.
Diffstat (limited to 'src/theory/arith/congruence_manager.h')
-rw-r--r-- | src/theory/arith/congruence_manager.h | 119 |
1 files changed, 28 insertions, 91 deletions
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index b4e009169..8e369ff9a 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -57,43 +57,19 @@ private: private: ArithCongruenceManager& d_acm; public: - ArithCongruenceNotify(ArithCongruenceManager& acm): d_acm(acm) {} - - bool eqNotifyTriggerEquality(TNode equality, bool value) { - Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl; - if (value) { - return d_acm.propagate(equality); - } else { - return d_acm.propagate(equality.notNode()); - } - } - - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { - Unreachable(); - } - - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { - Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl; - if (value) { - return d_acm.propagate(t1.eqNode(t2)); - } else { - return d_acm.propagate(t1.eqNode(t2).notNode()); - } - } - - void eqNotifyConstantTermMerge(TNode t1, TNode t2) { - Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; - if (t1.getKind() == kind::CONST_BOOLEAN) { - d_acm.propagate(t1.iffNode(t2)); - } else { - d_acm.propagate(t1.eqNode(t2)); - } - } - - void eqNotifyNewClass(TNode t) { } - void eqNotifyPreMerge(TNode t1, TNode t2) { } - void eqNotifyPostMerge(TNode t1, TNode t2) { } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } + ArithCongruenceNotify(ArithCongruenceManager& acm); + + bool eqNotifyTriggerEquality(TNode equality, bool value); + + bool eqNotifyTriggerPredicate(TNode predicate, bool value); + + bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value); + + void eqNotifyConstantTermMerge(TNode t1, TNode t2); + void eqNotifyNewClass(TNode t); + void eqNotifyPreMerge(TNode t1, TNode t2); + void eqNotifyPostMerge(TNode t1, TNode t2); + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); }; ArithCongruenceNotify d_notify; @@ -117,66 +93,27 @@ 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); - } + void raiseConflict(Node conflict); public: - bool inConflict() const{ - return d_inConflict.isRaised(); - }; + bool inConflict() const; - bool hasMorePropagations() const { - return !d_propagatations.empty(); - } + bool hasMorePropagations() const; - const Node getNextPropagation() { - Assert(hasMorePropagations()); - Node prop = d_propagatations.front(); - d_propagatations.dequeue(); - return prop; - } + const Node getNextPropagation(); - bool canExplain(TNode n) const { - return d_explanationMap.find(n) != d_explanationMap.end(); - } + bool canExplain(TNode n) const; void setMasterEqualityEngine(eq::EqualityEngine* eq); private: - Node externalToInternal(TNode n) const{ - Assert(canExplain(n)); - ExplainMap::const_iterator iter = d_explanationMap.find(n); - size_t pos = (*iter).second; - return d_propagatations[pos]; - } - - void pushBack(TNode n){ - d_explanationMap.insert(n, d_propagatations.size()); - d_propagatations.enqueue(n); - - ++(d_statistics.d_propagations); - } - - void pushBack(TNode n, TNode r){ - d_explanationMap.insert(r, d_propagatations.size()); - d_explanationMap.insert(n, d_propagatations.size()); - d_propagatations.enqueue(n); + Node externalToInternal(TNode n) const; - ++(d_statistics.d_propagations); - } + void pushBack(TNode n); - void pushBack(TNode n, TNode r, TNode w){ - d_explanationMap.insert(w, d_propagatations.size()); - d_explanationMap.insert(r, d_propagatations.size()); - d_explanationMap.insert(n, d_propagatations.size()); - d_propagatations.enqueue(n); + void pushBack(TNode n, TNode r); - ++(d_statistics.d_propagations); - } + void pushBack(TNode n, TNode r, TNode w); bool propagate(TNode x); void explain(TNode literal, std::vector<TNode>& assumptions); @@ -207,21 +144,21 @@ public: } /** Assert an equality. */ - void watchedVariableIsZero(Constraint eq); + void watchedVariableIsZero(ConstraintCP eq); /** Assert a conjunction from lb and ub. */ - void watchedVariableIsZero(Constraint lb, Constraint ub); + void watchedVariableIsZero(ConstraintCP lb, ConstraintCP ub); /** Assert that the value cannot be zero. */ - void watchedVariableCannotBeZero(Constraint c); + void watchedVariableCannotBeZero(ConstraintCP c); /** Assert that the value cannot be zero. */ - void watchedVariableCannotBeZero(Constraint c, Constraint d); + void watchedVariableCannotBeZero(ConstraintCP c, ConstraintCP d); /** Assert that the value is congruent to a constant. */ - void equalsConstant(Constraint eq); - void equalsConstant(Constraint lb, Constraint ub); + void equalsConstant(ConstraintCP eq); + void equalsConstant(ConstraintCP lb, ConstraintCP ub); void addSharedTerm(Node x); |