diff options
Diffstat (limited to 'src/theory/shared_terms_database.h')
-rw-r--r-- | src/theory/shared_terms_database.h | 27 |
1 files changed, 16 insertions, 11 deletions
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index 5ca625751..bc4db97ee 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -78,28 +78,35 @@ private: SharedTermsDatabase& d_sharedTerms; public: EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {} - bool eqNotifyTriggerEquality(TNode equality, bool value) { + bool eqNotifyTriggerEquality(TNode equality, bool value) override + { d_sharedTerms.propagateEquality(equality, value); return true; } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + bool eqNotifyTriggerPredicate(TNode predicate, bool value) override + { Unreachable(); return true; } - bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) { + bool eqNotifyTriggerTermEquality(theory::TheoryId tag, + TNode t1, + TNode t2, + bool value) override + { return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value); } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) { + void eqNotifyConstantTermMerge(TNode t1, TNode t2) override + { d_sharedTerms.conflict(t1, t2, true); } - void eqNotifyNewClass(TNode t) { } - void eqNotifyPreMerge(TNode t1, TNode t2) { } - void eqNotifyPostMerge(TNode t1, TNode t2) { } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { } + void eqNotifyNewClass(TNode t) override {} + void eqNotifyPreMerge(TNode t1, TNode t2) override {} + void eqNotifyPostMerge(TNode t1, TNode t2) override {} + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {} }; /** The notify class for d_equalityEngine */ @@ -245,9 +252,7 @@ protected: /** * This method gets called on backtracks from the context manager. */ - void contextNotifyPop() { - backtrack(); - } + void contextNotifyPop() override { backtrack(); } }; } |