diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-17 20:19:24 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-17 20:19:24 -0600 |
commit | 11bc0e4c3147b0fce3033b6a4290d8730aa401ad (patch) | |
tree | ce273375634b5e9ea3981855f57f693125b6f8cd /examples/api | |
parent | 990ff24487fd0b6998231894825eb9cd4610494e (diff) |
Updates to the unit tests, api, and examples for datatypes (#3459)
* Updates to the unit tests, api, and examples for datatypes
* Format
Diffstat (limited to 'examples/api')
-rw-r--r-- | examples/api/datatypes-new.cpp | 12 | ||||
-rw-r--r-- | examples/api/datatypes.cpp | 2 |
2 files changed, 10 insertions, 4 deletions
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index 8c6257725..efbd33645 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -27,7 +27,7 @@ void test(Solver& slv, Sort& consListSort) // the complete spec for the datatype from the DatatypeSort, and // this Datatype object has constructor symbols (and others) filled in. - Datatype consList = consListSort.getDatatype(); + const Datatype& consList = consListSort.getDatatype(); // t = cons 0 nil // @@ -103,7 +103,7 @@ void test(Solver& slv, Sort& consListSort) Sort paramConsIntListSort = paramConsListSort.instantiate(std::vector<Sort>{slv.getIntegerSort()}); - Datatype paramConsList = paramConsListSort.getDatatype(); + const Datatype& paramConsList = paramConsListSort.getDatatype(); std::cout << "parameterized datatype sort is " << std::endl; for (const DatatypeConstructor& ctor : paramConsList) @@ -169,7 +169,13 @@ int main() << ">>> Alternatively, use declareDatatype" << std::endl; std::cout << std::endl; - std::vector<DatatypeConstructorDecl> ctors = {cons, nil}; + DatatypeConstructorDecl cons2("cons"); + DatatypeSelectorDecl head2("head", slv.getIntegerSort()); + DatatypeSelectorDecl tail2("tail", DatatypeDeclSelfSort()); + cons2.addSelector(head2); + cons2.addSelector(tail2); + DatatypeConstructorDecl nil2("nil"); + std::vector<DatatypeConstructorDecl> ctors = {cons2, nil2}; Sort consListSort2 = slv.declareDatatype("list2", ctors); test(slv, consListSort2); diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp index dabc1228f..34d440e3e 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/datatypes.cpp @@ -114,7 +114,7 @@ int main() { DatatypeType paramConsListType = em.mkDatatypeType(paramConsListSpec); Type paramConsIntListType = paramConsListType.instantiate(std::vector<Type>{em.integerType()}); - Datatype paramConsList = paramConsListType.getDatatype(); + const Datatype& paramConsList = paramConsListType.getDatatype(); std::cout << "parameterized datatype sort is " << std::endl; for (const DatatypeConstructor& ctor : paramConsList) |