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/arrays | |
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/arrays')
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 12 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 2 |
2 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 3c48c7907..bcdb75845 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -420,7 +420,7 @@ void TheoryArrays::preRegisterTerm(TNode node) case kind::STORE: { // Invariant: array terms should be preregistered before being added to the equality engine Assert(!d_equalityEngine.hasTerm(node)); - d_equalityEngine.addTriggerTerm(node); + d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY); TNode a = node[0]; // TNode i = node[1]; @@ -446,7 +446,7 @@ void TheoryArrays::preRegisterTerm(TNode node) default: // Variables etc if (node.getType().isArray()) { - d_equalityEngine.addTriggerTerm(node); + d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY); Assert(d_equalityEngine.getSize(node) == 1); } else { @@ -504,7 +504,7 @@ Node TheoryArrays::explain(TNode literal) void TheoryArrays::addSharedTerm(TNode t) { Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl; - d_equalityEngine.addTriggerTerm(t); + d_equalityEngine.addTriggerTerm(t, THEORY_ARRAY); if (t.getType().isArray()) { d_sharedArrays.insert(t,true); } @@ -583,7 +583,7 @@ void TheoryArrays::computeCareGraph() TNode x = r1[1]; TNode y = r2[1]; - if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) { + if (!d_equalityEngine.isTriggerTerm(x, THEORY_ARRAY) || !d_equalityEngine.isTriggerTerm(y, THEORY_ARRAY)) { Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): not connected to shared terms, skipping" << std::endl; continue; } @@ -596,8 +596,8 @@ void TheoryArrays::computeCareGraph() } // Get representative trigger terms - TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x); - TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y); + TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAY); + TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_ARRAY); EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared); switch (eqStatusDomain) { diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 146a2145b..639b03df8 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -241,7 +241,7 @@ class TheoryArrays : public Theory { Unreachable(); } - bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) { + bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ")" << std::endl; if (value) { if (t1.getType().isArray()) { |