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

9 files changed, 50 insertions, 51 deletions

diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt
index 48318012f..b340ec8ba 100644
--- a/test/api/CMakeLists.txt
+++ b/test/api/CMakeLists.txt
@@ -29,10 +29,9 @@ add_custom_target(apitests
   COMMAND ctest --output-on-failure -L "api" -j${CTEST_NTHREADS} $$ARGS
   DEPENDS build-apitests)
 
-set(CVC5_API_TEST_FLAGS
-  -D__BUILDING_CVC5_API_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
+set(CVC5_API_TEST_FLAGS -D__BUILDING_CVC5_API_TEST)
 
-macro(cvc4_add_api_test name)
+macro(cvc5_add_api_test name)
   set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/api/)
   add_executable(${name} ${name}.cpp)
   target_link_libraries(${name} PUBLIC main-test)
@@ -44,14 +43,14 @@ macro(cvc4_add_api_test name)
   add_dependencies(build-apitests ${name})
 endmacro()
 
-cvc4_add_api_test(boilerplate)
-cvc4_add_api_test(ouroborous)
-cvc4_add_api_test(reset_assertions)
-cvc4_add_api_test(sep_log_api)
-cvc4_add_api_test(smt2_compliance)
-cvc4_add_api_test(two_solvers)
-cvc4_add_api_test(issue5074)
-cvc4_add_api_test(issue4889)
+cvc5_add_api_test(boilerplate)
+cvc5_add_api_test(ouroborous)
+cvc5_add_api_test(reset_assertions)
+cvc5_add_api_test(sep_log_api)
+cvc5_add_api_test(smt2_compliance)
+cvc5_add_api_test(two_solvers)
+cvc5_add_api_test(issue5074)
+cvc5_add_api_test(issue4889)
 
 # if we've built using libedit, then we want the interactive shell tests
 if (USE_EDITLINE)
diff --git a/test/api/boilerplate.cpp b/test/api/boilerplate.cpp
index 74714a753..0f561e7cf 100644
--- a/test/api/boilerplate.cpp
+++ b/test/api/boilerplate.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * A simple start-up/tear-down test for CVC4.
+ * A simple start-up/tear-down test for cvc5.
  *
  * This simple test just makes sure that the public interface is
  * minimally functional.  It is useful as a template to use for other
