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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Mon, 10 Jan 2022 19:27:04 +0000 (11:27 -0800)
committer	GitHub <noreply@github.com>
	Mon, 10 Jan 2022 19:27:04 +0000 (19:27 +0000)
commit	acba737109e440f0b57494bc999dd80169ae64ea
tree	86ed5594ba0f4d6c208d1eb5d5721878210e662e	tree
parent	966407c1490695bdac2a4d95397625adbcce433a	commit \| diff

api: Remove Sort::isComparableTo(). (#7903)

Since we do not support arithmetic subtyping on the API level anymore,
this function is obsolete. Consequently, this now requires that
replacement terms as arguments to Term::substitute() are of the same
sort as the replaced terms.

15 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/api/cpp/cvc5_checks.h		diff \| blob \| history
src/api/java/io/github/cvc5/api/Sort.java		diff \| blob \| history
src/api/java/jni/sort.cpp		diff \| blob \| history
src/api/python/cvc5.pxd		diff \| blob \| history
src/api/python/cvc5.pxi		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
test/regress/regress1/sygus/node-discrete.sy		diff \| blob \| history
test/unit/api/cpp/datatype_api_black.cpp		diff \| blob \| history
test/unit/api/cpp/sort_black.cpp		diff \| blob \| history
test/unit/api/java/DatatypeTest.java		diff \| blob \| history
test/unit/api/java/SortTest.java		diff \| blob \| history
test/unit/api/python/test_datatype_api.py		diff \| blob \| history
test/unit/api/python/test_sort.py		diff \| blob \| history

RSS Atom