Refactor quantifiers engine initialization (#5813)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 26 Jan 2021 18:43:50 +0000 (12:43 -0600)
committerGitHub <noreply@github.com>
Tue, 26 Jan 2021 18:43:50 +0000 (12:43 -0600)
commitca648afb2a7574991b1dc9817c1b8e2546548073
tree30bcc19878be364e9e2c61bc10e9974acf198f30
parent022dbeb9e2dc925cf0dcffb75ea57aedf09395de
Refactor quantifiers engine initialization (#5813)

This is a step towards breaking up the quantifiers engine.

The key change is that QuantifiersEngine will not be passed as a pointer to the modules it contains. This PR makes it so that necessary modules take a QuantifiersState, which will eventually be extended as needed with additional query methods. For now, modules will take both until the dependencies on QuantifersEngine are removed.

This required that QuantifiersEngine now lives in TheoryQuantifiers, instead of in TheoryEngine, since the QuantifiersEngine must be initialized with QuantifiersState, which is a member of TheoryQuantifiers. Now, TheoryEngine retrieves the QuantifiersEngine from TheoryQuantifiers prior to finishing initialization on theories.
54 files changed:
src/theory/quantifiers/anti_skolem.cpp
src/theory/quantifiers/anti_skolem.h
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/conjecture_generator.h
src/theory/quantifiers/ematching/instantiation_engine.cpp
src/theory/quantifiers/ematching/instantiation_engine.h
src/theory/quantifiers/equality_query.cpp
src/theory/quantifiers/equality_query.h
src/theory/quantifiers/first_order_model.cpp
src/theory/quantifiers/first_order_model.h
src/theory/quantifiers/fmf/bounded_integers.cpp
src/theory/quantifiers/fmf/bounded_integers.h
src/theory/quantifiers/fmf/full_model_check.cpp
src/theory/quantifiers/fmf/full_model_check.h
src/theory/quantifiers/fmf/model_builder.cpp
src/theory/quantifiers/fmf/model_builder.h
src/theory/quantifiers/fmf/model_engine.cpp
src/theory/quantifiers/fmf/model_engine.h
src/theory/quantifiers/inst_strategy_enumerative.cpp
src/theory/quantifiers/inst_strategy_enumerative.h
src/theory/quantifiers/instantiate.cpp
src/theory/quantifiers/instantiate.h
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quant_conflict_find.h
src/theory/quantifiers/quant_split.cpp
src/theory/quantifiers/quant_split.h
src/theory/quantifiers/quant_util.cpp
src/theory/quantifiers/quant_util.h
src/theory/quantifiers/quantifiers_modules.cpp
src/theory/quantifiers/quantifiers_modules.h
src/theory/quantifiers/skolemize.cpp
src/theory/quantifiers/skolemize.h
src/theory/quantifiers/sygus/cegis_unif.cpp
src/theory/quantifiers/sygus/cegis_unif.h
src/theory/quantifiers/sygus/synth_conjecture.cpp
src/theory/quantifiers/sygus/synth_conjecture.h
src/theory/quantifiers/sygus/synth_engine.cpp
src/theory/quantifiers/sygus/synth_engine.h
src/theory/quantifiers/sygus/term_database_sygus.cpp
src/theory/quantifiers/sygus/term_database_sygus.h
src/theory/quantifiers/sygus_inst.cpp
src/theory/quantifiers/sygus_inst.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.cpp
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h