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

15 files changed, 42 insertions, 58 deletions

diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index e495fd4d6..79a44f426 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -20,7 +20,7 @@ configure_file(rational.h.in rational.h)
 configure_file(integer.h.in integer.h)
 configure_file(real_algebraic_number.h.in real_algebraic_number.h)
 
-libcvc4_add_sources(
+libcvc5_add_sources(
   abstract_value.cpp
   abstract_value.h
   bin_heap.h
@@ -84,13 +84,13 @@ libcvc4_add_sources(
 )
 
 if(CVC5_USE_CLN_IMP)
-  libcvc4_add_sources(rational_cln_imp.cpp integer_cln_imp.cpp)
+  libcvc5_add_sources(rational_cln_imp.cpp integer_cln_imp.cpp)
 endif()
 
 if(CVC5_USE_GMP_IMP)
-  libcvc4_add_sources(rational_gmp_imp.cpp integer_gmp_imp.cpp)
+  libcvc5_add_sources(rational_gmp_imp.cpp integer_gmp_imp.cpp)
 endif()
 
 if(CVC5_USE_POLY_IMP)
-  libcvc4_add_sources(real_algebraic_number_poly_imp.cpp real_algebraic_number_poly_imp.h)
+  libcvc5_add_sources(real_algebraic_number_poly_imp.cpp real_algebraic_number_poly_imp.h)
 endif()
diff --git a/src/util/integer.h.in b/src/util/integer.h.in
index cfcef4ae2..3fb53a835 100644
--- a/src/util/integer.h.in
+++ b/src/util/integer.h.in
@@ -13,7 +13,7 @@
  * A multi-precision integer constant.
  */
 
-// these gestures are used to avoid a public header dependence on cvc4autoconfig.h
+// these gestures are used to avoid a public header dependence on base/cvc5config.h
 
 #if @CVC5_NEED_INT64_T_OVERLOADS@
 #  define CVC5_NEED_INT64_T_OVERLOADS
@@ -28,14 +28,8 @@
 
 #ifdef CVC5_CLN_IMP
 #  include "util/integer_cln_imp.h"
-#  if SWIG
-     %include "util/integer_cln_imp.h"
-#  endif /* SWIG */
 #endif /* CVC5_CLN_IMP */
 
 #ifdef CVC5_GMP_IMP
 #  include "util/integer_gmp_imp.h"
-#  if SWIG
-     %include "util/integer_gmp_imp.h"
-#  endif /* SWIG */
 #endif /* CVC5_GMP_IMP */
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index f54630d23..a9e4f6f0a 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -15,7 +15,7 @@
 #include <sstream>
 #include <string>
 
-#include "cvc4autoconfig.h"
+#include "base/cvc5config.h"
 #include "util/integer.h"
 
 #ifndef CVC5_CLN_IMP
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 303567dc6..80bc406ee 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -29,13 +29,13 @@
 #include <string>
 
 #include "base/exception.h"
-#include "cvc4_export.h"  // remove when Cvc language support is removed
+#include "cvc5_export.h"  // remove when Cvc language support is removed
 
 namespace cvc5 {
 
 class Rational;
 
-class CVC4_EXPORT Integer
+class CVC5_EXPORT Integer
 {
   friend class cvc5::Rational;
 
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index 52e408a37..f33a90408 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -13,15 +13,13 @@
  * A multi-precision rational constant.
  */
 
-#include "util/integer.h"
-
 #include <cmath>
 #include <sstream>
 #include <string>
 
-#include "cvc4autoconfig.h"
-
 #include "base/check.h"
+#include "base/cvc5config.h"
+#include "util/integer.h"
 #include "util/rational.h"
 
 #ifndef CVC5_GMP_IMP
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index f2d568d13..ff2ea9815 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -23,13 +23,13 @@
 #include <iosfwd>
 #include <string>
 
-#include "cvc4_export.h"  // remove when Cvc language support is removed
+#include "cvc5_export.h"  // remove when Cvc language support is removed
 
 namespace cvc5 {
 
 class Rational;
 
-class CVC4_EXPORT Integer
+class CVC5_EXPORT Integer
 {
   friend class cvc5::Rational;
 
diff --git a/src/util/rational.h.in b/src/util/rational.h.in
index c8b673d7e..981fceab2 100644
--- a/src/util/rational.h.in
+++ b/src/util/rational.h.in
@@ -13,7 +13,7 @@
  * A multi-precision rational constant.
  */
 
-// these gestures are used to avoid a public header dependence on cvc4autoconfig.h
+// these gestures are used to avoid a public header dependence on base/cvc5config.h
 
 #if @CVC5_NEED_INT64_T_OVERLOADS@
 #  define CVC5_NEED_INT64_T_OVERLOADS
@@ -28,14 +28,8 @@
 
 #ifdef CVC5_CLN_IMP
 #  include "util/rational_cln_imp.h"
-#  if SWIG
-     %include "util/rational_cln_imp.h"
-#  endif /* SWIG */
 #endif /* CVC5_CLN_IMP */
 
 #ifdef CVC5_GMP_IMP
 #  include "util/rational_gmp_imp.h"
-#  if SWIG
-     %include "util/rational_gmp_imp.h"
-#  endif /* SWIG */
 #endif /* CVC5_GMP_IMP */
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index 93816bd20..728b2d97e 100644
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -12,12 +12,11 @@
  *
  * A multi-precision rational constant.
  */
-#include "util/rational.h"
-
 #include <sstream>
 #include <string>
 
-#include "cvc4autoconfig.h"
+#include "base/cvc5config.h"
+#include "util/rational.h"
 
 #ifndef CVC5_CLN_IMP
 #error "This source should only ever be built if CVC5_CLN_IMP is on !"
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 9745bbdad..67e73f7e9 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -31,7 +31,7 @@
 #include <string>
 
 #include "base/exception.h"
-#include "cvc4_export.h"  // remove when Cvc language support is removed
+#include "cvc5_export.h"  // remove when Cvc language support is removed
 #include "util/integer.h"
 #include "util/maybe.h"
 
@@ -52,7 +52,7 @@ namespace cvc5 {
  * in danger of invoking the char* constructor, from whence you will segfault.
  */
 
-class CVC4_EXPORT Rational
+class CVC5_EXPORT Rational
 {
  public:
   /**
@@ -337,7 +337,7 @@ struct RationalHashFunction
   inline size_t operator()(const cvc5::Rational& r) const { return r.hash(); }
 }; /* struct RationalHashFunction */
 
-std::ostream& operator<<(std::ostream& os, const Rational& n) CVC4_EXPORT;
+std::ostream& operator<<(std::ostream& os, const Rational& n) CVC5_EXPORT;
 
 }  // namespace cvc5
 
diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
index 24e6e96d7..0997b8b09 100644
--- a/src/util/rational_gmp_imp.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -12,15 +12,14 @@
  *
  * A multi-precision rational constant.
  */
-#include "util/rational.h"
-
 #include <cmath>
 #include <sstream>
 #include <string>
 
-#include "cvc4autoconfig.h"
+#include "base/cvc5config.h"
+#include "util/rational.h"
 
-#ifndef CVC5_GMP_IMP  // Make sure this comes after cvc4autoconfig.h
+#ifndef CVC5_GMP_IMP  // Make sure this comes after base/cvc5config.h
 #error "This source should only ever be built if CVC5_GMP_IMP is on !"
 #endif /* CVC5_GMP_IMP */
 
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index 0961adc73..fd7492a87 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -22,7 +22,7 @@
 
 #include <string>
 
-#include "cvc4_export.h"  // remove when Cvc language support is removed
+#include "cvc5_export.h"  // remove when Cvc language support is removed
 #include "util/gmp_util.h"
 #include "util/integer.h"
 #include "util/maybe.h"
@@ -44,7 +44,7 @@ namespace cvc5 {
  * in danger of invoking the char* constructor, from whence you will segfault.
  */
 
-class CVC4_EXPORT Rational
+class CVC5_EXPORT Rational
 {
  public:
   /**
@@ -327,7 +327,7 @@ struct RationalHashFunction
   inline size_t operator()(const cvc5::Rational& r) const { return r.hash(); }
 }; /* struct RationalHashFunction */
 
-std::ostream& operator<<(std::ostream& os, const Rational& n) CVC4_EXPORT;
+std::ostream& operator<<(std::ostream& os, const Rational& n) CVC5_EXPORT;
 
 }  // namespace cvc5
 
diff --git a/src/util/real_algebraic_number.h.in b/src/util/real_algebraic_number.h.in
index 8eb8b35fb..077c260f6 100644
--- a/src/util/real_algebraic_number.h.in
+++ b/src/util/real_algebraic_number.h.in
@@ -13,7 +13,7 @@
  * A real algebraic number constant.
  */
 
-// these gestures are used to avoid a public header dependence on cvc4autoconfig.h
+// these gestures are used to avoid a public header dependence on base/cvc5config.h
 
 #if /* use libpoly */ @CVC5_USE_POLY_IMP@
 #  define CVC5_POLY_IMP
diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp
index 736970129..58af26193 100644
--- a/src/util/real_algebraic_number_poly_imp.cpp
+++ b/src/util/real_algebraic_number_poly_imp.cpp
@@ -13,10 +13,10 @@
  * Implementation of RealAlgebraicNumber based on libpoly.
  */
 
-#include "cvc4autoconfig.h"
+#include "base/cvc5config.h"
 #include "util/real_algebraic_number.h"
 
-#ifndef CVC5_POLY_IMP  // Make sure this comes after cvc4autoconfig.h
+#ifndef CVC5_POLY_IMP  // Make sure this comes after base/cvc5config.h
 #error "This source should only ever be built if CVC5_POLY_IMP is on!"
 #endif /* CVC5_POLY_IMP */
 
diff --git a/src/util/safe_print.h b/src/util/safe_print.h
index ba0704d9c..e3280bb55 100644
--- a/src/util/safe_print.h
+++ b/src/util/safe_print.h
@@ -43,7 +43,7 @@
 #include <cstring>
 #include <string>
 
-#include "cvc4_export.h"
+#include "cvc5_export.h"
 
 namespace cvc5 {
 
@@ -52,7 +52,7 @@ namespace cvc5 {
  * signal handler.
  */
 template <size_t N>
-void CVC4_EXPORT safe_print(int fd, const char (&msg)[N])
+void CVC5_EXPORT safe_print(int fd, const char (&msg)[N])
 {
   ssize_t nb = N - 1;
   if (write(fd, msg, nb) != nb) {
@@ -96,7 +96,7 @@ auto toStringImpl(const T& obj, int) -> decltype(toString(obj))
  * @param obj The object to print
  */
 template <typename T>
-void CVC4_EXPORT safe_print(int fd, const T& obj)
+void CVC5_EXPORT safe_print(int fd, const T& obj)
 {
   const char* s =
       toStringImpl(obj, /* prefer the method that uses `toString()` */ 0);
@@ -108,25 +108,25 @@ void CVC4_EXPORT safe_print(int fd, const T& obj)
 }
 
 template <>
-void CVC4_EXPORT safe_print(int fd, const std::string& msg);
+void CVC5_EXPORT safe_print(int fd, const std::string& msg);
 template <>
-void CVC4_EXPORT safe_print(int fd, const int64_t& _i);
+void CVC5_EXPORT safe_print(int fd, const int64_t& _i);
 template <>
-void CVC4_EXPORT safe_print(int fd, const int32_t& i);
+void CVC5_EXPORT safe_print(int fd, const int32_t& i);
 template <>
-void CVC4_EXPORT safe_print(int fd, const uint64_t& _i);
+void CVC5_EXPORT safe_print(int fd, const uint64_t& _i);
 template <>
-void CVC4_EXPORT safe_print(int fd, const uint32_t& i);
+void CVC5_EXPORT safe_print(int fd, const uint32_t& i);
 template <>
-void CVC4_EXPORT safe_print(int fd, const double& _d);
+void CVC5_EXPORT safe_print(int fd, const double& _d);
 template <>
-void CVC4_EXPORT safe_print(int fd, const float& f);
+void CVC5_EXPORT safe_print(int fd, const float& f);
 template <>
-void CVC4_EXPORT safe_print(int fd, const bool& b);
+void CVC5_EXPORT safe_print(int fd, const bool& b);
 template <>
-void CVC4_EXPORT safe_print(int fd, void* const& addr);
+void CVC5_EXPORT safe_print(int fd, void* const& addr);
 template <>
-void CVC4_EXPORT safe_print(int fd, const timespec& t);
+void CVC5_EXPORT safe_print(int fd, const timespec& t);
 
 /** Prints an integer in hexadecimal. Safe to use in a signal handler. */
 void safe_print_hex(int fd, uint64_t i);
diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h
index 72c67d24a..16364cba2 100644
--- a/src/util/unsafe_interrupt_exception.h
+++ b/src/util/unsafe_interrupt_exception.h
@@ -20,11 +20,11 @@
 #define CVC5__UNSAFE_INTERRUPT_EXCEPTION_H
 
 #include "base/exception.h"
-#include "cvc4_export.h"
+#include "cvc5_export.h"
 
 namespace cvc5 {
 
-class CVC4_EXPORT UnsafeInterruptException : public cvc5::Exception
+class CVC5_EXPORT UnsafeInterruptException : public cvc5::Exception
 {
  public:
   UnsafeInterruptException() :