From f48b987d63fef3f698e02c9a48fdba33ffb1c564 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 11 Mar 2020 22:45:03 -0500 Subject: Simplifications to the Datatypes API (#4040) Removes DatatypeSelectorDecl and DatatypeDeclSelfSort. Add selectors is now inlined. A special case is added for the "self selector", instead of using a class as a dummy argument. I updated the Python files, although would be helpful to double check this is correct. Co-authored-by: makaimann --- examples/api/datatypes-new.cpp | 18 ++++++------------ examples/api/python/datatypes.py | 18 ++++++------------ 2 files changed, 12 insertions(+), 24 deletions(-) (limited to 'examples/api') 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 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) -- cgit v1.2.3