}
void ArithCongruenceManager::addSharedTerm(Node x){
- d_ee.addTriggerTerm(x);
+ d_ee.addTriggerTerm(x, THEORY_ARITH);
}
}/* CVC4::theory::arith namespace */
Unreachable();
}
- bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
+ 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));
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];
default:
// Variables etc
if (node.getType().isArray()) {
- d_equalityEngine.addTriggerTerm(node);
+ d_equalityEngine.addTriggerTerm(node, THEORY_ARRAY);
Assert(d_equalityEngine.getSize(node) == 1);
}
else {
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);
}
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;
}
}
// 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) {
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()) {
}
}
-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);
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);
};
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)) {
d_addedSharedTermsSize = d_addedSharedTermsSize + 1;
d_termsToTheories[search_pair] = theories;
if (!d_equalityEngine.hasTerm(term)) {
- d_equalityEngine.addTriggerTerm(term);
+ d_equalityEngine.addTriggerTerm(term, THEORY_UF);
}
} else {
Assert(theories != (*find).second);
return true;
}
- bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
+ bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) {
if (value) {
d_sharedTerms.mergeSharedTerms(t1, t2);
}
#include <string>
#include <iostream>
+#include <strings.h>
+
namespace CVC4 {
class TheoryEngine;
/** A set of all theories */
static const Set AllTheories = (1 << theory::THEORY_LAST) - 1;
+ /** Pops a first theory off the set */
+ static inline TheoryId setPop(Set& set) {
+ uint32_t i = ffs(set); // Find First Set (bit)
+ if (i == 0) { return THEORY_LAST; }
+ TheoryId id = (TheoryId)(i-1);
+ set = setRemove(id, set);
+ return id;
+ }
+
+ /** Returns the size of a set of theories */
+ static inline size_t setSize(Set set) {
+ size_t count = 0;
+ while (setPop(set) != THEORY_LAST) {
+ ++ count;
+ }
+ return count;
+ }
+
+ /** Returns the index size of a set of theories */
+ static inline size_t setIndex(TheoryId id, Set set) {
+ Assert (setContains(id, set));
+ size_t count = 0;
+ while (setPop(set) != id) {
+ ++ count;
+ }
+ return count;
+ }
+
/** Add the theory to the set. If no set specified, just returns a singleton set */
static inline Set setInsert(TheoryId theory, Set set = 0) {
return set | (1 << theory);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
addTerm(d_true);
addTerm(d_false);
+
+ d_triggerDatabaseAllocatedSize = 100000;
+ d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize);
}
+EqualityEngine::~EqualityEngine() throw(AssertionException) {
+ free(d_triggerDatabase);
+}
+
EqualityEngine::EqualityEngine(context::Context* context, std::string name)
: ContextNotifyObj(context)
, d_nodesCount(context, 0)
, d_assertedEqualitiesCount(context, 0)
, d_equalityTriggersCount(context, 0)
-, d_individualTriggersSize(context, 0)
, d_constantRepresentativesSize(context, 0)
, d_constantsSize(context, 0)
, d_stats(name)
+, d_triggerDatabaseSize(context, 0)
+, d_triggerTermSetUpdatesSize(context, 0)
{
init();
}
, d_nodesCount(context, 0)
, d_assertedEqualitiesCount(context, 0)
, d_equalityTriggersCount(context, 0)
-, d_individualTriggersSize(context, 0)
, d_constantRepresentativesSize(context, 0)
, d_constantsSize(context, 0)
, d_stats(name)
+, d_triggerDatabaseSize(context, 0)
+, d_triggerTermSetUpdatesSize(context, 0)
{
init();
}
// Add it to the equality graph
d_equalityGraph.push_back(+null_edge);
// Mark the no-individual trigger
- d_nodeIndividualTrigger.push_back(+null_id);
+ d_nodeIndividualTrigger.push_back(+null_set_id);
// Mark non-constant by default
d_constantRepresentative.push_back(node.isConst() ? newId : +null_id);
// Add the equality node to the nodes
}
// Notify the trigger term merges
- EqualityNodeId class2triggerId = d_nodeIndividualTrigger[class2Id];
- if (class2triggerId != +null_id) {
- EqualityNodeId class1triggerId = d_nodeIndividualTrigger[class1Id];
- if (class1triggerId == +null_id) {
- // If class1 is not an individual trigger, but class2 is, mark it
- d_nodeIndividualTrigger[class1Id] = class2triggerId;
+ TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id];
+ if (class2triggerRef != +null_set_id) {
+ TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id];
+ if (class1triggerRef == +null_set_id) {
+ // If class1 doesn't have individual triggers, but class2 does, mark it
+ d_nodeIndividualTrigger[class1Id] = class2triggerRef;
// Add it to the list for backtracking
- d_individualTriggers.push_back(class1Id);
- d_individualTriggersSize = d_individualTriggersSize + 1;
+ d_triggerTermSetUpdates.push_back(TriggerSetUpdate(class1Id, +null_set_id));
+ d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
} else {
- // Notify when done
- if (d_performNotify) {
- if (!d_notify.eqNotifyTriggerTermEquality(d_nodes[class1triggerId], d_nodes[class2triggerId], true)) {
- return false;
+ // Get the triggers
+ TriggerTermSet& class1triggers = getTriggerTermSet(class1triggerRef);
+ TriggerTermSet& class2triggers = getTriggerTermSet(class2triggerRef);
+
+ // Initialize the merged set
+ d_newSetTags = Theory::setUnion(class1triggers.tags, class2triggers.tags);
+ d_newSetTriggersSize = 0;
+
+ int i1 = 0;
+ int i2 = 0;
+ Theory::Set tags1 = class1triggers.tags;
+ Theory::Set tags2 = class2triggers.tags;
+ TheoryId tag1 = Theory::setPop(tags1);
+ TheoryId tag2 = Theory::setPop(tags2);
+
+ // Comparing the THEORY_LAST is OK because all other theories are
+ // smaller, and will therefore be preferred
+ while (tag1 != THEORY_LAST || tag2 != THEORY_LAST)
+ {
+ if (tag1 < tag2) {
+ // copy tag1
+ d_newSetTriggers[d_newSetTriggersSize++] = class1triggers.triggers[i1++];
+ tag1 = Theory::setPop(tags1);
+ } else if (tag1 > tag2) {
+ // copy tag2
+ d_newSetTriggers[d_newSetTriggersSize++] = class2triggers.triggers[i2++];
+ tag2 = Theory::setPop(tags2);
+ } else {
+ // copy tag1
+ EqualityNodeId tag1id = d_newSetTriggers[d_newSetTriggersSize++] = class1triggers.triggers[i1++];
+ // since they are both tagged notify of merge
+ if (d_performNotify) {
+ EqualityNodeId tag2id = class2triggers.triggers[i2++];
+ if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) {
+ return false;
+ }
+ }
+ // Next tags
+ tag1 = Theory::setPop(tags1);
+ tag2 = Theory::setPop(tags2);
}
- }
+ }
+
+ // Add the new trigger set, if different from previous one
+ if (class1triggers.tags != class2triggers.tags) {
+ // Add it to the list for backtracking
+ d_triggerTermSetUpdates.push_back(TriggerSetUpdate(class1Id, class1triggerRef));
+ d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
+ // Mark the the new set as a trigger
+ d_nodeIndividualTrigger[class1Id] = newTriggerTermSet();
+ }
}
}
d_equalityEdges.resize(2 * d_assertedEqualitiesCount);
}
- if (d_individualTriggers.size() > d_individualTriggersSize) {
+ if (d_triggerTermSetUpdates.size() > d_triggerTermSetUpdatesSize) {
// 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;
+ for (int i = d_triggerTermSetUpdates.size() - 1, i_end = d_triggerTermSetUpdatesSize; i >= i_end; -- i) {
+ const TriggerSetUpdate& update = d_triggerTermSetUpdates[i];
+ d_nodeIndividualTrigger[update.classId] = update.oldValue;
}
- d_individualTriggers.resize(d_individualTriggersSize);
+ d_triggerTermSetUpdates.resize(d_triggerTermSetUpdatesSize);
}
if (d_constantRepresentatives.size() > d_constantRepresentativesSize) {
return getEqualityNode(getEqualityNode(t).getFind()).getSize();
}
-void EqualityEngine::addTriggerTerm(TNode t)
+void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
{
- Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ")" << std::endl;
+ Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
+ Assert(tag != THEORY_LAST);
// Add the term if it's not already there
addTerm(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
+ // Possibly existing set of triggers
+ 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) {
- d_notify.eqNotifyTriggerTermEquality(t, d_nodes[d_nodeIndividualTrigger[classId]], true);
+ EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag);
+ d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true);
}
} else {
+
+ // Setup the data for the new set
+ if (triggerSetRef != null_set_id) {
+ // Get the existing set
+ TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef);
+ // Initialize the new set for copy/insert
+ d_newSetTags = Theory::setInsert(tag, triggerSet.tags);
+ d_newSetTriggersSize = 0;
+ // Copy into to new one, and insert the new tag/id
+ unsigned i = 0;
+ Theory::Set tags = d_newSetTags;
+ TheoryId current;
+ while ((current = Theory::setPop(tags)) != THEORY_LAST) {
+ // Remove from the tags
+ tags = Theory::setRemove(current, tags);
+ // Insert the id into the triggers
+ d_newSetTriggers[d_newSetTriggersSize++] =
+ current == tag ? eqNodeId : triggerSet.triggers[i++];
+ }
+ } else {
+ // Setup a singleton
+ d_newSetTags = Theory::setInsert(tag);
+ d_newSetTriggers[0] = eqNodeId;
+ d_newSetTriggersSize = 1;
+ }
+
// 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;
+ d_triggerTermSetUpdates.push_back(TriggerSetUpdate(classId, triggerSetRef));
+ d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
+ // Mark the the new set as a trigger
+ d_nodeIndividualTrigger[classId] = newTriggerTermSet();
}
}
-bool EqualityEngine::isTriggerTerm(TNode t) const {
+bool EqualityEngine::isTriggerTerm(TNode t, TheoryId tag) const {
if (!hasTerm(t)) return false;
EqualityNodeId classId = getEqualityNode(t).getFind();
- return d_nodeIndividualTrigger[classId] != +null_id;
+ TriggerTermSetRef triggerSetRef = d_nodeIndividualTrigger[classId];
+ return triggerSetRef != +null_set_id && getTriggerTermSet(triggerSetRef).hasTrigger(tag);
}
-TNode EqualityEngine::getTriggerTermRepresentative(TNode t) const {
- Assert(isTriggerTerm(t));
+TNode EqualityEngine::getTriggerTermRepresentative(TNode t, TheoryId tag) const {
+ Assert(isTriggerTerm(t, tag));
EqualityNodeId classId = getEqualityNode(t).getFind();
- return d_nodes[d_nodeIndividualTrigger[classId]];
+ const TriggerTermSet& triggerSet = getTriggerTermSet(d_nodeIndividualTrigger[classId]);
+ unsigned i = 0;
+ Theory::Set tags = triggerSet.tags;
+ while (Theory::setPop(tags) != tag) {
+ ++ i;
+ }
+ return d_nodes[triggerSet.triggers[i]];
}
void EqualityEngine::storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId) {
}
}
+EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet() {
+ // Size of the required set
+ size_t size = sizeof(TriggerTermSet) + d_newSetTriggersSize*sizeof(EqualityNodeId);
+ // Align the size
+ size = (size + 7) & ~((size_t)7);
+ // Reallocate if necessary
+ if (d_triggerDatabaseSize + size > d_triggerDatabaseAllocatedSize) {
+ d_triggerDatabaseAllocatedSize *= 2;
+ d_triggerDatabase = (char*) realloc(d_triggerDatabase, d_triggerDatabaseAllocatedSize);
+ }
+ // New reference
+ TriggerTermSetRef newTriggerSetRef = d_triggerDatabaseSize;
+ // Update the size
+ d_triggerDatabaseSize = d_triggerDatabaseSize + size;
+ // Copy the information
+ TriggerTermSet& newSet = getTriggerTermSet(newTriggerSetRef);
+ newSet.tags = d_newSetTags;
+ for (unsigned i = 0; i < d_newSetTriggersSize; ++i) {
+ newSet.triggers[i] = d_newSetTriggers[i];
+ }
+ // Return the new reference
+ return newTriggerSetRef;
+}
+
+
} // Namespace uf
} // Namespace theory
} // Namespace CVC4
#include "util/output.h"
#include "util/stats.h"
#include "theory/rewriter.h"
+#include "theory/theory.h"
namespace CVC4 {
namespace theory {
/**
* Notifies about the merge of two trigger terms.
*
+ * @param tag the theory that both triggers were tagged with
* @param t1 a term marked as trigger
* @param t2 a term marked as trigger
* @param value true if equal, false if dis-equal
*/
- virtual bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) = 0;
+ virtual bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) = 0;
/**
* Notifies about the merge of two constant terms.
public:
bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
- bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) { return true; }
+ bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { return true; }
};
*/
std::vector<TriggerId> d_nodeTriggers;
- /**
- * List of terms that are marked as individual triggers.
- */
- std::vector<EqualityNodeId> d_individualTriggers;
-
- /**
- * Size of the individual triggers list.
- */
- context::CDO<unsigned> d_individualTriggersSize;
-
- /**
- * Map from ids to the individual trigger id representative.
- */
- std::vector<EqualityNodeId> d_nodeIndividualTrigger;
-
/**
* Map from ids to the id of the constant that is the representative.
*/
*/
void init();
+ /** Set of trigger terms */
+ struct TriggerTermSet {
+ /** Set of theories in this set */
+ Theory::Set tags;
+ /** The trigger terms */
+ EqualityNodeId triggers[0];
+ /** Returns the theory tags */
+ Theory::Set hasTrigger(TheoryId tag) const { return Theory::setContains(tag, tags); }
+ /** Returns a trigger by tag */
+ EqualityNodeId getTrigger(TheoryId tag) const {
+ return triggers[Theory::setIndex(tag, tags)];
+ }
+ };
+
+ /** Internal tags for creating a new set */
+ Theory::Set d_newSetTags;
+
+ /** Internal triggers for creating a new set */
+ EqualityNodeId d_newSetTriggers[THEORY_LAST];
+
+ /** Size of the internal triggers array */
+ unsigned d_newSetTriggersSize;
+
+ /** The information about trigger terms is stored in this easily maintained memory. */
+ char* d_triggerDatabase;
+
+ /** Allocated size of the trigger term database */
+ size_t d_triggerDatabaseAllocatedSize ;
+
+ /** Reference for the trigger terms set */
+ typedef size_t TriggerTermSetRef;
+
+ /** Null reference */
+ static const TriggerTermSetRef null_set_id = (size_t)(-1);
+
+ /** Create new trigger term set based on the internally set information */
+ TriggerTermSetRef newTriggerTermSet();
+
+ /** Get the trigger set give a reference */
+ TriggerTermSet& getTriggerTermSet(TriggerTermSetRef ref) {
+ Assert(ref < d_triggerDatabaseSize);
+ return *(reinterpret_cast<TriggerTermSet*>(d_triggerDatabase + ref));
+ }
+
+ /** Get the trigger set give a reference */
+ const TriggerTermSet& getTriggerTermSet(TriggerTermSetRef ref) const {
+ Assert(ref < d_triggerDatabaseSize);
+ return *(reinterpret_cast<const TriggerTermSet*>(d_triggerDatabase + ref));
+ }
+
+ /** Used part of the trigger term database */
+ context::CDO<size_t> d_triggerDatabaseSize;
+
+ struct TriggerSetUpdate {
+ EqualityNodeId classId;
+ TriggerTermSetRef oldValue;
+ TriggerSetUpdate(EqualityNodeId classId = null_id, TriggerTermSetRef oldValue = null_set_id)
+ : classId(classId), oldValue(oldValue) {}
+ };
+
+ /**
+ * List of trigger updates for backtracking.
+ */
+ std::vector<TriggerSetUpdate> d_triggerTermSetUpdates;
+
+ /**
+ * Size of the individual triggers list.
+ */
+ context::CDO<unsigned> d_triggerTermSetUpdatesSize;
+
+ /**
+ * Map from ids to the individual trigger set representatives.
+ */
+ std::vector<TriggerTermSetRef> d_nodeIndividualTrigger;
+
public:
/**
/**
* Just a destructor.
*/
- virtual ~EqualityEngine() throw(AssertionException) {}
+ virtual ~EqualityEngine() throw(AssertionException);
/**
* Adds a term to the term database.
void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions);
/**
- * Add term to the trigger terms. The notify class will get notified
- * when two trigger terms become equal or dis-equal. The notification
- * will not happen on all the terms, but only on the ones that are
- * represent the class.
+ * Add term to the set of trigger terms with a corresponding tag. The notify class will get
+ * notified when two trigger terms with the same tag become equal or dis-equal. The notification
+ * will not happen on all the terms, but only on the ones that are represent the class. Note that
+ * a term can be added more than once with different tags, and each tag apperance will merit
+ * it's own notification.
+ *
+ * @param t the trigger term
+ * @param tag tag for this trigger (do NOT use THEORY_LAST)
*/
- void addTriggerTerm(TNode t);
+ void addTriggerTerm(TNode t, TheoryId theoryTag);
/**
* Returns true if t is a trigger term or in the same equivalence
* class as some other trigger term.
*/
- bool isTriggerTerm(TNode t) const;
+ bool isTriggerTerm(TNode t, TheoryId theoryTag) const;
/**
* Returns the representative trigger term of the given term.
*
* @param t the term to check where isTriggerTerm(t) should be true
*/
- TNode getTriggerTermRepresentative(TNode t) const;
+ TNode getTriggerTermRepresentative(TNode t, TheoryId theoryTag) const;
/**
* Adds a notify trigger for equality. When equality becomes true eqNotifyTriggerEquality
void TheoryUF::addSharedTerm(TNode t) {
Debug("uf::sharing") << "TheoryUF::addSharedTerm(" << t << ")" << std::endl;
- d_equalityEngine.addTriggerTerm(t);
+ d_equalityEngine.addTriggerTerm(t, THEORY_UF);
}
void TheoryUF::computeCareGraph() {
continue;
}
- if (!d_equalityEngine.isTriggerTerm(x) || !d_equalityEngine.isTriggerTerm(y)) {
+ if (!d_equalityEngine.isTriggerTerm(x, THEORY_UF) || !d_equalityEngine.isTriggerTerm(y, THEORY_UF)) {
// Not connected to shared terms, we don't care
continue;
}
// 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_UF);
+ TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
switch (eqStatusDomain) {
}
}
- bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
- Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl;
+ bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
+ Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << std::endl;
if (value) {
return d_uf.propagate(t1.eqNode(t2));
} else {
projects / cvc5.git / commitdiff