diff options
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 |