Skip to content

Commit

Permalink
Reorganize issues in C++ API tests. (cvc5#11106)
Browse files Browse the repository at this point in the history
  • Loading branch information
@aniemetz
aniemetz authored Aug 6, 2024
1 parent 92eee34 commit fe5a65e
Show file tree
Hide file tree
Showing 69 changed files with 205 additions and 163 deletions.
103 changes: 23 additions & 80 deletions test/api/c/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,87 +31,30 @@ add_custom_target(capitests

set(CVC5_API_TEST_FLAGS -D__BUILDING_CVC5_API_TEST -Dcvc5_obj_EXPORTS)

macro(cvc5_add_capi_test name)
set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/api/c)
set(testname capi_${name})
add_executable(${testname} ${name}.c)
target_link_libraries(${testname} PUBLIC main-test)
target_compile_definitions(${testname} PRIVATE ${CVC5_API_TEST_FLAGS})
set_target_properties(${testname}
macro(cvc5_add_capi_test name dir)
set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/api/c/${dir})
set(cname capi_${name})
add_executable(${cname} ${name}.c)
target_link_libraries(${cname} PUBLIC main-test)
target_compile_definitions(${cname} PRIVATE ${CVC5_API_TEST_FLAGS})
set_target_properties(${cname}
PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir})
add_test(api/c/${testname} ${ENV_PATH_CMD} ${test_bin_dir}/${testname})
set_tests_properties(api/c/${testname} PROPERTIES LABELS "api capi")
if("${dir}" STREQUAL "")
set(testname api/c/${cname})
else()
set(testname api/c/${dir}/${cname})
endif()
add_test(${testname} ${ENV_PATH_CMD} ${test_bin_dir}/${cname})
set_tests_properties(${testname} PROPERTIES LABELS "api capi")
# set_tests_properties(api/cpp/${name} PROPERTIES FIXTURES_REQUIRED build_capitests_fixture)
add_dependencies(build-capitests ${testname})
add_dependencies(build-capitests ${cname})
endmacro()

cvc5_add_capi_test(boilerplate)
cvc5_add_capi_test(ouroborous)
cvc5_add_capi_test(reset_assertions)
cvc5_add_capi_test(sep_log_api)
cvc5_add_capi_test(smt2_compliance)
cvc5_add_capi_test(two_solvers)
cvc5_add_capi_test(issue11069)
#cvc5_add_capi_test(issue5074)
#cvc5_add_capi_test(issue5893)
#cvc5_add_capi_test(issue4889)
#cvc5_add_capi_test(issue6111)
#cvc5_add_capi_test(issue7000)
#cvc5_add_capi_test(proj-issue306)
#cvc5_add_capi_test(proj-issue308)
#cvc5_add_capi_test(proj-issue334)
#cvc5_add_capi_test(proj-issue337)
#cvc5_add_capi_test(proj-issue344)
#cvc5_add_capi_test(proj-issue345)
#cvc5_add_capi_test(proj-issue373)
#cvc5_add_capi_test(proj-issue377)
#cvc5_add_capi_test(proj-issue378)
#cvc5_add_capi_test(proj-issue379)
#cvc5_add_capi_test(proj-issue381)
#cvc5_add_capi_test(proj-issue382)
#cvc5_add_capi_test(proj-issue383)
#cvc5_add_capi_test(proj-issue386)
#cvc5_add_capi_test(proj-issue388)
#cvc5_add_capi_test(proj-issue395)
#cvc5_add_capi_test(proj-issue399)
#cvc5_add_capi_test(proj-issue413)
#cvc5_add_capi_test(proj-issue414)
#cvc5_add_capi_test(proj-issue416)
#cvc5_add_capi_test(proj-issue418)
#cvc5_add_capi_test(proj-issue420)
#cvc5_add_capi_test(proj-issue421)
#cvc5_add_capi_test(proj-issue422)
#cvc5_add_capi_test(proj-issue423)
#cvc5_add_capi_test(proj-issue426)
#cvc5_add_capi_test(proj-issue429)
#cvc5_add_capi_test(proj-issue431)
#cvc5_add_capi_test(proj-issue434)
#cvc5_add_capi_test(proj-issue435)
#cvc5_add_capi_test(proj-issue436)
#cvc5_add_capi_test(proj-issue440)
#cvc5_add_capi_test(proj-issue445)
#cvc5_add_capi_test(proj-issue455)
#cvc5_add_capi_test(proj-issue484)
#cvc5_add_capi_test(proj-issue538)
#cvc5_add_capi_test(proj-issue567)
#cvc5_add_capi_test(proj-issue570)
#cvc5_add_capi_test(proj-issue573)
#cvc5_add_capi_test(proj-issue574)
#cvc5_add_capi_test(proj-issue575)
#cvc5_add_capi_test(proj-issue576)
#cvc5_add_capi_test(proj-issue580)
#cvc5_add_capi_test(proj-issue581)
#cvc5_add_capi_test(proj-issue587)
#cvc5_add_capi_test(proj-issue600)
#cvc5_add_capi_test(proj-issue611)
#cvc5_add_capi_test(proj-issue612)
#cvc5_add_capi_test(proj-issue618)
#cvc5_add_capi_test(proj-issue621)
#cvc5_add_capi_test(proj-issue644)
#cvc5_add_capi_test(proj-issue646)
#cvc5_add_capi_test(proj-issue652)
#cvc5_add_capi_test(proj-issue654)
#cvc5_add_capi_test(proj-issue655)
#cvc5_add_capi_test(proj-issue656)
#cvc5_add_capi_test(proj-issue657)
#cvc5_add_capi_test(proj-issue666)
cvc5_add_capi_test(boilerplate "")
cvc5_add_capi_test(ouroborous "")
cvc5_add_capi_test(reset_assertions "")
cvc5_add_capi_test(sep_log_api "")
cvc5_add_capi_test(smt2_compliance "")
cvc5_add_capi_test(two_solvers "")

