From 7be22fb6cac25031efc242708719555624f54791 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 11 Sep 2018 10:30:07 -0700 Subject: [PATCH] cmake: Various CMakeLists.txt fixes/cleanup. --- CMakeLists.txt | 73 +++++++++++++++++---------------------- cmake/ConfigureCVC4.cmake | 27 +++++++++------ contrib/CMakeLists.txt | 0 doc/CMakeLists.txt | 4 +++ src/prop/CMakeLists.txt | 2 -- 5 files changed, 53 insertions(+), 53 deletions(-) delete mode 100644 contrib/CMakeLists.txt delete mode 100644 src/prop/CMakeLists.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index 24b6d0320..b4e567769 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,5 +1,9 @@ cmake_minimum_required(VERSION 3.1) +if(POLICY CMP0075) + cmake_policy(SET CMP0075 NEW) +endif() + #-----------------------------------------------------------------------------# project(cvc4) @@ -15,7 +19,8 @@ set(CVC4_EXTRAVERSION "-prerelease") # Full release string for CVC4. if(CVC4_RELEASE) - set(CVC4_RELEASE_STRING "${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}${CVC4_EXTRAVERSION}") + set(CVC4_RELEASE_STRING + "${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE}${CVC4_EXTRAVERSION}") else() set(CVC4_RELEASE_STRING "${CVC4_MAJOR}.${CVC4_MINOR}${CVC4_EXTRAVERSION}") endif() @@ -213,7 +218,7 @@ cvc4_option(ENABLE_ASAN "Enable ASAN build") cvc4_option(ENABLE_ASSERTIONS "Enable assertions") cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols") cvc4_option(ENABLE_DUMPING "Enable dumping") -cvc4_option(ENABLE_MUZZLE "Supress ALL non-result output") +cvc4_option(ENABLE_MUZZLE "Suppress ALL non-result output") cvc4_option(ENABLE_OPTIMIZED "Enable optimization") cvc4_option(ENABLE_PORTFOLIO "Enable portfolio support") cvc4_option(ENABLE_PROOFS "Enable proof support") @@ -264,13 +269,10 @@ set(SYMFPU_DIR "" CACHE STRING "Set SymFPU install directory") option(BUILD_BINDINGS_JAVA "Build Java bindings") option(BUILD_BINDINGS_PYTHON "Build Python bindings") -# All bindings: c,java,csharp,perl,php,python,ruby,tcl,ocaml - - #-----------------------------------------------------------------------------# # Internal cmake variables -set(OPT_LEVEL 3) +set(OPTIMIZATION_LEVEL 3) set(GPL_LIBS "") set(BUILD_TYPES Production Debug Testing Competition) @@ -284,15 +286,6 @@ set(CVC4_BUILD_PROFILE_DEBUG 0) set(CVC4_BUILD_PROFILE_TESTING 0) set(CVC4_BUILD_PROFILE_COMPETITION 0) -#-----------------------------------------------------------------------------# -# Compiler flags - -add_check_c_cxx_flag("-O${OPT_LEVEL}") -add_check_c_flag("-fexceptions") -add_check_c_cxx_flag("-Wno-deprecated") -add_check_cxx_flag("-Wsuggest-override") -add_check_cxx_flag("-Wnon-virtual-dtor") - #-----------------------------------------------------------------------------# # Build types @@ -302,7 +295,8 @@ endif() # Set the default build type to Production if(NOT CMAKE_BUILD_TYPE) - set(CMAKE_BUILD_TYPE Production CACHE STRING "Options are: ${BUILD_TYPES}" FORCE) + 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() @@ -316,12 +310,17 @@ 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() +#-----------------------------------------------------------------------------# +# Compiler flags + +add_check_c_cxx_flag("-O${OPTIMIZATION_LEVEL}") +add_check_c_flag("-fexceptions") +add_check_c_cxx_flag("-Wno-deprecated") +add_check_cxx_flag("-Wsuggest-override") +add_check_cxx_flag("-Wnon-virtual-dtor") + #-----------------------------------------------------------------------------# # Option defaults (three-valued options (cvc4_option(...))) @@ -352,8 +351,6 @@ if(NOT ENABLE_SHARED) set(BUILD_SHARED_LIBS OFF) endif() -find_package(PythonInterp REQUIRED) - #-----------------------------------------------------------------------------# # Enable the ctest testing framework @@ -366,10 +363,6 @@ find_package(GMP REQUIRED) libcvc4_link_libraries(${GMP_LIBRARIES}) libcvc4_include_directories(${GMP_INCLUDE_DIR}) -if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON) - set(BUILD_BINDINGS TRUE) -endif() - if(ENABLE_ASAN) set(CMAKE_REQUIRED_LIBRARIES -fsanitize=address) add_required_c_cxx_flag("-fsanitize=address") @@ -380,6 +373,8 @@ endif() if(ENABLE_ASSERTIONS) add_definitions(-DCVC4_ASSERTIONS) +else() + add_definitions(-DNDEBUG) endif() if(ENABLE_COVERAGE) @@ -398,8 +393,6 @@ endif() if(ENABLE_DUMPING) add_definitions(-DCVC4_DUMPING) -else() - add_definitions(-DNDEBUG) endif() if(ENABLE_DEBUG_SYMBOLS) @@ -414,7 +407,10 @@ if(ENABLE_PORTFOLIO) find_package(Boost 1.50.0 REQUIRED COMPONENTS thread) # Disable CLN for portfolio builds since it is not thread safe (uses an # unlocked hash table internally). - set(USE_CLN OFF) + if(USE_CLN) + message(WARNING "Disabling CLN support since portfolio is enabled.") + set(USE_CLN OFF) + endif() set(THREADS_PREFER_PTHREAD_FLAG ON) find_package(Threads REQUIRED) if(THREADS_HAVE_PTHREAD_ARG) @@ -556,11 +552,6 @@ endif() #-----------------------------------------------------------------------------# -set(VERSION "1.6.0-prerelease") -string(TIMESTAMP MAN_DATE "%Y-%m-%d") - -#-----------------------------------------------------------------------------# - include(GetGitRevisionDescription) get_git_head_revision(GIT_REFSPEC GIT_SHA1) git_local_changes(GIT_IS_DIRTY) @@ -577,18 +568,14 @@ execute_process( ) #-----------------------------------------------------------------------------# +# Generate CVC4's cvc4autoconfig.h header include(ConfigureCVC4) - -# Defined if using the CLN multi-precision arithmetic library. -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}) - configure_file(cvc4autoconfig.new.h.in cvc4autoconfig.h) include_directories(${CMAKE_CURRENT_BINARY_DIR}) #-----------------------------------------------------------------------------# +# Add subdirectories # signatures needs to come before src since it adds source files to libcvc4. if(ENABLE_PROOFS) @@ -597,14 +584,18 @@ endif() add_subdirectory(doc) add_subdirectory(src) -if(BUILD_BINDINGS) + +if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON) add_subdirectory(src/bindings) endif() + if(BUILD_BINDINGS_JAVA) add_subdirectory(test/java) endif() + add_subdirectory(test/regress) add_subdirectory(test/system) + if(ENABLE_UNIT_TESTING) add_subdirectory(test/unit) endif() diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCVC4.cmake index e3152f5ca..18061c778 100644 --- a/cmake/ConfigureCVC4.cmake +++ b/cmake/ConfigureCVC4.cmake @@ -11,12 +11,13 @@ include(CheckSymbolExists) # error). So we have to keep both happy. Probably the same underlying # issue as the hash specialization below, but let's check separately # for flexibility. - check_cxx_source_compiles( - "#include - void foo(long) {} - void foo(int64_t) {} - int main() { return 0; }" + " + #include + void foo(long) {} + void foo(int64_t) {} + int main() { return 0; } + " CVC4_NEED_INT64_T_OVERLOADS ) if(NOT CVC4_NEED_INT64_T_OVERLOADS) @@ -26,12 +27,13 @@ endif() # Check to see if this version/architecture of GNU C++ explicitly # instantiates std::hash or not. Some do, some don't. # See src/util/hash.h. - check_cxx_source_compiles( - "#include - #include - namespace std { template<> struct hash {}; } - int main() { return 0; }" + " + #include + #include + namespace std { template<> struct hash {}; } + int main() { return 0; } + " CVC4_NEED_HASH_UINT64_T_OVERLOAD ) if(CVC4_NEED_HASH_UINT64_T_OVERLOAD) @@ -61,3 +63,8 @@ check_c_source_compiles( " STRERROR_R_CHAR_P ) + +# Defined if using the CLN multi-precision arithmetic library. +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}) diff --git a/contrib/CMakeLists.txt b/contrib/CMakeLists.txt deleted file mode 100644 index e69de29bb..000000000 diff --git a/doc/CMakeLists.txt b/doc/CMakeLists.txt index 52867433e..6e9ba73fd 100644 --- a/doc/CMakeLists.txt +++ b/doc/CMakeLists.txt @@ -1,3 +1,7 @@ +# Set variables required for the documentation *.in files +string(TIMESTAMP MAN_DATE "%Y-%m-%d") +set(VERSION CVC4_RELEASE_STRING) + configure_file( ${CMAKE_CURRENT_SOURCE_DIR}/SmtEngine.3cvc_template.in ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.3cvc_template) diff --git a/src/prop/CMakeLists.txt b/src/prop/CMakeLists.txt deleted file mode 100644 index c7868e0f0..000000000 --- a/src/prop/CMakeLists.txt +++ /dev/null @@ -1,2 +0,0 @@ -add_subdirectory(bvminisat) -add_subdirectory(minisat) -- 2.30.2