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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 25 May 2022 20:52:08 +0000 (15:52 -0500)
committer	GitHub <noreply@github.com>
	Wed, 25 May 2022 20:52:08 +0000 (20:52 +0000)
commit	4689ed968658db8c499c0e232d3d2343e918fe6e
tree	e8899aaa74cabb405ddd300d22c12bdff8080203	tree
parent	19b18be61c365f8506785a41244b74d008fa5976	commit \| diff

Add model-based quantifier instantiation (#8729)

This is a straightforward reimplementation of Ge/deMoura from CAV 2009.

22 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/options/quantifiers_options.toml		diff \| blob \| history
src/preprocessing/passes/sort_infer.cpp		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/smt/solver_engine.cpp		diff \| blob \| history
src/theory/inference_id.cpp		diff \| blob \| history
src/theory/inference_id.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_mbqi.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/inst_strategy_mbqi.h	[new file with mode: 0644]	blob
src/theory/quantifiers/quantifiers_modules.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_modules.h		diff \| blob \| history
src/theory/quantifiers/skolemize.h		diff \| blob \| history
src/theory/smt_engine_subsolver.cpp		diff \| blob \| history
test/regress/cli/CMakeLists.txt		diff \| blob \| history
test/regress/cli/regress0/ho/issue6536.smt2		diff \| blob \| history
test/regress/cli/regress0/push-pop/inc-double-u.smt2		diff \| blob \| history
test/regress/cli/regress0/quantifiers/mbqi-simple.smt2	[new file with mode: 0644]	blob
test/regress/cli/regress1/bug567.smt2		diff \| blob \| history
test/regress/cli/regress1/fmf/issue3587.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/dt-tc-opt-small.smt2		diff \| blob \| history
test/regress/cli/regress1/quantifiers/issue3724-quant.smt2		diff \| blob \| history