git.libre-soc.org Git - cvc5.git/commit

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 31 Mar 2021 17:35:52 +0000 (12:35 -0500)
committer	GitHub <noreply@github.com>
	Wed, 31 Mar 2021 17:35:52 +0000 (17:35 +0000)
commit	613ecb885e64a2cb37ba82f1783f85afe8afe66c
tree	b6ca4052c8361ccae1b183520fe010864960453e	tree
parent	c28829ce6fc9861b8f0e902952c9983bba10820a	commit \| diff

Eliminate dependencies on quantifiers engine in internal quantifiers code (#6240)

This completes eliminating dependencies on quantifiers engine from internal quantifiers code. It eliminates quantifiers_engine.h as an include from src/theory/quantifiers/ apart from theory_quantifiers.cpp where it is owned.

Followup PRs will further eliminate circular dependencies that arose will refactoring quantifiers engine.

52 files changed:

src/theory/quantifiers/alpha_equivalence.cpp		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.h		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/instantiation_engine.h		diff \| blob \| history
src/theory/quantifiers/ematching/var_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.h		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.h		diff \| blob \| history
src/theory/quantifiers/inst_match.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match.h		diff \| blob \| history
src/theory/quantifiers/inst_match_trie.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.h		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.h		diff \| blob \| history
src/theory/quantifiers/quant_module.cpp		diff \| blob \| history
src/theory/quantifiers/quant_module.h		diff \| blob \| history
src/theory/quantifiers/quant_rep_bound_ext.cpp		diff \| blob \| history
src/theory/quantifiers/quant_split.cpp		diff \| blob \| history
src/theory/quantifiers/quant_split.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_modules.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_modules.h		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_module.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_engine.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_engine.h		diff \| blob \| history
src/theory/quantifiers/sygus_inst.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_inst.h		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_tuple_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history

RSS Atom