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

11 files changed, 107 insertions, 105 deletions

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index c8f1b8d4a..96e287f84 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -13,7 +13,7 @@
  * The cvc5 C++ API.
  */
 
-#include "cvc4_export.h"
+#include "cvc5_export.h"
 
 #ifndef CVC5__API__CVC5_H
 #define CVC5__API__CVC5_H
@@ -63,7 +63,7 @@ struct APIStatistics;
  * Base class for all API exceptions.
  * If thrown, all API objects may be in an unsafe state.
  */
-class CVC4_EXPORT CVC5ApiException : public std::exception
+class CVC5_EXPORT CVC5ApiException : public std::exception
 {
  public:
   /**
@@ -96,7 +96,7 @@ class CVC4_EXPORT CVC5ApiException : public std::exception
  * A recoverable API exception.
  * If thrown, API objects can still be used.
  */
-class CVC4_EXPORT CVC5ApiRecoverableException : public CVC5ApiException
+class CVC5_EXPORT CVC5ApiRecoverableException : public CVC5ApiException
 {
  public:
   /**
@@ -121,7 +121,7 @@ class CVC4_EXPORT CVC5ApiRecoverableException : public CVC5ApiException
 /**
  * Encapsulation of a three-valued solver result, with explanations.
  */
-class CVC4_EXPORT Result
+class CVC5_EXPORT Result
 {
   friend class Solver;
 
@@ -230,7 +230,7 @@ class CVC4_EXPORT Result
  * @param r the result to be serialized to the given output stream
  * @return the output stream
  */
-std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_EXPORT;
+std::ostream& operator<<(std::ostream& out, const Result& r) CVC5_EXPORT;
 
 /**
  * Serialize an UnknownExplanation to given stream.
@@ -239,7 +239,7 @@ std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_EXPORT;
  * @return the output stream
  */
 std::ostream& operator<<(std::ostream& out,
-                         enum Result::UnknownExplanation e) CVC4_EXPORT;
+                         enum Result::UnknownExplanation e) CVC5_EXPORT;
 
 /* -------------------------------------------------------------------------- */
 /* Sort                                                                       */
@@ -250,7 +250,7 @@ class Datatype;
 /**
  * The sort of a cvc5 term.
  */
-class CVC4_EXPORT Sort
+class CVC5_EXPORT Sort
 {
   friend class cvc5::Command;
   friend class DatatypeConstructor;
@@ -749,12 +749,12 @@ class CVC4_EXPORT Sort
  * @param s the sort to be serialized to the given output stream
  * @return the output stream
  */
-std::ostream& operator<<(std::ostream& out, const Sort& s) CVC4_EXPORT;
+std::ostream& operator<<(std::ostream& out, const Sort& s) CVC5_EXPORT;
 
 /**
  * Hash function for Sorts.
  */
-struct CVC4_EXPORT SortHashFunction
+struct CVC5_EXPORT SortHashFunction
 {
   size_t operator()(const Sort& s) const;
 };
@@ -768,7 +768,7 @@ struct CVC4_EXPORT SortHashFunction
  * An operator is a term that represents certain operators, instantiated
  * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT.
  */
-class CVC4_EXPORT Op
+class CVC5_EXPORT Op
 {
   friend class Solver;
   friend class Term;
@@ -896,7 +896,7 @@ class CVC4_EXPORT Op
 /**
  * A cvc5 Term.
  */
-class CVC4_EXPORT Term
+class CVC5_EXPORT Term
 {
   friend class cvc5::Command;
   friend class Datatype;
@@ -1285,7 +1285,7 @@ class CVC4_EXPORT Term
 /**
  * Hash function for Terms.
  */
-struct CVC4_EXPORT TermHashFunction
+struct CVC5_EXPORT TermHashFunction
 {
   size_t operator()(const Term& t) const;
 };
@@ -1296,7 +1296,7 @@ struct CVC4_EXPORT TermHashFunction
  * @param t the term to be serialized to the given output stream
  * @return the output stream
  */
-std::ostream& operator<<(std::ostream& out, const Term& t) CVC4_EXPORT;
+std::ostream& operator<<(std::ostream& out, const Term& t) CVC5_EXPORT;
 
 /**
  * Serialize a vector of terms to given stream.
@@ -1305,7 +1305,7 @@ std::ostream& operator<<(std::ostream& out, const Term& t) CVC4_EXPORT;
  * @return the output stream
  */
 std::ostream& operator<<(std::ostream& out,
-                         const std::vector<Term>& vector) CVC4_EXPORT;
+                         const std::vector<Term>& vector) CVC5_EXPORT;
 
 /**
  * Serialize a set of terms to the given stream.
@@ -1314,7 +1314,7 @@ std::ostream& operator<<(std::ostream& out,
  * @return the output stream
  */
 std::ostream& operator<<(std::ostream& out,
-                         const std::set<Term>& set) CVC4_EXPORT;
+                         const std::set<Term>& set) CVC5_EXPORT;
 
 /**
  * Serialize an unordered_set of terms to the given stream.
@@ -1325,7 +1325,7 @@ std::ostream& operator<<(std::ostream& out,
  */
 std::ostream& operator<<(std::ostream& out,
                          const std::unordered_set<Term, TermHashFunction>&
-                             unordered_set) CVC4_EXPORT;
+                             unordered_set) CVC5_EXPORT;
 
 /**
  * Serialize a map of terms to the given stream.
@@ -1336,7 +1336,7 @@ std::ostream& operator<<(std::ostream& out,
  */
 template <typename V>
 std::ostream& operator<<(std::ostream& out,
-                         const std::map<Term, V>& map) CVC4_EXPORT;
+                         const std::map<Term, V>& map) CVC5_EXPORT;
 
 /**
  * Serialize an unordered_map of terms to the given stream.
@@ -1348,7 +1348,7 @@ std::ostream& operator<<(std::ostream& out,
 template <typename V>
 std::ostream& operator<<(std::ostream& out,
                          const std::unordered_map<Term, V, TermHashFunction>&
-                             unordered_map) CVC4_EXPORT;
+                             unordered_map) CVC5_EXPORT;
 
 /**
  * Serialize an operator to given stream.
@@ -1356,12 +1356,12 @@ std::ostream& operator<<(std::ostream& out,
  * @param t the operator to be serialized to the given output stream
  * @return the output stream
  */
-std::ostream& operator<<(std::ostream& out, const Op& t) CVC4_EXPORT;
+std::ostream& operator<<(std::ostream& out, const Op& t) CVC5_EXPORT;
 
 /**
  * Hash function for Ops.
  */
-struct CVC4_EXPORT OpHashFunction
+struct CVC5_EXPORT OpHashFunction
 {
   size_t operator()(const Op& t) const;
 };
@@ -1376,7 +1376,7 @@ class DatatypeIterator;
 /**
  * A cvc5 datatype constructor declaration.
  */
-class CVC4_EXPORT DatatypeConstructorDecl
+class CVC5_EXPORT DatatypeConstructorDecl
 {
   friend class DatatypeDecl;
   friend class Solver;
@@ -1446,7 +1446,7 @@ class Solver;
 /**
  * A cvc5 datatype declaration.
  */
-class CVC4_EXPORT DatatypeDecl
+class CVC5_EXPORT DatatypeDecl
 {
   friend class DatatypeConstructorArg;
   friend class Solver;
@@ -1550,7 +1550,7 @@ class CVC4_EXPORT DatatypeDecl
 /**
  * A cvc5 datatype selector.
  */
-class CVC4_EXPORT DatatypeSelector
+class CVC5_EXPORT DatatypeSelector
 {
   friend class DatatypeConstructor;
   friend class Solver;
@@ -1619,7 +1619,7 @@ class CVC4_EXPORT DatatypeSelector
 /**
  * A cvc5 datatype constructor.
  */
-class CVC4_EXPORT DatatypeConstructor
+class CVC5_EXPORT DatatypeConstructor
 {
   friend class Datatype;
   friend class Solver;
@@ -1846,7 +1846,7 @@ class CVC4_EXPORT DatatypeConstructor
 /**
  * A cvc5 datatype.
  */
-class CVC4_EXPORT Datatype
+class CVC5_EXPORT Datatype
 {
   friend class Solver;
   friend class Sort;
@@ -2072,7 +2072,7 @@ class CVC4_EXPORT Datatype
  * @return the output stream
  */
 std::ostream& operator<<(std::ostream& out,
-                         const DatatypeDecl& dtdecl) CVC4_EXPORT;
+                         const DatatypeDecl& dtdecl) CVC5_EXPORT;
 
 /**
  * Serialize a datatype constructor declaration to given stream.
@@ -2081,7 +2081,7 @@ std::ostream& operator<<(std::ostream& out,
  * @return the output stream
  */
 std::ostream& operator<<(std::ostream& out,
-                         const DatatypeConstructorDecl& ctordecl) CVC4_EXPORT;
+                         const DatatypeConstructorDecl& ctordecl) CVC5_EXPORT;
 
 /**
  * Serialize a vector of datatype constructor declarations to given stream.
@@ -2092,7 +2092,7 @@ std::ostream& operator<<(std::ostream& out,
  */
 std::ostream& operator<<(std::ostream& out,
                          const std::vector<DatatypeConstructorDecl>& vector)
-    CVC4_EXPORT;
+    CVC5_EXPORT;
 
 /**
  * Serialize a datatype to given stream.
@@ -2100,7 +2100,7 @@ std::ostream& operator<<(std::ostream& out,
  * @param dtype the datatype to be serialized to given stream
  * @return the output stream
  */
-std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC4_EXPORT;
+std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC5_EXPORT;
 
 /**
  * Serialize a datatype constructor to given stream.
@@ -2109,7 +2109,7 @@ std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC4_EXPORT;
  * @return the output stream
  */
 std::ostream& operator<<(std::ostream& out,
-                         const DatatypeConstructor& ctor) CVC4_EXPORT;
+                         const DatatypeConstructor& ctor) CVC5_EXPORT;
 
 /**
  * Serialize a datatype selector to given stream.
@@ -2118,7 +2118,7 @@ std::ostream& operator<<(std::ostream& out,
  * @return the output stream
  */
 std::ostream& operator<<(std::ostream& out,
-                         const DatatypeSelector& stor) CVC4_EXPORT;
+                         const DatatypeSelector& stor) CVC5_EXPORT;
 
 /* -------------------------------------------------------------------------- */
 /* Grammar                                                                    */
@@ -2127,7 +2127,7 @@ std::ostream& operator<<(std::ostream& out,
 /**
  * A Sygus Grammar.
  */
-class CVC4_EXPORT Grammar
+class CVC5_EXPORT Grammar
 {
   friend class cvc5::Command;
   friend class Solver;
@@ -2272,7 +2272,7 @@ class CVC4_EXPORT Grammar
  * @param g the grammar to be serialized to the given output stream
  * @return the output stream
  */
-std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC4_EXPORT;
+std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC5_EXPORT;
 
 /* -------------------------------------------------------------------------- */
 /* Rounding Mode for Floating-Points                                          */
@@ -2292,7 +2292,7 @@ std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC4_EXPORT;
  * Standard 754.
  * \endverbatim
  */
-enum CVC4_EXPORT RoundingMode
+enum CVC5_EXPORT RoundingMode
 {
   /**
    * Round to the nearest even number.
@@ -2331,7 +2331,7 @@ enum CVC4_EXPORT RoundingMode
 /**
  * Hash function for RoundingModes.
  */
-struct CVC4_EXPORT RoundingModeHashFunction
+struct CVC5_EXPORT RoundingModeHashFunction
 {
   inline size_t operator()(const RoundingMode& rm) const;
 };
@@ -2347,7 +2347,7 @@ struct CVC4_EXPORT RoundingModeHashFunction
  * The value type can be queried (using `isInt`, `isString`, etc.) and
  * the stored value can be accessed (using `getInt`, `getString`, etc.).
  */
-class CVC4_EXPORT Stat
+class CVC5_EXPORT Stat
 {
   struct StatData;
 
@@ -2392,7 +2392,7 @@ class CVC4_EXPORT Stat
   std::unique_ptr<StatData> d_data;
 };
 
-std::ostream& operator<<(std::ostream& os, const Stat& sv) CVC4_EXPORT;
+std::ostream& operator<<(std::ostream& os, const Stat& sv) CVC5_EXPORT;
 
 /**
  * Represents a snapshot of the solver statistics.
@@ -2407,7 +2407,7 @@ std::ostream& operator<<(std::ostream& os, const Stat& sv) CVC4_EXPORT;
  * statistics that are expert, unchanged, or both, can be included as well.
  * A single statistic value is represented as `Stat`.
  */
-class CVC4_EXPORT Statistics
+class CVC5_EXPORT Statistics
 {
  public:
   friend Solver;
@@ -2458,7 +2458,8 @@ class CVC4_EXPORT Statistics
   /** Internal data */
   BaseType d_stats;
 };
-std::ostream& operator<<(std::ostream& out, const Statistics& stats) CVC4_EXPORT;
+std::ostream& operator<<(std::ostream& out,
+                         const Statistics& stats) CVC5_EXPORT;
 
 /* -------------------------------------------------------------------------- */
 /* Solver                                                                     */
@@ -2467,7 +2468,7 @@ std::ostream& operator<<(std::ostream& out, const Statistics& stats) CVC4_EXPORT
 /**
  * A cvc5 solver.
  */
-class CVC4_EXPORT Solver
+class CVC5_EXPORT Solver
 {
   friend class Datatype;
   friend class DatatypeDecl;
diff --git a/src/api/cpp/cvc5_checks.h b/src/api/cpp/cvc5_checks.h
index d332652fd..c30237ecd 100644
--- a/src/api/cpp/cvc5_checks.h
+++ b/src/api/cpp/cvc5_checks.h
@@ -20,7 +20,7 @@
 #ifndef CVC5__API__CHECKS_H
 #define CVC5__API__CHECKS_H
 
-namespace cvc4 {
+namespace cvc5 {
 namespace api {
 
 /* -------------------------------------------------------------------------- */
@@ -653,5 +653,5 @@ namespace api {
     }                                                                          \
   } while (0)
 }  // namespace api
-}  // namespace cvc4
+}  // namespace cvc5
 #endif
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 86e6d676d..7d0f7b9b7 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -13,7 +13,7 @@
  * The term kinds of the cvc5 C++ API.
  */
 
-#include "cvc4_export.h"
+#include "cvc5_export.h"
 
 #ifndef CVC5__API__CVC5_KIND_H
 #define CVC5__API__CVC5_KIND_H
@@ -35,7 +35,7 @@ namespace api {
  * checks for validity). The size of this type depends on the size of
  * cvc5::Kind (NodeValue::NBITS_KIND, currently 10 bits, see expr/node_value.h).
  */
-enum CVC4_EXPORT Kind : int32_t
+enum CVC5_EXPORT Kind : int32_t
 {
   /**
    * Internal kind.
@@ -185,9 +185,9 @@ enum CVC4_EXPORT Kind : int32_t
    * (e.g. for arithmetic terms in non-linear queries). However, it is not
    * supported by the parser. Moreover, the user of the API should be cautious
    * when using this operator. In general, all witness terms
-   * `(witness ((x Int)) F)` should be such that `(exists ((x Int)) F)` is a valid
-   * formula. If this is not the case, then the semantics in formulas that use
-   * witness terms may be unintuitive. For example, the following formula is
+   * `(witness ((x Int)) F)` should be such that `(exists ((x Int)) F)` is a
+   * valid formula. If this is not the case, then the semantics in formulas that
+   * use witness terms may be unintuitive. For example, the following formula is
    * unsatisfiable:
    * `(or (= (witness ((x Int)) false) 0) (not (= (witness ((x Int)) false) 0))`
    * whereas notice that `(or (= z 0) (not (= z 0)))` is true for any `z`.
@@ -393,7 +393,7 @@ enum CVC4_EXPORT Kind : int32_t
    *   - `Solver::mkOp(Kind kind, uint32_t param) const`
    *
    * Apply integer conversion to bit-vector.
-   
+
    * Parameters:
    *   - 1: Op of kind IAND
    *   - 2: Integer term
@@ -2341,11 +2341,12 @@ enum CVC4_EXPORT Kind : int32_t
    * a predicate P[x1...xn], and a term t[x1...xn]. A comprehension C with the
    * above form has members given by the following semantics:
    * @f[
-   *  \forall y. ( \exists x_1...x_n. P[x_1...x_n] \hat{} t[x_1...x_n] = y ) \Leftrightarrow (member y C)
+   *  \forall y. ( \exists x_1...x_n. P[x_1...x_n] \hat{} t[x_1...x_n] = y )
+   * \Leftrightarrow (member y C)
    * @f]
    * where y ranges over the element type of the (set) type of the
-   * comprehension. If @f$ t[x_1..x_n] @f$ is not provided, it is equivalent to y in the
-   * above formula.
+   * comprehension. If @f$ t[x_1..x_n] @f$ is not provided, it is equivalent to
+   * y in the above formula.
    *
    * Parameters:
    *   - 1: Term BOUND_VAR_LIST
@@ -3430,7 +3431,7 @@ enum CVC4_EXPORT Kind : int32_t
  * @param k the kind
  * @return the string representation of kind k
  */
-std::string kindToString(Kind k) CVC4_EXPORT;
+std::string kindToString(Kind k) CVC5_EXPORT;
 
 /**
  * Serialize a kind to given stream.
@@ -3438,12 +3439,12 @@ std::string kindToString(Kind k) CVC4_EXPORT;
  * @param k the kind to be serialized to the given output stream
  * @return the output stream
  */
-std::ostream& operator<<(std::ostream& out, Kind k) CVC4_EXPORT;
+std::ostream& operator<<(std::ostream& out, Kind k) CVC5_EXPORT;
 
 /**
  * Hash function for Kinds.
  */
-struct CVC4_EXPORT KindHashFunction
+struct CVC5_EXPORT KindHashFunction
 {
   /**
    * Hashes a Kind to a size_t.
diff --git a/src/api/parsekinds.py b/src/api/parsekinds.py
index cb1586995..30f182b02 100644
--- a/src/api/parsekinds.py
+++ b/src/api/parsekinds.py
@@ -34,7 +34,7 @@ US = '_'
 NL = '\n'
 
 # Enum Declarations
-ENUM_START = 'enum CVC4_EXPORT Kind'
+ENUM_START = 'enum CVC5_EXPORT Kind'
 ENUM_END = CCB + SC
 
 # Comments and Macro Tokens
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})