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

3 files changed, 74 insertions, 2 deletions

diff --git a/docs/cpp.rst b/docs/cpp.rst
new file mode 100644
index 000000000..eeeae257e
--- /dev/null
+++ b/docs/cpp.rst
@@ -0,0 +1,72 @@
+C++ API Documentation
+=====================
+
+Class Hierarchy
+---------------
+
+* namespace ``cvc5``
+
+  * namespace ``api``
+
+    * class :cpp:class:`cvc5::api::CVC5ApiException`
+
+    * class :cpp:class:`cvc5::api::CVC5ApiRecoverableException`
+
+    * class :doc:`cpp/datatype`
+
+      * class :ref:`Datatype::const_iterator<datatype>`
+
+    * class :doc:`cpp/datatypeconstructor`
+
+      * class :ref:`DatatypeConstructor::const_iterator<datatypeconstructor>`
+
+    * class :doc:`cpp/datatypeconstructordecl`
+
+    * class :doc:`cpp/datatypedecl`
+
+    * class :doc:`cpp/datatypeselector`
+
+    * class :doc:`cpp/grammar`
+
+    * class :doc:`cpp/op`
+
+    * class :doc:`cpp/result`
+
+    * class :doc:`cpp/solver`
+
+    * class :doc:`cpp/term`
+
+      * class :ref:`Term::const_iterator<term>`
+
+    * enum :doc:`cpp/kind`
+
+    * enum :doc:`cpp/roundingmode`
+
+    * struct :ref:`KindHashFunction<kind>`
+
+    * struct :ref:`OpHashFunction<op>`
+
+    * struct :ref:`SortHashFunction<sort>`
+
+
+
+Full API Documentation
+----------------------
+
+.. toctree::
+   :maxdepth: 2
+
+   cpp/datatype
+   cpp/datatypeconstructor
+   cpp/datatypeconstructordecl
+   cpp/datatypedecl
+   cpp/datatypeselector
+   cpp/exceptions
+   cpp/grammar
+   cpp/kind
+   cpp/op
+   cpp/result
+   cpp/roundingmode
+   cpp/solver
+   cpp/sort
+   cpp/term
diff --git a/docs/cpp/Doxyfile.in b/docs/cpp/Doxyfile.in
index 400b3dd0d..75a732ceb 100644
--- a/docs/cpp/Doxyfile.in
+++ b/docs/cpp/Doxyfile.in
@@ -2216,7 +2216,7 @@ INCLUDE_FILE_PATTERNS  =
 # recursively expanded use the := operator instead of the = operator.
 # This tag requires that the tag ENABLE_PREPROCESSING is set to YES.
 
-PREDEFINED             = DOXYGEN_SKIP CVC4_EXPORT=
+PREDEFINED             = DOXYGEN_SKIP CVC5_EXPORT=
 
 # If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then this
 # tag can be used to specify a list of macro names that should be expanded. The
diff --git a/docs/cpp/exceptions.rst b/docs/cpp/exceptions.rst
index 414f27a78..5fa65e5e5 100644
--- a/docs/cpp/exceptions.rst
+++ b/docs/cpp/exceptions.rst
@@ -1,7 +1,7 @@
 Exceptions
 ==========
 
-The CVC5 API communicates certain errors using exceptions. We broadly
+The cvc5 API communicates certain errors using exceptions. We broadly
 distinguish two types of exceptions: :cpp:class:`CVC5ApiException
 <cvc5::api::CVC5ApiException>` and :cpp:class:`CVC5ApiRecoverableException
 <cvc5::api::CVC5ApiRecoverableException>` (which is derived from