cmake: Add build configurations.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 26aa10f89d420dcee45dcd2ce102cc86e47eaada..7a3c13085475000b93d38c8e927e09ab6b28f9a1 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -131,12 +131,28 @@ message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
 
 #-----------------------------------------------------------------------------#
 
-option(ENABLE_PROOFS     "Enable proof support" 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_SYMFPU        "Use SymFPU for floating point support" OFF)
+option(ENABLE_DEBUG_SYMBOLS, "Enable debug symbols" OFF)
+option(ENABLE_DUMPING        "Enable dumpin" 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_SYMFPU            "Use SymFPU for floating point support" OFF)
+
+set(OPTIMIZATION_LEVEL 0)
+
+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)
+
 
 #-----------------------------------------------------------------------------#
 
@@ -150,8 +166,72 @@ find_package(GMP REQUIRED)
 cvc4_link_library(${GMP_LIBRARIES})
 include_directories(${GMP_INCLUDE_DIR})
 
+#-----------------------------------------------------------------------------#
+
+add_check_c_cxx_flag("-O${OPTIMIZATION_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)
+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})
+endif()
+message(STATUS "Building ${CMAKE_BUILD_TYPE} build")
+
+if(CMAKE_BUILD_TYPE STREQUAL "debug")
+  include(ConfigDebug)
+elseif(CMAKE_BUILD_TYPE STREQUAL "production")
+  include(ConfigProduction)
+elseif(CMAKE_BUILD_TYPE STREQUAL "testing")
+  include(ConfigTesting)
+elseif(CMAKE_BUILD_TYPE STREQUAL "competition")
+  include(ConfigCompetition)
+  # enable_static=yes
+  #TODO
+  # enable_static_binary=yes
+  #TODO
+endif()
+
+#-----------------------------------------------------------------------------#
+
+if(ENABLE_ASSERTIONS)
+  add_definitions(-DCVC4_ASSERTIONS)
+endif()
+
+if(ENABLE_DUMPING)
+  add_definitions(-DCVC4_DUMPING)
+endif()
+
+if(ENABLE_DEBUG_SYMBOLS)
+  add_check_c_cxx_flag("-ggdb3")
+endif()
+
 if(ENABLE_PROOFS)
+  #TODO RUN_REGRESSION_ARGS="${RUN_REGRESSION_ARGS:+$RUN_REGRESSION_ARGS }--enable-proof"
   add_definitions(-DCVC4_PROOF)
+  set(CVC4_PROOF 1)
+endif()
+
+if(ENABLE_REPLAY)
+  add_definitions(-DCVC4_REPLAY)
+endif()
+
+if(ENABLE_TRACING)
+  add_definitions(-DCVC4_TRACING)
+  set(CVC4_TRACING 1)
+endif()
+
+if(ENABLE_STATISTICS)
+  add_definitions(-DCVC4_STATISTICS_ON)
+endif()
+
+if(ENABLE_VALGRIND)
+  #TODO check if valgrind available
+  add_definitions(-DCVC4_VALGRIND)
 endif()
 
 if(USE_CADICAL)
@@ -205,11 +285,6 @@ endif()
 
 #-----------------------------------------------------------------------------#
 
-add_check_c_flag("-fexceptions")
-add_check_c_cxx_flag("-Wno-deprecated")
-
-#-----------------------------------------------------------------------------#
-
 set(VERSION "1.6.0-prerelease")
 string(TIMESTAMP MAN_DATE "%Y-%m-%d")
 
@@ -319,3 +394,67 @@ if(ENABLE_PROOFS)
   add_subdirectory(proofs/signatures)
   cvc4_link_library(signatures)
 endif()
