diff options
| -rw-r--r-- | examples/api/datatypes-new.cpp | 18 | ||||
| -rwxr-xr-x | examples/api/python/datatypes.py | 18 | ||||
| -rw-r--r-- | src/api/cvc4cpp.cpp | 50 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 65 | ||||
| -rw-r--r-- | src/api/python/cvc4.pxd | 13 | ||||
| -rw-r--r-- | src/api/python/cvc4.pxi | 32 | ||||
| -rw-r--r-- | test/unit/api/datatype_api_black.h | 38 | ||||
| -rw-r--r-- | test/unit/api/solver_black.h | 21 | ||||
| -rw-r--r-- | test/unit/api/sort_black.h | 24 | ||||
| -rw-r--r-- | test/unit/api/term_black.h | 6 |
10 files changed, 68 insertions, 217 deletions
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index c5773fa72..9cfc7992c 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -93,10 +93,8 @@ void test(Solver& slv, Sort& consListSort) sort); // give the datatype a name DatatypeConstructorDecl paramCons("cons"); DatatypeConstructorDecl paramNil("nil"); - DatatypeSelectorDecl paramHead("head", sort); - DatatypeSelectorDecl paramTail("tail", DatatypeDeclSelfSort()); - paramCons.addSelector(paramHead); - paramCons.addSelector(paramTail); + paramCons.addSelector("head", sort); + paramCons.addSelectorSelf("tail"); paramConsListSpec.addConstructor(paramCons); paramConsListSpec.addConstructor(paramNil); @@ -147,10 +145,8 @@ int main() DatatypeDecl consListSpec = slv.mkDatatypeDecl("list"); // give the datatype a name DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", slv.getIntegerSort()); - DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); - cons.addSelector(head); - cons.addSelector(tail); + cons.addSelector("head", slv.getIntegerSort()); + cons.addSelectorSelf("tail"); consListSpec.addConstructor(cons); DatatypeConstructorDecl nil("nil"); consListSpec.addConstructor(nil); @@ -172,10 +168,8 @@ int main() std::cout << std::endl; DatatypeConstructorDecl cons2("cons"); - DatatypeSelectorDecl head2("head", slv.getIntegerSort()); - DatatypeSelectorDecl tail2("tail", DatatypeDeclSelfSort()); - cons2.addSelector(head2); - cons2.addSelector(tail2); + cons2.addSelector("head", slv.getIntegerSort()); + cons2.addSelectorSelf("tail"); DatatypeConstructorDecl nil2("nil"); std::vector<DatatypeConstructorDecl> ctors = {cons2, nil2}; Sort consListSort2 = slv.declareDatatype("list2", ctors); diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py index c5eda1741..ded268d69 100755 --- a/examples/api/python/datatypes.py +++ b/examples/api/python/datatypes.py @@ -67,10 +67,8 @@ def test(slv, consListSort): paramConsListSpec = slv.mkDatatypeDecl("paramlist", sort) paramCons = pycvc4.DatatypeConstructorDecl("cons") paramNil = pycvc4.DatatypeConstructorDecl("nil") - paramHead = pycvc4.DatatypeSelectorDecl("head", sort) - paramTail = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort()) - paramCons.addSelector(paramHead) - paramCons.addSelector(paramTail) + paramCons.addSelector("head", sort) + paramCons.addSelectorSelf("tail") paramConsListSpec.addConstructor(paramCons) paramConsListSpec.addConstructor(paramNil) @@ -105,10 +103,8 @@ if __name__ == "__main__": consListSpec = slv.mkDatatypeDecl("list") # give the datatype a name cons = pycvc4.DatatypeConstructorDecl("cons") - head = pycvc4.DatatypeSelectorDecl("head", slv.getIntegerSort()) - tail = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort()) - cons.addSelector(head) - cons.addSelector(tail) + cons.addSelector("head", slv.getIntegerSort()) + cons.addSelectorSelf("tail") consListSpec.addConstructor(cons) nil = pycvc4.DatatypeConstructorDecl("nil") consListSpec.addConstructor(nil) @@ -127,10 +123,8 @@ if __name__ == "__main__": print("### Alternatively, use declareDatatype") cons2 = pycvc4.DatatypeConstructorDecl("cons") - head2 = pycvc4.DatatypeSelectorDecl("head", slv.getIntegerSort()) - tail2 = pycvc4.DatatypeSelectorDecl("tail", pycvc4.DatatypeDeclSelfSort()) - cons2.addSelector(head2) - cons2.addSelector(tail2) + cons2.addSelector("head", slv.getIntegerSort()) + cons2.addSelectorSelf("tail") nil2 = pycvc4.DatatypeConstructorDecl("nil") ctors = [cons2, nil2] consListSort2 = slv.declareDatatype("list2", ctors) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index ff25bbabb..037243ea4 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1737,32 +1737,6 @@ size_t TermHashFunction::operator()(const Term& t) const /* Datatypes */ /* -------------------------------------------------------------------------- */ -/* DatatypeSelectorDecl ----------------------------------------------------- */ - -DatatypeSelectorDecl::DatatypeSelectorDecl(const std::string& name, Sort sort) - : d_name(name), d_sort(sort) -{ -} - -DatatypeSelectorDecl::DatatypeSelectorDecl(const std::string& name, - DatatypeDeclSelfSort sort) - : d_name(name), d_sort(Sort(CVC4::Type())) -{ -} - -std::string DatatypeSelectorDecl::toString() const -{ - std::stringstream ss; - ss << d_name << ": " << d_sort; - return ss.str(); -} - -std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl) -{ - out << dtdecl.toString(); - return out; -} - /* DatatypeConstructorDecl -------------------------------------------------- */ DatatypeConstructorDecl::DatatypeConstructorDecl(const std::string& name) @@ -1770,17 +1744,16 @@ DatatypeConstructorDecl::DatatypeConstructorDecl(const std::string& name) { } -void DatatypeConstructorDecl::addSelector(const DatatypeSelectorDecl& stor) +void DatatypeConstructorDecl::addSelector(const std::string& name, Sort sort) { - CVC4::Type t = *stor.d_sort.d_type; - if (t.isNull()) - { - d_ctor->addArg(stor.d_name, DatatypeSelfType()); - } - else - { - d_ctor->addArg(stor.d_name, t); - } + CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) + << "non-null range sort for selector"; + d_ctor->addArg(name, *sort.d_type); +} + +void DatatypeConstructorDecl::addSelectorSelf(const std::string& name) +{ + d_ctor->addArg(name, DatatypeSelfType()); } std::string DatatypeConstructorDecl::toString() const @@ -1890,10 +1863,9 @@ bool DatatypeDecl::isNull() const { return isNullHelper(); } // to the new API. !!! CVC4::Datatype& DatatypeDecl::getDatatype(void) const { return *d_dtype; } -std::ostream& operator<<(std::ostream& out, - const DatatypeSelectorDecl& stordecl) +std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl) { - out << stordecl.toString(); + out << dtdecl.toString(); return out; } diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index dcf787b8e..7ccb73bc3 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -189,7 +189,6 @@ class CVC4_PUBLIC Sort { friend class DatatypeConstructorDecl; friend class DatatypeDecl; - friend class DatatypeSelectorDecl; friend class Op; friend class Solver; friend struct SortHashFunction; @@ -1138,51 +1137,6 @@ class DatatypeConstructorIterator; class DatatypeIterator; /** - * A place-holder sort to allow a DatatypeDecl to refer to itself. - * Self-sorted fields of DatatypeDecls will be properly sorted when a Sort is - * created for the DatatypeDecl. - */ -class CVC4_PUBLIC DatatypeDeclSelfSort -{ -}; - -/** - * A CVC4 datatype selector declaration. - */ -class CVC4_PUBLIC DatatypeSelectorDecl -{ - friend class DatatypeConstructorDecl; - - public: - /** - * Constructor. - * @param name the name of the datatype selector - * @param sort the sort of the datatype selector - * @return the DatatypeSelectorDecl - */ - DatatypeSelectorDecl(const std::string& name, Sort sort); - - /** - * Constructor. - * @param name the name of the datatype selector - * @param sort the sort of the datatype selector - * @return the DAtatypeSelectorDecl - */ - DatatypeSelectorDecl(const std::string& name, DatatypeDeclSelfSort sort); - - /** - * @return a string representation of this datatype selector - */ - std::string toString() const; - - private: - /* The name of the datatype selector. */ - std::string d_name; - /* The sort of the datatype selector. */ - Sort d_sort; -}; - -/** * A CVC4 datatype constructor declaration. */ class CVC4_PUBLIC DatatypeConstructorDecl @@ -1199,9 +1153,15 @@ class CVC4_PUBLIC DatatypeConstructorDecl /** * Add datatype selector declaration. - * @param stor the datatype selector declaration to add + * @param name the name of the datatype selector declaration to add + * @param sort the range sort of the datatype selector declaration to add + */ + void addSelector(const std::string& name, Sort sort); + /** + * Add datatype selector declaration whose range type is the datatype itself. + * @param name the name of the datatype selector declaration to add */ - void addSelector(const DatatypeSelectorDecl& stor); + void addSelectorSelf(const std::string& name); /** * @return a string representation of this datatype constructor declaration @@ -1768,15 +1728,6 @@ std::ostream& operator<<(std::ostream& out, const std::vector<DatatypeConstructorDecl>& vector); /** - * Serialize a datatype selector declaration to given stream. - * @param out the output stream - * @param stordecl the datatype selector declaration to be serialized - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, - const DatatypeSelectorDecl& stordecl) CVC4_PUBLIC; - -/** * Serialize a datatype to given stream. * @param out the output stream * @param dtdecl the datatype to be serialized to given stream diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index b8bf009af..bbff6f58b 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -55,7 +55,8 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": cdef cppclass DatatypeConstructorDecl: DatatypeConstructorDecl(const string& name) except + - void addSelector(const DatatypeSelectorDecl& stor) except + + void addSelector(const string& name, Sort sort) except + + void addSelectorSelf(const string& name) except + string toString() except + @@ -65,21 +66,11 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": string toString() except + - cdef cppclass DatatypeDeclSelfSort: - DatatypeDeclSelfSort() except + - - cdef cppclass DatatypeSelector: DatatypeSelector() except + string toString() except + - cdef cppclass DatatypeSelectorDecl: - DatatypeSelectorDecl(const string& name, Sort sort) except + - DatatypeSelectorDecl(const string& name, DatatypeDeclSelfSort sort) except + - string toString() except + - - cdef cppclass Op: Op() except + bint operator==(const Op&) except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index 7e0e2e3c8..d61fed0fc 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -11,9 +11,7 @@ from cvc4 cimport Datatype as c_Datatype from cvc4 cimport DatatypeConstructor as c_DatatypeConstructor from cvc4 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl from cvc4 cimport DatatypeDecl as c_DatatypeDecl -from cvc4 cimport DatatypeDeclSelfSort as c_DatatypeDeclSelfSort from cvc4 cimport DatatypeSelector as c_DatatypeSelector -from cvc4 cimport DatatypeSelectorDecl as c_DatatypeSelectorDecl from cvc4 cimport Result as c_Result from cvc4 cimport RoundingMode as c_RoundingMode from cvc4 cimport Op as c_Op @@ -131,8 +129,10 @@ cdef class DatatypeConstructorDecl: def __cinit__(self, str name): self.cddc = new c_DatatypeConstructorDecl(name.encode()) - def addSelector(self, DatatypeSelectorDecl stor): - self.cddc.addSelector(stor.cdsd[0]) + def addSelector(self, str name, Sort sort): + self.cddc.addSelector(name.encode(), sort.csort) + def addSelectorSelf(self, str name): + self.cddc.addSelectorSelf(name.encode()) def __str__(self): return self.cddc.toString().decode() @@ -159,12 +159,6 @@ cdef class DatatypeDecl: return self.cdd.toString().decode() -cdef class DatatypeDeclSelfSort: - cdef c_DatatypeDeclSelfSort cddss - def __cinit__(self): - self.cddss = c_DatatypeDeclSelfSort() - - cdef class DatatypeSelector: cdef c_DatatypeSelector cds def __cinit__(self): @@ -177,24 +171,6 @@ cdef class DatatypeSelector: return self.cds.toString().decode() -cdef class DatatypeSelectorDecl: - cdef c_DatatypeSelectorDecl* cdsd - def __cinit__(self, str name, sort): - if isinstance(sort, Sort): - self.cdsd = new c_DatatypeSelectorDecl( - <const string &> name.encode(), (<Sort?> sort).csort) - elif isinstance(sort, DatatypeDeclSelfSort): - self.cdsd = new c_DatatypeSelectorDecl( - <const string &> name.encode(), - (<DatatypeDeclSelfSort?> sort).cddss) - - def __str__(self): - return self.cdsd.toString().decode() - - def __repr__(self): - return self.cdsd.toString().decode() - - cdef class Op: cdef c_Op cop def __cinit__(self): diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h index f25282624..b404dfb13 100644 --- a/test/unit/api/datatype_api_black.h +++ b/test/unit/api/datatype_api_black.h @@ -44,8 +44,7 @@ void DatatypeBlack::testMkDatatypeSort() { DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); + cons.addSelector("head", d_solver.getIntegerSort()); dtypeSpec.addConstructor(cons); DatatypeConstructorDecl nil("nil"); dtypeSpec.addConstructor(nil); @@ -77,23 +76,18 @@ void DatatypeBlack::testMkDatatypeSorts() DatatypeDecl tree = d_solver.mkDatatypeDecl("tree"); DatatypeConstructorDecl node("node"); - DatatypeSelectorDecl left("left", unresTree); - node.addSelector(left); - DatatypeSelectorDecl right("right", unresTree); - node.addSelector(right); + node.addSelector("left", unresTree); + node.addSelector("right", unresTree); tree.addConstructor(node); DatatypeConstructorDecl leaf("leaf"); - DatatypeSelectorDecl data("data", unresList); - leaf.addSelector(data); + leaf.addSelector("data", unresList); tree.addConstructor(leaf); DatatypeDecl list = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl car("car", unresTree); - cons.addSelector(car); - DatatypeSelectorDecl cdr("cdr", unresTree); - cons.addSelector(cdr); + cons.addSelector("car", unresTree); + cons.addSelector("cdr", unresTree); list.addConstructor(cons); DatatypeConstructorDecl nil("nil"); @@ -137,10 +131,10 @@ void DatatypeBlack::testDatatypeStructs() // create datatype sort to test DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", intSort); - cons.addSelector(head); - DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); - cons.addSelector(tail); + cons.addSelector("head", intSort); + cons.addSelectorSelf("tail"); + Sort nullSort; + TS_ASSERT_THROWS(cons.addSelector("null", nullSort), CVC4ApiException&); dtypeSpec.addConstructor(cons); DatatypeConstructorDecl nil("nil"); dtypeSpec.addConstructor(nil); @@ -172,10 +166,8 @@ void DatatypeBlack::testDatatypeStructs() // create codatatype DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true); DatatypeConstructorDecl consStream("cons"); - DatatypeSelectorDecl headStream("head", intSort); - consStream.addSelector(headStream); - DatatypeSelectorDecl tailStream("tail", DatatypeDeclSelfSort()); - consStream.addSelector(tailStream); + consStream.addSelector("head", intSort); + consStream.addSelectorSelf("tail"); dtypeSpecStream.addConstructor(consStream); Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream); Datatype dtStream = dtypeSortStream.getDatatype(); @@ -213,10 +205,8 @@ void DatatypeBlack::testDatatypeNames() TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName()); TS_ASSERT(dtypeSpec.getName() == std::string("list")); DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", intSort); - cons.addSelector(head); - DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); - cons.addSelector(tail); + cons.addSelector("head", intSort); + cons.addSelectorSelf("tail"); dtypeSpec.addConstructor(cons); DatatypeConstructorDecl nil("nil"); dtypeSpec.addConstructor(nil); diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index aea41a42b..6d6557449 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -181,8 +181,7 @@ void SolverBlack::testMkDatatypeSort() { DatatypeDecl dtypeSpec = d_solver->mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); - cons.addSelector(head); + cons.addSelector("head", d_solver->getIntegerSort()); dtypeSpec.addConstructor(cons); DatatypeConstructorDecl nil("nil"); dtypeSpec.addConstructor(nil); @@ -631,10 +630,8 @@ void SolverBlack::testMkTermFromOp() DatatypeDecl listDecl = d_solver->mkDatatypeDecl("paramlist", sort); DatatypeConstructorDecl cons("cons"); DatatypeConstructorDecl nil("nil"); - DatatypeSelectorDecl head("head", sort); - DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); - cons.addSelector(head); - cons.addSelector(tail); + cons.addSelector("head", sort); + cons.addSelectorSelf("tail"); listDecl.addConstructor(cons); listDecl.addConstructor(nil); Sort listSort = d_solver->mkDatatypeSort(listDecl); @@ -941,10 +938,8 @@ void SolverBlack::testGetOp() // Test Datatypes -- more complicated DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); - DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); - cons.addSelector(head); - cons.addSelector(tail); + cons.addSelector("head", d_solver->getIntegerSort()); + cons.addSelectorSelf("tail"); consListSpec.addConstructor(cons); DatatypeConstructorDecl nil("nil"); consListSpec.addConstructor(nil); @@ -1044,10 +1039,8 @@ void SolverBlack::testSimplify() Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort()); DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); - DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); - cons.addSelector(head); - cons.addSelector(tail); + cons.addSelector("head", d_solver->getIntegerSort()); + cons.addSelectorSelf("tail"); consListSpec.addConstructor(cons); DatatypeConstructorDecl nil("nil"); consListSpec.addConstructor(nil); diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h index 1bac8a283..42d2dcb25 100644 --- a/test/unit/api/sort_black.h +++ b/test/unit/api/sort_black.h @@ -64,8 +64,7 @@ void SortBlack::testGetDatatype() // create datatype sort, check should not fail DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); + cons.addSelector("head", d_solver.getIntegerSort()); dtypeSpec.addConstructor(cons); DatatypeConstructorDecl nil("nil"); dtypeSpec.addConstructor(nil); @@ -82,10 +81,8 @@ void SortBlack::testDatatypeSorts() // create datatype sort to test DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", intSort); - cons.addSelector(head); - DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); - cons.addSelector(tail); + cons.addSelector("head", intSort); + cons.addSelectorSelf("tail"); dtypeSpec.addConstructor(cons); DatatypeConstructorDecl nil("nil"); dtypeSpec.addConstructor(nil); @@ -126,8 +123,7 @@ void SortBlack::testInstantiate() DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort); DatatypeConstructorDecl paramCons("cons"); DatatypeConstructorDecl paramNil("nil"); - DatatypeSelectorDecl paramHead("head", sort); - paramCons.addSelector(paramHead); + paramCons.addSelector("head", sort); paramDtypeSpec.addConstructor(paramCons); paramDtypeSpec.addConstructor(paramNil); Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); @@ -136,8 +132,7 @@ void SortBlack::testInstantiate() // instantiate non-parametric datatype sort, check should fail DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); + cons.addSelector("head", d_solver.getIntegerSort()); dtypeSpec.addConstructor(cons); DatatypeConstructorDecl nil("nil"); dtypeSpec.addConstructor(nil); @@ -272,8 +267,7 @@ void SortBlack::testGetDatatypeParamSorts() DatatypeDecl paramDtypeSpec = d_solver.mkDatatypeDecl("paramlist", sort); DatatypeConstructorDecl paramCons("cons"); DatatypeConstructorDecl paramNil("nil"); - DatatypeSelectorDecl paramHead("head", sort); - paramCons.addSelector(paramHead); + paramCons.addSelector("head", sort); paramDtypeSpec.addConstructor(paramCons); paramDtypeSpec.addConstructor(paramNil); Sort paramDtypeSort = d_solver.mkDatatypeSort(paramDtypeSpec); @@ -281,8 +275,7 @@ void SortBlack::testGetDatatypeParamSorts() // create non-parametric datatype sort, check should fail DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); + cons.addSelector("head", d_solver.getIntegerSort()); dtypeSpec.addConstructor(cons); DatatypeConstructorDecl nil("nil"); dtypeSpec.addConstructor(nil); @@ -295,8 +288,7 @@ void SortBlack::testGetDatatypeArity() // create datatype sort, check should not fail DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", d_solver.getIntegerSort()); - cons.addSelector(head); + cons.addSelector("head", d_solver.getIntegerSort()); dtypeSpec.addConstructor(cons); DatatypeConstructorDecl nil("nil"); dtypeSpec.addConstructor(nil); diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index 8f63c55ec..78d6ee5cc 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -199,10 +199,8 @@ void TermBlack::testGetOp() DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort); DatatypeConstructorDecl cons("cons"); DatatypeConstructorDecl nil("nil"); - DatatypeSelectorDecl head("head", sort); - DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); - cons.addSelector(head); - cons.addSelector(tail); + cons.addSelector("head", sort); + cons.addSelectorSelf("tail"); listDecl.addConstructor(cons); listDecl.addConstructor(nil); Sort listSort = d_solver.mkDatatypeSort(listDecl); |