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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 4 Apr 2018 01:29:26 +0000 (20:29 -0500)
committer	Andres Noetzli <andres.noetzli@gmail.com>
	Wed, 4 Apr 2018 01:29:26 +0000 (18:29 -0700)
commit	eaebc10c50ca44644edd430ed3f555092a0fb27a
tree	e1944b5c0a2e9fbb38beb2f308009b563ab4a2bd	tree
parent	fee2021bb7419630853cbd0b20afa1af5e2eb1e9	commit \| diff

Option to turn arbitrary input into sygus (#1704)

Preprocessing pass that turns an arbitrary (e.g. smt2) input into a sygus conjecture, which is helpful for Horn clause solving.

This includes improvements to the robustness of the sygus solver.

src/Makefile.am		diff \| blob \| history
src/options/quantifiers_options.toml		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.h		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.h		diff \| blob \| history
src/theory/quantifiers/sygus_inference.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus_inference.h	[new file with mode: 0644]	blob
test/regress/Makefile.tests		diff \| blob \| history
test/regress/regress1/quantifiers/sygus-infer-nested.smt2	[new file with mode: 0644]	blob

RSS Atom