diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-14 13:07:17 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-14 13:07:17 -0500 |
| commit | 42cd0a7bcbe993870d76d8cc9db7acc0a9ae70f9 (patch) | |
| tree | 1335e7efe55bb0df162c03b37e77c364efde666a /src/theory/strings | |
| parent | ee055dddf887ed001fee1834ba845fb81e20e27e (diff) | |
Simplify equality engine notifications (#4896)
Previously, there was methods for being informed just before and just after equivalence classes are merged (eqNotifyPreMerge and eqNotifyPostMerge). The purpose of this was to allow e.g. the theory to inspect the equivalence classes in question before the equality engine modified them. However this is no longer used, and moreover is discouraged since Theory should generally buffer their usage of EqualityEngine while it is making internal calls.
TheoryStrings was the only theory to use eqNotifyPreMerge (somewhat arbitrarily), all others used eqNotifyPostMerge. This makes post-merge the default, renames it to eqNotifyMerge and removes pre notifications.
This will simplify the work of the new theory combination methods as well as leading to fewer spurious calls to callbacks in equality engine.
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/solver_state.cpp | 2 | ||||
| -rw-r--r-- | src/theory/strings/solver_state.h | 4 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.h | 11 |
3 files changed, 7 insertions, 10 deletions
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 06a86935f..970b832a9 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -129,7 +129,7 @@ void SolverState::eqNotifyNewClass(TNode t) } } -void SolverState::eqNotifyPreMerge(TNode t1, TNode t2) +void SolverState::eqNotifyMerge(TNode t1, TNode t2) { EqcInfo* e2 = getOrMakeEqcInfo(t2, false); if (e2) diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index 2eee90ca4..8d3162b38 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -82,8 +82,8 @@ class SolverState //-------------------------------------- notifications for equalities /** called when a new equivalence class is created */ void eqNotifyNewClass(TNode t); - /** called when two equivalence classes will merge */ - void eqNotifyPreMerge(TNode t1, TNode t2); + /** called when two equivalence classes merge */ + void eqNotifyMerge(TNode t1, TNode t2); /** called when two equivalence classes are made disequal */ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); //-------------------------------------- end notifications for equalities diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 29c3cd64c..1d3261115 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -166,14 +166,11 @@ class TheoryStrings : public Theory { Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl; d_str.eqNotifyNewClass(t); } - void eqNotifyPreMerge(TNode t1, TNode t2) override + void eqNotifyMerge(TNode t1, TNode t2) override { - Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl; - d_state.eqNotifyPreMerge(t1, t2); - } - void eqNotifyPostMerge(TNode t1, TNode t2) override - { - Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl; + Debug("strings") << "NotifyClass::eqNotifyMerge(" << t1 << ", " << t2 + << std::endl; + d_state.eqNotifyMerge(t1, t2); } void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override { |