diff options
| -rw-r--r-- | src/theory/arith/congruence_manager.cpp | 2 | ||||
| -rw-r--r-- | src/theory/arith/congruence_manager.h | 2 | ||||
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 12 | ||||
| -rw-r--r-- | src/theory/arrays/theory_arrays.h | 2 | ||||
| -rw-r--r-- | src/theory/bv/bv_subtheory.cpp | 2 | ||||
| -rw-r--r-- | src/theory/bv/bv_subtheory.h | 4 | ||||
| -rw-r--r-- | src/theory/shared_terms_database.cpp | 2 | ||||
| -rw-r--r-- | src/theory/shared_terms_database.h | 2 | ||||
| -rw-r--r-- | src/theory/theory.h | 30 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 185 | ||||
| -rw-r--r-- | src/theory/uf/equality_engine.h | 116 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 8 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.h | 4 |
13 files changed, 292 insertions, 79 deletions
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 39468e928..649e34134 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -300,7 +300,7 @@ void ArithCongruenceManager::equalsConstant(Constraint lb, Constraint ub){ } void ArithCongruenceManager::addSharedTerm(Node x){ - d_ee.addTriggerTerm(x); + d_ee.addTriggerTerm(x, THEORY_ARITH); } }/* CVC4::theory::arith namespace */ diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 18ecbeb9d..5e4616628 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -56,7 +56,7 @@ private: 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)); 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()) { 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)) { diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index 235d6959c..90037b90b 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -58,7 +58,7 @@ void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theo 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); diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index b04f835e7..c044097ff 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -117,7 +117,7 @@ private: 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); } diff --git a/src/theory/theory.h b/src/theory/theory.h index 9ac07d849..36255d1d6 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -38,6 +38,8 @@ #include <string> #include <iostream> +#include <strings.h> + namespace CVC4 { class TheoryEngine; @@ -612,6 +614,34 @@ public: /** 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); diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index f9220c7f3..2527893ff 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -62,8 +62,15 @@ void EqualityEngine::init() { 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) @@ -74,10 +81,11 @@ EqualityEngine::EqualityEngine(context::Context* context, std::string name) , 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(); } @@ -91,10 +99,11 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c , 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(); } @@ -162,7 +171,7 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { // 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 @@ -423,22 +432,67 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect } // 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(); + } } } @@ -513,12 +567,13 @@ void EqualityEngine::backtrack() { 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) { @@ -935,9 +990,10 @@ size_t EqualityEngine::getSize(TNode t) 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); @@ -947,31 +1003,67 @@ void EqualityEngine::addTriggerTerm(TNode 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) { @@ -1010,6 +1102,31 @@ void EqualityEngine::getUseListTerms(TNode t, std::set<TNode>& output) { } } +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 diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 047e9de49..c59436aaf 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -32,6 +32,7 @@ #include "util/output.h" #include "util/stats.h" #include "theory/rewriter.h" +#include "theory/theory.h" namespace CVC4 { namespace theory { @@ -244,11 +245,12 @@ public: /** * 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. @@ -267,7 +269,7 @@ class EqualityEngineNotifyNone : public EqualityEngineNotify { 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; } }; @@ -557,21 +559,6 @@ private: 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. */ std::vector<EqualityNodeId> d_constantRepresentative; @@ -666,6 +653,81 @@ private: */ 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: /** @@ -681,7 +743,7 @@ public: /** * Just a destructor. */ - virtual ~EqualityEngine() throw(AssertionException) {} + virtual ~EqualityEngine() throw(AssertionException); /** * Adds a term to the term database. @@ -764,25 +826,29 @@ public: 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 diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 7f173a0c4..0b9e1b3a7 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -345,7 +345,7 @@ EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) { 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() { @@ -405,14 +405,14 @@ 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) { diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 9017928b7..1dfcb86f0 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -63,8 +63,8 @@ public: } } - 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 { |