diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/api/datatype_api_black.h | 286 | ||||
-rw-r--r-- | test/unit/parser/parser_black.h | 5 |
2 files changed, 290 insertions, 1 deletions
diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h index c9eaf103e..180db8f32 100644 --- a/test/unit/api/datatype_api_black.h +++ b/test/unit/api/datatype_api_black.h @@ -32,6 +32,10 @@ class DatatypeBlack : public CxxTest::TestSuite void testDatatypeStructs(); void testDatatypeNames(); + void testParametricDatatype(); + + void testDatatypeSimplyRec(); + private: Solver d_solver; }; @@ -233,3 +237,285 @@ void DatatypeBlack::testDatatypeNames() // possible to construct null datatype declarations if not using solver TS_ASSERT_THROWS(DatatypeDecl().getName(), CVC4ApiException&); } + +void DatatypeBlack::testParametricDatatype() +{ + std::vector<Sort> v; + Sort t1 = d_solver.mkParamSort("T1"); + Sort t2 = d_solver.mkParamSort("T2"); + v.push_back(t1); + v.push_back(t2); + DatatypeDecl pairSpec = d_solver.mkDatatypeDecl("pair", v); + + DatatypeConstructorDecl mkpair = + d_solver.mkDatatypeConstructorDecl("mk-pair"); + mkpair.addSelector("first", t1); + mkpair.addSelector("second", t2); + pairSpec.addConstructor(mkpair); + + Sort pairType = d_solver.mkDatatypeSort(pairSpec); + + TS_ASSERT(pairType.getDatatype().isParametric()); + + v.clear(); + v.push_back(d_solver.getIntegerSort()); + v.push_back(d_solver.getIntegerSort()); + Sort pairIntInt = pairType.instantiate(v); + v.clear(); + v.push_back(d_solver.getRealSort()); + v.push_back(d_solver.getRealSort()); + Sort pairRealReal = pairType.instantiate(v); + v.clear(); + v.push_back(d_solver.getRealSort()); + v.push_back(d_solver.getIntegerSort()); + Sort pairRealInt = pairType.instantiate(v); + v.clear(); + v.push_back(d_solver.getIntegerSort()); + v.push_back(d_solver.getRealSort()); + Sort pairIntReal = pairType.instantiate(v); + + TS_ASSERT_DIFFERS(pairIntInt, pairRealReal); + TS_ASSERT_DIFFERS(pairIntReal, pairRealReal); + TS_ASSERT_DIFFERS(pairRealInt, pairRealReal); + TS_ASSERT_DIFFERS(pairIntInt, pairIntReal); + TS_ASSERT_DIFFERS(pairIntInt, pairRealInt); + TS_ASSERT_DIFFERS(pairIntReal, pairRealInt); + + TS_ASSERT(pairRealReal.isComparableTo(pairRealReal)); + TS_ASSERT(!pairIntReal.isComparableTo(pairRealReal)); + TS_ASSERT(!pairRealInt.isComparableTo(pairRealReal)); + TS_ASSERT(!pairIntInt.isComparableTo(pairRealReal)); + TS_ASSERT(!pairRealReal.isComparableTo(pairRealInt)); + TS_ASSERT(!pairIntReal.isComparableTo(pairRealInt)); + TS_ASSERT(pairRealInt.isComparableTo(pairRealInt)); + TS_ASSERT(!pairIntInt.isComparableTo(pairRealInt)); + TS_ASSERT(!pairRealReal.isComparableTo(pairIntReal)); + TS_ASSERT(pairIntReal.isComparableTo(pairIntReal)); + TS_ASSERT(!pairRealInt.isComparableTo(pairIntReal)); + TS_ASSERT(!pairIntInt.isComparableTo(pairIntReal)); + TS_ASSERT(!pairRealReal.isComparableTo(pairIntInt)); + TS_ASSERT(!pairIntReal.isComparableTo(pairIntInt)); + TS_ASSERT(!pairRealInt.isComparableTo(pairIntInt)); + TS_ASSERT(pairIntInt.isComparableTo(pairIntInt)); + + TS_ASSERT(pairRealReal.isSubsortOf(pairRealReal)); + TS_ASSERT(!pairIntReal.isSubsortOf(pairRealReal)); + TS_ASSERT(!pairRealInt.isSubsortOf(pairRealReal)); + TS_ASSERT(!pairIntInt.isSubsortOf(pairRealReal)); + TS_ASSERT(!pairRealReal.isSubsortOf(pairRealInt)); + TS_ASSERT(!pairIntReal.isSubsortOf(pairRealInt)); + TS_ASSERT(pairRealInt.isSubsortOf(pairRealInt)); + TS_ASSERT(!pairIntInt.isSubsortOf(pairRealInt)); + TS_ASSERT(!pairRealReal.isSubsortOf(pairIntReal)); + TS_ASSERT(pairIntReal.isSubsortOf(pairIntReal)); + TS_ASSERT(!pairRealInt.isSubsortOf(pairIntReal)); + TS_ASSERT(!pairIntInt.isSubsortOf(pairIntReal)); + TS_ASSERT(!pairRealReal.isSubsortOf(pairIntInt)); + TS_ASSERT(!pairIntReal.isSubsortOf(pairIntInt)); + TS_ASSERT(!pairRealInt.isSubsortOf(pairIntInt)); + TS_ASSERT(pairIntInt.isSubsortOf(pairIntInt)); +} + +void DatatypeBlack::testDatatypeSimplyRec() +{ + /* Create mutual datatypes corresponding to this definition block: + * + * DATATYPE + * wlist = leaf(data: list), + * list = cons(car: wlist, cdr: list) | nil, + * ns = elem(ndata: set(wlist)) | elemArray(ndata2: array(list, list)) + * END; + */ + // Make unresolved types as placeholders + std::set<Sort> unresTypes; + Sort unresWList = d_solver.mkUninterpretedSort("wlist"); + Sort unresList = d_solver.mkUninterpretedSort("list"); + Sort unresNs = d_solver.mkUninterpretedSort("ns"); + unresTypes.insert(unresWList); + unresTypes.insert(unresList); + unresTypes.insert(unresNs); + + DatatypeDecl wlist = d_solver.mkDatatypeDecl("wlist"); + DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); + leaf.addSelector("data", unresList); + wlist.addConstructor(leaf); + + DatatypeDecl list = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("car", unresWList); + cons.addSelector("cdr", unresList); + list.addConstructor(cons); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + list.addConstructor(nil); + + DatatypeDecl ns = d_solver.mkDatatypeDecl("ns"); + DatatypeConstructorDecl elem = d_solver.mkDatatypeConstructorDecl("elem"); + elem.addSelector("ndata", d_solver.mkSetSort(unresWList)); + ns.addConstructor(elem); + DatatypeConstructorDecl elemArray = + d_solver.mkDatatypeConstructorDecl("elemArray"); + elemArray.addSelector("ndata", d_solver.mkArraySort(unresList, unresList)); + ns.addConstructor(elemArray); + + std::vector<DatatypeDecl> dtdecls; + dtdecls.push_back(wlist); + dtdecls.push_back(list); + dtdecls.push_back(ns); + // this is well-founded and has no nested recursion + std::vector<Sort> dtsorts; + TS_ASSERT_THROWS_NOTHING(dtsorts = + d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + TS_ASSERT(dtsorts.size() == 3); + TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[1].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[2].getDatatype().isWellFounded()); + TS_ASSERT(!dtsorts[0].getDatatype().hasNestedRecursion()); + TS_ASSERT(!dtsorts[1].getDatatype().hasNestedRecursion()); + TS_ASSERT(!dtsorts[2].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * ns2 = elem2(ndata: array(int,ns2)) | nil2 + * END; + */ + unresTypes.clear(); + Sort unresNs2 = d_solver.mkUninterpretedSort("ns2"); + unresTypes.insert(unresNs2); + + DatatypeDecl ns2 = d_solver.mkDatatypeDecl("ns2"); + DatatypeConstructorDecl elem2 = d_solver.mkDatatypeConstructorDecl("elem2"); + elem2.addSelector("ndata", + d_solver.mkArraySort(d_solver.getIntegerSort(), unresNs2)); + ns2.addConstructor(elem2); + DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil2"); + ns2.addConstructor(nil2); + + dtdecls.clear(); + dtdecls.push_back(ns2); + + dtsorts.clear(); + // this is not well-founded due to non-simple recursion + TS_ASSERT_THROWS_NOTHING(dtsorts = + d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + TS_ASSERT(dtsorts.size() == 1); + TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray()); + TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort() + == dtsorts[0]); + TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * list3 = cons3(car: ns3, cdr: list3) | nil3, + * ns3 = elem3(ndata: set(list3)) + * END; + */ + unresTypes.clear(); + Sort unresNs3 = d_solver.mkUninterpretedSort("ns3"); + unresTypes.insert(unresNs3); + Sort unresList3 = d_solver.mkUninterpretedSort("list3"); + unresTypes.insert(unresList3); + + DatatypeDecl list3 = d_solver.mkDatatypeDecl("list3"); + DatatypeConstructorDecl cons3 = d_solver.mkDatatypeConstructorDecl("cons3"); + cons3.addSelector("car", unresNs3); + cons3.addSelector("cdr", unresList3); + list3.addConstructor(cons3); + DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil3"); + list3.addConstructor(nil3); + + DatatypeDecl ns3 = d_solver.mkDatatypeDecl("ns3"); + DatatypeConstructorDecl elem3 = d_solver.mkDatatypeConstructorDecl("elem3"); + elem3.addSelector("ndata", d_solver.mkSetSort(unresList3)); + ns3.addConstructor(elem3); + + dtdecls.clear(); + dtdecls.push_back(list3); + dtdecls.push_back(ns3); + + dtsorts.clear(); + // both are well-founded and have nested recursion + TS_ASSERT_THROWS_NOTHING(dtsorts = + d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + TS_ASSERT(dtsorts.size() == 2); + TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[1].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); + TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * list4 = cons(car: set(ns4), cdr: list4) | nil, + * ns4 = elem(ndata: list4) + * END; + */ + unresTypes.clear(); + Sort unresNs4 = d_solver.mkUninterpretedSort("ns4"); + unresTypes.insert(unresNs4); + Sort unresList4 = d_solver.mkUninterpretedSort("list4"); + unresTypes.insert(unresList4); + + DatatypeDecl list4 = d_solver.mkDatatypeDecl("list4"); + DatatypeConstructorDecl cons4 = d_solver.mkDatatypeConstructorDecl("cons4"); + cons4.addSelector("car", d_solver.mkSetSort(unresNs4)); + cons4.addSelector("cdr", unresList4); + list4.addConstructor(cons4); + DatatypeConstructorDecl nil4 = d_solver.mkDatatypeConstructorDecl("nil4"); + list4.addConstructor(nil4); + + DatatypeDecl ns4 = d_solver.mkDatatypeDecl("ns4"); + DatatypeConstructorDecl elem4 = d_solver.mkDatatypeConstructorDecl("elem3"); + elem4.addSelector("ndata", unresList4); + ns4.addConstructor(elem4); + + dtdecls.clear(); + dtdecls.push_back(list4); + dtdecls.push_back(ns4); + + dtsorts.clear(); + // both are well-founded and have nested recursion + TS_ASSERT_THROWS_NOTHING(dtsorts = + d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + TS_ASSERT(dtsorts.size() == 2); + TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[1].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); + TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion()); + + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * list5[X] = cons(car: X, cdr: list5[list5[X]]) | nil + * END; + */ + unresTypes.clear(); + Sort unresList5 = d_solver.mkSortConstructorSort("list5", 1); + unresTypes.insert(unresList5); + + std::vector<Sort> v; + Sort x = d_solver.mkParamSort("X"); + v.push_back(x); + DatatypeDecl list5 = d_solver.mkDatatypeDecl("list5", v); + + std::vector<Sort> args; + args.push_back(x); + Sort urListX = unresList5.instantiate(args); + args[0] = urListX; + Sort urListListX = unresList5.instantiate(args); + + DatatypeConstructorDecl cons5 = d_solver.mkDatatypeConstructorDecl("cons5"); + cons5.addSelector("car", x); + cons5.addSelector("cdr", urListListX); + list5.addConstructor(cons5); + DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("nil5"); + list5.addConstructor(nil5); + + dtdecls.clear(); + dtdecls.push_back(list5); + + // well-founded and has nested recursion + TS_ASSERT_THROWS_NOTHING(dtsorts = + d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + TS_ASSERT(dtsorts.size() == 1); + TS_ASSERT(dtsorts[0].getDatatype().isWellFounded()); + TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion()); +} diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index a829d9a8d..f1691edd4 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -254,7 +254,10 @@ public: tryGoodInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null END;"); tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) | nil END;"); //tryGoodInput("DATATYPE tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); - tryGoodInput("DATATYPE trex = Foo | Bar END; DATATYPE tree = node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); + tryGoodInput( + "DATATYPE trex = Foo | Bar END; DATATYPE tree = " + "node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list " + "OF tree,cdr:BITVECTOR(32)) END;"); } void testBadCvc4Inputs() { |