diff --git a/test/api/interactive_shell.py b/test/api/interactive_shell.py
index 3c8a1d5a8..c09f5f08b 100644
--- a/test/api/interactive_shell.py
+++ b/test/api/interactive_shell.py
@@ -24,7 +24,7 @@ def check_iteractive_shell():
     """
 
     # Open cvc5
-    child = pexpect.spawnu("bin/cvc4", timeout=1)
+    child = pexpect.spawnu("bin/cvc5", timeout=1)
 
     # We expect to see the cvc5 prompt
     child.expect("cvc5>")
diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt
index d6d14b310..246755492 100644
--- a/test/api/python/CMakeLists.txt
+++ b/test/api/python/CMakeLists.txt
@@ -27,7 +27,7 @@ if(RET_PYTEST)
       "Could not find Python module pytest. Install via `pip install pytest'.")
 endif()
 
-macro(cvc4_add_python_api_test name filename)
+macro(cvc5_add_python_api_test name filename)
 
   #   we create test target 'api/<output_dir>/myapitest'
   #   and run it with 'ctest -R "api/<output_dir>/myapitest"'.
@@ -38,7 +38,7 @@ macro(cvc4_add_python_api_test name filename)
 
 endmacro()
 
-cvc4_add_python_api_test(pytest_datatype_api test_datatype_api.py)
-cvc4_add_python_api_test(pytest_grammar test_grammar.py)
-cvc4_add_python_api_test(pytest_term test_term.py)
-cvc4_add_python_api_test(pytest_to_python_obj test_to_python_obj.py)
+cvc5_add_python_api_test(pytest_datatype_api test_datatype_api.py)
+cvc5_add_python_api_test(pytest_grammar test_grammar.py)
+cvc5_add_python_api_test(pytest_term test_term.py)
+cvc5_add_python_api_test(pytest_to_python_obj test_to_python_obj.py)
diff --git a/test/api/python/test_datatype_api.py b/test/api/python/test_datatype_api.py
index 81c5478e8..06f4e0f3d 100644
--- a/test/api/python/test_datatype_api.py
+++ b/test/api/python/test_datatype_api.py
@@ -13,12 +13,12 @@
 
 import pytest
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 
 def test_datatype_simply_rec():
-    solver = pycvc4.Solver()
+    solver = pycvc5.Solver()
 
     # Create mutual datatypes corresponding to this definition block:
     #
diff --git a/test/api/python/test_grammar.py b/test/api/python/test_grammar.py
index 30f01b59f..f83bee548 100644
--- a/test/api/python/test_grammar.py
+++ b/test/api/python/test_grammar.py
@@ -15,15 +15,15 @@
 
 import pytest
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 def test_add_rule():
-  solver = pycvc4.Solver()
+  solver = pycvc5.Solver()
   boolean = solver.getBooleanSort()
   integer = solver.getIntegerSort()
 
-  nullTerm = pycvc4.Term(solver)
+  nullTerm = pycvc5.Term(solver)
   start = solver.mkVar(boolean)
   nts = solver.mkVar(boolean)
 
@@ -50,11 +50,11 @@ def test_add_rule():
     g.addRule(start, solver.mkBoolean(false))
 
 def test_add_rules():
-  solver = pycvc4.Solver()
+  solver = pycvc5.Solver()
   boolean = solver.getBooleanSort()
   integer = solver.getIntegerSort()
 
-  nullTerm = pycvc4.Term(solver)
+  nullTerm = pycvc5.Term(solver)
   start = solver.mkVar(boolean)
   nts = solver.mkVar(boolean)
 
@@ -79,10 +79,10 @@ def test_add_rules():
     g.addRules(start, solver.mkBoolean(False))
 
 def testAddAnyConstant():
-  solver = pycvc4.Solver()
+  solver = pycvc5.Solver()
   boolean = solver.getBooleanSort()
 
-  nullTerm = pycvc4.Term(solver)
+  nullTerm = pycvc5.Term(solver)
   start = solver.mkVar(boolean)
   nts = solver.mkVar(boolean)
 
@@ -103,10 +103,10 @@ def testAddAnyConstant():
 
 
 def testAddAnyVariable():
-  solver = pycvc4.Solver()
+  solver = pycvc5.Solver()
   boolean = solver.getBooleanSort()
 
-  nullTerm = pycvc4.Term(solver)
+  nullTerm = pycvc5.Term(solver)
   x = solver.mkVar(boolean)
   start = solver.mkVar(boolean)
   nts = solver.mkVar(boolean)
diff --git a/test/api/python/test_term.py b/test/api/python/test_term.py
index e47caaf5c..c0625095b 100644
--- a/test/api/python/test_term.py
+++ b/test/api/python/test_term.py
@@ -13,12 +13,12 @@
 
 import pytest
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 
 def test_getitem():
-    solver = pycvc4.Solver()
+    solver = pycvc5.Solver()
     intsort = solver.getIntegerSort()
     x = solver.mkConst(intsort, 'x')
     y = solver.mkConst(intsort, 'y')
@@ -29,7 +29,7 @@ def test_getitem():
 
 
 def test_get_kind():
-    solver = pycvc4.Solver()
+    solver = pycvc5.Solver()
     intsort = solver.getIntegerSort()
     x = solver.mkConst(intsort, 'x')
     y = solver.mkConst(intsort, 'y')
@@ -52,7 +52,7 @@ def test_get_kind():
 
 
 def test_eq():
-    solver = pycvc4.Solver()
+    solver = pycvc5.Solver()
     usort = solver.mkUninterpretedSort('u')
     x = solver.mkConst(usort, 'x')
     y = solver.mkConst(usort, 'y')
@@ -66,7 +66,7 @@ def test_eq():
 
 
 def test_get_sort():
-    solver = pycvc4.Solver()
+    solver = pycvc5.Solver()
     intsort = solver.getIntegerSort()
     bvsort8 = solver.mkBitVectorSort(8)
 
@@ -83,7 +83,7 @@ def test_get_sort():
     assert solver.mkTerm(kinds.BVConcat, a, b).getSort() == solver.mkBitVectorSort(16)
 
 def test_get_op():
-    solver = pycvc4.Solver()
+    solver = pycvc5.Solver()
     intsort = solver.getIntegerSort()
     funsort = solver.mkFunctionSort(intsort, intsort)
 
@@ -107,7 +107,7 @@ def test_get_op():
 
 
 def test_const_sequence_elements():
-    solver = pycvc4.Solver()
+    solver = pycvc5.Solver()
     realsort = solver.getRealSort()
     seqsort = solver.mkSequenceSort(realsort)
     s = solver.mkEmptySequence(seqsort)
diff --git a/test/api/python/test_to_python_obj.py b/test/api/python/test_to_python_obj.py
index 5d55201de..d8094f801 100644
--- a/test/api/python/test_to_python_obj.py
+++ b/test/api/python/test_to_python_obj.py
@@ -14,12 +14,12 @@
 from fractions import Fraction
 import pytest
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 
 def testGetBool():
-    solver = pycvc4.Solver()
+    solver = pycvc5.Solver()
     t = solver.mkTrue()
     f = solver.mkFalse()
     assert t.toPythonObj() == True
@@ -27,13 +27,13 @@ def testGetBool():
 
 
 def testGetInt():
-    solver = pycvc4.Solver()
+    solver = pycvc5.Solver()
     two = solver.mkInteger(2)
     assert two.toPythonObj() == 2
 
 
 def testGetReal():
-    solver = pycvc4.Solver()
+    solver = pycvc5.Solver()
     half = solver.mkReal("1/2")
     assert half.toPythonObj() == Fraction(1, 2)
 
@@ -45,13 +45,13 @@ def testGetReal():
 
 
 def testGetBV():
-    solver = pycvc4.Solver()
+    solver = pycvc5.Solver()
     three = solver.mkBitVector(8, 3)
     assert three.toPythonObj() == 3
 
 
 def testGetArray():
-    solver = pycvc4.Solver()
+    solver = pycvc5.Solver()
     arrsort = solver.mkArraySort(solver.getRealSort(), solver.getRealSort())
     zero_array = solver.mkConstArray(arrsort, solver.mkInteger(0))
     stores = solver.mkTerm(kinds.Store, zero_array, solver.mkInteger(1), solver.mkInteger(2))
@@ -68,17 +68,17 @@ def testGetArray():
 
 
 def testGetSymbol():
-    solver = pycvc4.Solver()
+    solver = pycvc5.Solver()
     solver.mkConst(solver.getBooleanSort(), "x")
 
 
 def testGetString():
-    solver = pycvc4.Solver()
+    solver = pycvc5.Solver()
 
     s1 = '"test\n"😃\\u{a}'
     t1 = solver.mkString(s1)
     assert s1 == t1.toPythonObj()
 
-    s2 = '❤️CVC4❤️'
+    s2 = '❤️cvc5❤️'
     t2 = solver.mkString(s2)
     assert s2 == t2.toPythonObj()
diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp
index c01d16bfc..04d4ce41d 100644
--- a/test/api/sep_log_api.cpp
+++ b/test/api/sep_log_api.cpp
@@ -37,7 +37,7 @@ int validate_exception(void)
   Solver slv;
 
   /*
-   * Setup some options for CVC4 -- we explictly want to use a simplistic
+   * Setup some options for cvc5 -- we explictly want to use a simplistic
    * theory (e.g., QF_IDL)
    */
   slv.setLogic("QF_IDL");
@@ -129,7 +129,7 @@ int validate_getters(void)
 {
   Solver slv;
 
-  /* Setup some options for CVC4 */
+  /* Setup some options for cvc5 */
   slv.setLogic("QF_ALL_SUPPORTED");
   slv.setOption("produce-models", "true");
   slv.setOption("incremental", "false");