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

2 files changed, 25 insertions, 23 deletions

diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py
index b4a19afa8..74eda63bc 100644
--- a/test/python/unit/api/test_solver.py
+++ b/test/python/unit/api/test_solver.py
@@ -12,14 +12,14 @@
 ##
 
 import pytest
-import pycvc4
+import pycvc5
 import sys
 
-from pycvc4 import kinds
+from pycvc5 import kinds
 
 @pytest.fixture
 def solver():
-    return pycvc4.Solver()
+    return pycvc5.Solver()
 
 def test_recoverable_exception(solver):
     solver.setOption("produce-models", "true")
@@ -31,9 +31,9 @@ def test_recoverable_exception(solver):
 def test_supports_floating_point(solver):
     if solver.supportsFloatingPoint():
       try:
-          solver.mkRoundingMode(pycvc4.RoundNearestTiesToEven)
+          solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
       except RuntimeError:
           pytest.fail()
     else:
         with pytest.raises(RuntimeError):
-          solver.mkRoundingMode(pycvc4.RoundNearestTiesToEven)
+          solver.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
diff --git a/test/python/unit/api/test_sort.py b/test/python/unit/api/test_sort.py
index b4aa3a11f..5e86382ee 100644
--- a/test/python/unit/api/test_sort.py
+++ b/test/python/unit/api/test_sort.py
@@ -1,27 +1,29 @@
-#####################
-## test_sort.py
-## Top contributors (to current version):
-##   Yoni Zohar
-## This file is part of the CVC4 project.
-## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
-## in the top-level source directory and their institutional affiliations.
-## All rights reserved.  See the file COPYING in the top-level source
-## directory for licensing information.
+###############################################################################
+# Top contributors (to current version):
+#   Yoni Zohar, Makai Mann
+#
+# This file is part of the cvc5 project.
+#
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+# #############################################################################
+#
+# Unit tests for sort API.
+#
+# Obtained by translating test/unit/api/sort_black.cpp
 ##
-## ########################################################
-##
-## Unit tests for sort API.
-## Obtained by translating test/unit/api/sort_black.cpp
 
 import pytest
-import pycvc4
-from pycvc4 import kinds
-from pycvc4 import Sort
+import pycvc5
+from pycvc5 import kinds
+from pycvc5 import Sort
 
 
 @pytest.fixture
 def solver():
-    return pycvc4.Solver()
+    return pycvc5.Solver()
 
 
 def create_datatype_sort(solver):
@@ -561,6 +563,6 @@ def test_sort_scoped_tostring(solver):
     uninterp_sort = solver.mkUninterpretedSort(name)
     assert str(bvsort8) == "(_ BitVec 8)"
     assert str(uninterp_sort) == name
-    solver2 = pycvc4.Solver()
+    solver2 = pycvc5.Solver()
     assert str(bvsort8) == "(_ BitVec 8)"
     assert str(uninterp_sort) == name