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 --- test/unit/api/datatype_api_black.h | 38 ++++++++++++++------------------------ test/unit/api/solver_black.h | 21 +++++++-------------- test/unit/api/sort_black.h | 24 ++++++++---------------- test/unit/api/term_black.h | 6 ++---- 4 files changed, 31 insertions(+), 58 deletions(-) (limited to 'test/unit') 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); -- cgit v1.2.3