summaryrefslogtreecommitdiff
path: root/src/theory/uf/equality_engine_impl.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/uf/equality_engine_impl.h')
-rw-r--r--src/theory/uf/equality_engine_impl.h189
1 files changed, 170 insertions, 19 deletions
diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h
index b31d04a32..77c8e80b4 100644
--- a/src/theory/uf/equality_engine_impl.h
+++ b/src/theory/uf/equality_engine_impl.h
@@ -91,6 +91,8 @@ EqualityNodeId EqualityEngine<NotifyClass>::newNode(TNode node, bool isApplicati
d_nodeTriggers.push_back(+null_trigger);
// Add it to the equality graph
d_equalityGraph.push_back(+null_edge);
+ // Mark the no-individual trigger
+ d_nodeIndividualTrigger.push_back(+null_id);
// Add the equality node to the nodes
d_equalityNodes.push_back(EqualityNode(newId));
@@ -176,15 +178,27 @@ void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason)
Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
// Add the terms if they are not already in the database
- EqualityNodeId t1Id = getNodeId(t1);
- EqualityNodeId t2Id = getNodeId(t2);
+ addTerm(t1);
+ addTerm(t2);
// Add to the queue and propagate
+ EqualityNodeId t1Id = getNodeId(t1);
+ EqualityNodeId t2Id = getNodeId(t2);
enqueue(MergeCandidate(t1Id, t2Id, MERGED_THROUGH_EQUALITY, reason));
propagate();
}
template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addDisequality(TNode t1, TNode t2, TNode reason) {
+
+ Debug("equality") << "EqualityEngine::addDisequality(" << t1 << "," << t2 << ")" << std::endl;
+
+ Node equality = t1.eqNode(t2);
+ addEquality(equality, d_false, reason);
+}
+
+
+template <typename NotifyClass>
TNode EqualityEngine<NotifyClass>::getRepresentative(TNode t) const {
Debug("equality") << "EqualityEngine::getRepresentative(" << t << ")" << std::endl;
@@ -304,6 +318,24 @@ void EqualityEngine<NotifyClass>::merge(EqualityNode& class1, EqualityNode& clas
// Now merge the lists
class1.merge<true>(class2);
+
+ // Notfiy the triggers
+ EqualityNodeId class1triggerId = d_nodeIndividualTrigger[class1Id];
+ EqualityNodeId class2triggerId = d_nodeIndividualTrigger[class2Id];
+ if (class2triggerId != +null_id) {
+ if (class1triggerId == +null_id) {
+ // If class1 is not an individual trigger, but class2 is, mark it
+ d_nodeIndividualTrigger[class1Id] = class2triggerId;
+ // Add it to the list for backtracking
+ d_individualTriggers.push_back(class1Id);
+ d_individualTriggersSize = d_individualTriggersSize + 1;
+ } else {
+ // Notify when done
+ if (d_performNotify) {
+ d_notify.notify(d_nodes[class1triggerId], d_nodes[class2triggerId]);
+ }
+ }
+ }
}
template <typename NotifyClass>
@@ -437,11 +469,19 @@ void EqualityEngine<NotifyClass>::backtrack() {
d_equalityEdges.resize(2 * d_assertedEqualitiesCount);
}
+ if (d_individualTriggers.size() > d_individualTriggersSize) {
+ // Unset the individual triggers
+ for (int i = d_individualTriggers.size() - 1, i_end = d_individualTriggersSize; i >= i_end; -- i) {
+ d_nodeIndividualTrigger[d_individualTriggers[i]] = +null_id;
+ }
+ d_individualTriggers.resize(d_individualTriggersSize);
+ }
+
if (d_equalityTriggers.size() > d_equalityTriggersCount) {
// Unlink the triggers from the lists
for (int i = d_equalityTriggers.size() - 1, i_end = d_equalityTriggersCount; i >= i_end; -- i) {
- const Trigger& trigger = d_equalityTriggers[i];
- d_nodeTriggers[trigger.classId] = trigger.nextTrigger;
+ const Trigger& trigger = d_equalityTriggers[i];
+ d_nodeTriggers[trigger.classId] = trigger.nextTrigger;
}
// Get rid of the triggers
d_equalityTriggers.resize(d_equalityTriggersCount);
@@ -470,6 +510,7 @@ void EqualityEngine<NotifyClass>::backtrack() {
d_nodes.resize(d_nodesCount);
d_applications.resize(d_nodesCount);
d_nodeTriggers.resize(d_nodesCount);
+ d_nodeIndividualTrigger.resize(d_nodesCount);
d_equalityGraph.resize(d_nodesCount);
d_equalityNodes.resize(d_nodesCount);
}
@@ -614,6 +655,13 @@ void EqualityEngine<NotifyClass>::getExplanation(EqualityNodeId t1Id, EqualityNo
}
template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addTriggerDisequality(TNode t1, TNode t2, TNode trigger) {
+ Node equality = t1.eqNode(t2);
+ addTerm(equality);
+ addTriggerEquality(equality, d_false, trigger);
+}
+
+template <typename NotifyClass>
void EqualityEngine<NotifyClass>::addTriggerEquality(TNode t1, TNode t2, TNode trigger) {
Debug("equality") << "EqualityEngine::addTrigger(" << t1 << ", " << t2 << ", " << trigger << ")" << std::endl;
@@ -651,7 +699,9 @@ void EqualityEngine<NotifyClass>::addTriggerEquality(TNode t1, TNode t2, TNode t
// If the trigger is already on, we propagate
if (t1classId == t2classId) {
Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << "): triggered at setup time" << std::endl;
- d_notify.notifyEquality(trigger); // Don't care about the return value
+ if (d_performNotify) {
+ d_notify.notify(trigger); // Don't care about the return value
+ }
}
Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl;
@@ -690,31 +740,30 @@ void EqualityEngine<NotifyClass>::propagate() {
Assert(node1.getFind() == t1classId);
Assert(node2.getFind() == t2classId);
+ // Add the actuall equality to the equality graph
+ addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason);
+
+ // One more equality added
+ d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
+
// Depending on the merge preference (such as size), merge them
std::vector<TriggerId> triggers;
if (node2.getSize() > node1.getSize()) {
Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl;
- merge(node2, node1, triggers);
d_assertedEqualities.push_back(Equality(t2classId, t1classId));
+ merge(node2, node1, triggers);
} else {
Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl;
- merge(node1, node2, triggers);
d_assertedEqualities.push_back(Equality(t1classId, t2classId));
+ merge(node1, node2, triggers);
}
- // Add the actuall equality to the equality graph
- addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason);
-
- // One more equality added
- d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
-
- Assert(2*d_assertedEqualities.size() == d_equalityEdges.size());
- Assert(d_assertedEqualities.size() == d_assertedEqualitiesCount);
-
// Notify the triggers
- for (size_t trigger = 0, trigger_end = triggers.size(); trigger < trigger_end && !done; ++ trigger) {
- // Notify the trigger and exit if it fails
- done = !d_notify.notifyEquality(d_equalityTriggersOriginal[triggers[trigger]]);
+ if (d_performNotify) {
+ for (size_t trigger = 0, trigger_end = triggers.size(); trigger < trigger_end && !done; ++ trigger) {
+ // Notify the trigger and exit if it fails
+ done = !d_notify.notify(d_equalityTriggersOriginal[triggers[trigger]]);
+ }
}
}
}
@@ -736,6 +785,108 @@ void EqualityEngine<NotifyClass>::debugPrintGraph() const {
}
}
+class ScopedBool {
+ bool& watch;
+ bool oldValue;
+public:
+ ScopedBool(bool& watch, bool newValue)
+ : watch(watch), oldValue(watch) {
+ watch = newValue;
+ }
+ ~ScopedBool() {
+ watch = oldValue;
+ }
+};
+
+template <typename NotifyClass>
+bool EqualityEngine<NotifyClass>::areEqual(TNode t1, TNode t2)
+{
+ // Don't notify during this check
+ ScopedBool turnOfNotify(d_performNotify, false);
+
+ // Push the context, so that we can remove the terms later
+ d_context->push();
+
+ // Add the terms
+ addTerm(t1);
+ addTerm(t2);
+ bool equal = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind();
+
+ // Pop the context (triggers new term removal)
+ d_context->pop();
+
+ // Return whether the two terms are equal
+ return equal;
+}
+
+template <typename NotifyClass>
+bool EqualityEngine<NotifyClass>::areDisequal(TNode t1, TNode t2)
+{
+ // Don't notify during this check
+ ScopedBool turnOfNotify(d_performNotify, false);
+
+ // Push the context, so that we can remove the terms later
+ d_context->push();
+
+ // Add the terms
+ addTerm(t1);
+ addTerm(t2);
+
+ // Check (t1 = t2) = false
+ Node equality1 = t1.eqNode(t2);
+ addTerm(equality1);
+ if (getEqualityNode(equality1).getFind() == getEqualityNode(d_false).getFind()) {
+ return true;
+ }
+
+ // Check (t2 = t1) = false
+ Node equality2 = t2.eqNode(t1);
+ addTerm(equality2);
+ if (getEqualityNode(equality2).getFind() == getEqualityNode(d_false).getFind()) {
+ return true;
+ }
+
+ // Pop the context (triggers new term removal)
+ d_context->pop();
+
+ // Return whether the terms are disequal
+ return false;
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addTriggerTerm(TNode t)
+{
+ Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ")" << std::endl;
+
+ // Add the term if it's not already there
+ addTerm(t);
+
+ // Get the node id
+ EqualityNodeId eqNodeId = getNodeId(t);
+ EqualityNode& eqNode = getEqualityNode(eqNodeId);
+ EqualityNodeId classId = eqNode.getFind();
+
+ if (d_nodeIndividualTrigger[classId] != +null_id) {
+ // No need to keep it, just propagate the existing individual triggers
+ if (d_performNotify) {
+ d_notify.notify(t, d_nodes[d_nodeIndividualTrigger[classId]]);
+ }
+ } else {
+ // Add it to the list for backtracking
+ d_individualTriggers.push_back(classId);
+ d_individualTriggersSize = d_individualTriggersSize + 1;
+ // Mark the class id as a trigger
+ d_nodeIndividualTrigger[classId] = eqNodeId;
+ }
+}
+
+template <typename NotifyClass>
+bool EqualityEngine<NotifyClass>::isTriggerTerm(TNode t) const {
+ if (!hasTerm(t)) return false;
+ EqualityNodeId classId = getEqualityNode(t).getFind();
+ return d_nodeIndividualTrigger[classId] != +null_id;
+}
+
} // Namespace uf
} // Namespace theory
} // Namespace CVC4
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback