cmake: Added 3-valued option handling (to enable detection of user-set options).

5 files changed, 132 insertions, 90 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index ade953fcd..e2813d549 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -43,6 +43,7 @@ set(CMAKE_C_STANDARD 99)
 set(CMAKE_CXX_STANDARD 11)
 
 #-----------------------------------------------------------------------------#
+# Macros
 
 include(CheckCCompilerFlag)
 include(CheckCXXCompilerFlag)
@@ -110,6 +111,18 @@ macro(cvc4_link_library library)
   set(CVC4_LIBRARIES ${CVC4_LIBRARIES} ${library})
 endmacro()
 
+macro(cvc4_option var description)
+  set(${var} AUTO CACHE STRING "${description}")
+  # Provide drop down menu options in cmake-gui
+  set_property(CACHE ${var} PROPERTY STRINGS AUTO ON OFF)
+endmacro()
+
+macro(cvc4_set_option var value)
+  if(${var} STREQUAL "AUTO")
+    set(${var} ${value})
+  endif()
+endmacro()
+
 #-----------------------------------------------------------------------------#
 
 set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
@@ -119,47 +132,53 @@ message(STATUS "LIB directory is '${CMAKE_BINARY_DIR}/lib'")
 message(STATUS "BIN directory is '${CMAKE_BINARY_DIR}/bin'")
 
 #-----------------------------------------------------------------------------#
+# User options
+
+# License
+option(ENABLE_GPL                "Enable GPL dependencies" OFF)
+
+# General build options
+# >> 3-valued: AUTO ON OFF, allows to detect if set by user
+#              this is only necessary for options set for build types!
+cvc4_option(ENABLE_ASSERTIONS    " Enable assertions")
+cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols")
+cvc4_option(ENABLE_DUMPING       "Enable dumpin")
+cvc4_option(ENABLE_MUZZLE        "completely silence CVC4; remove ALL non-result output from build")
+cvc4_option(ENABLE_OPTIMIZED     "Enable optimization")
+cvc4_option(ENABLE_PROOFS        "Enable proof support")
+cvc4_option(ENABLE_REPLAY        "Enable the replay feature")
+cvc4_option(ENABLE_TRACING       "Enable tracing")
+cvc4_option(ENABLE_STATISTICS    "Enable statistics")
+cvc4_option(ENABLE_VALGRIND      "Enable valgrind instrumentation")
+# >> 2-valued: ON OFF, for options where we don't need to detect if set by user
+
+# Optional dependencies
+option(USE_CADICAL               "Use CaDiCaL SAT solver")
+option(USE_CLN                   "Use CLN instead of GMP")
+option(USE_CRYPTOMINISAT         "Use CryptoMiniSat SAT solver")
+option(USE_LFSC                  "Use LFSC proof checker")
+option(USE_READLINE              "Use readline for better interactive support" OFF)
+option(USE_SYMFPU                "Use SymFPU for floating point support")
 
-set(build_types Debug Production)
-if(NOT CMAKE_BUILD_TYPE)
-    message(STATUS "No build type set, options are: ${build_types}")
-    set(CMAKE_BUILD_TYPE Production CACHE STRING "Options are: ${build_types}" FORCE)
-    # Provide drop down menu options in cmake-gui
-    set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${build_types})
-endif()
-message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
 
 #-----------------------------------------------------------------------------#
+# Internal cmake variables
 
-option(ENABLE_GPL            "Enable GPL dependencies" OFF)
-option(USE_BSD_ONLY          "Disable all GPL dependencies" OFF)
-
-option(ENABLE_DEBUG_SYMBOLS, "Enable debug symbols" OFF)
-option(ENABLE_DUMPING        "Enable dumpin" OFF)
-option(ENABLE_MUZZLE         "completely silence CVC4; remove ALL non-result output from build" OFF)
-option(ENABLE_PROOFS         "Enable proof support" OFF)
-option(ENABLE_REPLAY         "Enable the replay feature" OFF)
-option(ENABLE_TRACING        "Enable tracing" OFF)
-option(ENABLE_STATISTICS     "Enable statistics" OFF)
-option(ENABLE_VALGRIND       "Enable valgrind instrumentation" OFF)
-
-option(USE_CADICAL           "Use CaDiCaL SAT solver" OFF)
-option(USE_CLN               "Use CLN instead of GMP" OFF)
-option(USE_CRYPTOMINISAT     "Use CryptoMiniSat SAT solver" OFF)
-option(USE_LFSC              "Use LFSC proof checker" OFF)
-option(USE_READLINE          "Use readline for better interactive support" OFF)
-option(USE_SYMFPU            "Use SymFPU for floating point support" OFF)
-
-set(OPTIMIZATION_LEVEL 0)
+set(OPT_LEVEL 3)
 set(GPL_LIBS "")
-set(USE_GPL_LIBS ON)
+
+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)
-
+# Whether CVC4 is built with the (optional) GPLed library dependences.
+set(CVC4_GPL_DEPS 0)
 
 #-----------------------------------------------------------------------------#
 
@@ -171,18 +190,21 @@ cvc4_link_library(${GMP_LIBRARIES})
 include_directories(${GMP_INCLUDE_DIR})
 
 #-----------------------------------------------------------------------------#
+# Compiler flags
 
-add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}")
+add_check_c_cxx_flag("-O${OPT_LEVEL}")
 add_check_c_flag("-fexceptions")
 add_check_c_cxx_flag("-Wno-deprecated")
 add_check_c_cxx_flag("-Wsuggest-override")
 add_check_cxx_flag("-Wnon-virtual-dtor")
 
-set(build_types production debug testing competition)
+#-----------------------------------------------------------------------------#
+# Build types
+
 if(NOT CMAKE_BUILD_TYPE)
-    set(CMAKE_BUILD_TYPE production CACHE STRING "Options are: ${build_types}" FORCE)
-    # Provide drop down menu options in cmake-gui
-    set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${build_types})
+  set(CMAKE_BUILD_TYPE production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE)
+  # Provide drop down menu options in cmake-gui
+  set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${BUILD_TYPES})
 endif()
 message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
 
@@ -202,16 +224,14 @@ endif()
 
 #-----------------------------------------------------------------------------#
 
-if(USE_BSD_ONLY)
-  set(USE_GPL_LIBS OFF)
-endif()
-
 if(ENABLE_ASSERTIONS)
   add_definitions(-DCVC4_ASSERTIONS)
 endif()
 
 if(ENABLE_DUMPING)
   add_definitions(-DCVC4_DUMPING)
+else()
+  add_definitions(-DNDEBUG)
 endif()
 
 if(ENABLE_DEBUG_SYMBOLS)
@@ -313,10 +333,13 @@ else()
   set(CVC4_USE_SYMFPU 0)
 endif()
 
-if(NOT USE_GPL_LIBS AND GPL_LIBS)
-  message(FATAL_ERROR
-    "Bad configuration detected: BSD-licensed code only, but also requested "
-    "GPLed libraries: ${GPL_LIBS}")
+if(GPL_LIBS)
+  if(NOT ENABLE_GPL)
+    message(FATAL_ERROR
+      "Bad configuration detected: BSD-licensed code only, but also requested "
+      "GPLed libraries: ${GPL_LIBS}")
+  endif()
+  set(CVC4_GPL_DEPS 1)
 endif()
 
 #-----------------------------------------------------------------------------#
@@ -351,8 +374,6 @@ set(BOOST_HAS_THREAD_ATTR 0)
 set(CVC4_CLN_IMP ${CVC4_USE_CLN_IMP})
 # Defined if using the GMP multi-precision arithmetic library.
 set(CVC4_GMP_IMP ${CVC4_USE_GMP_IMP})
-# Whether CVC4 is built with the (optional) GPLed library dependences.
-set(CVC4_GPL_DEPS 0)
 # Defined if the requested minimum BOOST version is satisfied
 set(HAVE_BOOST 1)
 # Define to 1 if you have <boost/system/error_code.hpp>
@@ -443,6 +464,7 @@ endif()
 message("CVC4 ${CVC4_RELEASE_STRING}")
 message("")
 message("Build profile     : ${CVC4_BUILD_PROFILE_STRING}")
+message("Optimized         : ${ENABLE_OPTIMIZED}")
 message("Optimization level: ${OPTIMIZATION_LEVEL}")
 message("Debug symbols     : ${ENABLE_DEBUG_SYMBOLS}")
 message("Proofs            : ${ENABLE_PROOFS}")
@@ -490,38 +512,35 @@ message("CFLAGS            : ${CMAKE_C_FLAGS}")
 message("")
 
 if(GPL_LIBS)
