diff options
Diffstat (limited to 'test/unit/api')
| -rw-r--r-- | test/unit/api/CMakeLists.txt | 10 | ||||
| -rw-r--r-- | test/unit/api/datatype_api_black.cpp (renamed from test/unit/api/datatype_api_black.h) | 306 | ||||
| -rw-r--r-- | test/unit/api/result_black.cpp | 115 | ||||
| -rw-r--r-- | test/unit/api/result_black.h | 132 |
4 files changed, 255 insertions, 308 deletions
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index 1412c7f66..a8c696c00 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -12,10 +12,10 @@ # Add unit tests cvc4_add_unit_test_black(datatype_api_black api) -cvc4_add_unit_test_black(op_black api) +cvc4_add_cxx_unit_test_black(op_black api) cvc4_add_unit_test_black(result_black api) -cvc4_add_unit_test_black(solver_black api) -cvc4_add_unit_test_black(sort_black api) -cvc4_add_unit_test_black(term_black api) -cvc4_add_unit_test_black(grammar_black api) +cvc4_add_cxx_unit_test_black(solver_black api) +cvc4_add_cxx_unit_test_black(sort_black api) +cvc4_add_cxx_unit_test_black(term_black api) +cvc4_add_cxx_unit_test_black(grammar_black api) diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.cpp index 4564b261a..f61637221 100644 --- a/test/unit/api/datatype_api_black.h +++ b/test/unit/api/datatype_api_black.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file datatype_api_black.h +/*! \file datatype_api_black.cpp ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Aina Niemetz, Andres Noetzli @@ -14,39 +14,11 @@ ** Black box testing of the datatype classes of the C++ API. **/ -#include <cxxtest/TestSuite.h> - -#include "api/cvc4cpp.h" +#include "test_api.h" using namespace CVC4::api; -class DatatypeBlack : public CxxTest::TestSuite -{ - public: - void setUp() override; - void tearDown() override; - - void testMkDatatypeSort(); - void testMkDatatypeSorts(); - - void testDatatypeStructs(); - void testDatatypeNames(); - - void testParametricDatatype(); - - void testDatatypeSimplyRec(); - - void testDatatypeSpecializedCons(); - - private: - Solver d_solver; -}; - -void DatatypeBlack::setUp() {} - -void DatatypeBlack::tearDown() {} - -void DatatypeBlack::testMkDatatypeSort() +TEST_F(TestApi, mkDatatypeSort) { DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); @@ -58,12 +30,12 @@ void DatatypeBlack::testMkDatatypeSort() Datatype d = listSort.getDatatype(); DatatypeConstructor consConstr = d[0]; DatatypeConstructor nilConstr = d[1]; - TS_ASSERT_THROWS(d[2], CVC4ApiException&); - TS_ASSERT_THROWS_NOTHING(consConstr.getConstructorTerm()); - TS_ASSERT_THROWS_NOTHING(nilConstr.getConstructorTerm()); + EXPECT_THROW(d[2], CVC4ApiException); + ASSERT_NO_THROW(consConstr.getConstructorTerm()); + ASSERT_NO_THROW(nilConstr.getConstructorTerm()); } -void DatatypeBlack::testMkDatatypeSorts() +TEST_F(TestApi, mkDatatypeSorts) { /* Create two mutual datatypes corresponding to this definition * block: @@ -103,33 +75,32 @@ void DatatypeBlack::testMkDatatypeSorts() dtdecls.push_back(tree); dtdecls.push_back(list); std::vector<Sort> dtsorts; - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == dtdecls.size()); - for (unsigned i = 0, ndecl = dtdecls.size(); i < ndecl; i++) + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), dtdecls.size()); + for (size_t i = 0, ndecl = dtdecls.size(); i < ndecl; i++) { - TS_ASSERT(dtsorts[i].isDatatype()); - TS_ASSERT(!dtsorts[i].getDatatype().isFinite()); - TS_ASSERT(dtsorts[i].getDatatype().getName() == dtdecls[i].getName()); + ASSERT_TRUE(dtsorts[i].isDatatype()); + EXPECT_FALSE(dtsorts[i].getDatatype().isFinite()); + EXPECT_EQ(dtsorts[i].getDatatype().getName(), dtdecls[i].getName()); } // verify the resolution was correct Datatype dtTree = dtsorts[0].getDatatype(); DatatypeConstructor dtcTreeNode = dtTree[0]; - TS_ASSERT(dtcTreeNode.getName() == "node"); + EXPECT_EQ(dtcTreeNode.getName(), "node"); DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0]; - TS_ASSERT(dtsTreeNodeLeft.getName() == "left"); + EXPECT_EQ(dtsTreeNodeLeft.getName(), "left"); // argument type should have resolved to be recursive - TS_ASSERT(dtsTreeNodeLeft.getRangeSort().isDatatype()); - TS_ASSERT(dtsTreeNodeLeft.getRangeSort() == dtsorts[0]); + EXPECT_TRUE(dtsTreeNodeLeft.getRangeSort().isDatatype()); + EXPECT_EQ(dtsTreeNodeLeft.getRangeSort(), dtsorts[0]); // fails due to empty datatype std::vector<DatatypeDecl> dtdeclsBad; DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD"); dtdeclsBad.push_back(emptyD); - TS_ASSERT_THROWS(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException&); + EXPECT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException); } -void DatatypeBlack::testDatatypeStructs() +TEST_F(TestApi, datatypeStructs) { Sort intSort = d_solver.getIntegerSort(); Sort boolSort = d_solver.getBooleanSort(); @@ -140,21 +111,21 @@ void DatatypeBlack::testDatatypeStructs() cons.addSelector("head", intSort); cons.addSelectorSelf("tail"); Sort nullSort; - TS_ASSERT_THROWS(cons.addSelector("null", nullSort), CVC4ApiException&); + EXPECT_THROW(cons.addSelector("null", nullSort), CVC4ApiException); dtypeSpec.addConstructor(cons); DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("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()); + EXPECT_FALSE(dt.isCodatatype()); + EXPECT_FALSE(dt.isTuple()); + EXPECT_FALSE(dt.isRecord()); + EXPECT_FALSE(dt.isFinite()); + EXPECT_TRUE(dt.isWellFounded()); // get constructor DatatypeConstructor dcons = dt[0]; Term consTerm = dcons.getConstructorTerm(); - TS_ASSERT(dcons.getNumSelectors() == 2); + EXPECT_EQ(dcons.getNumSelectors(), 2); // create datatype sort to test DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum"); @@ -166,8 +137,8 @@ void DatatypeBlack::testDatatypeStructs() dtypeSpecEnum.addConstructor(cc); Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum); Datatype dtEnum = dtypeSortEnum.getDatatype(); - TS_ASSERT(!dtEnum.isTuple()); - TS_ASSERT(dtEnum.isFinite()); + EXPECT_FALSE(dtEnum.isTuple()); + EXPECT_TRUE(dtEnum.isFinite()); // create codatatype DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true); @@ -178,39 +149,39 @@ void DatatypeBlack::testDatatypeStructs() dtypeSpecStream.addConstructor(consStream); Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream); Datatype dtStream = dtypeSortStream.getDatatype(); - TS_ASSERT(dtStream.isCodatatype()); - TS_ASSERT(!dtStream.isFinite()); + EXPECT_TRUE(dtStream.isCodatatype()); + EXPECT_FALSE(dtStream.isFinite()); // codatatypes may be well-founded - TS_ASSERT(dtStream.isWellFounded()); + EXPECT_TRUE(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()); + EXPECT_TRUE(dtTuple.isTuple()); + EXPECT_FALSE(dtTuple.isRecord()); + EXPECT_TRUE(dtTuple.isFinite()); + EXPECT_TRUE(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()); + EXPECT_TRUE(recSort.isDatatype()); Datatype dtRecord = recSort.getDatatype(); - TS_ASSERT(!dtRecord.isTuple()); - TS_ASSERT(dtRecord.isRecord()); - TS_ASSERT(!dtRecord.isFinite()); - TS_ASSERT(dtRecord.isWellFounded()); + EXPECT_FALSE(dtRecord.isTuple()); + EXPECT_TRUE(dtRecord.isRecord()); + EXPECT_FALSE(dtRecord.isFinite()); + EXPECT_TRUE(dtRecord.isWellFounded()); } -void DatatypeBlack::testDatatypeNames() +TEST_F(TestApi, datatypeNames) { Sort intSort = d_solver.getIntegerSort(); // create datatype sort to test DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName()); - TS_ASSERT(dtypeSpec.getName() == std::string("list")); + ASSERT_NO_THROW(dtypeSpec.getName()); + EXPECT_EQ(dtypeSpec.getName(), std::string("list")); DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); cons.addSelector("head", intSort); cons.addSelectorSelf("tail"); @@ -219,28 +190,28 @@ void DatatypeBlack::testDatatypeNames() 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&); + EXPECT_EQ(dt.getName(), std::string("list")); + ASSERT_NO_THROW(dt.getConstructor("nil")); + ASSERT_NO_THROW(dt["cons"]); + ASSERT_THROW(dt.getConstructor("head"), CVC4ApiException); + ASSERT_THROW(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&); + EXPECT_EQ(dcons.getName(), std::string("cons")); + ASSERT_NO_THROW(dcons.getSelector("head")); + ASSERT_NO_THROW(dcons["tail"]); + ASSERT_THROW(dcons.getSelector("cons"), CVC4ApiException); // get selector DatatypeSelector dselTail = dcons[1]; - TS_ASSERT(dselTail.getName() == std::string("tail")); - TS_ASSERT(dselTail.getRangeSort() == dtypeSort); + EXPECT_EQ(dselTail.getName(), std::string("tail")); + EXPECT_EQ(dselTail.getRangeSort(), dtypeSort); // possible to construct null datatype declarations if not using solver - TS_ASSERT_THROWS(DatatypeDecl().getName(), CVC4ApiException&); + ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException); } -void DatatypeBlack::testParametricDatatype() +TEST_F(TestApi, parametricDatatype) { std::vector<Sort> v; Sort t1 = d_solver.mkParamSort("T1"); @@ -257,7 +228,7 @@ void DatatypeBlack::testParametricDatatype() Sort pairType = d_solver.mkDatatypeSort(pairSpec); - TS_ASSERT(pairType.getDatatype().isParametric()); + EXPECT_TRUE(pairType.getDatatype().isParametric()); v.clear(); v.push_back(d_solver.getIntegerSort()); @@ -276,49 +247,49 @@ void DatatypeBlack::testParametricDatatype() 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)); + EXPECT_NE(pairIntInt, pairRealReal); + EXPECT_NE(pairIntReal, pairRealReal); + EXPECT_NE(pairRealInt, pairRealReal); + EXPECT_NE(pairIntInt, pairIntReal); + EXPECT_NE(pairIntInt, pairRealInt); + EXPECT_NE(pairIntReal, pairRealInt); + + EXPECT_TRUE(pairRealReal.isComparableTo(pairRealReal)); + EXPECT_FALSE(pairIntReal.isComparableTo(pairRealReal)); + EXPECT_FALSE(pairRealInt.isComparableTo(pairRealReal)); + EXPECT_FALSE(pairIntInt.isComparableTo(pairRealReal)); + EXPECT_FALSE(pairRealReal.isComparableTo(pairRealInt)); + EXPECT_FALSE(pairIntReal.isComparableTo(pairRealInt)); + EXPECT_TRUE(pairRealInt.isComparableTo(pairRealInt)); + EXPECT_FALSE(pairIntInt.isComparableTo(pairRealInt)); + EXPECT_FALSE(pairRealReal.isComparableTo(pairIntReal)); + EXPECT_TRUE(pairIntReal.isComparableTo(pairIntReal)); + EXPECT_FALSE(pairRealInt.isComparableTo(pairIntReal)); + EXPECT_FALSE(pairIntInt.isComparableTo(pairIntReal)); + EXPECT_FALSE(pairRealReal.isComparableTo(pairIntInt)); + EXPECT_FALSE(pairIntReal.isComparableTo(pairIntInt)); + EXPECT_FALSE(pairRealInt.isComparableTo(pairIntInt)); + EXPECT_TRUE(pairIntInt.isComparableTo(pairIntInt)); + + EXPECT_TRUE(pairRealReal.isSubsortOf(pairRealReal)); + EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealReal)); + EXPECT_FALSE(pairRealInt.isSubsortOf(pairRealReal)); + EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealReal)); + EXPECT_FALSE(pairRealReal.isSubsortOf(pairRealInt)); + EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealInt)); + EXPECT_TRUE(pairRealInt.isSubsortOf(pairRealInt)); + EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealInt)); + EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntReal)); + EXPECT_TRUE(pairIntReal.isSubsortOf(pairIntReal)); + EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntReal)); + EXPECT_FALSE(pairIntInt.isSubsortOf(pairIntReal)); + EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntInt)); + EXPECT_FALSE(pairIntReal.isSubsortOf(pairIntInt)); + EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntInt)); + EXPECT_TRUE(pairIntInt.isSubsortOf(pairIntInt)); } -void DatatypeBlack::testDatatypeSimplyRec() +TEST_F(TestApi, datatypeSimplyRec) { /* Create mutual datatypes corresponding to this definition block: * @@ -365,15 +336,14 @@ void DatatypeBlack::testDatatypeSimplyRec() 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()); + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 3); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[2].getDatatype().isWellFounded()); + EXPECT_FALSE(dtsorts[0].getDatatype().hasNestedRecursion()); + EXPECT_FALSE(dtsorts[1].getDatatype().hasNestedRecursion()); + EXPECT_FALSE(dtsorts[2].getDatatype().hasNestedRecursion()); /* Create mutual datatypes corresponding to this definition block: * DATATYPE @@ -397,14 +367,13 @@ void DatatypeBlack::testDatatypeSimplyRec() 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()); + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 1); + ASSERT_TRUE(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray()); + EXPECT_EQ(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort(), + dtsorts[0]); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); /* Create mutual datatypes corresponding to this definition block: * DATATYPE @@ -437,13 +406,12 @@ void DatatypeBlack::testDatatypeSimplyRec() 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()); + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 2); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); + EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion()); /* Create mutual datatypes corresponding to this definition block: * DATATYPE @@ -476,13 +444,12 @@ void DatatypeBlack::testDatatypeSimplyRec() 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()); + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 2); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); + EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion()); /* Create mutual datatypes corresponding to this definition block: * DATATYPE @@ -515,14 +482,13 @@ void DatatypeBlack::testDatatypeSimplyRec() 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()); + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 1); + EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded()); + EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion()); } -void DatatypeBlack::testDatatypeSpecializedCons() +TEST_F(TestApi, datatypeSpecializedCons) { /* Create mutual datatypes corresponding to this definition block: * DATATYPE @@ -555,9 +521,8 @@ void DatatypeBlack::testDatatypeSpecializedCons() std::vector<Sort> dtsorts; // make the datatype sorts - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == 1); + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 1); Datatype d = dtsorts[0].getDatatype(); DatatypeConstructor nilc = d[0]; @@ -568,9 +533,8 @@ void DatatypeBlack::testDatatypeSpecializedCons() Term testConsTerm; // get the specialized constructor term for list[Int] - TS_ASSERT_THROWS_NOTHING(testConsTerm = - nilc.getSpecializedConstructorTerm(listInt)); - TS_ASSERT(testConsTerm != nilc.getConstructorTerm()); + ASSERT_NO_THROW(testConsTerm = nilc.getSpecializedConstructorTerm(listInt)); + EXPECT_NE(testConsTerm, nilc.getConstructorTerm()); // error to get the specialized constructor term for Int - TS_ASSERT_THROWS(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException&); + EXPECT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException); } diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp new file mode 100644 index 000000000..260845495 --- /dev/null +++ b/test/unit/api/result_black.cpp @@ -0,0 +1,115 @@ +/********************* */ +/*! \file result_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of the Result class + **/ + +#include "test_api.h" + +using namespace CVC4::api; + +class TestApiResultBlack : public TestApi +{ +}; + +TEST_F(TestApiResultBlack, isNull) +{ + Result res_null; + ASSERT_TRUE(res_null.isNull()); + ASSERT_FALSE(res_null.isSat()); + ASSERT_FALSE(res_null.isUnsat()); + ASSERT_FALSE(res_null.isSatUnknown()); + ASSERT_FALSE(res_null.isEntailed()); + ASSERT_FALSE(res_null.isNotEntailed()); + ASSERT_FALSE(res_null.isEntailmentUnknown()); + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(u_sort, "x"); + d_solver.assertFormula(x.eqTerm(x)); + Result res = d_solver.checkSat(); + ASSERT_FALSE(res.isNull()); +} + +TEST_F(TestApiResultBlack, eq) +{ + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(u_sort, "x"); + d_solver.assertFormula(x.eqTerm(x)); + Result res; + Result res2 = d_solver.checkSat(); + Result res3 = d_solver.checkSat(); + res = res2; + EXPECT_EQ(res, res2); + EXPECT_EQ(res3, res2); +} + +TEST_F(TestApiResultBlack, isSat) +{ + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(u_sort, "x"); + d_solver.assertFormula(x.eqTerm(x)); + Result res = d_solver.checkSat(); + ASSERT_TRUE(res.isSat()); + ASSERT_FALSE(res.isSatUnknown()); +} + +TEST_F(TestApiResultBlack, isUnsat) +{ + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkVar(u_sort, "x"); + d_solver.assertFormula(x.eqTerm(x).notTerm()); + Result res = d_solver.checkSat(); + ASSERT_TRUE(res.isUnsat()); + ASSERT_FALSE(res.isSatUnknown()); +} + +TEST_F(TestApiResultBlack, isSatUnknown) +{ + d_solver.setLogic("QF_NIA"); + d_solver.setOption("incremental", "false"); + d_solver.setOption("solve-int-as-bv", "32"); + Sort int_sort = d_solver.getIntegerSort(); + Term x = d_solver.mkVar(int_sort, "x"); + d_solver.assertFormula(x.eqTerm(x).notTerm()); + Result res = d_solver.checkSat(); + ASSERT_FALSE(res.isSat()); + ASSERT_TRUE(res.isSatUnknown()); +} + +TEST_F(TestApiResultBlack, isEntailed) +{ + d_solver.setOption("incremental", "true"); + Sort u_sort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkConst(u_sort, "x"); + Term y = d_solver.mkConst(u_sort, "y"); + Term a = x.eqTerm(y).notTerm(); + Term b = x.eqTerm(y); + d_solver.assertFormula(a); + Result entailed = d_solver.checkEntailed(a); + ASSERT_TRUE(entailed.isEntailed()); + ASSERT_FALSE(entailed.isEntailmentUnknown()); + Result not_entailed = d_solver.checkEntailed(b); + ASSERT_TRUE(not_entailed.isNotEntailed()); + ASSERT_FALSE(not_entailed.isEntailmentUnknown()); +} + +TEST_F(TestApiResultBlack, isEntailmentUnknown) +{ + d_solver.setLogic("QF_NIA"); + d_solver.setOption("incremental", "false"); + d_solver.setOption("solve-int-as-bv", "32"); + Sort int_sort = d_solver.getIntegerSort(); + Term x = d_solver.mkVar(int_sort, "x"); + d_solver.assertFormula(x.eqTerm(x).notTerm()); + Result res = d_solver.checkEntailed(x.eqTerm(x)); + ASSERT_FALSE(res.isEntailed()); + ASSERT_TRUE(res.isEntailmentUnknown()); + EXPECT_EQ(res.getUnknownExplanation(), "UNKNOWN_REASON"); +} diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h deleted file mode 100644 index aaa59e506..000000000 --- a/test/unit/api/result_black.h +++ /dev/null @@ -1,132 +0,0 @@ -/********************* */ -/*! \file result_black.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Black box testing of the Result class - **/ - -#include <cxxtest/TestSuite.h> - -#include "api/cvc4cpp.h" - -using namespace CVC4::api; - -class ResultBlack : public CxxTest::TestSuite -{ - public: - void setUp() { d_solver.reset(new Solver()); } - void tearDown() override { d_solver.reset(nullptr); } - - void testIsNull(); - void testEq(); - void testIsSat(); - void testIsUnsat(); - void testIsSatUnknown(); - void testIsEntailed(); - void testIsEntailmentUnknown(); - - private: - std::unique_ptr<Solver> d_solver; -}; - -void ResultBlack::testIsNull() -{ - Result res_null; - TS_ASSERT(res_null.isNull()); - TS_ASSERT(!res_null.isSat()); - TS_ASSERT(!res_null.isUnsat()); - TS_ASSERT(!res_null.isSatUnknown()); - TS_ASSERT(!res_null.isEntailed()); - TS_ASSERT(!res_null.isNotEntailed()); - TS_ASSERT(!res_null.isEntailmentUnknown()); - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x)); - Result res = d_solver->checkSat(); - TS_ASSERT(!res.isNull()); -} - -void ResultBlack::testEq() -{ - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x)); - Result res; - Result res2 = d_solver->checkSat(); - Result res3 = d_solver->checkSat(); - res = res2; - TS_ASSERT_EQUALS(res, res2); - TS_ASSERT_EQUALS(res3, res2); -} - -void ResultBlack::testIsSat() -{ - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x)); - Result res = d_solver->checkSat(); - TS_ASSERT(res.isSat()); - TS_ASSERT(!res.isSatUnknown()); -} - -void ResultBlack::testIsUnsat() -{ - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkVar(u_sort, "x"); - d_solver->assertFormula(x.eqTerm(x).notTerm()); - Result res = d_solver->checkSat(); - TS_ASSERT(res.isUnsat()); - TS_ASSERT(!res.isSatUnknown()); -} - -void ResultBlack::testIsSatUnknown() -{ - d_solver->setLogic("QF_NIA"); - d_solver->setOption("incremental", "false"); - d_solver->setOption("solve-int-as-bv", "32"); - Sort int_sort = d_solver->getIntegerSort(); - Term x = d_solver->mkVar(int_sort, "x"); - d_solver->assertFormula(x.eqTerm(x).notTerm()); - Result res = d_solver->checkSat(); - TS_ASSERT(!res.isSat()); - TS_ASSERT(res.isSatUnknown()); -} - -void ResultBlack::testIsEntailed() -{ - d_solver->setOption("incremental", "true"); - Sort u_sort = d_solver->mkUninterpretedSort("u"); - Term x = d_solver->mkConst(u_sort, "x"); - Term y = d_solver->mkConst(u_sort, "y"); - Term a = x.eqTerm(y).notTerm(); - Term b = x.eqTerm(y); - d_solver->assertFormula(a); - Result entailed = d_solver->checkEntailed(a); - TS_ASSERT(entailed.isEntailed()); - TS_ASSERT(!entailed.isEntailmentUnknown()); - Result not_entailed = d_solver->checkEntailed(b); - TS_ASSERT(not_entailed.isNotEntailed()); - TS_ASSERT(!not_entailed.isEntailmentUnknown()); -} - -void ResultBlack::testIsEntailmentUnknown() -{ - d_solver->setLogic("QF_NIA"); - d_solver->setOption("incremental", "false"); - d_solver->setOption("solve-int-as-bv", "32"); - Sort int_sort = d_solver->getIntegerSort(); - Term x = d_solver->mkVar(int_sort, "x"); - d_solver->assertFormula(x.eqTerm(x).notTerm()); - Result res = d_solver->checkEntailed(x.eqTerm(x)); - TS_ASSERT(!res.isEntailed()); - TS_ASSERT(res.isEntailmentUnknown()); - TS_ASSERT_EQUALS(res.getUnknownExplanation(), "UNKNOWN_REASON"); -} - |