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

author	Haniel Barbosa <hanielbbarbosa@gmail.com>
	Wed, 27 Nov 2019 20:52:36 +0000 (17:52 -0300)
committer	GitHub <noreply@github.com>
	Wed, 27 Nov 2019 20:52:36 +0000 (17:52 -0300)
commit	46eeb6a507c31b4ac65b0ef70c32898667097377
tree	06b34813dd1bc3dcc25479bf4c72ef3252655b77	tree
parent	bd2793a68e021ab58ab07db0cac67cf3d6806ead	commit \| diff

Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502)

14 files changed:

src/options/quantifiers_options.toml		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/quantifiers/fun_def_evaluator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_engine.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress1/sygus/list_recursor.sy		diff \| blob \| history
test/regress/regress1/sygus/rec-fun-swap.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/rec-fun-sygus.sy		diff \| blob \| history
test/regress/regress1/sygus/rec-fun-while-1.sy		diff \| blob \| history
test/regress/regress1/sygus/rec-fun-while-2.sy		diff \| blob \| history
test/regress/regress1/sygus/rec-fun-while-infinite.sy		diff \| blob \| history