cmake: Refactor and clean up build profile printing.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 53c7466c593d8e2201edd4ad99a165b6143df743..4120e598474dd41f962b79b59700873392a3804a 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -275,15 +275,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
 
@@ -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 8c2fda2d45ea11fcedfad473cbba27d146f3ab84..f40cd46bed3fc958ed4077404e3c39e98f78af71 100644 (file)
--- 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 9decc07be3f067037b4010d27394894615e2b5d8..9f58d35480a6aca230bd8e5c174d83530113452d 100644 (file)
--- 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 336e582b91e4beb2c22d6233b4249bb3faae4ea2..1b30dc1aa97130fe4cccd09c97d7941f67018842 100644 (file)
--- 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 7b948084f3f80ad84b5ff8eddc5e3d066fe0522c..9627bcd5262ccb28550281c78962ebe8f29f6900 100644 (file)
--- 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)