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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 24 Mar 2021 22:44:52 +0000 (17:44 -0500)
committer	GitHub <noreply@github.com>
	Wed, 24 Mar 2021 22:44:52 +0000 (22:44 +0000)
commit	77b75a69e51b742e1448d754b6886c10ef76e79f
tree	b3c4f9793fc0db34494e1d914286e32a1bd4c04c	tree
parent	cfe207563479a1e9e13d52bdd93446a8c816636a	commit \| diff

Use inference manager to access intantiate utility instead of quantifiers engine (#6198)

Towards breaking dependencies on quantifers engine.

20 files changed:

src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/im_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_simple.h		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.h		diff \| blob \| history
src/theory/quantifiers/fmf/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_builder.h		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.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/quantifiers_modules.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_inst.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history