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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 26 Mar 2021 16:47:22 +0000 (11:47 -0500)
committer	GitHub <noreply@github.com>
	Fri, 26 Mar 2021 16:47:22 +0000 (11:47 -0500)
commit	72f70f1573651bcbf5f327c7a3411ece0e607e3f
tree	d2e57f33fdbb6a260b0f523aa4cf2b621474e374	tree
parent	fa6c3db414d27f47e0bee55480df939e78c14eb3	commit \| diff

Pass term registry to quantifiers modules (#6216)

24 files changed:

src/theory/datatypes/sygus_extension.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/instantiation_engine.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/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.h		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/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_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/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

RSS Atom