From 73a4978e53972716a800014fcbf6ac254ba2c6f3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 4 Apr 2022 13:35:38 -0500 Subject: [PATCH] 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. --- src/api/cpp/cvc5.cpp | 3 +- src/api/cpp/cvc5.h | 43 +++++++++++--- .../io/github/cvc5/DatatypeConstructor.java | 32 +++++++--- .../java/io/github/cvc5/DatatypeSelector.java | 14 ++++- src/api/java/jni/datatype_constructor.cpp | 6 +- src/api/python/cvc5.pxd | 2 +- src/api/python/cvc5.pxi | 59 +++++++++++++++---- src/parser/parser.cpp | 2 +- src/parser/smt2/Smt2.g | 2 +- test/unit/api/cpp/datatype_api_black.cpp | 4 +- test/unit/api/cpp/solver_black.cpp | 17 +++--- test/unit/api/java/DatatypeTest.java | 4 +- test/unit/api/python/test_datatype_api.py | 4 +- 13 files changed, 140 insertions(+), 52 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 768ec181b..610330b76 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -3692,8 +3692,7 @@ Term DatatypeConstructor::getTerm() const CVC5_API_TRY_CATCH_END; } -Term DatatypeConstructor::getInstantiatedConstructorTerm( - const Sort& retSort) const +Term DatatypeConstructor::getInstantiatedTerm(const Sort& retSort) const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index ef366cfe5..44a30bfed 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -2018,13 +2018,23 @@ class CVC5_EXPORT DatatypeSelector std::string getName() const; /** - * Get the selector operator of this datatype selector. + * Get the selector term of this datatype selector. + * + * Selector terms are a class of function-like terms of selector + * sort (Sort::isDatatypeSelector()), and should be used as the first + * argument of Terms of kind #APPLY_SELECTOR. + * * @return the selector term */ Term getTerm() const; /** - * Get the updater operator of this datatype selector. + * Get the updater term of this datatype selector. + * + * Similar to selectors, updater terms are a class of function-like terms of + * updater Sort (Sort::isDatatypeUpdater()), and should be used as the first + * argument of Terms of kind #APPLY_UPDATER. + * * @return the updater term */ Term getUpdaterTerm() const; @@ -2093,13 +2103,25 @@ class CVC5_EXPORT DatatypeConstructor std::string getName() const; /** - * Get the constructor operator of this datatype constructor. + * Get the constructor term of this datatype constructor. + * + * Datatype constructors are a special class of function-like terms whose sort + * is datatype constructor (Sort::isDatatypeConstructor()). All datatype + * constructors, including nullary ones, should be used as the + * first argument to Terms whose kind is #APPLY_CONSTRUCTOR. For example, + * the nil list can be constructed by + * `Solver::mkTerm(APPLY_CONSTRUCTOR, {t})`, where `t` is the term returned + * by this method. + * + * @note This method should not be used for parametric datatypes. Instead, + * use the method DatatypeConstructor::getInstantiatedTerm() below. + * * @return the constructor term */ Term getTerm() const; /** - * Get the constructor operator of this datatype constructor whose return + * Get the constructor term of this datatype constructor whose return * type is retSort. This method is intended to be used on constructors of * parametric datatypes and can be seen as returning the constructor * term that has been explicitly cast to the given sort. @@ -2127,7 +2149,7 @@ class CVC5_EXPORT DatatypeConstructor * DatatypeConstructor is the one corresponding to nil, and retSort is * `(List Int)`. * - * @note the returned constructor term `t` is an operator, while + * @note the returned constructor term `t` is the constructor, while * `Solver::mkTerm(APPLY_CONSTRUCTOR, {t})` is used to construct the * above (nullary) application of nil. * @@ -2136,11 +2158,16 @@ class CVC5_EXPORT DatatypeConstructor * @param retSort the desired return sort of the constructor * @return the constructor term */ - Term getInstantiatedConstructorTerm(const Sort& retSort) const; + Term getInstantiatedTerm(const Sort& retSort) const; /** - * Get the tester operator of this datatype constructor. - * @return the tester operator + * Get the tester term of this datatype constructor. + * + * Similar to constructors, testers are a class of function-like terms of + * tester sort (Sort::isDatatypeConstructor()) which should be used as the + * first argument of Terms of kind #APPLY_TESTER. + * + * @return the tester term */ Term getTesterTerm() const; diff --git a/src/api/java/io/github/cvc5/DatatypeConstructor.java b/src/api/java/io/github/cvc5/DatatypeConstructor.java index 94a838d95..5a07d2c5e 100644 --- a/src/api/java/io/github/cvc5/DatatypeConstructor.java +++ b/src/api/java/io/github/cvc5/DatatypeConstructor.java @@ -47,7 +47,18 @@ public class DatatypeConstructor extends AbstractPointer implements IterablegetInstantiatedConstructorTerm(*sort)); + Term* retPointer = new Term(current->getInstantiatedTerm(*sort)); return (jlong)retPointer; CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 52d697492..2e6dfa493 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -86,7 +86,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": DatatypeSelector operator[](const string& name) except + string getName() except + Term getTerm() except + - Term getInstantiatedConstructorTerm(const Sort& retSort) except + + Term getInstantiatedTerm(const Sort& retSort) except + Term getTesterTerm() except + size_t getNumSelectors() except + DatatypeSelector getSelector(const string& name) except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 90aa5decc..a02adec33 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -257,16 +257,34 @@ cdef class DatatypeConstructor: return self.cdc.getName().decode() def getTerm(self): - """ - :return: The constructor operator as a term. + """ + Get the constructor term of this datatype constructor. + + Datatype constructors are a special class of function-like terms + whose sort is datatype constructor + (:py:meth:`Sort.isDatatypeConstructor()`). All datatype + constructors, including nullary ones, should be used as the first + argument to Terms whose kind is + :py:obj:`APPLY_CONSTRUCTOR `. + For example, the nil list can be constructed via + ``Solver.mkTerm(APPLY_CONSTRUCTOR, [nil])``, where nil is the Term + returned by this method. + + .. note:: + + This method should not be used for parametric datatypes. + Instead, use the method + :py:meth:`DatatypeConstructor.getInstantiatedTerm()` below. + + :return: The constructor term. """ cdef Term term = Term(self.solver) term.cterm = self.cdc.getTerm() return term - def getInstantiatedConstructorTerm(self, Sort retSort): + def getInstantiatedTerm(self, Sort retSort): """ - Get the constructor operator of this datatype constructor whose + Get the constructor term of this datatype constructor whose return type is retSort. This method is intended to be used on constructors of parametric datatypes and can be seen as returning the constructor term that has been explicitly cast to the given @@ -294,7 +312,7 @@ cdef class DatatypeConstructor: .. note:: - The returned constructor term ``t`` is an operator, while + The returned constructor term ``t`` is the constructor, while ``Solver.mkTerm(APPLY_CONSTRUCTOR, [t])`` is used to construct the above (nullary) application of nil. @@ -302,16 +320,21 @@ cdef class DatatypeConstructor: versions. :param retSort: The desired return sort of the constructor. - :return: The constructor operator as a term. + :return: The constructor term. """ cdef Term term = Term(self.solver) - term.cterm = self.cdc.getInstantiatedConstructorTerm(retSort.csort) + term.cterm = self.cdc.getInstantiatedTerm(retSort.csort) return term def getTesterTerm(self): """ - :return: The tester operator that is related to this constructor, - as a term. + Get the tester term of this datatype constructor. + + Similar to constructors, testers are a class of function-like terms + of tester sort (:py:meth:`Sort.isDatatypeTester`), and should + be used as the first argument of Terms of kind APPLY_TESTER. + + :return: The tester term for this constructor. """ cdef Term term = Term(self.solver) term.cterm = self.cdc.getTesterTerm() @@ -496,7 +519,14 @@ cdef class DatatypeSelector: def getTerm(self): """ - :return: The selector opeartor of this datatype selector as a term. + Get the selector term of this datatype selector. + + Selector terms are a class of function-like terms of selector + sort (:py:meth:`Sort.isDatatypeSelector()`), and should be used as + the first argument of Terms of kind + :py:obj:`APPLY_SELECTOR `. + + :return: The selector term of this datatype selector. """ cdef Term term = Term(self.solver) term.cterm = self.cds.getTerm() @@ -504,7 +534,14 @@ cdef class DatatypeSelector: def getUpdaterTerm(self): """ - :return: The updater opeartor of this datatype selector as a term. + Get the updater term of this datatype selector. + + Similar to selectors, updater terms are a class of function-like + terms of updater Sort (:py:meth:`Sort.isDatatypeUpdater()`), and + should be used as the first argument of Terms of kind + :py:ob:`APPLY_UPDATER `. + + :return: The updater term of this datatype selector. """ cdef Term term = Term(self.solver) term.cterm = self.cds.getUpdaterTerm() diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 5bd4c1c9c..cb26ffd8c 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -567,7 +567,7 @@ cvc5::Term Parser::applyTypeAscription(cvc5::Term t, cvc5::Sort s) // lookup by name cvc5::DatatypeConstructor dc = d.getConstructor(t.toString()); // ask the constructor for the specialized constructor term - t = dc.getInstantiatedConstructorTerm(s); + t = dc.getInstantiatedTerm(s); } // the type of t does not match the sort s by design (constructor type // vs datatype type), thus we use an alternative check here. diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 188f6ad06..b54ad6461 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1384,7 +1384,7 @@ termNonVariable[cvc5::Term& expr, cvc5::Term& expr2] { // lookup constructor by name cvc5::DatatypeConstructor dc = dt.getConstructor(f.toString()); - cvc5::Term scons = dc.getInstantiatedConstructorTerm(expr.getSort()); + cvc5::Term scons = dc.getInstantiatedTerm(expr.getSort()); // take the type of the specialized constructor instead type = scons.getSort(); } diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index ad0c56701..b29e232e0 100644 --- a/test/unit/api/cpp/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp @@ -587,10 +587,10 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons) Term testConsTerm; // get the specialized constructor term for list[Int] - ASSERT_NO_THROW(testConsTerm = nilc.getInstantiatedConstructorTerm(listInt)); + ASSERT_NO_THROW(testConsTerm = nilc.getInstantiatedTerm(listInt)); ASSERT_NE(testConsTerm, nilc.getTerm()); // error to get the specialized constructor term for Int - ASSERT_THROW(nilc.getInstantiatedConstructorTerm(isort), CVC5ApiException); + ASSERT_THROW(nilc.getInstantiatedTerm(isort), CVC5ApiException); } } // namespace test } // namespace cvc5::internal diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 1e0ff5a66..bcbbe0ac0 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -3057,15 +3057,14 @@ TEST_F(TestApiBlackSolver, proj_issue382) Term t53 = d_solver.mkTerm(MATCH_BIND_CASE, {d_solver.mkTerm(VARIABLE_LIST, {t52}), t52, t18}); Term t73 = d_solver.mkVar(s1, "_x78"); - Term t81 = - d_solver.mkTerm(MATCH_BIND_CASE, - {d_solver.mkTerm(VARIABLE_LIST, {t73}), - d_solver.mkTerm(APPLY_CONSTRUCTOR, - {s6.getDatatype() - .getConstructor("_x20") - .getInstantiatedConstructorTerm(s6), - t73}), - t18}); + Term t81 = d_solver.mkTerm( + MATCH_BIND_CASE, + {d_solver.mkTerm(VARIABLE_LIST, {t73}), + d_solver.mkTerm( + APPLY_CONSTRUCTOR, + {s6.getDatatype().getConstructor("_x20").getInstantiatedTerm(s6), + t73}), + t18}); Term t82 = d_solver.mkTerm(MATCH, {t13, t53, t53, t53, t81}); Term t325 = d_solver.mkTerm( APPLY_SELECTOR, diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java index 557db2f9b..01e2d2989 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -590,10 +590,10 @@ class DatatypeTest AtomicReference atomicTerm = new AtomicReference<>(); // get the specialized constructor term for list[Int] - assertDoesNotThrow(() -> atomicTerm.set(nilc.getInstantiatedConstructorTerm(listInt))); + assertDoesNotThrow(() -> atomicTerm.set(nilc.getInstantiatedTerm(listInt))); Term testConsTerm = atomicTerm.get(); assertNotEquals(testConsTerm, nilc.getTerm()); // error to get the specialized constructor term for Int - assertThrows(CVC5ApiException.class, () -> nilc.getInstantiatedConstructorTerm(isort)); + assertThrows(CVC5ApiException.class, () -> nilc.getInstantiatedTerm(isort)); } } diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index 09d5ce05e..a2b79ca7e 100644 --- a/test/unit/api/python/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py @@ -557,8 +557,8 @@ def test_datatype_specialized_cons(solver): testConsTerm = Term(solver) # get the specialized constructor term for list[Int] - testConsTerm = nilc.getInstantiatedConstructorTerm(listInt) + testConsTerm = nilc.getInstantiatedTerm(listInt) assert testConsTerm != nilc.getTerm() # error to get the specialized constructor term for Int with pytest.raises(RuntimeError): - nilc.getInstantiatedConstructorTerm(isort) + nilc.getInstantiatedTerm(isort) -- 2.30.2