diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-04-21 10:21:34 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-21 10:21:34 -0700 |
commit | ae5ee4b07dc3d3c792e7fe7f382ff490dd28aca4 (patch) | |
tree | a7c2ab8013f46dbea75fcd6e7da3fb83e2012b2f /cmake | |
parent | 86aa9bc35ba9dc9a57913a2ffc71619c7657cc35 (diff) |
Goodbye CVC4, hello cvc5! (#6371)
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
Diffstat (limited to 'cmake')
-rw-r--r-- | cmake/ConfigCompetition.cmake | 30 | ||||
-rw-r--r-- | cmake/ConfigDebug.cmake | 16 | ||||
-rw-r--r-- | cmake/ConfigProduction.cmake | 16 | ||||
-rw-r--r-- | cmake/ConfigTesting.cmake | 16 | ||||
-rw-r--r-- | cmake/ConfigureCvc5.cmake (renamed from cmake/ConfigureCVC4.cmake) | 0 | ||||
-rw-r--r-- | cmake/Helpers.cmake | 20 | ||||
-rw-r--r-- | cmake/cvc5Config.cmake.in (renamed from cmake/CVC4Config.cmake.in) | 8 |
7 files changed, 53 insertions, 53 deletions
diff --git a/cmake/ConfigCompetition.cmake b/cmake/ConfigCompetition.cmake index 615371915..785f792d4 100644 --- a/cmake/ConfigCompetition.cmake +++ b/cmake/ConfigCompetition.cmake @@ -18,30 +18,30 @@ add_check_c_cxx_flag("-fno-enforce-eh-specs") # OPTLEVEL=9 set(OPTIMIZATION_LEVEL 9) # enable_debug_symbols=no -cvc4_set_option(ENABLE_DEBUG_SYMBOLS OFF) +cvc5_set_option(ENABLE_DEBUG_SYMBOLS OFF) # enable_statistics=no -cvc4_set_option(ENABLE_STATISTICS OFF) +cvc5_set_option(ENABLE_STATISTICS OFF) # enable_assertions=no -cvc4_set_option(ENABLE_ASSERTIONS OFF) +cvc5_set_option(ENABLE_ASSERTIONS OFF) # enable_proof=no -cvc4_set_option(ENABLE_PROOFS OFF) +cvc5_set_option(ENABLE_PROOFS OFF) # enable_tracing=no -cvc4_set_option(ENABLE_TRACING OFF) +cvc5_set_option(ENABLE_TRACING OFF) # enable_dumping=no -cvc4_set_option(ENABLE_DUMPING OFF) +cvc5_set_option(ENABLE_DUMPING OFF) # enable_muzzle=yes -cvc4_set_option(ENABLE_MUZZLE ON) +cvc5_set_option(ENABLE_MUZZLE ON) # enable_valgrind=no # enable_shared=no -cvc4_set_option(ENABLE_SHARED OFF) -cvc4_set_option(ENABLE_UNIT_TESTING OFF) +cvc5_set_option(ENABLE_SHARED OFF) +cvc5_set_option(ENABLE_UNIT_TESTING OFF) # By default, we include all dependencies in our competition build that are # required to achieve the best performance set(ENABLE_GPL ON) -cvc4_set_option(USE_CADICAL ON) -cvc4_set_option(USE_CLN ON) -cvc4_set_option(USE_CRYPTOMINISAT ON) -cvc4_set_option(USE_EDITLINE OFF) -cvc4_set_option(USE_GLPK ON) -cvc4_set_option(USE_SYMFPU ON) +cvc5_set_option(USE_CADICAL ON) +cvc5_set_option(USE_CLN ON) +cvc5_set_option(USE_CRYPTOMINISAT ON) +cvc5_set_option(USE_EDITLINE OFF) +cvc5_set_option(USE_GLPK ON) +cvc5_set_option(USE_SYMFPU ON) diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake index d89104bb4..bab629607 100644 --- a/cmake/ConfigDebug.cmake +++ b/cmake/ConfigDebug.cmake @@ -15,21 +15,21 @@ add_definitions(-DCVC5_DEBUG) add_check_c_cxx_flag("-fno-inline") set(OPTIMIZATION_LEVEL "g") # enable_debug_symbols=yes -cvc4_set_option(ENABLE_DEBUG_SYMBOLS ON) +cvc5_set_option(ENABLE_DEBUG_SYMBOLS ON) # enable_statistics=yes -cvc4_set_option(ENABLE_STATISTICS ON) +cvc5_set_option(ENABLE_STATISTICS ON) # enable_assertions=yes -cvc4_set_option(ENABLE_ASSERTIONS ON) +cvc5_set_option(ENABLE_ASSERTIONS ON) # enable_proof=yes -cvc4_set_option(ENABLE_PROOFS ON) +cvc5_set_option(ENABLE_PROOFS ON) # enable_tracing=yes -cvc4_set_option(ENABLE_TRACING ON) +cvc5_set_option(ENABLE_TRACING ON) # enable_dumping=yes -cvc4_set_option(ENABLE_DUMPING ON) +cvc5_set_option(ENABLE_DUMPING ON) # enable_muzzle=no -cvc4_set_option(ENABLE_MUZZLE OFF) +cvc5_set_option(ENABLE_MUZZLE OFF) # enable_valgrind=optional -cvc4_set_option(ENABLE_UNIT_TESTING ON) +cvc5_set_option(ENABLE_UNIT_TESTING ON) # Reset visibility for debug builds (https://github.com/CVC4/CVC4/issues/324) set(CMAKE_CXX_VISIBILITY_PRESET default) diff --git a/cmake/ConfigProduction.cmake b/cmake/ConfigProduction.cmake index b33d42a01..5d94f038e 100644 --- a/cmake/ConfigProduction.cmake +++ b/cmake/ConfigProduction.cmake @@ -14,18 +14,18 @@ # OPTLEVEL=3 set(OPTIMIZATION_LEVEL 3) # enable_debug_symbols=no -cvc4_set_option(ENABLE_DEBUG_SYMBOLS OFF) +cvc5_set_option(ENABLE_DEBUG_SYMBOLS OFF) # enable_statistics=yes -cvc4_set_option(ENABLE_STATISTICS ON) +cvc5_set_option(ENABLE_STATISTICS ON) # enable_assertions=no -cvc4_set_option(ENABLE_ASSERTIONS OFF) +cvc5_set_option(ENABLE_ASSERTIONS OFF) # enable_proof=yes -cvc4_set_option(ENABLE_PROOFS ON) +cvc5_set_option(ENABLE_PROOFS ON) # enable_tracing=no -cvc4_set_option(ENABLE_TRACING OFF) +cvc5_set_option(ENABLE_TRACING OFF) # enable_dumping=yes -cvc4_set_option(ENABLE_DUMPING ON) +cvc5_set_option(ENABLE_DUMPING ON) # enable_muzzle=no -cvc4_set_option(ENABLE_MUZZLE OFF) +cvc5_set_option(ENABLE_MUZZLE OFF) # enable_valgrind=no -cvc4_set_option(ENABLE_UNIT_TESTING OFF) +cvc5_set_option(ENABLE_UNIT_TESTING OFF) diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake index 56086e6a0..e1e1ef6f6 100644 --- a/cmake/ConfigTesting.cmake +++ b/cmake/ConfigTesting.cmake @@ -14,18 +14,18 @@ # OPTLEVEL=2 set(OPTIMIZATION_LEVEL 2) # enable_debug_symbols=yes -cvc4_set_option(ENABLE_DEBUG_SYMBOLS ON) +cvc5_set_option(ENABLE_DEBUG_SYMBOLS ON) # enable_statistics=yes -cvc4_set_option(ENABLE_STATISTICS ON) +cvc5_set_option(ENABLE_STATISTICS ON) # enable_assertions=yes -cvc4_set_option(ENABLE_ASSERTIONS ON) +cvc5_set_option(ENABLE_ASSERTIONS ON) # enable_proof=yes -cvc4_set_option(ENABLE_PROOFS ON) +cvc5_set_option(ENABLE_PROOFS ON) # enable_tracing=yes -cvc4_set_option(ENABLE_TRACING ON) +cvc5_set_option(ENABLE_TRACING ON) # enable_dumping=yes -cvc4_set_option(ENABLE_DUMPING ON) +cvc5_set_option(ENABLE_DUMPING ON) # enable_muzzle=no -cvc4_set_option(ENABLE_MUZZLE OFF) +cvc5_set_option(ENABLE_MUZZLE OFF) # enable_valgrind=no -cvc4_set_option(ENABLE_UNIT_TESTING ON) +cvc5_set_option(ENABLE_UNIT_TESTING ON) diff --git a/cmake/ConfigureCVC4.cmake b/cmake/ConfigureCvc5.cmake index 009e9969b..009e9969b 100644 --- a/cmake/ConfigureCVC4.cmake +++ b/cmake/ConfigureCvc5.cmake diff --git a/cmake/Helpers.cmake b/cmake/Helpers.cmake index bb102e482..10bcf96de 100644 --- a/cmake/Helpers.cmake +++ b/cmake/Helpers.cmake @@ -99,20 +99,20 @@ macro(add_required_c_cxx_flag flag) add_required_cxx_flag(${flag}) endmacro() -# CVC4 Boolean options are three-valued to detect if an option was set by the +# cvc5 Boolean options are three-valued to detect if an option was set by the # user. The available values are: IGNORE (default), ON, OFF # Default options do not override options that were set by the user, i.e., -# cvc4_set_option only sets an option if it's value is still IGNORE. +# cvc5_set_option only sets an option if it's value is still IGNORE. # This e.g., allows the user to disable proofs for debug builds (where proofs # are enabled by default). -macro(cvc4_option var description) +macro(cvc5_option var description) set(${var} IGNORE CACHE STRING "${description}") # Provide drop down menu options in cmake-gui set_property(CACHE ${var} PROPERTY STRINGS IGNORE ON OFF) endmacro() # Only set option if the user did not set an option. -macro(cvc4_set_option var value) +macro(cvc5_set_option var value) if(${var} STREQUAL "IGNORE") set(${var} ${value}) endif() @@ -145,12 +145,12 @@ function(print_config str var) endfunction() -# Collect all source files that are required to build libcvc4 in LIBCVC4_SRCS -# or LIBCVC4_GEN_SRCS. If GENERATED is the first argument the sources are -# added to LIBCVC4_GEN_SRCS. All sources are prepended with the absolute +# Collect all source files that are required to build libcvc5 in LIBCVC5_SRCS +# or LIBCVC5_GEN_SRCS. If GENERATED is the first argument the sources are +# added to LIBCVC5_GEN_SRCS. All sources are prepended with the absolute # current path path. CMAKE_CURRENT_BINARY_DIR is prepended # to generated source files. -macro(libcvc4_add_sources) +macro(libcvc5_add_sources) set(_sources ${ARGV}) # Check if the first argument is GENERATED. @@ -158,10 +158,10 @@ macro(libcvc4_add_sources) if(${_generated} STREQUAL "GENERATED") list(REMOVE_AT _sources 0) set(_cur_path ${CMAKE_CURRENT_BINARY_DIR}) - set(_append_to LIBCVC4_GEN_SRCS) + set(_append_to LIBCVC5_GEN_SRCS) else() set(_cur_path ${CMAKE_CURRENT_SOURCE_DIR}) - set(_append_to LIBCVC4_SRCS) + set(_append_to LIBCVC5_SRCS) endif() # Prepend source files with current path. diff --git a/cmake/CVC4Config.cmake.in b/cmake/cvc5Config.cmake.in index c85973a6a..6b238fb38 100644 --- a/cmake/CVC4Config.cmake.in +++ b/cmake/cvc5Config.cmake.in @@ -17,13 +17,13 @@ set(CVC5_BINDINGS_JAVA @BUILD_BINDINGS_JAVA@) set(CVC5_BINDINGS_PYTHON @BUILD_BINDINGS_PYTHON@) set(CVC5_BINDINGS_PYTHON_VERSION @BUILD_BINDINGS_PYTHON_VERSION@) -if(NOT TARGET CVC4::cvc4) - include(${CMAKE_CURRENT_LIST_DIR}/CVC4Targets.cmake) +if(NOT TARGET cvc5::cvc5) + include(${CMAKE_CURRENT_LIST_DIR}/cvc5Targets.cmake) endif() # TODO(project wishue #83): enable these lines -# if(CVC5_BINDINGS_JAVA AND NOT TARGET CVC4::cvc4jar) +# if(CVC5_BINDINGS_JAVA AND NOT TARGET cvc5::cvc5jar) # set_and_check(CVC5_JNI_PATH "@PACKAGE_LIBRARY_INSTALL_DIR@") -# include(${CMAKE_CURRENT_LIST_DIR}/CVC4JavaTargets.cmake) +# include(${CMAKE_CURRENT_LIST_DIR}/cvc5JavaTargets.cmake) # endif() |