-  message("CVC4 license      : GPLv3 (due to optional libraries; see below)")
-  message("")
   message(
+  "CVC4 license      : GPLv3 (due to optional libraries; see below)"
+  "\n"
+  "\n"
   "Please note that CVC4 will be built against the following GPLed libraries:"
-  )
-  message(${GPL_LIBS})
-  message(
+  "\n"
+  "${GPL_LIBS}"
+  "\n"
   "As these libraries are covered under the GPLv3, so is this build of CVC4."
-  )
-  message(
+  "\n"
   "CVC4 is also available to you under the terms of the (modified) BSD license."
-  )
-  message(
-  "If you prefer to license CVC4 under those terms, please configure CVC4 to\n"
-  "disable all optional GPLed library dependences (-DUSE_BSD_ONLY=ON)."
+  "\n"
+  "If you prefer to license CVC4 under those terms, please configure CVC4 to"
+  "\n"
+  "disable all optional GPLed library dependences (-DENABLE_BSD_ONLY=ON)."
   )
 else()
-  message("CVC4 license      : modified BSD")
-  message("")
-  message(
-  "Please note that this configuration is NOT built against any GPL'ed"
-  )
-  message(
-  "libraries, so it is covered by the (modified) BSD license.  This is,"
-  )
-  message(
-  "however, not the best-performing configuration of CVC4.  To build against"
-  )
   message(
-  "GPL'ed libraries which improve CVC4's performance, re-configure with "
+  "CVC4 license      : modified BSD"
+  "\n"
+  "\n"
+  "Note that this configuration is NOT built against any GPL'ed libraries, so"
+  "\n"
+  "it is covered by the (modified) BSD license.  This is, however, not the best"
+  "\n"
+  "performing configuration of CVC4.  To build against GPL'ed libraries which"
+  "\n"
+  "improve CVC4's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
   )
-  message("'-DENABLE_BEST -DENABLE_GPL'.")
 endif()
 
 message("")
diff --git a/cmake/ConfigCompetition.cmake b/cmake/ConfigCompetition.cmake
index af4df5257..3abed1da7 100644
--- a/cmake/ConfigCompetition.cmake
+++ b/cmake/ConfigCompetition.cmake
@@ -5,15 +5,25 @@ add_check_c_cxx_flag("-fexpensive-optimizations")
 add_check_c_cxx_flag("-fno-enforce-eh-specs")
 # OPTLEVEL=9
 # enable_optimized=yes
-set(OPTIMIZATION_LEVEL, 9)
+cvc4_set_option(ENABLE_OPTIMIZED ON)
+set(OPTIMIZATION_LEVEL 9)
 # enable_debug_symbols=no
+cvc4_set_option(ENABLE_DEBUG_SYMBOLS OFF)
 # enable_statistics=no
+cvc4_set_option(ENABLE_STATISTICS OFF)
 # enable_replay=no
+cvc4_set_option(ENABLE_REPLAY OFF)
 # enable_assertions=no
+cvc4_set_option(ENABLE_ASSERTIONS OFF)
 # enable_proof=no
+cvc4_set_option(ENABLE_PROOFS, OFF)
 # enable_tracing=no
+cvc4_set_option(ENABLE_TRACING OFF)
 # enable_dumping=no
+cvc4_set_option(ENABLE_DUMPING OFF)
 # enable_muzzle=yes
-set(ENABLE_MUZZLE ON)
+cvc4_set_option(ENABLE_MUZZLE ON)
 # enable_valgrind=no
+cvc4_set_option(ENABLE_VALGRIND OFF)
 # enable_shared=no
+set(BUILD_SHARED_LIBS OFF)
diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake
index c2ab7f935..8d6b6cb99 100644
--- a/cmake/ConfigDebug.cmake
+++ b/cmake/ConfigDebug.cmake
@@ -3,20 +3,23 @@ add_definitions(-DCVC4_DEBUG)
 set(CVC4_DEBUG 1)
 add_check_c_cxx_flag("-fno-inline")
 # enable_optimized=no
+cvc4_set_option(ENABLE_OPTIMIZED OFF)
+set(OPTIMIZATION_LEVEL 0)
 add_c_cxx_flag("-Og")
 # enable_debug_symbols=yes
-set(ENABLE_DEBUG_SYMBOLS ON)
+cvc4_set_option(ENABLE_DEBUG_SYMBOLS ON)
 # enable_statistics=yes
