diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-21 20:15:52 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-05-21 20:15:52 +0000 |
| commit | 6ce8f5cc5d7767d5ff9e74bc08d3c8a364ad8bf1 (patch) | |
| tree | 67622f3ea73388f3a93ae381b0b8a6de92049f70 /src/theory/bv | |
| parent | fdd00c4dbfa64da59c65d5d1fef3e8505a842cc8 (diff) | |
Updating equality manager to handle tagged trigger terms. Notifications are pushed out for relationships between terms tagged with the same tag. No performance impact.
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/bv_subtheory.cpp | 2 | ||||
| -rw-r--r-- | src/theory/bv/bv_subtheory.h | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/bv/bv_subtheory.cpp b/src/theory/bv/bv_subtheory.cpp index 502d59f8d..fa36236c9 100644 --- a/src/theory/bv/bv_subtheory.cpp +++ b/src/theory/bv/bv_subtheory.cpp @@ -233,7 +233,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool } } -bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) { +bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl; if (value) { return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY); diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index db7bad30c..d508976ae 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -102,7 +102,7 @@ class EqualitySolver : public SubtheorySolver { NotifyClass(TheoryBV* bv): d_bv(bv) {} bool eqNotifyTriggerEquality(TNode equality, bool value); bool eqNotifyTriggerPredicate(TNode predicate, bool value); - bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value); + bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value); bool eqNotifyConstantTermMerge(TNode t1, TNode t2); }; @@ -121,7 +121,7 @@ public: bool addAssertions(const std::vector<TNode>& assertions, Theory::Effort e); void explain(TNode literal, std::vector<TNode>& assumptions); void addSharedTerm(TNode t) { - d_equalityEngine.addTriggerTerm(t); + d_equalityEngine.addTriggerTerm(t, THEORY_BV); } EqualityStatus getEqualityStatus(TNode a, TNode b) { if (d_equalityEngine.areEqual(a, b)) { |