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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Mon, 29 Jul 2019 18:58:09 +0000 (13:58 -0500)
committer	GitHub <noreply@github.com>
	Mon, 29 Jul 2019 18:58:09 +0000 (13:58 -0500)
commit	90eddb069c3c9abf96719ac20aff45b44af86207
tree	5e9b48565fdcc33ecbc094ae5e14101e6e4ccb3c	tree
parent	3aba99657b39ccc0ab400c7ed9778673a3acddd7	commit \| diff

Support get-abduct smt2 command (#3122)

21 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/bindings/java/CMakeLists.txt		diff \| blob \| history
src/options/quantifiers_options.toml		diff \| blob \| history
src/options/smt_options.toml		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/preprocessing/passes/sygus_abduct.cpp	[deleted file]	blob \| history
src/preprocessing/passes/sygus_abduct.h	[deleted file]	blob \| history
src/preprocessing/preprocessing_pass_registry.cpp		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/theory/logic_info.cpp		diff \| blob \| history
src/theory/logic_info.h		diff \| blob \| history
src/theory/quantifiers/expr_miner.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_abduct.cpp	[new file with mode: 0644]	blob
src/theory/quantifiers/sygus/sygus_abduct.h	[new file with mode: 0644]	blob
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress1/sygus-abduct-test-user.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sygus-abduct-test.smt2		diff \| blob \| history