summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/uf/equality_engine.cpp59
-rw-r--r--src/theory/uf/equality_engine.h3
2 files changed, 26 insertions, 36 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 8885abe6b..338076e78 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -88,10 +88,6 @@ void EqualityEngine::init() {
d_triggerDatabaseAllocatedSize = 100000;
d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize);
- //We can't notify during the initialization because it notifies
- // QuantifiersEngine.AddTermToDatabase that try to access to the uf
- // instantiator that currently doesn't exist.
- ScopedBool sb(d_performNotify, false);
addTermInternal(d_true);
addTermInternal(d_false);
@@ -111,7 +107,6 @@ EqualityEngine::EqualityEngine(context::Context* context,
d_masterEqualityEngine(0),
d_context(context),
d_done(context, false),
- d_performNotify(true),
d_notify(s_notifyNone),
d_applicationLookupsCount(context, 0),
d_nodesCount(context, 0),
@@ -141,7 +136,6 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify,
d_masterEqualityEngine(0),
d_context(context),
d_done(context, false),
- d_performNotify(true),
d_notify(notify),
d_applicationLookupsCount(context, 0),
d_nodesCount(context, 0),
@@ -381,10 +375,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
{
// Notify e.g. the theory that owns this equality engine that there is a
// new equivalence class.
- if (d_performNotify)
- {
- d_notify.eqNotifyNewClass(t);
- }
+ d_notify.eqNotifyNewClass(t);
if (d_constantsAreTriggers && d_isConstant[result])
{
// Non-Boolean constants are trigger terms for all tags
@@ -506,9 +497,7 @@ bool EqualityEngine::assertEquality(TNode eq,
}
// notify the theory
- if (d_performNotify) {
- d_notify.eqNotifyDisequal(eq[0], eq[1], reason);
- }
+ d_notify.eqNotifyDisequal(eq[0], eq[1], reason);
Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl;
@@ -608,7 +597,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
// Determine if we should notify the owner of this class of this merge.
// The second part of this check is needed due to the internal implementation
// of this class. It ensures that we are merging terms and not operators.
- if (d_performNotify && class1Id == cc1.getFind() && class2Id == cc2.getFind())
+ if (class1Id == cc1.getFind() && class2Id == cc2.getFind())
{
doNotify = true;
}
@@ -797,11 +786,11 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
EqualityNodeId tag1id = newSetTriggers[newSetTriggersSize++] =
class1triggers.d_triggers[i1++];
// since they are both tagged notify of merge
- if (d_performNotify) {
- EqualityNodeId tag2id = class2triggers.d_triggers[i2++];
- if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) {
- return false;
- }
+ EqualityNodeId tag2id = class2triggers.d_triggers[i2++];
+ if (!d_notify.eqNotifyTriggerTermEquality(
+ tag1, d_nodes[tag1id], d_nodes[tag2id], true))
+ {
+ return false;
}
// Next tags
tag1 = TheoryIdSetUtil::setPop(tags1);
@@ -1934,9 +1923,8 @@ void EqualityEngine::propagate() {
d_assertedEqualities.push_back(Equality(null_id, null_id));
d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
// Notify
- if (d_performNotify) {
- d_notify.eqNotifyConstantTermMerge(d_nodes[t1classId], d_nodes[t2classId]);
- }
+ d_notify.eqNotifyConstantTermMerge(d_nodes[t1classId],
+ d_nodes[t2classId]);
// Empty the queue and exit
continue;
}
@@ -1995,7 +1983,8 @@ void EqualityEngine::propagate() {
}
// Notify the triggers
- if (d_performNotify && !d_done) {
+ if (!d_done)
+ {
for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) {
const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[triggers[trigger_i]];
if (triggerInfo.d_trigger.getKind() == kind::EQUAL)
@@ -2217,12 +2206,16 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
TriggerTermSetRef triggerSetRef = d_nodeIndividualTrigger[classId];
if (triggerSetRef != +null_set_id && getTriggerTermSet(triggerSetRef).hasTrigger(tag)) {
// If the term already is in the equivalence class that a tagged representative, just notify
- if (d_performNotify) {
- EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag);
- Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << "): already have this trigger in class with " << d_nodes[triggerId] << std::endl;
- if (eqNodeId != triggerId && !d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) {
- d_done = true;
- }
+ EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag);
+ Debug("equality::trigger")
+ << d_name << "::eq::addTriggerTerm(" << t << ", " << tag
+ << "): already have this trigger in class with " << d_nodes[triggerId]
+ << std::endl;
+ if (eqNodeId != triggerId
+ && !d_notify.eqNotifyTriggerTermEquality(
+ tag, t, d_nodes[triggerId], true))
+ {
+ d_done = true;
}
} else {
@@ -2602,10 +2595,10 @@ bool EqualityEngine::propagateTriggerTermDisequalities(
// Store the propagation
storePropagatedDisequality(currentTag, myRep, tagRep);
// Notify
- if (d_performNotify) {
- if (!d_notify.eqNotifyTriggerTermEquality(currentTag, d_nodes[myRep], d_nodes[tagRep], false)) {
- d_done = true;
- }
+ if (!d_notify.eqNotifyTriggerTermEquality(
+ currentTag, d_nodes[myRep], d_nodes[tagRep], false))
+ {
+ d_done = true;
}
}
}
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 024774593..c0e7b3478 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -120,9 +120,6 @@ private:
/** If we are done, we don't except any new assertions */
context::CDO<bool> d_done;
- /** Whether to notify or not (temporarily disabled on equality checks) */
- bool d_performNotify;
-
/** The class to notify when a representative changes for a term */
EqualityEngineNotify& d_notify;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback