diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-24 11:35:37 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-24 11:35:37 -0600 |
commit | 90fe2a057cdcdaea34f0a03f837159d9adb45914 (patch) | |
tree | d8054e7cff139891f49bb1205c739afbbeeae7f0 /test/unit | |
parent | a431edc5eba8b04812768b475b240725fb07d8c6 (diff) |
Add missing functions to new C++ API (#3769)
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/api/datatype_api_black.h | 116 | ||||
-rw-r--r-- | test/unit/api/sort_black.h | 81 | ||||
-rw-r--r-- | test/unit/api/term_black.h | 102 |
3 files changed, 297 insertions, 2 deletions
diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h index b9c671a30..2d7a9c12b 100644 --- a/test/unit/api/datatype_api_black.h +++ b/test/unit/api/datatype_api_black.h @@ -28,6 +28,9 @@ class DatatypeBlack : public CxxTest::TestSuite void testMkDatatypeSort(); + void testDatatypeStructs(); + void testDatatypeNames(); + private: Solver d_solver; }; @@ -50,8 +53,117 @@ void DatatypeBlack::testMkDatatypeSort() DatatypeConstructor consConstr = d[0]; DatatypeConstructor nilConstr = d[1]; TS_ASSERT_THROWS(d[2], CVC4ApiException&); - TS_ASSERT(consConstr.isResolved()); - TS_ASSERT(nilConstr.isResolved()); TS_ASSERT_THROWS_NOTHING(consConstr.getConstructorTerm()); TS_ASSERT_THROWS_NOTHING(nilConstr.getConstructorTerm()); } + +void DatatypeBlack::testDatatypeStructs() +{ + Sort intSort = d_solver.getIntegerSort(); + Sort boolSort = d_solver.getBooleanSort(); + + // 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); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype dt = dtypeSort.getDatatype(); + TS_ASSERT(!dt.isCodatatype()); + TS_ASSERT(!dt.isTuple()); + TS_ASSERT(!dt.isRecord()); + TS_ASSERT(!dt.isFinite()); + TS_ASSERT(dt.isWellFounded()); + // get constructor + DatatypeConstructor dcons = dt[0]; + Term consTerm = dcons.getConstructorTerm(); + TS_ASSERT(dcons.getNumSelectors() == 2); + // get tester name: notice this is only to support the Z3-style datatypes + // prior to SMT-LIB 2.6 where testers where changed to indexed symbols. + TS_ASSERT_THROWS_NOTHING(dcons.getTesterName()); + + // create datatype sort to test + DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum"); + DatatypeConstructorDecl ca("A"); + dtypeSpecEnum.addConstructor(ca); + DatatypeConstructorDecl cb("B"); + dtypeSpecEnum.addConstructor(cb); + DatatypeConstructorDecl cc("C"); + dtypeSpecEnum.addConstructor(cc); + Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum); + Datatype dtEnum = dtypeSortEnum.getDatatype(); + TS_ASSERT(!dtEnum.isTuple()); + TS_ASSERT(dtEnum.isFinite()); + + // 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); + dtypeSpecStream.addConstructor(consStream); + Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream); + Datatype dtStream = dtypeSortStream.getDatatype(); + TS_ASSERT(dtStream.isCodatatype()); + TS_ASSERT(!dtStream.isFinite()); + // codatatypes may be well-founded + TS_ASSERT(dtStream.isWellFounded()); + + // create tuple + Sort tupSort = d_solver.mkTupleSort({boolSort}); + Datatype dtTuple = tupSort.getDatatype(); + TS_ASSERT(dtTuple.isTuple()); + TS_ASSERT(!dtTuple.isRecord()); + TS_ASSERT(dtTuple.isFinite()); + TS_ASSERT(dtTuple.isWellFounded()); + + // create record + std::vector<std::pair<std::string, Sort>> fields = { + std::make_pair("b", boolSort), std::make_pair("i", intSort)}; + Sort recSort = d_solver.mkRecordSort(fields); + TS_ASSERT(recSort.isDatatype()); + Datatype dtRecord = recSort.getDatatype(); + TS_ASSERT(!dtRecord.isTuple()); + TS_ASSERT(dtRecord.isRecord()); + TS_ASSERT(!dtRecord.isFinite()); + TS_ASSERT(dtRecord.isWellFounded()); +} + +void DatatypeBlack::testDatatypeNames() +{ + Sort intSort = d_solver.getIntegerSort(); + + // 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); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype dt = dtypeSort.getDatatype(); + TS_ASSERT(dt.getName() == std::string("list")); + TS_ASSERT_THROWS_NOTHING(dt.getConstructor("nil")); + TS_ASSERT_THROWS_NOTHING(dt["cons"]); + TS_ASSERT_THROWS(dt.getConstructor("head"), CVC4ApiException&); + TS_ASSERT_THROWS(dt.getConstructor(""), CVC4ApiException&); + + DatatypeConstructor dcons = dt[0]; + TS_ASSERT(dcons.getName() == std::string("cons")); + TS_ASSERT_THROWS_NOTHING(dcons.getSelector("head")); + TS_ASSERT_THROWS_NOTHING(dcons["tail"]); + TS_ASSERT_THROWS(dcons.getSelector("cons"), CVC4ApiException&); + + // get selector + DatatypeSelector dselTail = dcons[1]; + TS_ASSERT(dselTail.getName() == std::string("tail")); +} diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h index 4ea29b8d7..1bac8a283 100644 --- a/test/unit/api/sort_black.h +++ b/test/unit/api/sort_black.h @@ -27,6 +27,7 @@ class SortBlack : public CxxTest::TestSuite void tearDown() override; void testGetDatatype(); + void testDatatypeSorts(); void testInstantiate(); void testGetFunctionArity(); void testGetFunctionDomainSorts(); @@ -47,6 +48,9 @@ class SortBlack : public CxxTest::TestSuite void testGetTupleLength(); void testGetTupleSorts(); + void testSortCompare(); + void testSortSubtyping(); + private: Solver d_solver; }; @@ -72,6 +76,49 @@ void SortBlack::testGetDatatype() TS_ASSERT_THROWS(bvSort.getDatatype(), CVC4ApiException&); } +void SortBlack::testDatatypeSorts() +{ + Sort intSort = d_solver.getIntegerSort(); + // 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); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype dt = dtypeSort.getDatatype(); + TS_ASSERT(!dtypeSort.isConstructor()); + TS_ASSERT_THROWS(dtypeSort.getConstructorCodomainSort(), CVC4ApiException&); + TS_ASSERT_THROWS(dtypeSort.getConstructorDomainSorts(), CVC4ApiException&); + TS_ASSERT_THROWS(dtypeSort.getConstructorArity(), CVC4ApiException&); + + // get constructor + DatatypeConstructor dcons = dt[0]; + Term consTerm = dcons.getConstructorTerm(); + Sort consSort = consTerm.getSort(); + TS_ASSERT(consSort.isConstructor()); + TS_ASSERT(!consSort.isTester()); + TS_ASSERT(!consSort.isSelector()); + TS_ASSERT(consSort.getConstructorArity() == 2); + std::vector<Sort> consDomSorts = consSort.getConstructorDomainSorts(); + TS_ASSERT(consDomSorts[0] == intSort); + TS_ASSERT(consDomSorts[1] == dtypeSort); + TS_ASSERT(consSort.getConstructorCodomainSort() == dtypeSort); + + // get tester + Term isConsTerm = dcons.getTesterTerm(); + TS_ASSERT(isConsTerm.getSort().isTester()); + + // get selector + DatatypeSelector dselTail = dcons[1]; + Term tailTerm = dselTail.getSelectorTerm(); + TS_ASSERT(tailTerm.getSort().isSelector()); +} + void SortBlack::testInstantiate() { // instantiate parametric datatype, check should not fail @@ -277,3 +324,37 @@ void SortBlack::testGetTupleSorts() Sort bvSort = d_solver.mkBitVectorSort(32); TS_ASSERT_THROWS(bvSort.getTupleSorts(), CVC4ApiException&); } + +void SortBlack::testSortCompare() +{ + Sort boolSort = d_solver.getBooleanSort(); + Sort intSort = d_solver.getIntegerSort(); + Sort bvSort = d_solver.mkBitVectorSort(32); + Sort bvSort2 = d_solver.mkBitVectorSort(32); + TS_ASSERT(bvSort >= bvSort2); + TS_ASSERT(bvSort <= bvSort2); + TS_ASSERT((intSort > boolSort) != (intSort < boolSort)); + TS_ASSERT((intSort > bvSort || intSort == bvSort) == (intSort >= bvSort)); +} + +void SortBlack::testSortSubtyping() +{ + Sort intSort = d_solver.getIntegerSort(); + Sort realSort = d_solver.getRealSort(); + TS_ASSERT(intSort.isSubsortOf(realSort)); + TS_ASSERT(!realSort.isSubsortOf(intSort)); + TS_ASSERT(intSort.isComparableTo(realSort)); + TS_ASSERT(realSort.isComparableTo(intSort)); + + Sort arraySortII = d_solver.mkArraySort(intSort, intSort); + Sort arraySortIR = d_solver.mkArraySort(intSort, realSort); + TS_ASSERT(!arraySortII.isComparableTo(intSort)); + // we do not support subtyping for arrays + TS_ASSERT(!arraySortII.isComparableTo(arraySortIR)); + + Sort setSortI = d_solver.mkSetSort(intSort); + Sort setSortR = d_solver.mkSetSort(realSort); + // we support subtyping for sets + TS_ASSERT(setSortI.isSubsortOf(setSortR)); + TS_ASSERT(setSortR.isComparableTo(setSortI)); +} diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index ea619db7c..8f63c55ec 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -39,6 +39,10 @@ class TermBlack : public CxxTest::TestSuite void testIteTerm(); void testTermAssignment(); + void testTermCompare(); + void testTermChildren(); + void testSubstitute(); + void testIsConst(); private: Solver d_solver; @@ -652,3 +656,101 @@ void TermBlack::testTermAssignment() t2 = d_solver.mkReal(2); TS_ASSERT_EQUALS(t1, d_solver.mkReal(1)); } + +void TermBlack::testTermCompare() +{ + Term t1 = d_solver.mkReal(1); + Term t2 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2)); + Term t3 = d_solver.mkTerm(PLUS, d_solver.mkReal(2), d_solver.mkReal(2)); + TS_ASSERT(t2 >= t3); + TS_ASSERT(t2 <= t3); + TS_ASSERT((t1 > t2) != (t1 < t2)); + TS_ASSERT((t1 > t2 || t1 == t2) == (t1 >= t2)); +} + +void TermBlack::testTermChildren() +{ + // simple term 2+3 + Term two = d_solver.mkReal(2); + Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkReal(3)); + TS_ASSERT(t1[0] == two); + TS_ASSERT(t1.getNumChildren() == 2); + Term tnull; + TS_ASSERT_THROWS(tnull.getNumChildren(), CVC4ApiException&); + + // apply term f(2) + Sort intSort = d_solver.getIntegerSort(); + Sort fsort = d_solver.mkFunctionSort(intSort, intSort); + Term f = d_solver.mkConst(fsort, "f"); + Term t2 = d_solver.mkTerm(APPLY_UF, f, two); + // due to our higher-order view of terms, we treat f as a child of APPLY_UF + TS_ASSERT(t2.getNumChildren() == 2); + TS_ASSERT_EQUALS(t2[0], f); + TS_ASSERT_EQUALS(t2[1], two); + TS_ASSERT_THROWS(tnull[0], CVC4ApiException&); +} + +void TermBlack::testSubstitute() +{ + Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); + Term one = d_solver.mkReal(1); + Term ttrue = d_solver.mkTrue(); + Term xpx = d_solver.mkTerm(PLUS, x, x); + Term onepone = d_solver.mkTerm(PLUS, one, one); + + TS_ASSERT_EQUALS(xpx.substitute(x, one), onepone); + TS_ASSERT_EQUALS(onepone.substitute(one, x), xpx); + // incorrect due to type + TS_ASSERT_THROWS(xpx.substitute(one, ttrue), CVC4ApiException&); + + // simultaneous substitution + Term y = d_solver.mkConst(d_solver.getIntegerSort(), "y"); + Term xpy = d_solver.mkTerm(PLUS, x, y); + Term xpone = d_solver.mkTerm(PLUS, y, one); + std::vector<Term> es; + std::vector<Term> rs; + es.push_back(x); + rs.push_back(y); + es.push_back(y); + rs.push_back(one); + TS_ASSERT_EQUALS(xpy.substitute(es, rs), xpone); + + // incorrect substitution due to arity + rs.pop_back(); + TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&); + + // incorrect substitution due to types + rs.push_back(ttrue); + TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&); + + // null cannot substitute + Term tnull; + TS_ASSERT_THROWS(tnull.substitute(one, x), CVC4ApiException&); + TS_ASSERT_THROWS(xpx.substitute(tnull, x), CVC4ApiException&); + TS_ASSERT_THROWS(xpx.substitute(x, tnull), CVC4ApiException&); + rs.pop_back(); + rs.push_back(tnull); + TS_ASSERT_THROWS(xpy.substitute(es, rs), CVC4ApiException&); + es.clear(); + rs.clear(); + es.push_back(x); + rs.push_back(y); + TS_ASSERT_THROWS(tnull.substitute(es, rs), CVC4ApiException&); + es.push_back(tnull); + rs.push_back(one); + TS_ASSERT_THROWS(xpx.substitute(es, rs), CVC4ApiException&); +} + +void TermBlack::testIsConst() +{ + Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); + Term one = d_solver.mkReal(1); + Term xpone = d_solver.mkTerm(PLUS, x, one); + Term onepone = d_solver.mkTerm(PLUS, one, one); + TS_ASSERT(!x.isConst()); + TS_ASSERT(one.isConst()); + TS_ASSERT(!xpone.isConst()); + TS_ASSERT(!onepone.isConst()); + Term tnull; + TS_ASSERT_THROWS(tnull.isConst(), CVC4ApiException&); +} |