-set(ENABLE_STATISTICS ON)
+cvc4_set_option(ENABLE_STATISTICS ON)
 # enable_replay=yes
-set(ENABLE_REPLAY ON)
+cvc4_set_option(ENABLE_REPLAY ON)
 # enable_assertions=yes
-set(ENABLE_ASSERTIONS ON)
+cvc4_set_option(ENABLE_ASSERTIONS ON)
 # enable_proof=yes
-set(ENABLE_PROOFS, ON)
+cvc4_set_option(ENABLE_PROOFS ON)
 # enable_tracing=yes
-set(ENABLE_TRACING ON)
+cvc4_set_option(ENABLE_TRACING ON)
 # enable_dumping=yes
-set(ENABLE_DUMPING ON)
+cvc4_set_option(ENABLE_DUMPING ON)
 # enable_muzzle=no
+cvc4_set_option(ENABLE_MUZZLE OFF)
 # enable_valgrind=optional
diff --git a/cmake/ConfigProduction.cmake b/cmake/ConfigProduction.cmake
index 27bb7270d..9e85188e6 100644
--- a/cmake/ConfigProduction.cmake
+++ b/cmake/ConfigProduction.cmake
@@ -1,16 +1,23 @@
 set(CVC4_BUILD_PROFILE_PRODUCTION 1)
 # OPTLEVEL=3
 # enable_optimized=yes
-set(OPTIMIZATION_LEVEL, 3)
+cvc4_set_option(ENABLE_OPTIMIZED ON)
+set(OPTIMIZATION_LEVEL 3)
 # enable_debug_symbols=no
+cvc4_set_option(ENABLE_DEBUG_SYMBOLS OFF)
 # enable_statistics=yes
-set(ENABLE_STATISTICS ON)
+cvc4_set_option(ENABLE_STATISTICS ON)
 # enable_replay=no
+cvc4_set_option(ENABLE_REPLAY OFF)
 # enable_assertions=no
+cvc4_set_option(ENABLE_ASSERTIONS OFF)
 # enable_proof=yes
-set(ENABLE_PROOFS, ON)
+cvc4_set_option(ENABLE_PROOFS ON)
 # enable_tracing=no
+cvc4_set_option(ENABLE_TRACING OFF)
 # enable_dumping=yes
-set(ENABLE_DUMPING ON)
+cvc4_set_option(ENABLE_DUMPING ON)
 # enable_muzzle=no
+cvc4_set_option(ENABLE_MUZZLE OFF)
 # enable_valgrind=no
+cvc4_set_option(ENABLE_VALGRIND OFF)
diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake
index 4d6094ce8..ad0049988 100644
--- a/cmake/ConfigTesting.cmake
+++ b/cmake/ConfigTesting.cmake
@@ -1,20 +1,23 @@
 set(CVC4_BUILD_PROFILE_TESTING 1)
 # OPTLEVEL=2
 # enable_optimized=yes
-set(OPTIMIZATION_LEVEL, 2)
+cvc4_set_option(ENABLE_OPTIMIZED ON)
+set(OPTIMIZATION_LEVEL 2)
 # enable_debug_symbols=yes
-add_check_c_cxx_flag("-ggdb3")
+cvc4_set_option(ENABLE_DEBUG_SYMBOLS ON)
 # enable_statistics=yes
-set(ENABLE_STATISTICS ON)
+cvc4_set_option(ENABLE_STATISTICS ON)
 # enable_replay=yes
-set(ENABLE_REPLAY ON)
+cvc4_set_option(ENABLE_REPLAY ON)
 # enable_assertions=yes
-set(ENABLE_ASSERTIONS ON)
+cvc4_set_option(ENABLE_ASSERTIONS ON)
 # enable_proof=yes
-set(ENABLE_PROOFS, ON)
+cvc4_set_option(ENABLE_PROOFS, ON)
 # enable_tracing=yes
-set(ENABLE_TRACING ON)
+cvc4_set_option(ENABLE_TRACING ON)
 # enable_dumping=yes
-set(ENABLE_DUMPING ON)
+cvc4_set_option(ENABLE_DUMPING ON)
 # enable_muzzle=no
+cvc4_set_option(ENABLE_MUZZLE OFF)
 # enable_valgrind=no
+cvc4_set_option(ENABLE_VALGRIND OFF)