From 40272d5f3a6568293679d5816adc533831b0677f Mon Sep 17 00:00:00 2001 From: yoni206 Date: Tue, 16 Nov 2021 20:56:37 +0200 Subject: [PATCH] =?utf8?q?Translating=20API=20tests=20to=20Python=20?= =?utf8?q?=E2=80=94=20part=201=20(#7597)?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit This PR translates some of the API tests from here to Python. The other tests are translated in a private branch and will be added in a separate PR. --- test/CMakeLists.txt | 1 + test/api/CMakeLists.txt | 64 ++--------------------- test/api/cpp/CMakeLists.txt | 56 ++++++++++++++++++++ test/api/{ => cpp}/boilerplate.cpp | 0 test/api/{ => cpp}/issue4889.cpp | 0 test/api/{ => cpp}/issue5074.cpp | 0 test/api/{ => cpp}/issue6111.cpp | 0 test/api/{ => cpp}/ouroborous.cpp | 0 test/api/{ => cpp}/proj-issue306.cpp | 0 test/api/{ => cpp}/proj-issue334.cpp | 0 test/api/{ => cpp}/reset_assertions.cpp | 0 test/api/{ => cpp}/sep_log_api.cpp | 0 test/api/{ => cpp}/smt2_compliance.cpp | 0 test/api/{ => cpp}/two_solvers.cpp | 0 test/api/python/CMakeLists.txt | 35 +++++++++++++ test/api/python/boilerplate.py | 24 +++++++++ test/api/python/issue4889.py | 31 +++++++++++ test/api/python/issue5074.py | 25 +++++++++ test/api/python/issue6111.py | 48 +++++++++++++++++ test/binary/CMakeLists.txt | 42 +++++++++++++++ test/{api => binary}/interactive_shell.py | 0 test/unit/api/python/CMakeLists.txt | 8 +-- 22 files changed, 269 insertions(+), 65 deletions(-) create mode 100644 test/api/cpp/CMakeLists.txt rename test/api/{ => cpp}/boilerplate.cpp (100%) rename test/api/{ => cpp}/issue4889.cpp (100%) rename test/api/{ => cpp}/issue5074.cpp (100%) rename test/api/{ => cpp}/issue6111.cpp (100%) rename test/api/{ => cpp}/ouroborous.cpp (100%) rename test/api/{ => cpp}/proj-issue306.cpp (100%) rename test/api/{ => cpp}/proj-issue334.cpp (100%) rename test/api/{ => cpp}/reset_assertions.cpp (100%) rename test/api/{ => cpp}/sep_log_api.cpp (100%) rename test/api/{ => cpp}/smt2_compliance.cpp (100%) rename test/api/{ => cpp}/two_solvers.cpp (100%) create mode 100644 test/api/python/CMakeLists.txt create mode 100644 test/api/python/boilerplate.py create mode 100644 test/api/python/issue4889.py create mode 100644 test/api/python/issue5074.py create mode 100644 test/api/python/issue6111.py create mode 100644 test/binary/CMakeLists.txt rename test/{api => binary}/interactive_shell.py (100%) diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 5f96d2b9b..3108582d9 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -37,6 +37,7 @@ add_custom_target(check add_subdirectory(regress) add_subdirectory(api EXCLUDE_FROM_ALL) +add_subdirectory(binary 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 index 56adf73e7..5fb0e9357 100644 --- a/test/api/CMakeLists.txt +++ b/test/api/CMakeLists.txt @@ -13,65 +13,7 @@ # The build system configuration. ## -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(CVC5_API_TEST_FLAGS -D__BUILDING_CVC5_API_TEST) - -macro(cvc5_add_api_test name) - set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/api/) - add_executable(${name} ${name}.cpp) - target_link_libraries(${name} PUBLIC main-test) - target_compile_definitions(${name} PRIVATE ${CVC5_API_TEST_FLAGS}) - set_target_properties(${name} - PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir}) - add_test(api/${name} ${test_bin_dir}/${name}) - set_tests_properties(api/${name} PROPERTIES LABELS "api") - add_dependencies(build-apitests ${name}) -endmacro() - -cvc5_add_api_test(boilerplate) -cvc5_add_api_test(ouroborous) -cvc5_add_api_test(reset_assertions) -cvc5_add_api_test(sep_log_api) -cvc5_add_api_test(smt2_compliance) -cvc5_add_api_test(two_solvers) -cvc5_add_api_test(issue5074) -cvc5_add_api_test(issue4889) -cvc5_add_api_test(issue6111) -cvc5_add_api_test(proj-issue306) -cvc5_add_api_test(proj-issue334) - -# 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() +add_subdirectory(cpp) +if (BUILD_BINDINGS_PYTHON) + add_subdirectory(python) endif() diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt new file mode 100644 index 000000000..eae57f3b9 --- /dev/null +++ b/test/api/cpp/CMakeLists.txt @@ -0,0 +1,56 @@ +############################################################################### +# Top contributors (to current version): +# Aina Niemetz, Andrew V. Jones, Gereon Kremer +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 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. +# ############################################################################# +# +# The build system configuration. +## + +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(CVC5_API_TEST_FLAGS -D__BUILDING_CVC5_API_TEST) + +macro(cvc5_add_api_test name) + set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/api/cpp) + add_executable(${name} ${name}.cpp) + target_link_libraries(${name} PUBLIC main-test) + target_compile_definitions(${name} PRIVATE ${CVC5_API_TEST_FLAGS}) + set_target_properties(${name} + PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir}) + add_test(api/cpp/${name} ${test_bin_dir}/${name}) + set_tests_properties(api/cpp/${name} PROPERTIES LABELS "api") + add_dependencies(build-apitests ${name}) +endmacro() + +cvc5_add_api_test(boilerplate) +cvc5_add_api_test(ouroborous) +cvc5_add_api_test(reset_assertions) +cvc5_add_api_test(sep_log_api) +cvc5_add_api_test(smt2_compliance) +cvc5_add_api_test(two_solvers) +cvc5_add_api_test(issue5074) +cvc5_add_api_test(issue4889) +cvc5_add_api_test(issue6111) +cvc5_add_api_test(proj-issue306) +cvc5_add_api_test(proj-issue334) diff --git a/test/api/boilerplate.cpp b/test/api/cpp/boilerplate.cpp similarity index 100% rename from test/api/boilerplate.cpp rename to test/api/cpp/boilerplate.cpp diff --git a/test/api/issue4889.cpp b/test/api/cpp/issue4889.cpp similarity index 100% rename from test/api/issue4889.cpp rename to test/api/cpp/issue4889.cpp diff --git a/test/api/issue5074.cpp b/test/api/cpp/issue5074.cpp similarity index 100% rename from test/api/issue5074.cpp rename to test/api/cpp/issue5074.cpp diff --git a/test/api/issue6111.cpp b/test/api/cpp/issue6111.cpp similarity index 100% rename from test/api/issue6111.cpp rename to test/api/cpp/issue6111.cpp diff --git a/test/api/ouroborous.cpp b/test/api/cpp/ouroborous.cpp similarity index 100% rename from test/api/ouroborous.cpp rename to test/api/cpp/ouroborous.cpp diff --git a/test/api/proj-issue306.cpp b/test/api/cpp/proj-issue306.cpp similarity index 100% rename from test/api/proj-issue306.cpp rename to test/api/cpp/proj-issue306.cpp diff --git a/test/api/proj-issue334.cpp b/test/api/cpp/proj-issue334.cpp similarity index 100% rename from test/api/proj-issue334.cpp rename to test/api/cpp/proj-issue334.cpp diff --git a/test/api/reset_assertions.cpp b/test/api/cpp/reset_assertions.cpp similarity index 100% rename from test/api/reset_assertions.cpp rename to test/api/cpp/reset_assertions.cpp diff --git a/test/api/sep_log_api.cpp b/test/api/cpp/sep_log_api.cpp similarity index 100% rename from test/api/sep_log_api.cpp rename to test/api/cpp/sep_log_api.cpp diff --git a/test/api/smt2_compliance.cpp b/test/api/cpp/smt2_compliance.cpp similarity index 100% rename from test/api/smt2_compliance.cpp rename to test/api/cpp/smt2_compliance.cpp diff --git a/test/api/two_solvers.cpp b/test/api/cpp/two_solvers.cpp similarity index 100% rename from test/api/two_solvers.cpp rename to test/api/cpp/two_solvers.cpp diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt new file mode 100644 index 000000000..c9e00213a --- /dev/null +++ b/test/api/python/CMakeLists.txt @@ -0,0 +1,35 @@ +############################################################################### +# Top contributors (to current version): +# Yoni Zohar, Aina Niemetz, Mathias Preiner +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 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. +# ############################################################################# +# +# The build system configuration. +## + +# Add Python bindings API tests. +macro(cvc5_add_python_api_test name filename) +# We create test target 'api/python/myapitest' and run it with +# 'ctest -R "api/python/myapitest"'. + set(test_name api/python/${name}) + add_test (NAME ${test_name} + COMMAND ${PYTHON_EXECUTABLE} + ${CMAKE_CURRENT_SOURCE_DIR}/${filename} + # directory for importing the python bindings + WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python) + set_tests_properties(${test_name} + PROPERTIES LABELS "api" + ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH}:${CMAKE_SOURCE_DIR}/api/python) +endmacro() + +# add specific test files +cvc5_add_python_api_test(pyapi_boilerplate boilerplate.py) +cvc5_add_python_api_test(pyapi_issue4889 issue4889.py) +cvc5_add_python_api_test(pyapi_issue5074 issue5074.py) +cvc5_add_python_api_test(pyapi_issue6111 issue6111.py) diff --git a/test/api/python/boilerplate.py b/test/api/python/boilerplate.py new file mode 100644 index 000000000..148710051 --- /dev/null +++ b/test/api/python/boilerplate.py @@ -0,0 +1,24 @@ +############################################################################## +# Top contributors (to current version): +# Yoni Zohar +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 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. +# ############################################################################ +# +# A simple start-up/tear-down test for cvc5. +# +# This simple test just makes sure that the public interface is +# minimally functional. It is useful as a template to use for other +# system tests. +## + +import pycvc5 + +slv = pycvc5.Solver() +r = slv.checkEntailed(slv.mkBoolean(True)) +r.isEntailed() diff --git a/test/api/python/issue4889.py b/test/api/python/issue4889.py new file mode 100644 index 000000000..538c9f2ca --- /dev/null +++ b/test/api/python/issue4889.py @@ -0,0 +1,31 @@ +############################################################################## +# Top contributors (to current version): +# Yoni Zohar +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 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. +# ############################################################################ +# +# Test for issue #4889 +## + +import pycvc5 +from pycvc5 import kinds + +slv = pycvc5.Solver() +sort_int = slv.getIntegerSort() +sort_array = slv.mkArraySort(sort_int, sort_int) +sort_fp128 = slv.mkFloatingPointSort(15, 113) +sort_fp32 = slv.mkFloatingPointSort(8, 24) +sort_bool = slv.getBooleanSort() +const0 = slv.mkConst(sort_fp32, "_c0") +const1 = slv.mkConst(sort_fp32, "_c2") +const2 = slv.mkConst(sort_bool, "_c4") +ite = slv.mkTerm(kinds.Ite, const2, const1, const0) +rem = slv.mkTerm(kinds.FPRem, ite, const1) +isnan = slv.mkTerm(kinds.FPIsNan, rem) +slv.checkSatAssuming(isnan) diff --git a/test/api/python/issue5074.py b/test/api/python/issue5074.py new file mode 100644 index 000000000..05fc84ad6 --- /dev/null +++ b/test/api/python/issue5074.py @@ -0,0 +1,25 @@ +############################################################################## +# Top contributors (to current version): +# Yoni Zohar +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 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. +# ############################################################################ +# +# Test for issue #5074 +## + +import pycvc5 +from pycvc5 import kinds + +slv = pycvc5.Solver() +c1 = slv.mkConst(slv.getIntegerSort()) +t6 = slv.mkTerm(kinds.StringFromCode, c1) +t12 = slv.mkTerm(kinds.StringToRegexp, t6) +t14 = slv.mkTerm(kinds.StringReplaceRe, [t6, t12, t6]) +t16 = slv.mkTerm(kinds.StringContains, [t14, t14]) +slv.checkEntailed(t16) diff --git a/test/api/python/issue6111.py b/test/api/python/issue6111.py new file mode 100644 index 000000000..6a4ec3842 --- /dev/null +++ b/test/api/python/issue6111.py @@ -0,0 +1,48 @@ +############################################################################## +# Top contributors (to current version): +# Yoni Zohar +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 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. +# ############################################################################ +# +# Test for issue #6111 +## + +import pycvc5 +from pycvc5 import kinds + +solver = pycvc5.Solver() +solver.setLogic("QF_BV") +bvsort12979 = solver.mkBitVectorSort(12979) +input2_1 = solver.mkConst(bvsort12979, "intpu2_1") +zero = solver.mkBitVector(bvsort12979.getBitVectorSize(), "0", 10) + +args1 = [] +args1.append(zero) +args1.append(input2_1) +bvult_res = solver.mkTerm(kinds.BVUlt, args1) +solver.assertFormula(bvult_res) + +bvsort4 = solver.mkBitVectorSort(4) +concat_result_42 = solver.mkConst(bvsort4, "concat_result_42") +bvsort8 = solver.mkBitVectorSort(8) +concat_result_43 = solver.mkConst(bvsort8, "concat_result_43") + +args2 = [] +args2.append(concat_result_42) +args2.append( + solver.mkTerm(solver.mkOp(kinds.BVExtract, 7, 4), [concat_result_43])) +solver.assertFormula(solver.mkTerm(kinds.Equal, args2)) + +args3 = [] +args3.append(concat_result_42) +args3.append( + solver.mkTerm(solver.mkOp(kinds.BVExtract, 3, 0), [concat_result_43])) +solver.assertFormula(solver.mkTerm(kinds.Equal, args3)) + +print(solver.checkSat()) diff --git a/test/binary/CMakeLists.txt b/test/binary/CMakeLists.txt new file mode 100644 index 000000000..39186813b --- /dev/null +++ b/test/binary/CMakeLists.txt @@ -0,0 +1,42 @@ +############################################################################### +# Top contributors (to current version): +# Aina Niemetz, Andrew V. Jones, Gereon Kremer +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2021 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. +# ############################################################################# +# +# The build system configuration. +## +include_directories(.) +include_directories(${PROJECT_SOURCE_DIR}/src) +include_directories(${PROJECT_SOURCE_DIR}/src/include) +include_directories(${CMAKE_BINARY_DIR}/src) + +# if we've built using libedit, (--editline) 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_custom_target(binarytests + COMMAND ctest --output-on-failure -L "binary" -j${CTEST_NTHREADS} $$ARGS) + add_test( + NAME interactive_shell + COMMAND + "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/test/binary/interactive_shell.py" + WORKING_DIRECTORY "${CMAKE_BINARY_DIR}" + ) + set_tests_properties(interactive_shell PROPERTIES LABELS "binary") + endif() +endif() diff --git a/test/api/interactive_shell.py b/test/binary/interactive_shell.py similarity index 100% rename from test/api/interactive_shell.py rename to test/binary/interactive_shell.py diff --git a/test/unit/api/python/CMakeLists.txt b/test/unit/api/python/CMakeLists.txt index cbf9629ce..7184ba02c 100644 --- a/test/unit/api/python/CMakeLists.txt +++ b/test/unit/api/python/CMakeLists.txt @@ -16,17 +16,17 @@ # Check if the pytest Python module is installed. check_python_module("pytest") -# Add Python bindings API tests. +# Add Python bindings API unit tests. macro(cvc5_add_python_api_unit_test name filename) -# We create test target 'python/unit/api/myapitest' and run it with -# 'ctest -R "python/unit/api/myapitest"'. +# We create test target 'unit/api/python/myapitest' and run it with +# 'ctest -R "unit/api/python/myapitest"'. set(test_name unit/api/python/${name}) add_test (NAME ${test_name} COMMAND ${PYTHON_EXECUTABLE} -m pytest ${CMAKE_CURRENT_SOURCE_DIR}/${filename} # directory for importing the python bindings WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python) - set_tests_properties(${test_name} PROPERTIES LABELS "unit") + set_tests_properties(${test_name} PROPERTIES LABELS "unit python") endmacro() # add specific test files -- 2.30.2