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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Fri, 17 Dec 2021 04:24:23 +0000 (20:24 -0800)
committer	GitHub <noreply@github.com>
	Fri, 17 Dec 2021 04:24:23 +0000 (04:24 +0000)
commit	6c98b2f66aaee9e8f266bee816d730cc5ffee821
tree	3729b6641ef8890ccfad788ebc0f7d8c5e535b92	tree
parent	3973cfaa8763068a635f9091367b7642f322cbd9	commit \| diff

api: Add Solver::mkUnresolvedSort(). (#7817)

This adds a function to create unresolved sorts for mutually recursive
datatpes. This function creates an uninterpreted sort if the arity of
the unresolved sort is 0, and a sort constructor sort otherwise.

12 files changed:

RSS Atom

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/api/python/cvc5.pxd		diff \| blob \| history
src/api/python/cvc5.pxi		diff \| blob \| history
test/unit/api/cpp/datatype_api_black.cpp		diff \| blob \| history
test/unit/api/cpp/solver_black.cpp		diff \| blob \| history
test/unit/api/java/DatatypeTest.java		diff \| blob \| history
test/unit/api/java/SolverTest.java		diff \| blob \| history
test/unit/api/python/test_datatype_api.py		diff \| blob \| history
test/unit/api/python/test_solver.py		diff \| blob \| history