Replace Theory::Set with TheoryIdSet (#4959)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 28 Aug 2020 23:01:34 +0000 (18:01 -0500)
committerGitHub <noreply@github.com>
Fri, 28 Aug 2020 23:01:34 +0000 (18:01 -0500)
commit960147384b7953a352ca9c721f9b93bdac4ff178
tree2bbc6df18d6cebbe94f9cce9732fcc6c6096e341
parent48dfcfd271ff9fa04766e29fb82ba83290da1ad8
Replace Theory::Set with TheoryIdSet (#4959)

This makes it so that equality_engine.h does not include theory.h. This is a bad dependency since Theory contains EqualityEngine.

This dependency between equality engine and theory was due to the use of a helper (Theory::Set) for representing sets of theories that is inlined into Theory. This PR moves this definition and utilities to theory_id.h.

It fixes the resulting include dependencies which are broken by changing the include theory.h -> theory_id.h in equality_engine.h.

This avoids a circular dependency in the includes between Theory -> InferenceManager -> ProofEqualityEngine -> EqualityEngine -> Theory.
20 files changed:
src/theory/arith/congruence_manager.h
src/theory/model_manager.h
src/theory/quantifiers/first_order_model.h
src/theory/sets/cardinality_extension.cpp
src/theory/shared_terms_database.cpp
src/theory/shared_terms_database.h
src/theory/strings/solver_state.h
src/theory/term_registration_visitor.cpp
src/theory/term_registration_visitor.h
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_id.cpp
src/theory/theory_id.h
src/theory/theory_model.cpp
src/theory/theory_model.h
src/theory/theory_model_builder.h
src/theory/uf/equality_engine.cpp
src/theory/uf/equality_engine.h
src/theory/uf/ho_extension.h
src/theory/uf/proof_equality_engine.h