diff options
| -rw-r--r-- | CMakeLists.txt | 161 | ||||
| -rw-r--r-- | cmake/ConfigCompetition.cmake | 18 | ||||
| -rw-r--r-- | cmake/ConfigDebug.cmake | 22 | ||||
| -rw-r--r-- | cmake/ConfigProduction.cmake | 16 | ||||
| -rw-r--r-- | cmake/ConfigTesting.cmake | 20 | ||||
| -rw-r--r-- | src/base/CMakeLists.txt | 116 |
6 files changed, 287 insertions, 66 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 26aa10f89..7a3c13085 100644 --- 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 index 000000000..dade05ba4 --- /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 index 000000000..c2ab7f935 --- /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 index 000000000..27bb7270d --- /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 index 000000000..4d6094ce8 --- /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 810ffa253..ea44c4fc3 100644 --- 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 ) |