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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 21 Dec 2021 18:21:40 +0000 (12:21 -0600)
committer	GitHub <noreply@github.com>
	Tue, 21 Dec 2021 18:21:40 +0000 (18:21 +0000)
commit	36f93a1431e93979744f2c2a1f3d06b2b9008a4f
tree	4a05619d0c8705451f9358d31511c79471ea2f81	tree
parent	2b7bebc38a48a0bd600b2cd9b2dae7328a3c5d3f	commit \| diff

Support get-abduct-next (#7850)

Adds support for incremental abduction, adds regression for using push/pop in combination with get-abduct, and a use of get-abduct-next.

Adds this method to C++, java API.

Interpolation/abduction not yet supported in Python API, I'm waiting for @yoni206 to add this; getAbductNext will be added to Python API in followup PR.

22 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/api/java/io/github/cvc5/api/Solver.java		diff \| blob \| history
src/api/java/jni/solver.cpp		diff \| blob \| history
src/expr/symbol_manager.cpp		diff \| blob \| history
src/expr/symbol_manager.h		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/printer/printer.cpp		diff \| blob \| history
src/printer/printer.h		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.h		diff \| blob \| history
src/smt/abduction_solver.cpp		diff \| blob \| history
src/smt/abduction_solver.h		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/solver_engine.cpp		diff \| blob \| history
src/smt/solver_engine.h		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress1/abduction/simple-incremental-push-pop.smt2	[new file with mode: 0644]	blob
test/regress/regress1/abduction/simple-incremental.smt2	[new file with mode: 0644]	blob
test/unit/api/cpp/solver_black.cpp		diff \| blob \| history
test/unit/api/java/SolverTest.java		diff \| blob \| history

RSS Atom