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

17 files changed, 94 insertions, 95 deletions

diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index e99d92303..f0971db62 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -33,11 +33,10 @@ add_custom_target(units
   DEPENDS build-units)
 
 set(CVC5_UNIT_TEST_FLAGS_BLACK
-  -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
-  -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
+  -D__BUILDING_CVC5LIB_UNIT_TEST -D__BUILDING_CVC5PARSERLIB_UNIT_TEST)
 
 # Generate and add unit test.
-macro(cvc4_add_unit_test is_white name output_dir)
+macro(cvc5_add_unit_test is_white name output_dir)
   set(test_src ${CMAKE_CURRENT_LIST_DIR}/${name}.cpp)
   add_executable(${name} ${test_src})
   target_compile_definitions(${name} PRIVATE ${CVC5_UNIT_TEST_FLAGS_BLACK})
@@ -79,11 +78,11 @@ macro(cvc4_add_unit_test is_white name output_dir)
   set_tests_properties(${test_name} PROPERTIES LABELS "unit")
 endmacro()
 
-macro(cvc4_add_unit_test_black name output_dir)
-  cvc4_add_unit_test(FALSE ${name} ${output_dir})
+macro(cvc5_add_unit_test_black name output_dir)
+  cvc5_add_unit_test(FALSE ${name} ${output_dir})
 endmacro()
-macro(cvc4_add_unit_test_white name output_dir)
-  cvc4_add_unit_test(TRUE ${name} ${output_dir})
+macro(cvc5_add_unit_test_white name output_dir)
+  cvc5_add_unit_test(TRUE ${name} ${output_dir})
 endmacro()
 
 add_subdirectory(api)
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 899019b59..c01b1cfe0 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -14,13 +14,13 @@
 ##
 
 # Add unit tests.
