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/equality_engine.h | |
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/equality_engine.h')
-rw-r--r-- | src/theory/uf/equality_engine.h | 36 |
1 files changed, 20 insertions, 16 deletions
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 |