Use standard equality engine information in quantifiers state (#5824)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 28 Jan 2021 19:27:27 +0000 (13:27 -0600)
committerGitHub <noreply@github.com>
Thu, 28 Jan 2021 19:27:27 +0000 (13:27 -0600)
commit3234db430074e278258e6d687c07146a59769a92
tree17db55e1ff335c3998e1c4e172d174dc9f6e3b21
parent4cd2d73366aba081a38900ddc2f4f172ce9ed2f8
Use standard equality engine information in quantifiers state (#5824)

This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState.

This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery.
38 files changed:
src/theory/combination_engine.cpp
src/theory/combination_engine.h
src/theory/ee_manager.h
src/theory/ee_manager_distributed.cpp
src/theory/ee_manager_distributed.h
src/theory/ee_setup_info.h
src/theory/quantifiers/cegqi/ceg_instantiator.cpp
src/theory/quantifiers/ematching/candidate_generator.cpp
src/theory/quantifiers/ematching/ho_trigger.cpp
src/theory/quantifiers/ematching/inst_match_generator.cpp
src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
src/theory/quantifiers/ematching/instantiation_engine.cpp
src/theory/quantifiers/ematching/trigger.cpp
src/theory/quantifiers/ematching/var_match_generator.cpp
src/theory/quantifiers/equality_query.cpp
src/theory/quantifiers/equality_query.h
src/theory/quantifiers/fmf/full_model_check.cpp
src/theory/quantifiers/fmf/model_engine.cpp
src/theory/quantifiers/inst_match.cpp
src/theory/quantifiers/inst_match.h
src/theory/quantifiers/inst_match_trie.cpp
src/theory/quantifiers/inst_match_trie.h
src/theory/quantifiers/inst_strategy_enumerative.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quant_util.cpp
src/theory/quantifiers/quant_util.h
src/theory/quantifiers/relevant_domain.cpp
src/theory/quantifiers/relevant_domain.h
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h
src/theory/quantifiers/theory_quantifiers.cpp
src/theory/quantifiers/theory_quantifiers.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/theory_engine.cpp
src/theory/theory_state.cpp
src/theory/theory_state.h