-cvc4_add_unit_test_black(datatype_api_black api)
-cvc4_add_unit_test_black(grammar_black api)
-cvc4_add_unit_test_black(op_black api)
-cvc4_add_unit_test_white(op_white api)
-cvc4_add_unit_test_black(result_black api)
-cvc4_add_unit_test_black(solver_black api)
-cvc4_add_unit_test_white(solver_white api)
-cvc4_add_unit_test_black(sort_black api)
-cvc4_add_unit_test_black(term_black api)
-cvc4_add_unit_test_white(term_white api)
+cvc5_add_unit_test_black(datatype_api_black api)
+cvc5_add_unit_test_black(grammar_black api)
+cvc5_add_unit_test_black(op_black api)
+cvc5_add_unit_test_white(op_white api)
+cvc5_add_unit_test_black(result_black api)
+cvc5_add_unit_test_black(solver_black api)
+cvc5_add_unit_test_white(solver_white api)
+cvc5_add_unit_test_black(sort_black api)
+cvc5_add_unit_test_black(term_black api)
+cvc5_add_unit_test_white(term_white api)
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 5240d8020..c0258be9a 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1814,9 +1814,9 @@ TEST_F(TestApiBlackSolver, blockModelValues5)
 
 TEST_F(TestApiBlackSolver, setInfo)
 {
-  ASSERT_THROW(d_solver.setInfo("cvc4-lagic", "QF_BV"), CVC5ApiException);
+  ASSERT_THROW(d_solver.setInfo("cvc5-lagic", "QF_BV"), CVC5ApiException);
   ASSERT_THROW(d_solver.setInfo("cvc2-logic", "QF_BV"), CVC5ApiException);
-  ASSERT_THROW(d_solver.setInfo("cvc4-logic", "asdf"), CVC5ApiException);
+  ASSERT_THROW(d_solver.setInfo("cvc5-logic", "asdf"), CVC5ApiException);
 
   ASSERT_NO_THROW(d_solver.setInfo("source", "asdf"));
   ASSERT_NO_THROW(d_solver.setInfo("category", "asdf"));
diff --git a/test/unit/base/CMakeLists.txt b/test/unit/base/CMakeLists.txt
index 65d352c0b..89f28390e 100644
--- a/test/unit/base/CMakeLists.txt
+++ b/test/unit/base/CMakeLists.txt
@@ -14,4 +14,4 @@
 ##
 
 # Add unit tests.
-cvc4_add_unit_test_black(map_util_black base)
+cvc5_add_unit_test_black(map_util_black base)
diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt
index e5a8caf0f..565b828de 100644
--- a/test/unit/context/CMakeLists.txt
+++ b/test/unit/context/CMakeLists.txt
@@ -14,10 +14,10 @@
 ##
 
 # Add unit tests.
-cvc4_add_unit_test_black(cdlist_black context)
-cvc4_add_unit_test_black(cdhashmap_black context)
-cvc4_add_unit_test_white(cdhashmap_white context)
-cvc4_add_unit_test_black(cdo_black context)
-cvc4_add_unit_test_black(context_black context)
-cvc4_add_unit_test_black(context_mm_black context)
-cvc4_add_unit_test_white(context_white context)
+cvc5_add_unit_test_black(cdlist_black context)
+cvc5_add_unit_test_black(cdhashmap_black context)
+cvc5_add_unit_test_white(cdhashmap_white context)
+cvc5_add_unit_test_black(cdo_black context)
+cvc5_add_unit_test_black(context_black context)
+cvc5_add_unit_test_black(context_mm_black context)
+cvc5_add_unit_test_white(context_white context)
diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt
index 36c4cfb48..b15e89bbd 100644
--- a/test/unit/main/CMakeLists.txt
+++ b/test/unit/main/CMakeLists.txt
@@ -14,4 +14,4 @@
 ##
 
 # Add unit tests.
-cvc4_add_unit_test_black(interactive_shell_black main)
+cvc5_add_unit_test_black(interactive_shell_black main)
diff --git a/test/unit/memory.h b/test/unit/memory.h
index 68982077c..574488e21 100644
--- a/test/unit/memory.h
+++ b/test/unit/memory.h
@@ -19,7 +19,7 @@
  *
  * The WithLimitedMemory destructor will re-establish the previous limit.
  *
- * This class does not exist in CVC4_MEMORY_LIMITING_DISABLED is defined.
+ * This class does not exist in CVC5_MEMORY_LIMITING_DISABLED is defined.
  * This can be disabled for a variety of reasons.
  */
 
diff --git a/test/unit/node/CMakeLists.txt b/test/unit/node/CMakeLists.txt
index 5f4c3458c..c42e0452a 100644
--- a/test/unit/node/CMakeLists.txt
+++ b/test/unit/node/CMakeLists.txt
@@ -14,18 +14,18 @@
 ##
 
 # Add unit tests.
-cvc4_add_unit_test_black(attribute_black expr)
-cvc4_add_unit_test_white(attribute_white expr)
-cvc4_add_unit_test_black(kind_black expr)
-cvc4_add_unit_test_black(kind_map_black expr)
-cvc4_add_unit_test_black(node_black expr)
-cvc4_add_unit_test_black(node_algorithm_black expr)
-cvc4_add_unit_test_black(node_builder_black expr)
-cvc4_add_unit_test_black(node_manager_black expr)
-cvc4_add_unit_test_white(node_manager_white expr)
-cvc4_add_unit_test_black(node_self_iterator_black expr)
-cvc4_add_unit_test_black(node_traversal_black expr)
-cvc4_add_unit_test_white(node_white expr)
-cvc4_add_unit_test_black(symbol_table_black expr)
-cvc4_add_unit_test_black(type_cardinality_black expr)
-cvc4_add_unit_test_white(type_node_white expr)
+cvc5_add_unit_test_black(attribute_black expr)
+cvc5_add_unit_test_white(attribute_white expr)
+cvc5_add_unit_test_black(kind_black expr)
+cvc5_add_unit_test_black(kind_map_black expr)
+cvc5_add_unit_test_black(node_black expr)
+cvc5_add_unit_test_black(node_algorithm_black expr)
+cvc5_add_unit_test_black(node_builder_black expr)
+cvc5_add_unit_test_black(node_manager_black expr)
+cvc5_add_unit_test_white(node_manager_white expr)
+cvc5_add_unit_test_black(node_self_iterator_black expr)
+cvc5_add_unit_test_black(node_traversal_black expr)
+cvc5_add_unit_test_white(node_white expr)
+cvc5_add_unit_test_black(symbol_table_black expr)
+cvc5_add_unit_test_black(type_cardinality_black expr)
+cvc5_add_unit_test_white(type_node_white expr)
diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt
index 0044a1d97..890a38f76 100644
--- a/test/unit/parser/CMakeLists.txt
+++ b/test/unit/parser/CMakeLists.txt
@@ -14,5 +14,5 @@
 ##
 
 # Add unit tests.
-cvc4_add_unit_test_black(parser_black parser)
-cvc4_add_unit_test_black(parser_builder_black parser)
+cvc5_add_unit_test_black(parser_black parser)
+cvc5_add_unit_test_black(parser_builder_black parser)
diff --git a/test/unit/preprocessing/CMakeLists.txt b/test/unit/preprocessing/CMakeLists.txt
index c16cb07fc..0cebfb604 100644
--- a/test/unit/preprocessing/CMakeLists.txt
+++ b/test/unit/preprocessing/CMakeLists.txt
@@ -14,5 +14,5 @@
 ##
 
 # Add unit tests.
-cvc4_add_unit_test_white(pass_bv_gauss_white preprocessing)
-cvc4_add_unit_test_white(pass_foreign_theory_rewrite_white preprocessing)
+cvc5_add_unit_test_white(pass_bv_gauss_white preprocessing)
+cvc5_add_unit_test_white(pass_foreign_theory_rewrite_white preprocessing)
diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt
index 7cec81221..1b3e3c130 100644
--- a/test/unit/printer/CMakeLists.txt
+++ b/test/unit/printer/CMakeLists.txt
@@ -14,4 +14,4 @@
 ##
 
 # Add unit tests.
-cvc4_add_unit_test_black(smt2_printer_black printer)
+cvc5_add_unit_test_black(smt2_printer_black printer)
diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt
index 8e93c14f9..57143bf90 100644
--- a/test/unit/prop/CMakeLists.txt
+++ b/test/unit/prop/CMakeLists.txt
@@ -14,4 +14,4 @@
 ##
 
 # Add unit tests.
-cvc4_add_unit_test_white(cnf_stream_white prop)
+cvc5_add_unit_test_white(cnf_stream_white prop)
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 75dd8c32c..d0c0e2bd2 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -14,27 +14,27 @@
 ##
 
 # Add unit tests.
-cvc4_add_unit_test_black(regexp_operation_black theory)
-cvc4_add_unit_test_black(theory_black theory)
-cvc4_add_unit_test_white(evaluator_white theory)
-cvc4_add_unit_test_white(logic_info_white theory)
-cvc4_add_unit_test_white(sequences_rewriter_white theory)
-cvc4_add_unit_test_white(strings_rewriter_white theory)
-cvc4_add_unit_test_white(theory_arith_white theory)
-cvc4_add_unit_test_white(theory_bags_normal_form_white theory)
-cvc4_add_unit_test_white(theory_bags_rewriter_white theory)
-cvc4_add_unit_test_white(theory_bags_type_rules_white theory)
-cvc4_add_unit_test_white(theory_bv_rewriter_white theory)
-cvc4_add_unit_test_white(theory_bv_white theory)
-cvc4_add_unit_test_white(theory_bv_opt_white theory)
-cvc4_add_unit_test_white(theory_bv_int_blaster_white theory)
-cvc4_add_unit_test_white(theory_engine_white theory)
-cvc4_add_unit_test_white(theory_int_opt_white theory)
-cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
-cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory)
-cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory)
-cvc4_add_unit_test_white(theory_sets_type_rules_white theory)
-cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory)
-cvc4_add_unit_test_white(theory_strings_word_white theory)
-cvc4_add_unit_test_white(theory_white theory)
-cvc4_add_unit_test_white(type_enumerator_white theory)
+cvc5_add_unit_test_black(regexp_operation_black theory)
+cvc5_add_unit_test_black(theory_black theory)
+cvc5_add_unit_test_white(evaluator_white theory)
+cvc5_add_unit_test_white(logic_info_white theory)
+cvc5_add_unit_test_white(sequences_rewriter_white theory)
+cvc5_add_unit_test_white(strings_rewriter_white theory)
+cvc5_add_unit_test_white(theory_arith_white theory)
+cvc5_add_unit_test_white(theory_bags_normal_form_white theory)
+cvc5_add_unit_test_white(theory_bags_rewriter_white theory)
+cvc5_add_unit_test_white(theory_bags_type_rules_white theory)
+cvc5_add_unit_test_white(theory_bv_rewriter_white theory)
+cvc5_add_unit_test_white(theory_bv_white theory)
+cvc5_add_unit_test_white(theory_bv_opt_white theory)
+cvc5_add_unit_test_white(theory_bv_int_blaster_white theory)
+cvc5_add_unit_test_white(theory_engine_white theory)
+cvc5_add_unit_test_white(theory_int_opt_white theory)
+cvc5_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
+cvc5_add_unit_test_white(theory_quantifiers_bv_inverter_white theory)
+cvc5_add_unit_test_white(theory_sets_type_enumerator_white theory)
+cvc5_add_unit_test_white(theory_sets_type_rules_white theory)
+cvc5_add_unit_test_white(theory_strings_skolem_cache_black theory)
+cvc5_add_unit_test_white(theory_strings_word_white theory)
+cvc5_add_unit_test_white(theory_white theory)
+cvc5_add_unit_test_white(type_enumerator_white theory)
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index 85cc04c94..26ab40614 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -14,25 +14,25 @@
 ##
 
 # Add unit tests.
