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, 49 insertions, 56 deletions

diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt
index 868b7f97d..029397832 100644
--- a/src/main/CMakeLists.txt
+++ b/src/main/CMakeLists.txt
@@ -26,11 +26,11 @@ set(libmain_src_files
 )
 
 #-----------------------------------------------------------------------------#
-# Build object library since we will use the object files for cvc4-bin and
+# Build object library since we will use the object files for cvc5-bin and
 # main-test library.
 
 add_library(main OBJECT ${libmain_src_files})
-target_compile_definitions(main PRIVATE -D__BUILDING_CVC4DRIVER)
+target_compile_definitions(main PRIVATE -D__BUILDING_CVC5DRIVER)
 if(ENABLE_SHARED)
   set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE ON)
 endif()
@@ -39,8 +39,8 @@ endif()
 # supported for cmake version >= 3.12. Hence, we have to manually add the
 # library dependencies for main. As a consequence, include directories from
 # dependencies are not propagated and we need to manually add the include
-# directories of libcvc4 to main.
-add_dependencies(main cvc4 cvc4parser gen-tokens)
+# directories of libcvc5 to main.
+add_dependencies(main cvc5 cvc5parser gen-tokens)
 
 # Note: This should not be required anymore as soon as we get rid of the
 #       smt_engine.h include in src/main. smt_engine.h has transitive includes
@@ -56,35 +56,35 @@ target_include_directories(main PRIVATE ${GMP_INCLUDES})
 # that we don't have to include all object files of main into each api/unit
 # test. Do not link against main-test in any other case.
 add_library(main-test driver_unified.cpp $<TARGET_OBJECTS:main>)
-target_compile_definitions(main-test PRIVATE -D__BUILDING_CVC4DRIVER)
-target_link_libraries(main-test PUBLIC cvc4 cvc4parser)
+target_compile_definitions(main-test PRIVATE -D__BUILDING_CVC5DRIVER)
+target_link_libraries(main-test PUBLIC cvc5 cvc5parser)
 if(USE_CLN)
   target_link_libraries(main-test PUBLIC CLN)
 endif()
 target_link_libraries(main-test PUBLIC GMP)
 
 #-----------------------------------------------------------------------------#
-# cvc4 binary configuration
+# cvc5 binary configuration
 
-add_executable(cvc4-bin driver_unified.cpp main.cpp $<TARGET_OBJECTS:main>)
-target_compile_definitions(cvc4-bin PRIVATE -D__BUILDING_CVC4DRIVER)
-set_target_properties(cvc4-bin
+add_executable(cvc5-bin driver_unified.cpp main.cpp $<TARGET_OBJECTS:main>)
+target_compile_definitions(cvc5-bin PRIVATE -D__BUILDING_CVC5DRIVER)
+set_target_properties(cvc5-bin
   PROPERTIES
-    OUTPUT_NAME cvc4
+    OUTPUT_NAME cvc5
     RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
-target_link_libraries(cvc4-bin PUBLIC cvc4 cvc4parser)
+target_link_libraries(cvc5-bin PUBLIC cvc5 cvc5parser)
 if(USE_CLN)
-  target_link_libraries(cvc4-bin PUBLIC CLN)
+  target_link_libraries(cvc5-bin PUBLIC CLN)
 endif()
-target_link_libraries(cvc4-bin PUBLIC GMP)
+target_link_libraries(cvc5-bin PUBLIC GMP)
 
 if(PROGRAM_PREFIX)
   install(PROGRAMS
-    $<TARGET_FILE:cvc4-bin>
+    $<TARGET_FILE:cvc5-bin>
     DESTINATION ${CMAKE_INSTALL_BINDIR}
-    RENAME ${PROGRAM_PREFIX}cvc4)
+    RENAME ${PROGRAM_PREFIX}cvc5)
 else()
-  install(TARGETS cvc4-bin
+  install(TARGETS cvc5-bin
     DESTINATION ${CMAKE_INSTALL_BINDIR})
 endif()
 
@@ -93,13 +93,13 @@ endif()
 #   https://cmake.org/cmake/help/v3.0/prop_tgt/LINK_SEARCH_START_STATIC.html
 #   https://cmake.org/cmake/help/v3.0/prop_tgt/LINK_SEARCH_END_STATIC.html
 if(ENABLE_STATIC_BINARY)
-  set_target_properties(cvc4-bin PROPERTIES LINK_FLAGS -static)
-  set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_START_STATIC ON)
-  set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON)
+  set_target_properties(cvc5-bin PROPERTIES LINK_FLAGS -static)
+  set_target_properties(cvc5-bin PROPERTIES LINK_SEARCH_START_STATIC ON)
+  set_target_properties(cvc5-bin PROPERTIES LINK_SEARCH_END_STATIC ON)
 endif()
 
 if(USE_EDITLINE)
