From cdb338bb5c0fc033f6788549985c5a60ab1323b3 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 14 Sep 2020 21:21:03 -0700 Subject: [PATCH] Rename system tests to api tests and remove obsolete Java test. (#5066) --- src/main/CMakeLists.txt | 4 +- test/CMakeLists.txt | 6 +- test/api/CMakeLists.txt | 57 ++++++++++++++++++ test/{system => api}/boilerplate.cpp | 0 test/{system => api}/interactive_shell.py | 0 test/{system => api}/ouroborous.cpp | 0 test/{system => api}/reset_assertions.cpp | 0 test/{system => api}/sep_log_api.cpp | 0 test/{system => api}/smt2_compliance.cpp | 0 test/{system => api}/statistics.cpp | 0 test/{system => api}/two_solvers.cpp | 0 test/system/CMakeLists.txt | 59 ------------------- test/system/CVC4JavaTest.java | 70 ----------------------- 13 files changed, 62 insertions(+), 134 deletions(-) create mode 100644 test/api/CMakeLists.txt rename test/{system => api}/boilerplate.cpp (100%) rename test/{system => api}/interactive_shell.py (100%) rename test/{system => api}/ouroborous.cpp (100%) rename test/{system => api}/reset_assertions.cpp (100%) rename test/{system => api}/sep_log_api.cpp (100%) rename test/{system => api}/smt2_compliance.cpp (100%) rename test/{system => api}/statistics.cpp (100%) rename test/{system => api}/two_solvers.cpp (100%) delete mode 100644 test/system/CMakeLists.txt delete mode 100644 test/system/CVC4JavaTest.java diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index 8c11acf3b..5138d79b5 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -31,8 +31,8 @@ add_dependencies(main cvc4 cvc4parser gen-tokens) get_target_property(LIBCVC4_INCLUDES cvc4 INCLUDE_DIRECTORIES) target_include_directories(main PRIVATE ${LIBCVC4_INCLUDES}) -# main-test library is only used for linking against system and unit tests so -# that we don't have to include all object files of main into each unit/system +# main-test library is only used for linking against api and unit tests so +# that we don't have to include all object files of main into each api/unit # test. Do not link against main-test in any other case. add_library(main-test driver_unified.cpp $) target_compile_definitions(main-test PRIVATE -D__BUILDING_CVC4DRIVER) diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index cc05aff43..4c8b9d156 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -2,11 +2,11 @@ # Add target 'check', builds and runs # > unit tests # > regression tests of levels 0 and 1 -# > system tests +# > api tests add_custom_target(build-tests) -# Note: Do not add custom targets for running tests (regress, systemtests, +# Note: Do not add custom targets for running tests (regress, apitests, # units) as dependencies to other run targets. This will result in executing # tests multiple times. For example, if check would depend on regress it would # first run the command of the regress target (i.e., run all regression tests) @@ -24,7 +24,7 @@ add_custom_target(check if (NOT BUILD_LIB_ONLY) add_subdirectory(regress) endif() -add_subdirectory(system EXCLUDE_FROM_ALL) +add_subdirectory(api EXCLUDE_FROM_ALL) if(ENABLE_UNIT_TESTING) add_subdirectory(unit EXCLUDE_FROM_ALL) diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt new file mode 100644 index 000000000..8d9110e9f --- /dev/null +++ b/test/api/CMakeLists.txt @@ -0,0 +1,57 @@ +include_directories(.) +include_directories(${PROJECT_SOURCE_DIR}/src) +include_directories(${PROJECT_SOURCE_DIR}/src/include) +include_directories(${CMAKE_BINARY_DIR}/src) + +#-----------------------------------------------------------------------------# +# Add target 'apitests', builds and runs +# > api tests + +add_custom_target(build-apitests) +add_dependencies(build-tests build-apitests) + +add_custom_target(apitests + COMMAND ctest --output-on-failure -L "api" -j${CTEST_NTHREADS} $$ARGS + DEPENDS build-apitests) + +set(CVC4_API_TEST_FLAGS + -D__BUILDING_CVC4_API_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS) + +macro(cvc4_add_api_test name) + add_executable(${name} ${name}.cpp) + target_link_libraries(${name} main-test) + target_compile_definitions(${name} PRIVATE ${CVC4_API_TEST_FLAGS}) + add_test(api/${name} ${CMAKE_CURRENT_BINARY_DIR}/${name}) + set_tests_properties(api/${name} PROPERTIES LABELS "api") + add_dependencies(build-apitests ${name}) +endmacro() + +cvc4_add_api_test(boilerplate) +cvc4_add_api_test(ouroborous) +cvc4_add_api_test(reset_assertions) +cvc4_add_api_test(sep_log_api) +cvc4_add_api_test(smt2_compliance) +# TODO(cvc4-projects#209): Add methods for retrieving statistics to new API +# cvc4_add_api_test(statistics) +cvc4_add_api_test(two_solvers) + +# if we've built using libedit, then we want the interactive shell tests +if (USE_EDITLINE) + + # Check for pexpect -- zero return code is success + execute_process( + COMMAND ${PYTHON_EXECUTABLE} -c "import pexpect" + RESULT_VARIABLE PEXPECT_RC + ERROR_QUIET + ) + + # Add the test if we have pexpect + if(PEXPECT_RC EQUAL 0) + add_test( + NAME interactive_shell + COMMAND + "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/test/api/interactive_shell.py" + WORKING_DIRECTORY "${CMAKE_BINARY_DIR}" + ) + endif() +endif() diff --git a/test/system/boilerplate.cpp b/test/api/boilerplate.cpp similarity index 100% rename from test/system/boilerplate.cpp rename to test/api/boilerplate.cpp diff --git a/test/system/interactive_shell.py b/test/api/interactive_shell.py similarity index 100% rename from test/system/interactive_shell.py rename to test/api/interactive_shell.py diff --git a/test/system/ouroborous.cpp b/test/api/ouroborous.cpp similarity index 100% rename from test/system/ouroborous.cpp rename to test/api/ouroborous.cpp diff --git a/test/system/reset_assertions.cpp b/test/api/reset_assertions.cpp similarity index 100% rename from test/system/reset_assertions.cpp rename to test/api/reset_assertions.cpp diff --git a/test/system/sep_log_api.cpp b/test/api/sep_log_api.cpp similarity index 100% rename from test/system/sep_log_api.cpp rename to test/api/sep_log_api.cpp diff --git a/test/system/smt2_compliance.cpp b/test/api/smt2_compliance.cpp similarity index 100% rename from test/system/smt2_compliance.cpp rename to test/api/smt2_compliance.cpp diff --git a/test/system/statistics.cpp b/test/api/statistics.cpp similarity index 100% rename from test/system/statistics.cpp rename to test/api/statistics.cpp diff --git a/test/system/two_solvers.cpp b/test/api/two_solvers.cpp similarity index 100% rename from test/system/two_solvers.cpp rename to test/api/two_solvers.cpp diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt deleted file mode 100644 index a9c1a80db..000000000 --- a/test/system/CMakeLists.txt +++ /dev/null @@ -1,59 +0,0 @@ -include_directories(.) -include_directories(${PROJECT_SOURCE_DIR}/src) -include_directories(${PROJECT_SOURCE_DIR}/src/include) -include_directories(${CMAKE_BINARY_DIR}/src) - -#-----------------------------------------------------------------------------# -# Add target 'systemtests', builds and runs -# > system tests - -add_custom_target(build-systemtests) -add_dependencies(build-tests build-systemtests) - -add_custom_target(systemtests - COMMAND ctest --output-on-failure -L "system" -j${CTEST_NTHREADS} $$ARGS - DEPENDS build-systemtests) - -set(CVC4_SYSTEM_TEST_FLAGS - -D__BUILDING_CVC4_SYSTEM_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS) - -macro(cvc4_add_system_test name) - add_executable(${name} ${name}.cpp) - target_link_libraries(${name} main-test) - target_compile_definitions(${name} PRIVATE ${CVC4_SYSTEM_TEST_FLAGS}) - add_test(system/${name} ${CMAKE_CURRENT_BINARY_DIR}/${name}) - set_tests_properties(system/${name} PROPERTIES LABELS "system") - add_dependencies(build-systemtests ${name}) -endmacro() - -cvc4_add_system_test(boilerplate) -cvc4_add_system_test(ouroborous) -cvc4_add_system_test(reset_assertions) -cvc4_add_system_test(sep_log_api) -cvc4_add_system_test(smt2_compliance) -# TODO(cvc4-projects#209): Add methods for retrieving statistics to new API -# cvc4_add_system_test(statistics) -cvc4_add_system_test(two_solvers) - -# if we've built using libedit, then we want the interactive shell tests -if (USE_EDITLINE) - - # Check for pexpect -- zero return code is success - execute_process( - COMMAND ${PYTHON_EXECUTABLE} -c "import pexpect" - RESULT_VARIABLE PEXPECT_RC - ERROR_QUIET - ) - - # Add the test if we have pexpect - if(PEXPECT_RC EQUAL 0) - add_test( - NAME interactive_shell - COMMAND - "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/test/system/interactive_shell.py" - WORKING_DIRECTORY "${CMAKE_BINARY_DIR}" - ) - endif() -endif() - -# TODO: Move CVC4JavaTest.java to test/java and delete run_java_test (after full cmake migration) diff --git a/test/system/CVC4JavaTest.java b/test/system/CVC4JavaTest.java deleted file mode 100644 index c38cfab3d..000000000 --- a/test/system/CVC4JavaTest.java +++ /dev/null @@ -1,70 +0,0 @@ -/********************* */ -/*! \file CVC4JavaTest.java - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -import edu.nyu.acsys.CVC4.CVC4; - -import edu.nyu.acsys.CVC4.SmtEngine; -import edu.nyu.acsys.CVC4.ExprManager; -import edu.nyu.acsys.CVC4.Expr; -import edu.nyu.acsys.CVC4.Type; -import edu.nyu.acsys.CVC4.Kind; -import edu.nyu.acsys.CVC4.Result; -import edu.nyu.acsys.CVC4.Configuration; - -//import edu.nyu.acsys.CVC4.Exception; - -import edu.nyu.acsys.CVC4.Parser; -import edu.nyu.acsys.CVC4.ParserBuilder; - -public class CVC4JavaTest { - public static void main(String[] args) { - try { - System.loadLibrary("cvc4jni"); - - //CVC4.getDebugChannel().on("current"); - - System.out.println(Configuration.about()); - - String[] tags = Configuration.getDebugTags(); - System.out.print("available debug tags:"); - for(int i = 0; i < tags.length; ++i) { - System.out.print(" " + tags[i]); - } - System.out.println(); - - ExprManager em = new ExprManager(); - SmtEngine smt = new SmtEngine(em); - - Type t = em.booleanType(); - Expr a = em.mkVar("a", em.booleanType()); - Expr b = em.mkVar("b", em.booleanType()); - Expr e = new Expr(em.mkExpr(Kind.AND, a, b, new Expr(a).notExpr())); - System.out.println("==> " + e); - - Result r = smt.checkSat(e); - boolean correct = r.isSat() == Result.Sat.UNSAT; - - System.out.println(smt.getStatistics()); - - System.exit(correct ? 0 : 1); - } catch(Exception e) { - System.err.println(e); - System.exit(1); - } - } -} - -- 2.30.2