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

1 files changed, 21 insertions, 21 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()