From: Aina Niemetz Date: Wed, 2 Dec 2020 00:30:33 +0000 (-0800) Subject: google test: Infrastructure and first api test. (#5548) X-Git-Tag: cvc5-1.0.0~2530 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a87df2bb60a8739d4eb24b60efca79f8d2b7d806;p=cvc5.git google test: Infrastructure and first api test. (#5548) This sets up the infrastructure for migrating unit tests from CxxTest to Google Test. It further migrates api/datatype_api_black to the new infrastructure. --- diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index acc13c2ee..5da6b4208 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -61,10 +61,12 @@ jobs: run: | sudo apt-get update sudo apt-get install -y \ + build-essential \ ccache \ cxxtest \ libcln-dev \ libgmp-dev \ + libgtest-dev \ libedit-dev \ flex \ libfl-dev \ @@ -72,6 +74,10 @@ jobs: python3 -m pip install toml python3 -m pip install setuptools python3 -m pip install pexpect + cd /usr/src/googletest + sudo cmake . + sudo cmake --build . --target install + cd - echo "/usr/lib/ccache" >> $GITHUB_PATH # Note: macOS comes with a libedit; it does not need to brew-installed diff --git a/CMakeLists.txt b/CMakeLists.txt index 8eab22e4a..6c3ed4bbc 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -8,7 +8,7 @@ ## All rights reserved. See the file COPYING in the top-level source ## directory for licensing information. ## -cmake_minimum_required(VERSION 3.4) +cmake_minimum_required(VERSION 3.9) #-----------------------------------------------------------------------------# # Project configuration diff --git a/INSTALL.md b/INSTALL.md index b3308726b..5693dbc1c 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -46,7 +46,7 @@ compatible. - [GNU C and C++ (gcc and g++)](https://gcc.gnu.org) or [Clang](https://clang.llvm.org) (reasonably recent versions) -- [CMake >= 3.1](https://cmake.org) +- [CMake >= 3.9](https://cmake.org) - [GNU Bash](https://www.gnu.org/software/bash/) - [Python >= 2.7](https://www.python.org) + module [toml](https://pypi.org/project/toml/) @@ -195,6 +195,12 @@ provided with CVC4. See [Testing CVC4](#Testing-CVC4) below for more details. +### Google Test Unit Testing Framework (Unit Tests) + +[Google Test](https://github.com/google/googletest) is required to optionally +run CVC4's unit tests (included with the distribution). +See [Testing CVC4](#Testing-CVC4) below for more details. + ## Language bindings CVC4 provides a complete and flexible C++ API (see `examples/api` for diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index bb53c15b0..d65e022c9 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -13,6 +13,8 @@ # custom finder modules). set(CxxTest_HOME ${CXXTEST_DIR}) find_package(CxxTest REQUIRED) +find_package(GTest REQUIRED) +include(GoogleTest) include_directories(.) include_directories(${PROJECT_SOURCE_DIR}/src) @@ -35,10 +37,48 @@ set(CVC4_CXXTEST_FLAGS_BLACK -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS) set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_CXXTEST_FLAGS_BLACK}) +# Generate and add unit test. +macro(cvc4_add_unit_test is_white name output_dir) + set(test_src ${CMAKE_CURRENT_LIST_DIR}/${name}.cpp) + add_executable(${name} ${test_src}) + gtest_add_tests(TARGET ${name}) + target_link_libraries(${name} main-test) + target_link_libraries(${name} GTest::GTest) + target_link_libraries(${name} GTest::Main) + if(USE_LFSC) + # We don't link against LFSC, because CVC4 is already linked against it. + target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR}) + endif() + if(USE_POLY) + # We don't link against libpoly, because CVC4 is already linked against it. + target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR}) + endif() + if(${is_white}) + target_compile_options(${name} PRIVATE -fno-access-control) + endif() + add_dependencies(build-units ${name}) + # Generate into bin/test/unit/. + set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir}) + set_target_properties(${name} + PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir}) + # The test target is prefixed with test identifier 'unit/' and the path, + # e.g., for '/myunittest.h' + # we create test target 'unit//myunittest' + # and run it with 'ctest -R "example//myunittest"'. + if("${output_dir}" STREQUAL "") + set(test_name unit/${name}) + else() + set(test_name unit/${output_dir}/${name}) + endif() + add_test(${test_name} ${test_bin_dir}/${name}) + set_tests_properties(${test_name} PROPERTIES LABELS "unit") +endmacro() + # Generate and add unit test. # Note: we do not use cxxtest_add_test from the FindCxxTest module since it # does not allow test names containing '/'. -macro(cvc4_add_unit_test is_white name output_dir) +# !! This macro will be removed when all unit tests are migrated to Google Test. +macro(cvc4_add_cxx_unit_test is_white name output_dir) # generate the test sources set(test_src ${CMAKE_CURRENT_BINARY_DIR}/${name}.cpp) set(test_header ${CMAKE_CURRENT_LIST_DIR}/${name}.h) @@ -110,6 +150,15 @@ macro(cvc4_add_unit_test_white name output_dir) cvc4_add_unit_test(TRUE ${name} ${output_dir}) endmacro() +# !! Will be removed when all unit tests are migrated to Google Test. +macro(cvc4_add_cxx_unit_test_black name output_dir) + cvc4_add_cxx_unit_test(FALSE ${name} ${output_dir}) +endmacro() +# !! Will be removed when all unit tests are migrated to Google Test. +macro(cvc4_add_cxx_unit_test_white name output_dir) + cvc4_add_cxx_unit_test(TRUE ${name} ${output_dir}) +endmacro() + add_subdirectory(api) add_subdirectory(base) add_subdirectory(context) diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index 1412c7f66..9fcf881a8 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_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(op_black api) +cvc4_add_cxx_unit_test_black(result_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.cpp b/test/unit/api/datatype_api_black.cpp new file mode 100644 index 000000000..f61637221 --- /dev/null +++ b/test/unit/api/datatype_api_black.cpp @@ -0,0 +1,540 @@ +/********************* */ +/*! \file datatype_api_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Aina Niemetz, Andres Noetzli + ** 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 datatype classes of the C++ API. + ** + ** Black box testing of the datatype classes of the C++ API. + **/ + +#include "test_api.h" + +using namespace CVC4::api; + +TEST_F(TestApi, mkDatatypeSort) +{ + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", d_solver.getIntegerSort()); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + dtypeSpec.addConstructor(nil); + Sort listSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype d = listSort.getDatatype(); + DatatypeConstructor consConstr = d[0]; + DatatypeConstructor nilConstr = d[1]; + EXPECT_THROW(d[2], CVC4ApiException); + ASSERT_NO_THROW(consConstr.getConstructorTerm()); + ASSERT_NO_THROW(nilConstr.getConstructorTerm()); +} + +TEST_F(TestApi, mkDatatypeSorts) +{ + /* Create two mutual datatypes corresponding to this definition + * block: + * + * DATATYPE + * tree = node(left: tree, right: tree) | leaf(data: list), + * list = cons(car: tree, cdr: list) | nil + * END; + */ + // Make unresolved types as placeholders + std::set unresTypes; + Sort unresTree = d_solver.mkUninterpretedSort("tree"); + Sort unresList = d_solver.mkUninterpretedSort("list"); + unresTypes.insert(unresTree); + unresTypes.insert(unresList); + + DatatypeDecl tree = d_solver.mkDatatypeDecl("tree"); + DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node"); + node.addSelector("left", unresTree); + node.addSelector("right", unresTree); + tree.addConstructor(node); + + DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); + leaf.addSelector("data", unresList); + tree.addConstructor(leaf); + + DatatypeDecl list = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("car", unresTree); + cons.addSelector("cdr", unresTree); + list.addConstructor(cons); + + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + list.addConstructor(nil); + + std::vector dtdecls; + dtdecls.push_back(tree); + dtdecls.push_back(list); + std::vector dtsorts; + 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++) + { + 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]; + EXPECT_EQ(dtcTreeNode.getName(), "node"); + DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0]; + EXPECT_EQ(dtsTreeNodeLeft.getName(), "left"); + // argument type should have resolved to be recursive + EXPECT_TRUE(dtsTreeNodeLeft.getRangeSort().isDatatype()); + EXPECT_EQ(dtsTreeNodeLeft.getRangeSort(), dtsorts[0]); + + // fails due to empty datatype + std::vector dtdeclsBad; + DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD"); + dtdeclsBad.push_back(emptyD); + EXPECT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException); +} + +TEST_F(TestApi, datatypeStructs) +{ + Sort intSort = d_solver.getIntegerSort(); + Sort boolSort = d_solver.getBooleanSort(); + + // create datatype sort to test + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); + DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", intSort); + cons.addSelectorSelf("tail"); + Sort nullSort; + 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(); + 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(); + EXPECT_EQ(dcons.getNumSelectors(), 2); + + // create datatype sort to test + DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum"); + DatatypeConstructorDecl ca = d_solver.mkDatatypeConstructorDecl("A"); + dtypeSpecEnum.addConstructor(ca); + DatatypeConstructorDecl cb = d_solver.mkDatatypeConstructorDecl("B"); + dtypeSpecEnum.addConstructor(cb); + DatatypeConstructorDecl cc = d_solver.mkDatatypeConstructorDecl("C"); + dtypeSpecEnum.addConstructor(cc); + Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum); + Datatype dtEnum = dtypeSortEnum.getDatatype(); + EXPECT_FALSE(dtEnum.isTuple()); + EXPECT_TRUE(dtEnum.isFinite()); + + // create codatatype + DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true); + DatatypeConstructorDecl consStream = + d_solver.mkDatatypeConstructorDecl("cons"); + consStream.addSelector("head", intSort); + consStream.addSelectorSelf("tail"); + dtypeSpecStream.addConstructor(consStream); + Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream); + Datatype dtStream = dtypeSortStream.getDatatype(); + EXPECT_TRUE(dtStream.isCodatatype()); + EXPECT_FALSE(dtStream.isFinite()); + // codatatypes may be well-founded + EXPECT_TRUE(dtStream.isWellFounded()); + + // create tuple + Sort tupSort = d_solver.mkTupleSort({boolSort}); + Datatype dtTuple = tupSort.getDatatype(); + EXPECT_TRUE(dtTuple.isTuple()); + EXPECT_FALSE(dtTuple.isRecord()); + EXPECT_TRUE(dtTuple.isFinite()); + EXPECT_TRUE(dtTuple.isWellFounded()); + + // create record + std::vector> fields = { + std::make_pair("b", boolSort), std::make_pair("i", intSort)}; + Sort recSort = d_solver.mkRecordSort(fields); + EXPECT_TRUE(recSort.isDatatype()); + Datatype dtRecord = recSort.getDatatype(); + EXPECT_FALSE(dtRecord.isTuple()); + EXPECT_TRUE(dtRecord.isRecord()); + EXPECT_FALSE(dtRecord.isFinite()); + EXPECT_TRUE(dtRecord.isWellFounded()); +} + +TEST_F(TestApi, datatypeNames) +{ + Sort intSort = d_solver.getIntegerSort(); + + // create datatype sort to test + DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("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"); + dtypeSpec.addConstructor(cons); + DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); + dtypeSpec.addConstructor(nil); + Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec); + Datatype dt = dtypeSort.getDatatype(); + 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]; + 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]; + EXPECT_EQ(dselTail.getName(), std::string("tail")); + EXPECT_EQ(dselTail.getRangeSort(), dtypeSort); + + // possible to construct null datatype declarations if not using solver + ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException); +} + +TEST_F(TestApi, parametricDatatype) +{ + std::vector 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); + + EXPECT_TRUE(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); + + 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)); +} + +TEST_F(TestApi, datatypeSimplyRec) +{ + /* 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 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 dtdecls; + dtdecls.push_back(wlist); + dtdecls.push_back(list); + dtdecls.push_back(ns); + // this is well-founded and has no nested recursion + std::vector dtsorts; + 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 + * 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 + 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 + * 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 + 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 + * 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 + 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 + * 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 v; + Sort x = d_solver.mkParamSort("X"); + v.push_back(x); + DatatypeDecl list5 = d_solver.mkDatatypeDecl("list5", v); + + std::vector 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 + 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()); +} + +TEST_F(TestApi, datatypeSpecializedCons) +{ + /* Create mutual datatypes corresponding to this definition block: + * DATATYPE + * plist[X] = pcons(car: X, cdr: plist[X]) | pnil + * END; + */ + // Make unresolved types as placeholders + std::set unresTypes; + Sort unresList = d_solver.mkSortConstructorSort("plist", 1); + unresTypes.insert(unresList); + + std::vector v; + Sort x = d_solver.mkParamSort("X"); + v.push_back(x); + DatatypeDecl plist = d_solver.mkDatatypeDecl("plist", v); + + std::vector args; + args.push_back(x); + Sort urListX = unresList.instantiate(args); + + DatatypeConstructorDecl pcons = d_solver.mkDatatypeConstructorDecl("pcons"); + pcons.addSelector("car", x); + pcons.addSelector("cdr", urListX); + plist.addConstructor(pcons); + DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("pnil"); + plist.addConstructor(nil5); + + std::vector dtdecls; + dtdecls.push_back(plist); + + std::vector dtsorts; + // make the datatype sorts + ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes)); + ASSERT_EQ(dtsorts.size(), 1); + Datatype d = dtsorts[0].getDatatype(); + DatatypeConstructor nilc = d[0]; + + Sort isort = d_solver.getIntegerSort(); + std::vector iargs; + iargs.push_back(isort); + Sort listInt = dtsorts[0].instantiate(iargs); + + Term testConsTerm; + // get the specialized constructor term for list[Int] + ASSERT_NO_THROW(testConsTerm = nilc.getSpecializedConstructorTerm(listInt)); + EXPECT_NE(testConsTerm, nilc.getConstructorTerm()); + // error to get the specialized constructor term for Int + EXPECT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException); +} diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h deleted file mode 100644 index 4564b261a..000000000 --- a/test/unit/api/datatype_api_black.h +++ /dev/null @@ -1,576 +0,0 @@ -/********************* */ -/*! \file datatype_api_black.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Aina Niemetz, Andres Noetzli - ** 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 datatype classes of the C++ API. - ** - ** Black box testing of the datatype classes of the C++ API. - **/ - -#include - -#include "api/cvc4cpp.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() -{ - DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("head", d_solver.getIntegerSort()); - dtypeSpec.addConstructor(cons); - DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); - dtypeSpec.addConstructor(nil); - Sort listSort = d_solver.mkDatatypeSort(dtypeSpec); - 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()); -} - -void DatatypeBlack::testMkDatatypeSorts() -{ - /* Create two mutual datatypes corresponding to this definition - * block: - * - * DATATYPE - * tree = node(left: tree, right: tree) | leaf(data: list), - * list = cons(car: tree, cdr: list) | nil - * END; - */ - // Make unresolved types as placeholders - std::set unresTypes; - Sort unresTree = d_solver.mkUninterpretedSort("tree"); - Sort unresList = d_solver.mkUninterpretedSort("list"); - unresTypes.insert(unresTree); - unresTypes.insert(unresList); - - DatatypeDecl tree = d_solver.mkDatatypeDecl("tree"); - DatatypeConstructorDecl node = d_solver.mkDatatypeConstructorDecl("node"); - node.addSelector("left", unresTree); - node.addSelector("right", unresTree); - tree.addConstructor(node); - - DatatypeConstructorDecl leaf = d_solver.mkDatatypeConstructorDecl("leaf"); - leaf.addSelector("data", unresList); - tree.addConstructor(leaf); - - DatatypeDecl list = d_solver.mkDatatypeDecl("list"); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("car", unresTree); - cons.addSelector("cdr", unresTree); - list.addConstructor(cons); - - DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); - list.addConstructor(nil); - - std::vector dtdecls; - dtdecls.push_back(tree); - dtdecls.push_back(list); - std::vector 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++) - { - TS_ASSERT(dtsorts[i].isDatatype()); - TS_ASSERT(!dtsorts[i].getDatatype().isFinite()); - TS_ASSERT(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"); - DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0]; - TS_ASSERT(dtsTreeNodeLeft.getName() == "left"); - // argument type should have resolved to be recursive - TS_ASSERT(dtsTreeNodeLeft.getRangeSort().isDatatype()); - TS_ASSERT(dtsTreeNodeLeft.getRangeSort() == dtsorts[0]); - - // fails due to empty datatype - std::vector dtdeclsBad; - DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD"); - dtdeclsBad.push_back(emptyD); - TS_ASSERT_THROWS(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException&); -} - -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 = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("head", intSort); - cons.addSelectorSelf("tail"); - Sort nullSort; - TS_ASSERT_THROWS(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()); - // get constructor - DatatypeConstructor dcons = dt[0]; - Term consTerm = dcons.getConstructorTerm(); - TS_ASSERT(dcons.getNumSelectors() == 2); - - // create datatype sort to test - DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum"); - DatatypeConstructorDecl ca = d_solver.mkDatatypeConstructorDecl("A"); - dtypeSpecEnum.addConstructor(ca); - DatatypeConstructorDecl cb = d_solver.mkDatatypeConstructorDecl("B"); - dtypeSpecEnum.addConstructor(cb); - DatatypeConstructorDecl cc = d_solver.mkDatatypeConstructorDecl("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 = - d_solver.mkDatatypeConstructorDecl("cons"); - consStream.addSelector("head", intSort); - consStream.addSelectorSelf("tail"); - 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> 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"); - TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName()); - TS_ASSERT(dtypeSpec.getName() == std::string("list")); - DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); - cons.addSelector("head", intSort); - cons.addSelectorSelf("tail"); - 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.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")); - TS_ASSERT(dselTail.getRangeSort() == dtypeSort); - - // possible to construct null datatype declarations if not using solver - TS_ASSERT_THROWS(DatatypeDecl().getName(), CVC4ApiException&); -} - -void DatatypeBlack::testParametricDatatype() -{ - std::vector 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 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 dtdecls; - dtdecls.push_back(wlist); - dtdecls.push_back(list); - dtdecls.push_back(ns); - // this is well-founded and has no nested recursion - std::vector 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 v; - Sort x = d_solver.mkParamSort("X"); - v.push_back(x); - DatatypeDecl list5 = d_solver.mkDatatypeDecl("list5", v); - - std::vector 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()); -} - -void DatatypeBlack::testDatatypeSpecializedCons() -{ - /* Create mutual datatypes corresponding to this definition block: - * DATATYPE - * plist[X] = pcons(car: X, cdr: plist[X]) | pnil - * END; - */ - // Make unresolved types as placeholders - std::set unresTypes; - Sort unresList = d_solver.mkSortConstructorSort("plist", 1); - unresTypes.insert(unresList); - - std::vector v; - Sort x = d_solver.mkParamSort("X"); - v.push_back(x); - DatatypeDecl plist = d_solver.mkDatatypeDecl("plist", v); - - std::vector args; - args.push_back(x); - Sort urListX = unresList.instantiate(args); - - DatatypeConstructorDecl pcons = d_solver.mkDatatypeConstructorDecl("pcons"); - pcons.addSelector("car", x); - pcons.addSelector("cdr", urListX); - plist.addConstructor(pcons); - DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("pnil"); - plist.addConstructor(nil5); - - std::vector dtdecls; - dtdecls.push_back(plist); - - std::vector dtsorts; - // make the datatype sorts - TS_ASSERT_THROWS_NOTHING(dtsorts = - d_solver.mkDatatypeSorts(dtdecls, unresTypes)); - TS_ASSERT(dtsorts.size() == 1); - Datatype d = dtsorts[0].getDatatype(); - DatatypeConstructor nilc = d[0]; - - Sort isort = d_solver.getIntegerSort(); - std::vector iargs; - iargs.push_back(isort); - Sort listInt = dtsorts[0].instantiate(iargs); - - Term testConsTerm; - // get the specialized constructor term for list[Int] - TS_ASSERT_THROWS_NOTHING(testConsTerm = - nilc.getSpecializedConstructorTerm(listInt)); - TS_ASSERT(testConsTerm != nilc.getConstructorTerm()); - // error to get the specialized constructor term for Int - TS_ASSERT_THROWS(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException&); -} diff --git a/test/unit/base/CMakeLists.txt b/test/unit/base/CMakeLists.txt index 81d27c040..8274a5a46 100644 --- a/test/unit/base/CMakeLists.txt +++ b/test/unit/base/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(map_util_black base) +cvc4_add_cxx_unit_test_black(map_util_black base) diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt index 6752f0e78..51465c622 100644 --- a/test/unit/context/CMakeLists.txt +++ b/test/unit/context/CMakeLists.txt @@ -11,10 +11,10 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(cdlist_black context) -cvc4_add_unit_test_black(cdmap_black context) -cvc4_add_unit_test_white(cdmap_white context) -cvc4_add_unit_test_black(cdo_black context) -cvc4_add_unit_test_black(context_black context) -cvc4_add_unit_test_black(context_mm_black context) -cvc4_add_unit_test_white(context_white context) +cvc4_add_cxx_unit_test_black(cdlist_black context) +cvc4_add_cxx_unit_test_black(cdmap_black context) +cvc4_add_cxx_unit_test_white(cdmap_white context) +cvc4_add_cxx_unit_test_black(cdo_black context) +cvc4_add_cxx_unit_test_black(context_black context) +cvc4_add_cxx_unit_test_black(context_mm_black context) +cvc4_add_cxx_unit_test_white(context_white context) diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt index c10648c03..6c0abc4ab 100644 --- a/test/unit/expr/CMakeLists.txt +++ b/test/unit/expr/CMakeLists.txt @@ -11,20 +11,20 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(attribute_black expr) -cvc4_add_unit_test_white(attribute_white expr) -cvc4_add_unit_test_black(expr_manager_public expr) -cvc4_add_unit_test_black(expr_public expr) -cvc4_add_unit_test_black(kind_black expr) -cvc4_add_unit_test_black(kind_map_black expr) -cvc4_add_unit_test_black(node_black expr) -cvc4_add_unit_test_black(node_algorithm_black expr) -cvc4_add_unit_test_black(node_builder_black expr) -cvc4_add_unit_test_black(node_manager_black expr) -cvc4_add_unit_test_white(node_manager_white expr) -cvc4_add_unit_test_black(node_self_iterator_black expr) -cvc4_add_unit_test_black(node_traversal_black expr) -cvc4_add_unit_test_white(node_white expr) -cvc4_add_unit_test_black(symbol_table_black expr) -cvc4_add_unit_test_black(type_cardinality_public expr) -cvc4_add_unit_test_white(type_node_white expr) +cvc4_add_cxx_unit_test_black(attribute_black expr) +cvc4_add_cxx_unit_test_white(attribute_white expr) +cvc4_add_cxx_unit_test_black(expr_manager_public expr) +cvc4_add_cxx_unit_test_black(expr_public expr) +cvc4_add_cxx_unit_test_black(kind_black expr) +cvc4_add_cxx_unit_test_black(kind_map_black expr) +cvc4_add_cxx_unit_test_black(node_black expr) +cvc4_add_cxx_unit_test_black(node_algorithm_black expr) +cvc4_add_cxx_unit_test_black(node_builder_black expr) +cvc4_add_cxx_unit_test_black(node_manager_black expr) +cvc4_add_cxx_unit_test_white(node_manager_white expr) +cvc4_add_cxx_unit_test_black(node_self_iterator_black expr) +cvc4_add_cxx_unit_test_black(node_traversal_black expr) +cvc4_add_cxx_unit_test_white(node_white expr) +cvc4_add_cxx_unit_test_black(symbol_table_black expr) +cvc4_add_cxx_unit_test_black(type_cardinality_public expr) +cvc4_add_cxx_unit_test_white(type_node_white expr) diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt index 55307db95..59c197f04 100644 --- a/test/unit/main/CMakeLists.txt +++ b/test/unit/main/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(interactive_shell_black main) +cvc4_add_cxx_unit_test_black(interactive_shell_black main) diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt index 1bdcbd5f5..4202ea0c9 100644 --- a/test/unit/parser/CMakeLists.txt +++ b/test/unit/parser/CMakeLists.txt @@ -11,5 +11,5 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(parser_black parser) -cvc4_add_unit_test_black(parser_builder_black parser) +cvc4_add_cxx_unit_test_black(parser_black parser) +cvc4_add_cxx_unit_test_black(parser_builder_black parser) diff --git a/test/unit/preprocessing/CMakeLists.txt b/test/unit/preprocessing/CMakeLists.txt index 7e142f404..a2381ba90 100644 --- a/test/unit/preprocessing/CMakeLists.txt +++ b/test/unit/preprocessing/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_white(pass_bv_gauss_white preprocessing) +cvc4_add_cxx_unit_test_white(pass_bv_gauss_white preprocessing) diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt index 3b040d1fc..93c241af9 100644 --- a/test/unit/printer/CMakeLists.txt +++ b/test/unit/printer/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_black(smt2_printer_black printer) +cvc4_add_cxx_unit_test_black(smt2_printer_black printer) diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt index bed0575c6..f866e5ffa 100644 --- a/test/unit/prop/CMakeLists.txt +++ b/test/unit/prop/CMakeLists.txt @@ -11,4 +11,4 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_white(cnf_stream_white prop) +cvc4_add_cxx_unit_test_white(cnf_stream_white prop) diff --git a/test/unit/test_api.h b/test/unit/test_api.h new file mode 100644 index 000000000..72d0658a7 --- /dev/null +++ b/test/unit/test_api.h @@ -0,0 +1,27 @@ +/********************* */ +/*! \file datatype_api_black.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** 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 Common header for API unit test. + **/ + +#ifndef CVC4__TEST__UNIT__TEST_API_H +#define CVC4__TEST__UNIT__TEST_API_H + +#include "api/cvc4cpp.h" +#include "gtest/gtest.h" + +class TestApi : public ::testing::Test +{ + protected: + CVC4::api::Solver d_solver; +}; + +#endif diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 0eccbf436..334ded2d1 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -8,24 +8,24 @@ ## All rights reserved. See the file COPYING in the top-level source ## directory for licensing information. ## -cvc4_add_unit_test_black(regexp_operation_black theory) -cvc4_add_unit_test_black(theory_black theory) -cvc4_add_unit_test_white(evaluator_white theory) -cvc4_add_unit_test_white(logic_info_white theory) -cvc4_add_unit_test_white(sequences_rewriter_white theory) -cvc4_add_unit_test_white(strings_rewriter_white theory) -cvc4_add_unit_test_white(theory_arith_white theory) -cvc4_add_unit_test_white(theory_bags_normal_form_white theory) -cvc4_add_unit_test_white(theory_bags_rewriter_white theory) -cvc4_add_unit_test_white(theory_bags_type_rules_white theory) -cvc4_add_unit_test_white(theory_bv_rewriter_white theory) -cvc4_add_unit_test_white(theory_bv_white theory) -cvc4_add_unit_test_white(theory_engine_white theory) -cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) -cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory) -cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory) -cvc4_add_unit_test_white(theory_sets_type_rules_white theory) -cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory) -cvc4_add_unit_test_white(theory_strings_word_white theory) -cvc4_add_unit_test_white(theory_white theory) -cvc4_add_unit_test_white(type_enumerator_white theory) +cvc4_add_cxx_unit_test_black(regexp_operation_black theory) +cvc4_add_cxx_unit_test_black(theory_black theory) +cvc4_add_cxx_unit_test_white(evaluator_white theory) +cvc4_add_cxx_unit_test_white(logic_info_white theory) +cvc4_add_cxx_unit_test_white(sequences_rewriter_white theory) +cvc4_add_cxx_unit_test_white(strings_rewriter_white theory) +cvc4_add_cxx_unit_test_white(theory_arith_white theory) +cvc4_add_cxx_unit_test_white(theory_bags_normal_form_white theory) +cvc4_add_cxx_unit_test_white(theory_bags_rewriter_white theory) +cvc4_add_cxx_unit_test_white(theory_bags_type_rules_white theory) +cvc4_add_cxx_unit_test_white(theory_bv_rewriter_white theory) +cvc4_add_cxx_unit_test_white(theory_bv_white theory) +cvc4_add_cxx_unit_test_white(theory_engine_white theory) +cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_instantiator_white theory) +cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_inverter_white theory) +cvc4_add_cxx_unit_test_white(theory_sets_type_enumerator_white theory) +cvc4_add_cxx_unit_test_white(theory_sets_type_rules_white theory) +cvc4_add_cxx_unit_test_white(theory_strings_skolem_cache_black theory) +cvc4_add_cxx_unit_test_white(theory_strings_word_white theory) +cvc4_add_cxx_unit_test_white(theory_white theory) +cvc4_add_cxx_unit_test_white(type_enumerator_white theory) diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index 0fd7894fe..148ae9910 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -11,25 +11,25 @@ #-----------------------------------------------------------------------------# # Add unit tests -cvc4_add_unit_test_white(array_store_all_white util) -cvc4_add_unit_test_white(assert_white util) -cvc4_add_unit_test_black(binary_heap_black util) -cvc4_add_unit_test_black(bitvector_black util) -cvc4_add_unit_test_black(boolean_simplification_black util) -cvc4_add_unit_test_black(cardinality_public util) -cvc4_add_unit_test_white(check_white util) -cvc4_add_unit_test_black(configuration_black util) -cvc4_add_unit_test_black(datatype_black util) -cvc4_add_unit_test_black(exception_black util) +cvc4_add_cxx_unit_test_white(array_store_all_white util) +cvc4_add_cxx_unit_test_white(assert_white util) +cvc4_add_cxx_unit_test_black(binary_heap_black util) +cvc4_add_cxx_unit_test_black(bitvector_black util) +cvc4_add_cxx_unit_test_black(boolean_simplification_black util) +cvc4_add_cxx_unit_test_black(cardinality_public util) +cvc4_add_cxx_unit_test_white(check_white util) +cvc4_add_cxx_unit_test_black(configuration_black util) +cvc4_add_cxx_unit_test_black(datatype_black util) +cvc4_add_cxx_unit_test_black(exception_black util) if(CVC4_USE_SYMFPU) -cvc4_add_unit_test_black(floatingpoint_black util) +cvc4_add_cxx_unit_test_black(floatingpoint_black util) endif() -cvc4_add_unit_test_black(integer_black util) -cvc4_add_unit_test_white(integer_white util) -cvc4_add_unit_test_black(output_black util) -cvc4_add_unit_test_black(rational_black util) -cvc4_add_unit_test_white(rational_white util) +cvc4_add_cxx_unit_test_black(integer_black util) +cvc4_add_cxx_unit_test_white(integer_white util) +cvc4_add_cxx_unit_test_black(output_black util) +cvc4_add_cxx_unit_test_black(rational_black util) +cvc4_add_cxx_unit_test_white(rational_white util) if(CVC4_USE_POLY_IMP) -cvc4_add_unit_test_black(real_algebraic_number_black util) +cvc4_add_cxx_unit_test_black(real_algebraic_number_black util) endif() -cvc4_add_unit_test_black(stats_black util) +cvc4_add_cxx_unit_test_black(stats_black util)