diff options
Diffstat (limited to 'src/theory/sets/theory_sets.h')
-rw-r--r-- | src/theory/sets/theory_sets.h | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index fce57ca6c..4d0c74516 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -25,6 +25,7 @@ #include "theory/sets/skolem_cache.h" #include "theory/sets/solver_state.h" #include "theory/theory.h" +#include "theory/theory_eq_notify.h" #include "theory/uf/equality_engine.h" namespace CVC4 { @@ -82,16 +83,13 @@ class TheorySets : public Theory private: /** Functions to handle callbacks from equality engine */ - class NotifyClass : public eq::EqualityEngineNotify + class NotifyClass : public TheoryEqNotifyClass { public: - NotifyClass(TheorySetsPrivate& theory) : d_theory(theory) {} - bool eqNotifyTriggerPredicate(TNode predicate, bool value) override; - bool eqNotifyTriggerTermEquality(TheoryId tag, - TNode t1, - TNode t2, - bool value) override; - void eqNotifyConstantTermMerge(TNode t1, TNode t2) override; + NotifyClass(TheorySetsPrivate& theory, TheoryInferenceManager& im) + : TheoryEqNotifyClass(im), d_theory(theory) + { + } void eqNotifyNewClass(TNode t) override; void eqNotifyMerge(TNode t1, TNode t2) override; void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override; |