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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 20 Apr 2021 21:40:12 +0000 (16:40 -0500)
committer	GitHub <noreply@github.com>
	Tue, 20 Apr 2021 21:40:12 +0000 (21:40 +0000)
commit	cc8ce1bcdf8d6a4b508723063879e891a6cbd8c3
tree	fef63c0628404e673eca56947d19411198ba3ce2	tree
parent	18ce14653647a93319cc53eec9bc310d3a4c6f57	commit \| diff

Add instantiation pool feature to the API (#6358)

This adds the command declare-pool to the public API. It also adds parsing support for this feature, lifts the internal kinds to public kinds, adds an example regression, and a unit test for the new declare-pool solver method.

14 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/api/cpp/cvc5_kind.h		diff \| blob \| history
src/api/python/cvc4.pxd		diff \| blob \| history
src/api/python/cvc4.pxi		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/smt/command.cpp		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress1/quantifiers/pool-example.smt2	[new file with mode: 0644]	blob
test/unit/api/solver_black.cpp		diff \| blob \| history

RSS Atom