add_subdirectory(issues)
80 changes: 80 additions & 0 deletions test/api/c/issues/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
###############################################################################
# Top contributors (to current version):
# Aina Niemetz
#
# This file is part of the cvc5 project.
#
# Copyright (c) 2009-2024 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.
##

cvc5_add_capi_test(issue11069 "issues")

#cvc5_add_capi_test(issue5074)
#cvc5_add_capi_test(issue5893)
#cvc5_add_capi_test(issue4889)
#cvc5_add_capi_test(issue6111)
#cvc5_add_capi_test(issue7000)
#cvc5_add_capi_test(proj-issue306)
#cvc5_add_capi_test(proj-issue308)
#cvc5_add_capi_test(proj-issue334)
#cvc5_add_capi_test(proj-issue337)
#cvc5_add_capi_test(proj-issue344)
#cvc5_add_capi_test(proj-issue345)
#cvc5_add_capi_test(proj-issue373)
#cvc5_add_capi_test(proj-issue377)
#cvc5_add_capi_test(proj-issue378)
#cvc5_add_capi_test(proj-issue379)
#cvc5_add_capi_test(proj-issue381)
#cvc5_add_capi_test(proj-issue382)
#cvc5_add_capi_test(proj-issue383)
#cvc5_add_capi_test(proj-issue386)
#cvc5_add_capi_test(proj-issue388)
#cvc5_add_capi_test(proj-issue395)
#cvc5_add_capi_test(proj-issue399)
#cvc5_add_capi_test(proj-issue413)
#cvc5_add_capi_test(proj-issue414)
#cvc5_add_capi_test(proj-issue416)
#cvc5_add_capi_test(proj-issue418)
#cvc5_add_capi_test(proj-issue420)
#cvc5_add_capi_test(proj-issue421)
#cvc5_add_capi_test(proj-issue422)
#cvc5_add_capi_test(proj-issue423)
#cvc5_add_capi_test(proj-issue426)
#cvc5_add_capi_test(proj-issue429)
#cvc5_add_capi_test(proj-issue431)
#cvc5_add_capi_test(proj-issue434)
#cvc5_add_capi_test(proj-issue435)
#cvc5_add_capi_test(proj-issue436)
#cvc5_add_capi_test(proj-issue440)
#cvc5_add_capi_test(proj-issue445)
#cvc5_add_capi_test(proj-issue455)
#cvc5_add_capi_test(proj-issue484)
#cvc5_add_capi_test(proj-issue538)
#cvc5_add_capi_test(proj-issue567)
#cvc5_add_capi_test(proj-issue570)
#cvc5_add_capi_test(proj-issue573)
#cvc5_add_capi_test(proj-issue574)
#cvc5_add_capi_test(proj-issue575)
#cvc5_add_capi_test(proj-issue576)
#cvc5_add_capi_test(proj-issue580)
#cvc5_add_capi_test(proj-issue581)
#cvc5_add_capi_test(proj-issue587)
#cvc5_add_capi_test(proj-issue600)
#cvc5_add_capi_test(proj-issue611)
#cvc5_add_capi_test(proj-issue612)
#cvc5_add_capi_test(proj-issue618)
#cvc5_add_capi_test(proj-issue621)
#cvc5_add_capi_test(proj-issue644)
#cvc5_add_capi_test(proj-issue646)
#cvc5_add_capi_test(proj-issue652)
#cvc5_add_capi_test(proj-issue654)
#cvc5_add_capi_test(proj-issue655)
#cvc5_add_capi_test(proj-issue656)
#cvc5_add_capi_test(proj-issue657)
#cvc5_add_capi_test(proj-issue666)
0 test/api/c/issue11069.c → test/api/c/issues/issue11069.c
View file
File renamed without changes.
93 changes: 17 additions & 76 deletions test/api/cpp/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,8 @@
# 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
Expand All @@ -36,86 +34,29 @@ add_custom_target(apitests

set(CVC5_API_TEST_FLAGS -D__BUILDING_CVC5_API_TEST -Dcvc5_obj_EXPORTS)

macro(cvc5_add_api_test name)
set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/api/cpp)
macro(cvc5_add_api_test name dir)
set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/api/cpp/${dir})
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} ${ENV_PATH_CMD} ${test_bin_dir}/${name})
set_tests_properties(api/cpp/${name} PROPERTIES LABELS "api")
if("${dir}" STREQUAL "")
set(test_name api/cpp/${name})
else()
set(test_name api/cpp/${dir}/${name})
endif()
add_test(${test_name} ${ENV_PATH_CMD} ${test_bin_dir}/${name})
set_tests_properties(${test_name} PROPERTIES LABELS "api cppapi")
# set_tests_properties(api/cpp/${name} PROPERTIES FIXTURES_REQUIRED build_apitests_fixture)
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(issue11069)
cvc5_add_api_test(issue5074)
cvc5_add_api_test(issue5893)
cvc5_add_api_test(issue4889)
cvc5_add_api_test(issue6111)
cvc5_add_api_test(issue7000)
cvc5_add_api_test(proj-issue306)
cvc5_add_api_test(proj-issue308)
cvc5_add_api_test(proj-issue334)
cvc5_add_api_test(proj-issue337)
cvc5_add_api_test(proj-issue344)
cvc5_add_api_test(proj-issue345)
cvc5_add_api_test(proj-issue373)
cvc5_add_api_test(proj-issue377)
cvc5_add_api_test(proj-issue378)
cvc5_add_api_test(proj-issue379)
cvc5_add_api_test(proj-issue381)
cvc5_add_api_test(proj-issue382)
cvc5_add_api_test(proj-issue383)
cvc5_add_api_test(proj-issue386)
cvc5_add_api_test(proj-issue388)
cvc5_add_api_test(proj-issue395)
cvc5_add_api_test(proj-issue399)
cvc5_add_api_test(proj-issue413)
cvc5_add_api_test(proj-issue414)
cvc5_add_api_test(proj-issue416)
cvc5_add_api_test(proj-issue418)
cvc5_add_api_test(proj-issue420)
cvc5_add_api_test(proj-issue421)
cvc5_add_api_test(proj-issue422)
cvc5_add_api_test(proj-issue423)
cvc5_add_api_test(proj-issue426)
cvc5_add_api_test(proj-issue429)
cvc5_add_api_test(proj-issue431)
cvc5_add_api_test(proj-issue434)
cvc5_add_api_test(proj-issue435)
cvc5_add_api_test(proj-issue436)
cvc5_add_api_test(proj-issue440)
cvc5_add_api_test(proj-issue445)
cvc5_add_api_test(proj-issue455)
cvc5_add_api_test(proj-issue484)
cvc5_add_api_test(proj-issue538)
cvc5_add_api_test(proj-issue567)
cvc5_add_api_test(proj-issue570)
cvc5_add_api_test(proj-issue573)
cvc5_add_api_test(proj-issue574)
cvc5_add_api_test(proj-issue575)
cvc5_add_api_test(proj-issue576)
cvc5_add_api_test(proj-issue580)
cvc5_add_api_test(proj-issue581)
cvc5_add_api_test(proj-issue587)
cvc5_add_api_test(proj-issue600)
cvc5_add_api_test(proj-issue611)
cvc5_add_api_test(proj-issue612)
cvc5_add_api_test(proj-issue618)
cvc5_add_api_test(proj-issue621)
cvc5_add_api_test(proj-issue644)
cvc5_add_api_test(proj-issue646)
cvc5_add_api_test(proj-issue652)
cvc5_add_api_test(proj-issue654)
cvc5_add_api_test(proj-issue655)
cvc5_add_api_test(proj-issue656)
cvc5_add_api_test(proj-issue657)
cvc5_add_api_test(proj-issue666)
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 "")

