diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-28 18:01:34 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-28 18:01:34 -0500 |
commit | 960147384b7953a352ca9c721f9b93bdac4ff178 (patch) | |
tree | 2bbc6df18d6cebbe94f9cce9732fcc6c6096e341 /src/theory/uf | |
parent | 48dfcfd271ff9fa04766e29fb82ba83290da1ad8 (diff) |
Replace Theory::Set with TheoryIdSet (#4959)
This makes it so that equality_engine.h does not include theory.h. This is a bad dependency since Theory contains EqualityEngine.
This dependency between equality engine and theory was due to the use of a helper (Theory::Set) for representing sets of theories that is inlined into Theory. This PR moves this definition and utilities to theory_id.h.
It fixes the resulting include dependencies which are broken by changing the include theory.h -> theory_id.h in equality_engine.h.
This avoids a circular dependency in the includes between Theory -> InferenceManager -> ProofEqualityEngine -> EqualityEngine -> Theory.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 131 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.h | 36 | ||||
-rw-r--r-- | src/theory/uf/ho_extension.h | 1 | ||||
-rw-r--r-- | src/theory/uf/proof_equality_engine.h | 1 |
4 files changed, 103 insertions, 66 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 7bb857425..dd142edf4 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -17,6 +17,8 @@ #include "theory/uf/equality_engine.h" +#include "options/smt_options.h" +#include "proof/proof_manager.h" #include "smt/smt_statistics_registry.h" namespace CVC4 { @@ -386,13 +388,13 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { // Non-Boolean constants are trigger terms for all tags EqualityNodeId tId = getNodeId(t); // Setup the new set - Theory::Set newSetTags = 0; + TheoryIdSet newSetTags = 0; EqualityNodeId newSetTriggers[THEORY_LAST]; unsigned newSetTriggersSize = THEORY_LAST; for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++currentTheory) { - newSetTags = Theory::setInsert(currentTheory, newSetTags); + newSetTags = TheoryIdSetUtil::setInsert(currentTheory, newSetTags); newSetTriggers[currentTheory] = tId; } // Add it to the list for backtracking @@ -534,17 +536,17 @@ bool EqualityEngine::assertEquality(TNode eq, TriggerTermSet& aTriggerTerms = getTriggerTermSet(aTriggerRef); TriggerTermSet& bTriggerTerms = getTriggerTermSet(bTriggerRef); // Go through and notify the shared dis-equalities - Theory::Set aTags = aTriggerTerms.d_tags; - Theory::Set bTags = bTriggerTerms.d_tags; - TheoryId aTag = Theory::setPop(aTags); - TheoryId bTag = Theory::setPop(bTags); + TheoryIdSet aTags = aTriggerTerms.d_tags; + TheoryIdSet bTags = bTriggerTerms.d_tags; + TheoryId aTag = TheoryIdSetUtil::setPop(aTags); + TheoryId bTag = TheoryIdSetUtil::setPop(bTags); int a_i = 0, b_i = 0; while (aTag != THEORY_LAST && bTag != THEORY_LAST) { if (aTag < bTag) { - aTag = Theory::setPop(aTags); + aTag = TheoryIdSetUtil::setPop(aTags); ++ a_i; } else if (aTag > bTag) { - bTag = Theory::setPop(bTags); + bTag = TheoryIdSetUtil::setPop(bTags); ++ b_i; } else { // Same tags, notify @@ -567,8 +569,8 @@ bool EqualityEngine::assertEquality(TNode eq, } } // Pop the next tags - aTag = Theory::setPop(aTags); - bTag = Theory::setPop(bTags); + aTag = TheoryIdSetUtil::setPop(aTags); + bTag = TheoryIdSetUtil::setPop(bTags); } } } @@ -618,12 +620,12 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Trigger set of class 1 TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id]; - Theory::Set class1Tags = class1triggerRef == null_set_id + TheoryIdSet class1Tags = class1triggerRef == null_set_id ? 0 : getTriggerTermSet(class1triggerRef).d_tags; // Trigger set of class 2 TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id]; - Theory::Set class2Tags = class2triggerRef == null_set_id + TheoryIdSet class2Tags = class2triggerRef == null_set_id ? 0 : getTriggerTermSet(class2triggerRef).d_tags; @@ -633,8 +635,10 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect TaggedEqualitiesSet class1disequalitiesToNotify; // Individual tags - Theory::Set class1OnlyTags = Theory::setDifference(class1Tags, class2Tags); - Theory::Set class2OnlyTags = Theory::setDifference(class2Tags, class1Tags); + TheoryIdSet class1OnlyTags = + TheoryIdSetUtil::setDifference(class1Tags, class2Tags); + TheoryIdSet class2OnlyTags = + TheoryIdSetUtil::setDifference(class2Tags, class1Tags); // Only get disequalities if they are not both constant if (!class1isConstant || !class2isConstant) { @@ -760,17 +764,17 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect TriggerTermSet& class2triggers = getTriggerTermSet(class2triggerRef); // Initialize the merged set - Theory::Set newSetTags = - Theory::setUnion(class1triggers.d_tags, class2triggers.d_tags); + TheoryIdSet newSetTags = TheoryIdSetUtil::setUnion(class1triggers.d_tags, + class2triggers.d_tags); EqualityNodeId newSetTriggers[THEORY_LAST]; unsigned newSetTriggersSize = 0; int i1 = 0; int i2 = 0; - Theory::Set tags1 = class1triggers.d_tags; - Theory::Set tags2 = class2triggers.d_tags; - TheoryId tag1 = Theory::setPop(tags1); - TheoryId tag2 = Theory::setPop(tags2); + TheoryIdSet tags1 = class1triggers.d_tags; + TheoryIdSet tags2 = class2triggers.d_tags; + TheoryId tag1 = TheoryIdSetUtil::setPop(tags1); + TheoryId tag2 = TheoryIdSetUtil::setPop(tags2); // Comparing the THEORY_LAST is OK because all other theories are // smaller, and will therefore be preferred @@ -780,12 +784,12 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // copy tag1 newSetTriggers[newSetTriggersSize++] = class1triggers.d_triggers[i1++]; - tag1 = Theory::setPop(tags1); + tag1 = TheoryIdSetUtil::setPop(tags1); } else if (tag1 > tag2) { // copy tag2 newSetTriggers[newSetTriggersSize++] = class2triggers.d_triggers[i2++]; - tag2 = Theory::setPop(tags2); + tag2 = TheoryIdSetUtil::setPop(tags2); } else { // copy tag1 EqualityNodeId tag1id = newSetTriggers[newSetTriggersSize++] = @@ -798,8 +802,8 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect } } // Next tags - tag1 = Theory::setPop(tags1); - tag2 = Theory::setPop(tags2); + tag1 = TheoryIdSetUtil::setPop(tags1); + tag2 = TheoryIdSetUtil::setPop(tags2); } } @@ -1252,6 +1256,7 @@ void EqualityEngine::explainPredicate(TNode p, bool polarity, void EqualityEngine::explainLit(TNode lit, std::vector<TNode>& assumptions) { + Assert(lit.getKind() != kind::AND); bool polarity = lit.getKind() != kind::NOT; TNode atom = polarity ? lit : lit[0]; std::vector<TNode> tassumptions; @@ -1281,6 +1286,7 @@ void EqualityEngine::explainLit(TNode lit, std::vector<TNode>& assumptions) if (std::find(assumptions.begin(), assumptions.end(), a) == assumptions.end()) { + Assert(!a.isNull()); assumptions.push_back(a); } } @@ -1288,13 +1294,13 @@ void EqualityEngine::explainLit(TNode lit, std::vector<TNode>& assumptions) Node EqualityEngine::mkExplainLit(TNode lit) { + Assert(lit.getKind() != kind::AND); std::vector<TNode> assumptions; explainLit(lit, assumptions); Node ret; - NodeManager* nm = NodeManager::currentNM(); if (assumptions.empty()) { - ret = nm->mkConst(true); + ret = NodeManager::currentNM()->mkConst(true); } else if (assumptions.size() == 1) { @@ -1302,7 +1308,7 @@ Node EqualityEngine::mkExplainLit(TNode lit) } else { - ret = nm->mkNode(kind::AND, assumptions); + ret = NodeManager::currentNM()->mkNode(kind::AND, assumptions); } return ret; } @@ -2267,11 +2273,11 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) // uselists that have been asserted to false. All the representatives appearing on the other // side of such disequalities, that have the tag on, are put in a set. TaggedEqualitiesSet disequalitiesToNotify; - Theory::Set tags = Theory::setInsert(tag); + TheoryIdSet tags = TheoryIdSetUtil::setInsert(tag); getDisequalities(!d_isConstant[classId], classId, tags, disequalitiesToNotify); // Trigger data - Theory::Set newSetTags; + TheoryIdSet newSetTags; EqualityNodeId newSetTriggers[THEORY_LAST]; unsigned newSetTriggersSize; @@ -2280,23 +2286,23 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag) // Get the existing set TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef); // Initialize the new set for copy/insert - newSetTags = Theory::setInsert(tag, triggerSet.d_tags); + newSetTags = TheoryIdSetUtil::setInsert(tag, triggerSet.d_tags); newSetTriggersSize = 0; // Copy into to new one, and insert the new tag/id unsigned i = 0; - Theory::Set tags2 = newSetTags; + TheoryIdSet tags2 = newSetTags; TheoryId current; - while ((current = Theory::setPop(tags2)) != THEORY_LAST) + while ((current = TheoryIdSetUtil::setPop(tags2)) != THEORY_LAST) { // Remove from the tags - tags2 = Theory::setRemove(current, tags2); + tags2 = TheoryIdSetUtil::setRemove(current, tags2); // Insert the id into the triggers newSetTriggers[newSetTriggersSize++] = current == tag ? eqNodeId : triggerSet.d_triggers[i++]; } } else { // Setup a singleton - newSetTags = Theory::setInsert(tag); + newSetTags = TheoryIdSetUtil::setInsert(tag); newSetTriggers[0] = eqNodeId; newSetTriggersSize = 1; } @@ -2326,8 +2332,9 @@ TNode EqualityEngine::getTriggerTermRepresentative(TNode t, TheoryId tag) const EqualityNodeId classId = getEqualityNode(t).getFind(); const TriggerTermSet& triggerSet = getTriggerTermSet(d_nodeIndividualTrigger[classId]); unsigned i = 0; - Theory::Set tags = triggerSet.d_tags; - while (Theory::setPop(tags) != tag) { + TheoryIdSet tags = triggerSet.d_tags; + while (TheoryIdSetUtil::setPop(tags) != tag) + { ++ i; } return d_nodes[triggerSet.d_triggers[i]]; @@ -2381,7 +2388,11 @@ void EqualityEngine::getUseListTerms(TNode t, std::set<TNode>& output) { } } -EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet(Theory::Set newSetTags, EqualityNodeId* newSetTriggers, unsigned newSetTriggersSize) { +EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet( + TheoryIdSet newSetTags, + EqualityNodeId* newSetTriggers, + unsigned newSetTriggersSize) +{ // Size of the required set size_t size = sizeof(TriggerTermSet) + newSetTriggersSize*sizeof(EqualityNodeId); // Align the size @@ -2429,7 +2440,7 @@ bool EqualityEngine::hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId } Assert(d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end()) << "We propagated but there is no proof"; - bool result = Theory::setContains(tag, (*it).second); + bool result = TheoryIdSetUtil::setContains(tag, (*it).second); Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => " << (result ? "true" : "false") << std::endl; return result; } @@ -2446,12 +2457,12 @@ void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhs EqualityPair pair2(rhsId, lhsId); // Store the fact that we've propagated this already - Theory::Set notified = 0; + TheoryIdSet notified = 0; PropagatedDisequalitiesMap::const_iterator find = d_propagatedDisequalities.find(pair1); if (find == d_propagatedDisequalities.end()) { - notified = Theory::setInsert(tag); + notified = TheoryIdSetUtil::setInsert(tag); } else { - notified = Theory::setInsert(tag, (*find).second); + notified = TheoryIdSetUtil::setInsert(tag, (*find).second); } d_propagatedDisequalities[pair1] = notified; d_propagatedDisequalities[pair2] = notified; @@ -2493,12 +2504,16 @@ void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhs } } -void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classId, Theory::Set inputTags, TaggedEqualitiesSet& out) { +void EqualityEngine::getDisequalities(bool allowConstants, + EqualityNodeId classId, + TheoryIdSet inputTags, + TaggedEqualitiesSet& out) +{ // Must be empty on input Assert(out.size() == 0); // The class we are looking for, shouldn't have any of the tags we are looking for already set Assert(d_nodeIndividualTrigger[classId] == null_set_id - || Theory::setIntersection( + || TheoryIdSetUtil::setIntersection( getTriggerTermSet(d_nodeIndividualTrigger[classId]).d_tags, inputTags) == 0); @@ -2556,8 +2571,8 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI // Tags of the other gey TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef); // We only care if there are things in inputTags that is also in toCompareTags - Theory::Set commonTags = - Theory::setIntersection(inputTags, toCompareTriggerSet.d_tags); + TheoryIdSet commonTags = TheoryIdSetUtil::setIntersection( + inputTags, toCompareTriggerSet.d_tags); if (commonTags) { out.push_back(TaggedEquality(funId, toCompareTriggerSetRef, lhs)); } @@ -2573,8 +2588,11 @@ void EqualityEngine::getDisequalities(bool allowConstants, EqualityNodeId classI } -bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify) { - +bool EqualityEngine::propagateTriggerTermDisequalities( + TheoryIdSet tags, + TriggerTermSetRef triggerSetRef, + const TaggedEqualitiesSet& disequalitiesToNotify) +{ // No tags, no food if (!tags) { return !d_done; @@ -2592,8 +2610,8 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger const TaggedEquality& disequalityInfo = *it; const TriggerTermSet& disequalityTriggerSet = getTriggerTermSet(disequalityInfo.d_triggerSetRef); - Theory::Set commonTags = - Theory::setIntersection(disequalityTriggerSet.d_tags, tags); + TheoryIdSet commonTags = + TheoryIdSetUtil::setIntersection(disequalityTriggerSet.d_tags, tags); Assert(commonTags); // This is the actual function const FunctionApplication& fun = @@ -2608,7 +2626,10 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger } // Go through the tags, and add the disequalities TheoryId currentTag; - while (!d_done && ((currentTag = Theory::setPop(commonTags)) != THEORY_LAST)) { + while ( + !d_done + && ((currentTag = TheoryIdSetUtil::setPop(commonTags)) != THEORY_LAST)) + { // Get the tag representative EqualityNodeId tagRep = disequalityTriggerSet.getTrigger(currentTag); EqualityNodeId myRep = triggerSet.getTrigger(currentTag); @@ -2636,6 +2657,16 @@ bool EqualityEngine::propagateTriggerTermDisequalities(Theory::Set tags, Trigger return !d_done; } +TheoryIdSet EqualityEngine::TriggerTermSet::hasTrigger(TheoryId tag) const +{ + return TheoryIdSetUtil::setContains(tag, d_tags); +} + +EqualityNodeId EqualityEngine::TriggerTermSet::getTrigger(TheoryId tag) const +{ + return d_triggers[TheoryIdSetUtil::setIndex(tag, d_tags)]; +} + } // Namespace uf } // Namespace theory } // Namespace CVC4 diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 91dae2509..19a10eba8 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -32,7 +32,7 @@ #include "expr/kind_map.h" #include "expr/node.h" #include "theory/rewriter.h" -#include "theory/theory.h" +#include "theory/theory_id.h" #include "theory/uf/eq_proof.h" #include "theory/uf/equality_engine_iterator.h" #include "theory/uf/equality_engine_notify.h" @@ -500,18 +500,13 @@ private: /** Set of trigger terms */ struct TriggerTermSet { /** Set of theories in this set */ - Theory::Set d_tags; + TheoryIdSet d_tags; /** The trigger terms */ EqualityNodeId d_triggers[0]; /** Returns the theory tags */ - Theory::Set hasTrigger(TheoryId tag) const - { - return Theory::setContains(tag, d_tags); - } + TheoryIdSet hasTrigger(TheoryId tag) const; /** Returns a trigger by tag */ - EqualityNodeId getTrigger(TheoryId tag) const { - return d_triggers[Theory::setIndex(tag, d_tags)]; - } + EqualityNodeId getTrigger(TheoryId tag) const; };/* struct EqualityEngine::TriggerTermSet */ /** Are the constants triggers */ @@ -535,7 +530,9 @@ private: static const TriggerTermSetRef null_set_id = (TriggerTermSetRef)(-1); /** Create new trigger term set based on the internally set information */ - TriggerTermSetRef newTriggerTermSet(Theory::Set newSetTags, EqualityNodeId* newSetTriggers, unsigned newSetTriggersSize); + TriggerTermSetRef newTriggerTermSet(TheoryIdSet newSetTags, + EqualityNodeId* newSetTriggers, + unsigned newSetTriggersSize); /** Get the trigger set give a reference */ TriggerTermSet& getTriggerTermSet(TriggerTermSetRef ref) { @@ -607,7 +604,9 @@ private: /** * Map from equalities to the tags that have received the notification. */ - typedef context::CDHashMap<EqualityPair, Theory::Set, EqualityPairHashFunction> PropagatedDisequalitiesMap; + typedef context:: + CDHashMap<EqualityPair, TheoryIdSet, EqualityPairHashFunction> + PropagatedDisequalitiesMap; PropagatedDisequalitiesMap d_propagatedDisequalities; /** @@ -659,14 +658,19 @@ private: * @param inputTags the tags to filter the equalities * @param out the output equalities, as described above */ - void getDisequalities(bool allowConstants, EqualityNodeId classId, Theory::Set inputTags, TaggedEqualitiesSet& out); + void getDisequalities(bool allowConstants, + EqualityNodeId classId, + TheoryIdSet inputTags, + TaggedEqualitiesSet& out); /** * Propagates the remembered disequalities with given tags the original triggers for those tags, * and the set of disequalities produced by above. */ - bool propagateTriggerTermDisequalities(Theory::Set tags, - TriggerTermSetRef triggerSetRef, const TaggedEqualitiesSet& disequalitiesToNotify); + bool propagateTriggerTermDisequalities( + TheoryIdSet tags, + TriggerTermSetRef triggerSetRef, + const TaggedEqualitiesSet& disequalitiesToNotify); /** Name of the equality engine */ std::string d_name; @@ -792,8 +796,8 @@ private: */ void explainLit(TNode lit, std::vector<TNode>& assumptions); /** - * Explain literal, return the conjunction. This method relies on the above - * method. + * Explain literal, return the explanation as a conjunction. This method + * relies on the above method. */ Node mkExplainLit(TNode lit); //--------------------------- end standard safe explanation methods diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h index dc37808c9..25cb3623b 100644 --- a/src/theory/uf/ho_extension.h +++ b/src/theory/uf/ho_extension.h @@ -22,6 +22,7 @@ #include "context/cdo.h" #include "expr/node.h" #include "theory/theory_model.h" +#include "theory/theory_state.h" namespace CVC4 { namespace theory { diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h index 2ee379509..b71f72c53 100644 --- a/src/theory/uf/proof_equality_engine.h +++ b/src/theory/uf/proof_equality_engine.h @@ -21,6 +21,7 @@ #include <vector> #include "context/cdhashmap.h" +#include "context/cdhashset.h" #include "expr/lazy_proof.h" #include "expr/node.h" #include "expr/proof_node.h" |