diff options
| -rw-r--r-- | CMakeLists.txt | 35 | ||||
| -rw-r--r-- | cmake/ConfigCompetition.cmake | 1 | ||||
| -rw-r--r-- | cmake/ConfigDebug.cmake | 1 | ||||
| -rw-r--r-- | cmake/ConfigProduction.cmake | 1 | ||||
| -rw-r--r-- | cmake/ConfigTesting.cmake | 1 |
5 files changed, 11 insertions, 28 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 53c7466c5..4120e5984 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -276,15 +276,6 @@ set(GPL_LIBS "") set(BUILD_TYPES Production Debug Testing Competition) #-----------------------------------------------------------------------------# -# CVC4 build variables - -set(CVC4_DEBUG 0) -set(CVC4_BUILD_PROFILE_PRODUCTION 0) -set(CVC4_BUILD_PROFILE_DEBUG 0) -set(CVC4_BUILD_PROFILE_TESTING 0) -set(CVC4_BUILD_PROFILE_COMPETITION 0) - -#-----------------------------------------------------------------------------# # Build types if(ENABLE_ASAN) @@ -300,6 +291,8 @@ if(NOT CMAKE_BUILD_TYPE) endif() message(STATUS "Building ${CMAKE_BUILD_TYPE} build") +# Note: Module CodeCoverage requires the name of the debug build to conform +# to cmake standards (first letter uppercase). if(CMAKE_BUILD_TYPE STREQUAL "Debug") include(ConfigDebug) elseif(CMAKE_BUILD_TYPE STREQUAL "Production") @@ -602,21 +595,8 @@ endif() #-----------------------------------------------------------------------------# # Print build configuration -if(CVC4_BUILD_PROFILE_PRODUCTION) - set(CVC4_BUILD_PROFILE_STRING "production") -elseif(CVC4_BUILD_PROFILE_DEBUG) - set(CVC4_BUILD_PROFILE_STRING "debug") -elseif(CVC4_BUILD_PROFILE_TESTING) - set(CVC4_BUILD_PROFILE_STRING "testing") -elseif(CVC4_BUILD_PROFILE_COMPETITION) - set(CVC4_BUILD_PROFILE_STRING "competition") -endif() - -# Get all definitions added via add_definitions to print it below -get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS) -string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}") - -# Print configuration of 2-valued or 3-valued option 'var' with prefix 'str' +# Helper to print the configuration of a 2-valued or 3-valued option 'var' +# with prefix 'str'. macro(print_config str var) if(${var} STREQUAL "ON") set(OPT_VAL_STR "on") @@ -628,6 +608,13 @@ macro(print_config str var) message("${str} ${OPT_VAL_STR}") endmacro() +# Convert build type to lower case. +string(TOLOWER ${CMAKE_BUILD_TYPE} CVC4_BUILD_PROFILE_STRING) + +# Get all definitions added via add_definitions. +get_directory_property(CVC4_DEFINITIONS COMPILE_DEFINITIONS) +string(REPLACE ";" " " CVC4_DEFINITIONS "${CVC4_DEFINITIONS}") + message("CVC4 ${CVC4_RELEASE_STRING}") message("") message("Build profile : ${CVC4_BUILD_PROFILE_STRING}") diff --git a/cmake/ConfigCompetition.cmake b/cmake/ConfigCompetition.cmake index 8c2fda2d4..f40cd46be 100644 --- a/cmake/ConfigCompetition.cmake +++ b/cmake/ConfigCompetition.cmake @@ -1,4 +1,3 @@ -set(CVC4_BUILD_PROFILE_COMPETITION 1) add_definitions(-DCVC4_COMPETITION_MODE) add_check_c_cxx_flag("-funroll-all-loops") add_check_c_cxx_flag("-fexpensive-optimizations") diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake index 9decc07be..9f58d3548 100644 --- a/cmake/ConfigDebug.cmake +++ b/cmake/ConfigDebug.cmake @@ -1,4 +1,3 @@ -set(CVC4_BUILD_PROFILE_DEBUG 1) add_definitions(-DCVC4_DEBUG) set(CVC4_DEBUG 1) add_check_c_cxx_flag("-fno-inline") diff --git a/cmake/ConfigProduction.cmake b/cmake/ConfigProduction.cmake index 336e582b9..1b30dc1aa 100644 --- a/cmake/ConfigProduction.cmake +++ b/cmake/ConfigProduction.cmake @@ -1,4 +1,3 @@ -set(CVC4_BUILD_PROFILE_PRODUCTION 1) # OPTLEVEL=3 # enable_optimized=yes cvc4_set_option(ENABLE_OPTIMIZED ON) diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake index 7b948084f..9627bcd52 100644 --- a/cmake/ConfigTesting.cmake +++ b/cmake/ConfigTesting.cmake @@ -1,4 +1,3 @@ -set(CVC4_BUILD_PROFILE_TESTING 1) # OPTLEVEL=2 # enable_optimized=yes cvc4_set_option(ENABLE_OPTIMIZED ON) |