Dynamic allocation of equality engine in Theory (#4890)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 17 Aug 2020 19:38:16 +0000 (14:38 -0500)
committerGitHub <noreply@github.com>
Mon, 17 Aug 2020 19:38:16 +0000 (12:38 -0700)
commit4f82b6eb7cc921ba2c6470a5ca0027be8dfc04e9
tree4060becc52568fce247e9bd4e1660dfed33700dc
parent5c78f336b8276a2ed8916e2a9447a29a2caca069
Dynamic allocation of equality engine in Theory (#4890)

This commit updates Theory so that equality engines are allocated dynamically. The plan is to make this configurable based on the theory combination method.

The fundamental changes include:
- Add `d_equalityEngine` (raw) pointer to Theory, which is the "official" equality engine of the theory.
- Standardize methods for initializing Theory. This is now made more explicit in the documentation in theory.h, and includes a method `finishInitStandalone` for users of Theory that don't have an associated TheoryEngine.
- Refactor TheoryEngine::finishInit, including how Theory is initialized to incorporate the new policy.
- Things related to master equality engine are now specific to EqEngineManagerDistributed and hence can be removed from TheoryEngine. This will be further refactored in forthcoming PRs.

Note that the majority of changes are due to changing `d_equalityEngine.` to `d_equalityEngine->` throughout.
37 files changed:
src/proof/theory_proof.cpp
src/theory/arith/congruence_manager.cpp
src/theory/arith/congruence_manager.h
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arith/theory_arith_private.cpp
src/theory/arith/theory_arith_private.h
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.h
src/theory/bv/bv_subtheory_core.cpp
src/theory/bv/bv_subtheory_core.h
src/theory/bv/theory_bv.cpp
src/theory/bv/theory_bv.h
src/theory/datatypes/theory_datatypes.cpp
src/theory/datatypes/theory_datatypes.h
src/theory/ee_manager_distributed.cpp
src/theory/ee_manager_distributed.h
src/theory/fp/theory_fp.cpp
src/theory/fp/theory_fp.h
src/theory/quantifiers/theory_quantifiers.cpp
src/theory/quantifiers/theory_quantifiers.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/strings/solver_state.cpp
src/theory/strings/solver_state.h
src/theory/strings/term_registry.cpp
src/theory/strings/term_registry.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory.cpp
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h