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/.

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()