+
+#-----------------------------------------------------------------------------#
+
+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()
+
+message("CVC4 ${CVC4_RELEASE_STRING}")
+message("")
+message("Build profile     : ${CVC4_BUILD_PROFILE_STRING}")
+message("Optimization level: ${OPTIMIZATION_LEVEL}")
+message("Debug symbols     : ${ENABLE_DEBUG_SYMBOLS}")
+message("Proofs            : ${ENABLE_PROOFS}")
+message("Statistics        : ${ENABLE_STATISTICS}")
+message("Replay            : ${ENABLE_REPLAY}")
+message("Assertions        : ${ENABLE_ASSERTIONS}")
+message("Tracing           : ${ENABLE_TRACING}")
+message("Dumping           : ${ENABLE_DUMPING}")
+#message("Muzzle            : ${ENABLE_MUZZLE}")
+#message("")
+#message("Unit tests   : ${support_unit_tests}")
+#message("gcov support : ${enable_coverage}")
+#message("gprof support: ${enable_profiling}")
+#message("")
+#message("Static libs  : ${enable_static}")
+#message("Shared libs  : ${enable_shared}")
+#message("Static binary: ${enable_static_binary}")
+#message("Compat lib   : ${CVC4_BUILD_LIBCOMPAT}")
+#message("Bindings     : ${bindings_to_be_built}")
+#message("")
+#message("Multithreaded: ${support_multithreaded}")
+#message("Portfolio    : ${with_portfolio}")
+message("")
+#message("ABC          : ${{with_abc}")
+message("CaDiCaL           : ${USE_CADICAL}")
+message("Cryptominisat     : ${USE_CRYPTOMINISAT}")
+#message("GLPK              : ${USE_GLPK}")
+message("LFSC              : ${USE_LFSC}")
+#message("MP library   : ${mplibrary}")
+#message("Readline     : ${with_readline}")
+message("SymFPU            : ${USE_SYMFPU}")
+message("")
+#message("CPPFLAGS     : ${CPPFLAGS}")
+message("CXXFLAGS     : ${CMAKE_CXX_FLAGS}")
+message("CFLAGS       : ${CMAKE_C_FLAGS}")
+#message("LIBS         : ${LIBS}")
+#message("LDFLAGS      : ${LDFLAGS}")
+#message("")
+#message("libcvc4 version        : ${{CVC4_LIBRARY_VERSION}")
+#message("libcvc4parser version  : ${CVC4_PARSER_LIBRARY_VERSION}")
+#message("libcvc4compat version  : ${CVC4_COMPAT_LIBRARY_VERSION_or_nobuild}")
+#message("libcvc4bindings version: ${CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild}")
+#message("")
+#message("Install into : ${prefix}")
+#message("")
+#message("CVC4 license : ${license}")
+#message("")
+#message("${licensewarn}Now just type make, followed by make check or make install, as you like.")

diff --git a/cmake/ConfigCompetition.cmake b/cmake/ConfigCompetition.cmake
new file mode 100644 (file)
index 0000000..dade05b
--- /dev/null
+++ b/cmake/ConfigCompetition.cmake
@@ -0,0 +1,18 @@
+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")
+add_check_c_cxx_flag("-fno-enforce-eh-specs")
+# OPTLEVEL=9
+# enable_optimized=yes
+set(OPTIMIZATION_LEVEL, 9)
+# enable_debug_symbols=no
+# enable_statistics=no
+# enable_replay=no
+# enable_assertions=no
+# enable_proof=no
+# enable_tracing=no
+# enable_dumping=no
+# enable_muzzle=yes
+# enable_valgrind=no
+# enable_shared=no

diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake
new file mode 100644 (file)
index 0000000..c2ab7f9
--- /dev/null
+++ b/cmake/ConfigDebug.cmake
@@ -0,0 +1,22 @@
+set(CVC4_BUILD_PROFILE_DEBUG 1)
+add_definitions(-DCVC4_DEBUG)
+set(CVC4_DEBUG 1)
+add_check_c_cxx_flag("-fno-inline")
+# enable_optimized=no
+add_c_cxx_flag("-Og")
+# enable_debug_symbols=yes
+set(ENABLE_DEBUG_SYMBOLS ON)
+# enable_statistics=yes
+set(ENABLE_STATISTICS ON)
+# enable_replay=yes
+set(ENABLE_REPLAY ON)
+# enable_assertions=yes
+set(ENABLE_ASSERTIONS ON)
+# enable_proof=yes
+set(ENABLE_PROOFS, ON)
+# enable_tracing=yes
+set(ENABLE_TRACING ON)
+# enable_dumping=yes
+set(ENABLE_DUMPING ON)
+# enable_muzzle=no
+# enable_valgrind=optional

diff --git a/cmake/ConfigProduction.cmake b/cmake/ConfigProduction.cmake
new file mode 100644 (file)
index 0000000..27bb727
--- /dev/null
+++ b/cmake/ConfigProduction.cmake
@@ -0,0 +1,16 @@
+set(CVC4_BUILD_PROFILE_PRODUCTION 1)
+# OPTLEVEL=3
+# enable_optimized=yes
+set(OPTIMIZATION_LEVEL, 3)
+# enable_debug_symbols=no
+# enable_statistics=yes
+set(ENABLE_STATISTICS ON)
+# enable_replay=no
+# enable_assertions=no
+# enable_proof=yes
+set(ENABLE_PROOFS, ON)
+# enable_tracing=no
+# enable_dumping=yes
+set(ENABLE_DUMPING ON)
+# enable_muzzle=no
+# enable_valgrind=no

diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake
new file mode 100644 (file)
index 0000000..4d6094c
--- /dev/null
+++ b/cmake/ConfigTesting.cmake
@@ -0,0 +1,20 @@
+set(CVC4_BUILD_PROFILE_TESTING 1)
+# OPTLEVEL=2
+# enable_optimized=yes
+set(OPTIMIZATION_LEVEL, 2)
+# enable_debug_symbols=yes
+add_check_c_cxx_flag("-ggdb3")
+# enable_statistics=yes
+set(ENABLE_STATISTICS ON)
+# enable_replay=yes
+set(ENABLE_REPLAY ON)
+# enable_assertions=yes
+set(ENABLE_ASSERTIONS ON)
+# enable_proof=yes
+set(ENABLE_PROOFS, ON)
+# enable_tracing=yes
+set(ENABLE_TRACING ON)
+# enable_dumping=yes
+set(ENABLE_DUMPING ON)
+# enable_muzzle=no
+# enable_valgrind=no

diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt
index 810ffa2538af237556042b14299c24be3cf98710..ea44c4fc33b9e6404482994375e1761074cbcb65 100644 (file)
--- a/src/base/CMakeLists.txt
+++ b/src/base/CMakeLists.txt
@@ -17,6 +17,7 @@ set(base_src_files
 
 add_library(base SHARED ${base_src_files})
 set_target_properties(base PROPERTIES COMPILE_DEFINITIONS __BUILDING_CVC4LIB)
+add_dependencies(base tags_headers)
 
 #
 # Generate code for debug/trace tags
@@ -26,70 +27,75 @@ set(mktagheaders_script ${CMAKE_CURRENT_LIST_DIR}/mktagheaders)
 file(GLOB_RECURSE source_files ${PROJECT_SOURCE_DIR}/src/*.cpp ${PROJECT_SOURCE_DIR}/src/*.cc ${PROJECT_SOURCE_DIR}/src/*.h ${PROJECT_SOURCE_DIR}/src/*.g)
 string(REPLACE ";" " " source_files_list "${source_files}")
 
-add_custom_target(
-    debug_tags_tmp
-    COMMAND
-      ${mktags_script}
-      "Debug"
-      ${source_files_list}
-      > ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp
-    DEPENDS mktags
+add_custom_command(
+  OUTPUT Debug_tags.tmp
+  COMMAND
+    ${mktags_script}
+    "Debug"
+    ${source_files_list}
+    > ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp
+  DEPENDS mktags
 )
 
-add_custom_target(
-    trace_tags_tmp
-    COMMAND
-      ${mktags_script}
-      "Trace"
-      ${source_files_list}
-      > ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp
-    DEPENDS mktags
+add_custom_command(
+  OUTPUT Trace_tags.tmp
+  COMMAND
+    ${mktags_script}
+    "Trace"
+    ${source_files_list}
+    > ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp
+  DEPENDS mktags
 )
 
-add_custom_target(
-    debug_tags
-    COMMAND
-      diff -q
-      ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp 
-      ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags
-      &> /dev/null
-      || mv
-      ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp 
-      ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags
-      || true
-      DEPENDS debug_tags_tmp
+add_custom_command(
+  OUTPUT Debug_tags
+  COMMAND
+    diff -q
+    ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp
+    ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags
+    &> /dev/null
+    || mv
+    ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.tmp
+    ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags
+    || true
+  DEPENDS Debug_tags.tmp
 )
 
-add_custom_target(
-    trace_tags
-    COMMAND
-      diff -q
-      ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp 
-      ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags
-      &> /dev/null
-      || mv
-      ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp 
-      ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags
-      || true
-      DEPENDS trace_tags_tmp
+add_custom_command(
+  OUTPUT Trace_tags
+  COMMAND
+    diff -q
+    ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp
+    ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags
+    &> /dev/null
+    || mv
+    ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.tmp
+    ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags
+    || true
+  DEPENDS Trace_tags.tmp
 )
 
-add_custom_target(
-    debug_tags.h
-    COMMAND
-      ${mktagheaders_script}
-      "Debug_tags"
-      ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags
-      > ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.h
-      DEPENDS debug_tags
+add_custom_command(
+  OUTPUT Debug_tags.h
+  COMMAND
+    ${mktagheaders_script}
+    "Debug_tags"
+    ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags
+    > ${CMAKE_CURRENT_BINARY_DIR}/Debug_tags.h
+  DEPENDS Debug_tags
+)
+
+add_custom_command(
+  OUTPUT Trace_tags.h
+  COMMAND
+    ${mktagheaders_script}
+    "Trace_tags"
+    ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags
+    > ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.h
+  DEPENDS Trace_tags
 )
 
 add_custom_target(
-    trace_tags.h
-    COMMAND
-      ${mktagheaders_script}
-      "Trace_tags"
-      ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags
-      > ${CMAKE_CURRENT_BINARY_DIR}/Trace_tags.h
-      DEPENDS trace_tags
+  tags_headers
+  DEPENDS Debug_tags.h Trace_tags.h
 )