add_subdirectory(issues)
79 changes: 79 additions & 0 deletions test/api/cpp/issues/CMakeLists.txt
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,79 @@
###############################################################################
# Top contributors (to current version):
# Aina Niemetz
#
# This file is part of the cvc5 project.
#
# Copyright (c) 2009-2024 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.
##

cvc5_add_api_test(issue11069 "issues")
cvc5_add_api_test(issue5074 "issues")
cvc5_add_api_test(issue5893 "issues")
cvc5_add_api_test(issue4889 "issues")
cvc5_add_api_test(issue6111 "issues")
cvc5_add_api_test(issue7000 "issues")
cvc5_add_api_test(proj-issue306 "issues")
cvc5_add_api_test(proj-issue308 "issues")
cvc5_add_api_test(proj-issue334 "issues")
cvc5_add_api_test(proj-issue337 "issues")
cvc5_add_api_test(proj-issue344 "issues")
cvc5_add_api_test(proj-issue345 "issues")
cvc5_add_api_test(proj-issue373 "issues")
cvc5_add_api_test(proj-issue377 "issues")
cvc5_add_api_test(proj-issue378 "issues")
cvc5_add_api_test(proj-issue379 "issues")
cvc5_add_api_test(proj-issue381 "issues")
cvc5_add_api_test(proj-issue382 "issues")
cvc5_add_api_test(proj-issue383 "issues")
cvc5_add_api_test(proj-issue386 "issues")
cvc5_add_api_test(proj-issue388 "issues")
cvc5_add_api_test(proj-issue395 "issues")
cvc5_add_api_test(proj-issue399 "issues")
cvc5_add_api_test(proj-issue413 "issues")
cvc5_add_api_test(proj-issue414 "issues")
cvc5_add_api_test(proj-issue416 "issues")
cvc5_add_api_test(proj-issue418 "issues")
cvc5_add_api_test(proj-issue420 "issues")
cvc5_add_api_test(proj-issue421 "issues")
cvc5_add_api_test(proj-issue422 "issues")
cvc5_add_api_test(proj-issue423 "issues")
cvc5_add_api_test(proj-issue426 "issues")
cvc5_add_api_test(proj-issue429 "issues")
cvc5_add_api_test(proj-issue431 "issues")
cvc5_add_api_test(proj-issue434 "issues")
cvc5_add_api_test(proj-issue435 "issues")
cvc5_add_api_test(proj-issue436 "issues")
cvc5_add_api_test(proj-issue440 "issues")
cvc5_add_api_test(proj-issue445 "issues")
cvc5_add_api_test(proj-issue455 "issues")
cvc5_add_api_test(proj-issue484 "issues")
cvc5_add_api_test(proj-issue538 "issues")
cvc5_add_api_test(proj-issue567 "issues")
cvc5_add_api_test(proj-issue570 "issues")
cvc5_add_api_test(proj-issue573 "issues")
cvc5_add_api_test(proj-issue574 "issues")
cvc5_add_api_test(proj-issue575 "issues")
cvc5_add_api_test(proj-issue576 "issues")
cvc5_add_api_test(proj-issue580 "issues")
cvc5_add_api_test(proj-issue581 "issues")
cvc5_add_api_test(proj-issue587 "issues")
cvc5_add_api_test(proj-issue600 "issues")
cvc5_add_api_test(proj-issue611 "issues")
cvc5_add_api_test(proj-issue612 "issues")
cvc5_add_api_test(proj-issue618 "issues")
cvc5_add_api_test(proj-issue621 "issues")
cvc5_add_api_test(proj-issue644 "issues")
cvc5_add_api_test(proj-issue646 "issues")
cvc5_add_api_test(proj-issue652 "issues")
cvc5_add_api_test(proj-issue654 "issues")
cvc5_add_api_test(proj-issue655 "issues")
cvc5_add_api_test(proj-issue656 "issues")
cvc5_add_api_test(proj-issue657 "issues")
cvc5_add_api_test(proj-issue666 "issues")
0 test/api/cpp/issue11069.cpp → test/api/cpp/issues/issue11069.cpp
View file
File renamed without changes.
0 test/api/cpp/issue4889.cpp → test/api/cpp/issues/issue4889.cpp
View file
File renamed without changes.
0 test/api/cpp/issue5074.cpp → test/api/cpp/issues/issue5074.cpp
View file
File renamed without changes.
0 test/api/cpp/issue5893.cpp → test/api/cpp/issues/issue5893.cpp
View file
File renamed without changes.
0 test/api/cpp/issue6111.cpp → test/api/cpp/issues/issue6111.cpp
View file
File renamed without changes.
0 test/api/cpp/issue7000.cpp → test/api/cpp/issues/issue7000.cpp
View file
File renamed without changes.
0 test/api/cpp/proj-issue306.cpp → test/api/cpp/issues/proj-issue306.cpp
View file
File renamed without changes.
0 test/api/cpp/proj-issue308.cpp → test/api/cpp/issues/proj-issue308.cpp
View file
File renamed without changes.
0 test/api/cpp/proj-issue334.cpp → test/api/cpp/issues/proj-issue334.cpp
View file
File renamed without changes.
0 test/api/cpp/proj-issue337.cpp → test/api/cpp/issues/proj-issue337.cpp
View file
File renamed without changes.
0 test/api/cpp/proj-issue344.cpp → test/api/cpp/issues/proj-issue344.cpp
View file
File renamed without changes.
1 change: 0 additions & 1 deletion test/api/cpp/proj-issue345.cpp → test/api/cpp/issues/proj-issue345.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,4 +33,3 @@ int main(void)
Term query = tm.mkTerm(Kind::AND, {t154, t154, t154, t154});
slv.checkSatAssuming(query.notTerm());
}

0 test/api/cpp/proj-issue373.cpp → test/api/cpp/issues/proj-issue373.cpp
View file
File renamed without changes.
0 test/api/cpp/proj-issue377.cpp → test/api/cpp/issues/proj-issue377.cpp
View file
File renamed without changes.
0 test/api/cpp/proj-issue378.cpp → test/api/cpp/issues/proj-issue378.cpp
View file
File renamed without changes.
0 test/api/cpp/proj-issue379.cpp → test/api/cpp/issues/proj-issue379.cpp
View file
File renamed without changes.
0 test/api/cpp/proj-issue381.cpp → test/api/cpp/issues/proj-issue381.cpp
View file
File renamed without changes.
0 test/api/cpp/proj-issue382.cpp → test/api/cpp/issues/proj-issue382.cpp
View file
File renamed without changes.
0 test/api/cpp/proj-issue383.cpp → test/api/cpp/issues/proj-issue383.cpp
View file
File renamed without changes.
0 test/api/cpp/proj-issue386.cpp → test/api/cpp/issues/proj-issue386.cpp
View file
File renamed without changes.
Loading

0 comments on commit fe5a65e

Please sign in to comment.