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, 50 insertions, 50 deletions

diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt
index 4eca7e442..02405a0cc 100644
--- a/src/api/python/CMakeLists.txt
+++ b/src/api/python/CMakeLists.txt
@@ -22,11 +22,11 @@ endif()
 find_package(PythonExtensions REQUIRED)
 find_package(Cython 0.29 REQUIRED)
 
-# Generate cvc4kinds.{pxd,pyx}
+# Generate cvc5kinds.{pxd,pyx}
 configure_file(genkinds.py.in genkinds.py)
 set(GENERATED_FILES
-  "${CMAKE_CURRENT_BINARY_DIR}/cvc4kinds.pxd"
-  "${CMAKE_CURRENT_BINARY_DIR}/cvc4kinds.pxi"
+  "${CMAKE_CURRENT_BINARY_DIR}/cvc5kinds.pxd"
+  "${CMAKE_CURRENT_BINARY_DIR}/cvc5kinds.pxi"
 )
 add_custom_command(
   OUTPUT
@@ -37,58 +37,58 @@ add_custom_command(
     "${PYTHON_EXECUTABLE}"
     "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py"
     --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h"
-    --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc4kinds"
+    --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc5kinds"
   DEPENDS
     "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py"
     "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h"
 )
 
-add_custom_target(cvc4kinds DEPENDS ${GENERATED_FILES})
+add_custom_target(cvc5kinds DEPENDS ${GENERATED_FILES})
 
-include_directories(${CMAKE_CURRENT_BINARY_DIR})   # for cvc4kinds.pxi
-add_cython_target(pycvc4 CXX)
+include_directories(${CMAKE_CURRENT_BINARY_DIR})   # for cvc5kinds.pxi
+add_cython_target(pycvc5 CXX)
 
-add_library(pycvc4
+add_library(pycvc5
             MODULE
-            ${pycvc4})
-add_dependencies(pycvc4 cvc4kinds)
+            ${pycvc5})
+add_dependencies(pycvc5 cvc5kinds)
 
-target_include_directories(pycvc4
+target_include_directories(pycvc5
   PRIVATE
   ${PYTHON_INCLUDE_DIRS}
   ${PROJECT_SOURCE_DIR}/src       # for API headers in src/api/cpp
-  ${CMAKE_BINARY_DIR}/src         # for cvc4_export.h
+  ${CMAKE_BINARY_DIR}/src         # for cvc5_export.h
 )
 
-target_link_libraries(pycvc4 cvc4 ${PYTHON_LIBRARIES})
+target_link_libraries(pycvc5 cvc5 ${PYTHON_LIBRARIES})
 
 # Disable -Werror and other warnings for code generated by Cython.
 # Note: Visibility is reset to default here since otherwise the PyInit_...
 # function will not be exported correctly
 # (https://github.com/cython/cython/issues/3380).
-set_target_properties(pycvc4
+set_target_properties(pycvc5
                       PROPERTIES
                       COMPILE_FLAGS
                         "-Wno-error -Wno-shadow -Wno-implicit-fallthrough"
                       CXX_VISIBILITY_PRESET default
                       VISIBILITY_INLINES_HIDDEN 0)
 
-python_extension_module(pycvc4)
+python_extension_module(pycvc5)
 
 # Installation based on https://bloerg.net/2012/11/10/cmake-and-distutils.html
 # Create a wrapper python directory and generate a distutils setup.py file
 configure_file(setup.py.in setup.py)
-set(PYCVC5_MODULE "${CMAKE_CURRENT_BINARY_DIR}/pycvc4")
+set(PYCVC5_MODULE "${CMAKE_CURRENT_BINARY_DIR}/pycvc5")
 file(MAKE_DIRECTORY "${PYCVC5_MODULE}")
 file(WRITE ${PYCVC5_MODULE}/__init__.py
 "import sys
-from .pycvc4 import *
-# fake a submodule for dotted imports, e.g. from pycvc4.kinds import *
+from .pycvc5 import *
+# fake a submodule for dotted imports, e.g. from pycvc5.kinds import *
 sys.modules['%s.%s'%(__name__, kinds.__name__)] = kinds")
 
-set(PYCVC5_LOC "${PYCVC5_MODULE}/$<TARGET_FILE_NAME:pycvc4>")
-add_custom_command(TARGET pycvc4 POST_BUILD
-    COMMAND ${CMAKE_COMMAND} -E rename $<TARGET_FILE:pycvc4> ${PYCVC5_LOC}
+set(PYCVC5_LOC "${PYCVC5_MODULE}/$<TARGET_FILE_NAME:pycvc5>")
+add_custom_command(TARGET pycvc5 POST_BUILD
+    COMMAND ${CMAKE_COMMAND} -E rename $<TARGET_FILE:pycvc5> ${PYCVC5_LOC}
 )
 
 # figure out if we're in a virtualenv
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc5.pxd
index 336def3dc..83d811a1d 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc5.pxd
@@ -5,7 +5,7 @@ from libcpp.set cimport set
 from libcpp.string cimport string
 from libcpp.vector cimport vector
 from libcpp.pair cimport pair
-from cvc4kinds cimport Kind
+from cvc5kinds cimport Kind
 
 
 cdef extern from "<iostream>" namespace "std":
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc5.pxi
index 48921dc87..0ee56cd55 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc5.pxi
@@ -9,27 +9,27 @@ from libcpp.set cimport set
 from libcpp.string cimport string
 from libcpp.vector cimport vector
 
-from cvc4 cimport cout
-from cvc4 cimport Datatype as c_Datatype
-from cvc4 cimport DatatypeConstructor as c_DatatypeConstructor
-from cvc4 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl
-from cvc4 cimport DatatypeDecl as c_DatatypeDecl
-from cvc4 cimport DatatypeSelector as c_DatatypeSelector
-from cvc4 cimport Result as c_Result
-from cvc4 cimport RoundingMode as c_RoundingMode
-from cvc4 cimport Op as c_Op
-from cvc4 cimport OpHashFunction as c_OpHashFunction
-from cvc4 cimport Solver as c_Solver
-from cvc4 cimport Grammar as c_Grammar
-from cvc4 cimport Sort as c_Sort
-from cvc4 cimport SortHashFunction as c_SortHashFunction
-from cvc4 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE
-from cvc4 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO
-from cvc4 cimport ROUND_NEAREST_TIES_TO_AWAY
-from cvc4 cimport Term as c_Term
-from cvc4 cimport TermHashFunction as c_TermHashFunction
-
-from cvc4kinds cimport Kind as c_Kind
+from cvc5 cimport cout
+from cvc5 cimport Datatype as c_Datatype
+from cvc5 cimport DatatypeConstructor as c_DatatypeConstructor
+from cvc5 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl
+from cvc5 cimport DatatypeDecl as c_DatatypeDecl
+from cvc5 cimport DatatypeSelector as c_DatatypeSelector
+from cvc5 cimport Result as c_Result
+from cvc5 cimport RoundingMode as c_RoundingMode
+from cvc5 cimport Op as c_Op
+from cvc5 cimport OpHashFunction as c_OpHashFunction
+from cvc5 cimport Solver as c_Solver
+from cvc5 cimport Grammar as c_Grammar
+from cvc5 cimport Sort as c_Sort
+from cvc5 cimport SortHashFunction as c_SortHashFunction
+from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE
+from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO
+from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY
+from cvc5 cimport Term as c_Term
+from cvc5 cimport TermHashFunction as c_TermHashFunction
+
+from cvc5kinds cimport Kind as c_Kind
 
 ################################## DECORATORS #################################
 def expand_list_arg(num_req_args=0):
diff --git a/src/api/python/genkinds.py.in b/src/api/python/genkinds.py.in
index a78372e71..8c8de35ac 100644
--- a/src/api/python/genkinds.py.in
+++ b/src/api/python/genkinds.py.in
@@ -56,7 +56,7 @@ KINDS_PXI_TOP = \
 r"""# distutils: language = c++
 # distutils: extra_compile_args = -std=c++11
 
-from cvc4kinds cimport *
+from cvc5kinds cimport *
 import sys
 from types import ModuleType
 
diff --git a/src/api/python/pycvc4.pyx b/src/api/python/pycvc4.pyx
deleted file mode 100644
index 40766341a..000000000
--- a/src/api/python/pycvc4.pyx
+++ /dev/null
@@ -1,2 +0,0 @@
-include "cvc4kinds.pxi"
-include "cvc4.pxi"
diff --git a/src/api/python/pycvc5.pyx b/src/api/python/pycvc5.pyx
new file mode 100644
index 000000000..f09300265
--- /dev/null
+++ b/src/api/python/pycvc5.pyx
@@ -0,0 +1,2 @@
+include "cvc5kinds.pxi"
+include "cvc5.pxi"
diff --git a/src/api/python/setup.py.in b/src/api/python/setup.py.in
index 8919dd3f1..231f27c2a 100644
--- a/src/api/python/setup.py.in
+++ b/src/api/python/setup.py.in
@@ -35,9 +35,9 @@ class PyCVC5Install(install):
         c.finalize_options()
         c.run()
 
-setup(name='pycvc4',
+setup(name='pycvc5',
       version='${CVC5_MAJOR}.${CVC5_MINOR}.${CVC5_RELEASE}',
-      packages=['pycvc4'],
-      package_dir={'pycvc4': '${CMAKE_CURRENT_BINARY_DIR}/pycvc4'},
-      package_data={'pycvc4': ['pycvc4.so']},
+      packages=['pycvc5'],
+      package_dir={'pycvc5': '${CMAKE_CURRENT_BINARY_DIR}/pycvc5'},
+      package_data={'pycvc5': ['pycvc5.so']},
       cmdclass={'install': PyCVC5Install})