From 8c9fff99a2be7369e33520a120e25e6d8c3ec07c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 13 Dec 2021 12:24:07 -0600 Subject: [PATCH] Fixes and additions for API for parametric datatypes (#7760) --- src/api/cpp/cvc5.cpp | 14 +++++++++++- src/api/cpp/cvc5.h | 14 ++++++++++-- src/api/java/io/github/cvc5/api/Datatype.java | 12 ++++++++++ .../github/cvc5/api/DatatypeConstructor.java | 9 ++++---- src/api/java/jni/datatype.cpp | 22 +++++++++++++++++++ src/api/java/jni/datatype_constructor.cpp | 6 ++--- src/api/python/cvc5.pxd | 3 ++- src/api/python/cvc5.pxi | 20 ++++++++++++++--- src/parser/parser.cpp | 2 +- src/parser/smt2/Smt2.g | 2 +- src/theory/arith/nl/iand_solver.cpp | 4 +++- test/unit/api/cpp/datatype_api_black.cpp | 11 ++++++++-- test/unit/api/java/DatatypeTest.java | 8 +++++-- test/unit/api/python/test_datatype_api.py | 10 ++++++--- 14 files changed, 113 insertions(+), 24 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index aa3e7fa3f..1e5738ed8 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -3804,7 +3804,7 @@ Term DatatypeConstructor::getConstructorTerm() const CVC5_API_TRY_CATCH_END; } -Term DatatypeConstructor::getSpecializedConstructorTerm( +Term DatatypeConstructor::getInstantiatedConstructorTerm( const Sort& retSort) const { CVC5_API_TRY_CATCH_BEGIN; @@ -4109,6 +4109,18 @@ size_t Datatype::getNumConstructors() const CVC5_API_TRY_CATCH_END; } +std::vector Datatype::getParameters() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_CHECK(isParametric()) << "Expected parametric datatype"; + //////// all checks before this line + std::vector params = d_dtype->getParameters(); + return Sort::typeNodeVectorToSorts(d_solver, params); + //////// + CVC5_API_TRY_CATCH_END; +} + bool Datatype::isParametric() const { CVC5_API_TRY_CATCH_BEGIN; diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index b65db16a3..e38030abe 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -315,6 +315,7 @@ class CVC5_EXPORT Sort friend class DatatypeConstructorDecl; friend class DatatypeSelector; friend class DatatypeDecl; + friend class Datatype; friend class Op; friend class Solver; friend class Grammar; @@ -434,7 +435,10 @@ class CVC5_EXPORT Sort bool isDatatype() const; /** - * Is this a parametric datatype sort? + * Is this a parametric datatype sort? A parametric datatype sort is either + * one that is returned by a call to Solver::mkDatatypeSort() or Solver::mkDatatypeSorts() for a + * parametric datatype, or an instantiated datatype sort returned by + * Sort::instantiate() for parametric datatype sort `s`. * @return true if the sort is a parametric datatype sort */ bool isParametricDatatype() const; @@ -1993,7 +1997,7 @@ class CVC5_EXPORT DatatypeConstructor * @param retSort the desired return sort of the constructor * @return the constructor term */ - Term getSpecializedConstructorTerm(const Sort& retSort) const; + Term getInstantiatedConstructorTerm(const Sort& retSort) const; /** * Get the tester operator of this datatype constructor. @@ -2244,6 +2248,12 @@ class CVC5_EXPORT Datatype /** @return the number of constructors for this Datatype. */ size_t getNumConstructors() const; + /** + * @return the parameters of this datatype, if it is parametric. An exception + * is thrown if this datatype is not parametric. + */ + std::vector getParameters() const; + /** @return true if this datatype is parametric */ bool isParametric() const; diff --git a/src/api/java/io/github/cvc5/api/Datatype.java b/src/api/java/io/github/cvc5/api/Datatype.java index bc33ba10b..39ea2bb19 100644 --- a/src/api/java/io/github/cvc5/api/Datatype.java +++ b/src/api/java/io/github/cvc5/api/Datatype.java @@ -108,6 +108,18 @@ public class Datatype extends AbstractPointer implements Iterable sorts = current->getParameters(); + std::vector sortPointers(sorts.size()); + for (size_t i = 0; i < sorts.size(); i++) + { + sortPointers[i] = reinterpret_cast(new Sort(sorts[i])); + } + jlongArray ret = env->NewLongArray(sorts.size()); + env->SetLongArrayRegion(ret, 0, sorts.size(), sortPointers.data()); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + /* * Class: io_github_cvc5_api_Datatype * Method: isParametric diff --git a/src/api/java/jni/datatype_constructor.cpp b/src/api/java/jni/datatype_constructor.cpp index 7fe5f21c6..de9e4fa4c 100644 --- a/src/api/java/jni/datatype_constructor.cpp +++ b/src/api/java/jni/datatype_constructor.cpp @@ -65,17 +65,17 @@ Java_io_github_cvc5_api_DatatypeConstructor_getConstructorTerm(JNIEnv* env, /* * Class: io_github_cvc5_api_DatatypeConstructor - * Method: getSpecializedConstructorTerm + * Method: getInstantiatedConstructorTerm * Signature: (JJ)J */ JNIEXPORT jlong JNICALL -Java_io_github_cvc5_api_DatatypeConstructor_getSpecializedConstructorTerm( +Java_io_github_cvc5_api_DatatypeConstructor_getInstantiatedConstructorTerm( JNIEnv* env, jobject, jlong pointer, jlong retSortPointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; DatatypeConstructor* current = (DatatypeConstructor*)pointer; Sort* sort = (Sort*)retSortPointer; - Term* retPointer = new Term(current->getSpecializedConstructorTerm(*sort)); + Term* retPointer = new Term(current->getInstantiatedConstructorTerm(*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 f5dc2aca2..2baed575a 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -51,6 +51,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": DatatypeSelector getSelector(const string& name) except + string getName() except + size_t getNumConstructors() except + + vector[Sort] getParameters() except + bint isParametric() except + bint isCodatatype() except + bint isTuple() except + @@ -76,7 +77,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": DatatypeSelector operator[](const string& name) except + string getName() except + Term getConstructorTerm() except + - Term getSpecializedConstructorTerm(const Sort& retSort) except + + Term getInstantiatedConstructorTerm(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 6220545a1..5c75047ef 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -153,6 +153,18 @@ cdef class Datatype: """ return self.cd.getNumConstructors() + def getParameters(self): + """ + :return: the parameters of this datatype, if it is parametric. An + exception is thrown if this datatype is not parametric. + """ + param_sorts = [] + for s in self.cd.getParameters(): + sort = Sort(self.solver) + sort.csort = s + param_sorts.append(sort) + return param_sorts + def isParametric(self): """:return: True if this datatype is parametric.""" return self.cd.isParametric() @@ -233,15 +245,17 @@ cdef class DatatypeConstructor: term.cterm = self.cdc.getConstructorTerm() return term - def getSpecializedConstructorTerm(self, Sort retSort): + def getInstantiatedConstructorTerm(self, Sort retSort): """ - Specialized method for parametric datatypes (see :cpp:func:`DatatypeConstructor::getSpecializedConstructorTerm() `). + Specialized method for parametric datatypes (see + :cpp:func:`DatatypeConstructor::getInstantiatedConstructorTerm() + `). :param retSort: the desired return sort of the constructor :return: the constructor operator as a term. """ cdef Term term = Term(self.solver) - term.cterm = self.cdc.getSpecializedConstructorTerm(retSort.csort) + term.cterm = self.cdc.getInstantiatedConstructorTerm(retSort.csort) return term def getTesterTerm(self): diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index c94e39748..1481d66fe 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -583,7 +583,7 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) // lookup by name api::DatatypeConstructor dc = d.getConstructor(t.toString()); // ask the constructor for the specialized constructor term - t = dc.getSpecializedConstructorTerm(s); + t = dc.getInstantiatedConstructorTerm(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 fe401b369..41cd4869a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1364,7 +1364,7 @@ termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2] { // lookup constructor by name api::DatatypeConstructor dc = dt.getConstructor(f.toString()); - api::Term scons = dc.getSpecializedConstructorTerm(expr.getSort()); + api::Term scons = dc.getInstantiatedConstructorTerm(expr.getSort()); // take the type of the specialized constructor instead type = scons.getSort(); } diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 92ecaf4e8..b5278a353 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -296,7 +296,9 @@ Node IAndSolver::bitwiseLemma(Node i) bitIAnd = d_iandUtils.createBitwiseIAndNode(x, y, high_bit, j); // enforce bitwise equality lem = nm->mkNode( - AND, lem, rewrite(d_iandUtils.iextract(high_bit, j, i)).eqNode(bitIAnd)); + AND, + lem, + rewrite(d_iandUtils.iextract(high_bit, j, i)).eqNode(bitIAnd)); } } return lem; diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index 745abc17c..fecf228a5 100644 --- a/test/unit/api/cpp/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp @@ -231,6 +231,7 @@ TEST_F(TestApiBlackDatatype, datatypeNames) dtypeSpec.addConstructor(nil); Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); Datatype dt = dtypeSort.getDatatype(); + ASSERT_THROW(dt.getParameters(), CVC5ApiException); ASSERT_EQ(dt.getName(), std::string("list")); ASSERT_NO_THROW(dt.getConstructor("nil")); ASSERT_NO_THROW(dt["cons"]); @@ -274,6 +275,8 @@ TEST_F(TestApiBlackDatatype, parametricDatatype) Sort pairType = d_solver.mkDatatypeSort(pairSpec); ASSERT_TRUE(pairType.getDatatype().isParametric()); + std::vector dparams = pairType.getDatatype().getParameters(); + ASSERT_TRUE(dparams[0] == t1 && dparams[1] == t2); v.clear(); v.push_back(d_solver.getIntegerSort()); @@ -576,12 +579,16 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons) iargs.push_back(isort); Sort listInt = dtsorts[0].instantiate(iargs); + std::vector liparams = listInt.getDatatype().getParameters(); + // the parameter of the datatype is not instantiated + ASSERT_TRUE(liparams.size() == 1 && liparams[0] == x); + Term testConsTerm; // get the specialized constructor term for list[Int] - ASSERT_NO_THROW(testConsTerm = nilc.getSpecializedConstructorTerm(listInt)); + ASSERT_NO_THROW(testConsTerm = nilc.getInstantiatedConstructorTerm(listInt)); ASSERT_NE(testConsTerm, nilc.getConstructorTerm()); // error to get the specialized constructor term for Int - ASSERT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC5ApiException); + ASSERT_THROW(nilc.getInstantiatedConstructorTerm(isort), CVC5ApiException); } } // namespace test } // namespace cvc5 diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java index fb23ea515..e94785b08 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -248,6 +248,8 @@ class DatatypeTest Sort pairType = d_solver.mkDatatypeSort(pairSpec); assertTrue(pairType.getDatatype().isParametric()); + Sort[] dparams = pairType.getDatatype().getParameters(); + assertTrue(dparams[0].equals(t1) && dparams[1].equals(t2)); v.clear(); v.add(d_solver.getIntegerSort()); @@ -562,10 +564,12 @@ class DatatypeTest AtomicReference atomicTerm = new AtomicReference<>(); // get the specialized constructor term for list[Int] - assertDoesNotThrow(() -> atomicTerm.set(nilc.getSpecializedConstructorTerm(listInt))); + assertDoesNotThrow( + () -> atomicTerm.set(nilc.getInstantiatedConstructorTerm(listInt))); Term testConsTerm = atomicTerm.get(); assertNotEquals(testConsTerm, nilc.getConstructorTerm()); // error to get the specialized constructor term for Int - assertThrows(CVC5ApiException.class, () -> nilc.getSpecializedConstructorTerm(isort)); + assertThrows(CVC5ApiException.class, + () -> nilc.getInstantiatedConstructorTerm(isort)); } } diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index 43124d4dc..af34e098e 100644 --- a/test/unit/api/python/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py @@ -155,6 +155,8 @@ def test_datatype_structs(solver): dtypeSpec.addConstructor(nil) dtypeSort = solver.mkDatatypeSort(dtypeSpec) dt = dtypeSort.getDatatype() + # not parametric datatype + with pytest.raises(RuntimeError): dt.getParameters() assert not dt.isCodatatype() assert not dt.isTuple() assert not dt.isRecord() @@ -262,7 +264,7 @@ def test_parametric_datatype(solver): v.append(t1) v.append(t2) pairSpec = solver.mkDatatypeDecl("pair", v) - + mkpair = solver.mkDatatypeConstructorDecl("mk-pair") mkpair.addSelector("first", t1) mkpair.addSelector("second", t2) @@ -271,6 +273,8 @@ def test_parametric_datatype(solver): pairType = solver.mkDatatypeSort(pairSpec) assert pairType.getDatatype().isParametric() + dparams = pairType.getDatatype().getParameters() + assert dparams[0]==t1 and dparams[1]==t2 v.clear() v.append(solver.getIntegerSort()) @@ -558,8 +562,8 @@ def test_datatype_specialized_cons(solver): testConsTerm = Term(solver) # get the specialized constructor term for list[Int] - testConsTerm = nilc.getSpecializedConstructorTerm(listInt) + testConsTerm = nilc.getInstantiatedConstructorTerm(listInt) assert testConsTerm != nilc.getConstructorTerm() # error to get the specialized constructor term for Int with pytest.raises(RuntimeError): - nilc.getSpecializedConstructorTerm(isort) + nilc.getInstantiatedConstructorTerm(isort) -- 2.30.2