-cvc4_add_unit_test_white(array_store_all_white util)
-cvc4_add_unit_test_white(assert_white util)
-cvc4_add_unit_test_black(binary_heap_black util)
-cvc4_add_unit_test_black(bitvector_black util)
-cvc4_add_unit_test_black(boolean_simplification_black util)
-cvc4_add_unit_test_black(cardinality_black util)
-cvc4_add_unit_test_white(check_white util)
-cvc4_add_unit_test_black(configuration_black util)
-cvc4_add_unit_test_black(datatype_black util)
-cvc4_add_unit_test_black(exception_black util)
+cvc5_add_unit_test_white(array_store_all_white util)
+cvc5_add_unit_test_white(assert_white util)
+cvc5_add_unit_test_black(binary_heap_black util)
+cvc5_add_unit_test_black(bitvector_black util)
+cvc5_add_unit_test_black(boolean_simplification_black util)
+cvc5_add_unit_test_black(cardinality_black util)
+cvc5_add_unit_test_white(check_white util)
+cvc5_add_unit_test_black(configuration_black util)
+cvc5_add_unit_test_black(datatype_black util)
+cvc5_add_unit_test_black(exception_black util)
 if(CVC5_USE_SYMFPU)
-cvc4_add_unit_test_black(floatingpoint_black util)
+cvc5_add_unit_test_black(floatingpoint_black util)
 endif()
