Simplify equality engine notifications (#4896)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 14 Aug 2020 18:07:17 +0000 (13:07 -0500)
committerGitHub <noreply@github.com>
Fri, 14 Aug 2020 18:07:17 +0000 (13:07 -0500)
commit42cd0a7bcbe993870d76d8cc9db7acc0a9ae70f9
tree1335e7efe55bb0df162c03b37e77c364efde666a
parentee055dddf887ed001fee1834ba845fb81e20e27e
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.
25 files changed:
src/theory/arith/congruence_manager.cpp
src/theory/arith/congruence_manager.h
src/theory/arrays/theory_arrays.h
src/theory/bv/bv_subtheory_core.h
src/theory/datatypes/theory_datatypes.cpp
src/theory/datatypes/theory_datatypes.h
src/theory/ee_manager_distributed.h
src/theory/fp/theory_fp.h
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/conjecture_generator.h
src/theory/sep/theory_sep.cpp
src/theory/sep/theory_sep.h
src/theory/sets/theory_sets.cpp
src/theory/sets/theory_sets.h
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/shared_terms_database.h
src/theory/strings/solver_state.cpp
src/theory/strings/solver_state.h
src/theory/strings/theory_strings.h
src/theory/theory_engine.h
src/theory/uf/equality_engine.cpp
src/theory/uf/equality_engine_notify.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h