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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 22 Dec 2021 16:56:51 +0000 (10:56 -0600)
committer	GitHub <noreply@github.com>
	Wed, 22 Dec 2021 16:56:51 +0000 (10:56 -0600)
commit	5c3cc154d0896568099c18ee6929439d49954e8f
tree	0385b1658e8f93122e0e395b145168860182bbfc	tree
parent	36f93a1431e93979744f2c2a1f3d06b2b9008a4f	commit \| diff

Add support for incremental + interpolants (#7853)

Adds support for incrementality + get-interpol, including the get-interpol-next command.

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/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/command.cpp		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/interpolation_solver.cpp		diff \| blob \| history
src/smt/interpolation_solver.h		diff \| blob \| history
src/smt/solver_engine.cpp		diff \| blob \| history
src/smt/solver_engine.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.h		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress1/sygus/interpol1-push-pop.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sygus/interpol3-next.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