-cvc4_add_unit_test_black(integer_black util)
-cvc4_add_unit_test_white(integer_white util)
-cvc4_add_unit_test_black(output_black util)
-cvc4_add_unit_test_black(rational_black util)
-cvc4_add_unit_test_white(rational_white util)
+cvc5_add_unit_test_black(integer_black util)
+cvc5_add_unit_test_white(integer_white util)
+cvc5_add_unit_test_black(output_black util)
+cvc5_add_unit_test_black(rational_black util)
+cvc5_add_unit_test_white(rational_white util)
 if(CVC5_USE_POLY_IMP)
-cvc4_add_unit_test_black(real_algebraic_number_black util)
+cvc5_add_unit_test_black(real_algebraic_number_black util)
 endif()
-cvc4_add_unit_test_black(stats_black util)
+cvc5_add_unit_test_black(stats_black util)
diff --git a/test/unit/util/check_white.cpp b/test/unit/util/check_white.cpp
index 335c8c3b2..ff4712c63 100644
--- a/test/unit/util/check_white.cpp
+++ b/test/unit/util/check_white.cpp
@@ -28,7 +28,7 @@ class TestUtilWhiteCheck : public TestInternal
   static constexpr uint32_t K_ONE = 1;
 
   // This test just checks that this statement compiles.
-  std::string terminalCvc4Fatal() const
+  std::string terminalCvc5Fatal() const
   {
     CVC5_FATAL() << "This is a test that confirms that CVC5_FATAL can be a "
                     "terminal statement in a function that has a non-void "
diff --git a/test/unit/util/configuration_black.cpp b/test/unit/util/configuration_black.cpp
index a651085c6..0b54af43a 100644
--- a/test/unit/util/configuration_black.cpp
+++ b/test/unit/util/configuration_black.cpp
@@ -77,7 +77,7 @@ TEST_F(TestUtilBlackConfiguration, static_flags)
 
 TEST_F(TestUtilBlackConfiguration, package_name)
 {
-  ASSERT_EQ(Configuration::getPackageName(), "cvc4");
+  ASSERT_EQ(Configuration::getPackageName(), "cvc5");
 }
 
 TEST_F(TestUtilBlackConfiguration, versions)
diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp
index 37937769c..8a98a9601 100644
--- a/test/unit/util/output_black.cpp
+++ b/test/unit/util/output_black.cpp
@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Black box testing of CVC4 output classes.
+ * Black box testing of cvc5 output classes.
  */
 
 #include <iostream>