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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Mon, 4 Apr 2022 18:35:38 +0000 (13:35 -0500)
committer	GitHub <noreply@github.com>
	Mon, 4 Apr 2022 18:35:38 +0000 (18:35 +0000)
commit	73a4978e53972716a800014fcbf6ac254ba2c6f3
tree	0b3134a79415065c9cbb5211ffd30d92a0cf22c7	tree
parent	f1559c05eb317a591bb18a832d0e87078d85218b	commit \| diff

Rename getInstantiatedConstructorTerm to getInstantiatedTerm (#8549)

This is in line with the change for non-parametric constructors (getConstructorTerm -> getTerm).

Also adds documentation to make the use of constructors, selectors, testers, updaters more clear.

13 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/DatatypeConstructor.java		diff \| blob \| history
src/api/java/io/github/cvc5/DatatypeSelector.java		diff \| blob \| history
src/api/java/jni/datatype_constructor.cpp		diff \| blob \| history
src/api/python/cvc5.pxd		diff \| blob \| history
src/api/python/cvc5.pxi		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/parser/smt2/Smt2.g		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/python/test_datatype_api.py		diff \| blob \| history