-  target_link_libraries(cvc4-bin PUBLIC ${Editline_LIBRARIES})
+  target_link_libraries(cvc5-bin PUBLIC ${Editline_LIBRARIES})
   target_link_libraries(main-test PUBLIC ${Editline_LIBRARIES})
   target_include_directories(main PUBLIC ${Editline_INCLUDE_DIRS})
 endif()
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 2481eda10..9b0ea4759 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Driver for cvc5 executable (cvc4).
+ * Driver for cvc5 executable (cvc5).
  */
 
 #include <stdio.h>
@@ -26,8 +26,8 @@
 
 #include "api/cpp/cvc5.h"
 #include "base/configuration.h"
+#include "base/cvc5config.h"
 #include "base/output.h"
-#include "cvc4autoconfig.h"
 #include "main/command_executor.h"
 #include "main/interactive_shell.h"
 #include "main/main.h"
@@ -91,7 +91,8 @@ void printUsage(Options& opts, bool full) {
   }
 }
 
-int runCvc4(int argc, char* argv[], Options& opts) {
+int runCvc5(int argc, char* argv[], Options& opts)
+{
   main::totalTime = std::make_unique<TotalTimer>();
   // For the signal handlers' benefit
   pOptions = &opts;
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 127b2c14d..516f9e621 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -27,7 +27,7 @@
 #include <vector>
 
 // This must go before HAVE_LIBEDITLINE.
-#include "cvc4autoconfig.h"
+#include "base/cvc5config.h"
 
 #if HAVE_LIBEDITLINE
 #include <editline/readline.h>
@@ -112,13 +112,13 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
     OutputLanguage lang = toOutputLanguage(d_options.getInputLanguage());
     switch(lang) {
       case output::LANG_CVC:
-        d_historyFilename = string(getenv("HOME")) + "/.cvc4_history";
+        d_historyFilename = string(getenv("HOME")) + "/.cvc5_history";
         commandsBegin = cvc_commands;
         commandsEnd =
             cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
         break;
       case output::LANG_TPTP:
-        d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp";
+        d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_tptp";
         commandsBegin = tptp_commands;
         commandsEnd =
             tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands);
@@ -126,7 +126,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
       default:
         if (language::isOutputLang_smt2(lang))
         {
-          d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
+          d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_smtlib2";
           commandsBegin = smt2_commands;
           commandsEnd =
               smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
diff --git a/src/main/main.cpp b/src/main/main.cpp
index a4e70be89..6a7baebb3 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -41,13 +41,13 @@ using namespace cvc5::language;
  * cvc5's main() routine is just an exception-safe wrapper around cvc5.
  * Please don't construct anything here.  Even if the constructor is
  * inside the try { }, an exception during destruction can cause
- * problems.  That's why main() wraps runCvc4() in the first place.
- * Put everything in runCvc4().
+ * problems.  That's why main() wraps runCvc5() in the first place.
+ * Put everything in runCvc5().
  */
 int main(int argc, char* argv[]) {
   Options opts;
   try {
-    return runCvc4(argc, argv, opts);
+    return runCvc5(argc, argv, opts);
   } catch(OptionException& e) {
 #ifdef CVC5_COMPETITION_MODE
     *opts.getOut() << "unknown" << endl;
diff --git a/src/main/main.h b/src/main/main.h
index 121f9d951..54abbdbe9 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -18,8 +18,8 @@
 #include <memory>
 #include <string>
 
+#include "base/cvc5config.h"
 #include "base/exception.h"
-#include "cvc4autoconfig.h"
 #include "options/options.h"
 
 #ifndef CVC5__MAIN__MAIN_H
@@ -62,19 +62,11 @@ extern bool segvSpin;
 /** A pointer to the options in play */
 extern thread_local Options* pOptions;
 
-/** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV.
- * This can throw a cvc5::Exception.
- */
-void cvc4_init();
-
-/** Shutdown the driver. Frees memory for the signal handlers. */
-void cvc4_shutdown() noexcept;
-
 }  // namespace main
 }  // namespace cvc5
 
-/** Actual Cvc4 driver functions **/
-int runCvc4(int argc, char* argv[], cvc5::Options&);
+/** Actual cvc5 driver functions **/
+int runCvc5(int argc, char* argv[], cvc5::Options&);
 void printUsage(cvc5::Options&, bool full = false);
 
 #endif /* CVC5__MAIN__MAIN_H */
diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp
index 9a6e34075..503bbc198 100644
--- a/src/main/signal_handlers.cpp
+++ b/src/main/signal_handlers.cpp
@@ -32,8 +32,8 @@
 
 #endif /* __WIN32__ */
 
+#include "base/cvc5config.h"
 #include "base/exception.h"
-#include "cvc4autoconfig.h"
 #include "main/command_executor.h"
 #include "main/main.h"
 #include "options/options.h"
@@ -73,8 +73,8 @@ void timeout_handler()
 #ifndef __WIN32__
 
 #ifdef HAVE_SIGALTSTACK
-size_t cvc4StackSize;
-void* cvc4StackBase;
+size_t stackSize;
+void* stackBase;
 #endif /* HAVE_SIGALTSTACK */
 
 /** Handler for SIGXCPU and SIGALRM, i.e., timeout. */
@@ -100,15 +100,15 @@ void sigint_handler(int sig, siginfo_t* info, void*)
 /** Handler for SIGSEGV (segfault). */
 void segv_handler(int sig, siginfo_t* info, void* c)
 {
-  uintptr_t extent = reinterpret_cast<uintptr_t>(cvc4StackBase) - cvc4StackSize;
+  uintptr_t extent = reinterpret_cast<uintptr_t>(stackBase) - stackSize;
   uintptr_t addr = reinterpret_cast<uintptr_t>(info->si_addr);
 #ifdef CVC5_DEBUG
   safe_print(STDERR_FILENO, "cvc5 suffered a segfault in DEBUG mode.\n");
   safe_print(STDERR_FILENO, "Offending address is ");
   safe_print(STDERR_FILENO, info->si_addr);
   safe_print(STDERR_FILENO, "\n");
-  // cerr << "base is " << (void*)cvc4StackBase << endl;
-  // cerr << "size is " << cvc4StackSize << endl;
+  // cerr << "base is " << (void*)stackBase << endl;
+  // cerr << "size is " << stackSize << endl;
   // cerr << "extent is " << (void*)extent << endl;
   if (addr >= extent && addr <= extent + 10 * 1024)
   {
@@ -211,7 +211,7 @@ void ill_handler(int sig, siginfo_t* info, void*)
 
 static terminate_handler default_terminator;
 
-void cvc4terminate()
+void cvc5terminate()
 {
   set_terminate(default_terminator);
 #ifdef CVC5_DEBUG
@@ -301,8 +301,8 @@ void install()
     throw Exception(string("sigaltstack() failure: ") + strerror(errno));
   }
 
-  cvc4StackSize = limit.rlim_cur;
-  cvc4StackBase = ss.ss_sp;
+  stackSize = limit.rlim_cur;
+  stackBase = ss.ss_sp;
 
   struct sigaction act4;
   act4.sa_sigaction = segv_handler;
@@ -325,16 +325,16 @@ void install()
 
 #endif /* __WIN32__ */
 
-  default_terminator = set_terminate(cvc4terminate);
+  default_terminator = set_terminate(cvc5terminate);
 }
 
 void cleanup() noexcept
 {
 #ifndef __WIN32__
 #ifdef HAVE_SIGALTSTACK
-  free(cvc4StackBase);
-  cvc4StackBase = NULL;
-  cvc4StackSize = 0;
+  free(stackBase);
+  stackBase = nullptr;
+  stackSize = 0;
 #endif /* HAVE_SIGALTSTACK */
 #endif /* __WIN32__ */
 }
diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp
index bd41ed7ed..82cfda017 100644
--- a/src/main/time_limit.cpp
+++ b/src/main/time_limit.cpp
@@ -41,7 +41,7 @@
 
 #include "time_limit.h"
 
-#include "cvc4autoconfig.h"
+#include "base/cvc5config.h"
 
 #if HAVE_SETITIMER
 #include <signal.h>