Rename CVC4_ macros to CVC5_. (#6327)

9 files changed, 56 insertions, 56 deletions

diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index b898e1344..fc5484a1f 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -21,7 +21,7 @@ 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)
-if(CVC4_USE_SYMFPU)
+if(CVC5_USE_SYMFPU)
 cvc4_add_unit_test_black(floatingpoint_black util)
 endif()
 cvc4_add_unit_test_black(integer_black util)
@@ -29,7 +29,7 @@ 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)
-if(CVC4_USE_POLY_IMP)
+if(CVC5_USE_POLY_IMP)
 cvc4_add_unit_test_black(real_algebraic_number_black util)
 endif()
 cvc4_add_unit_test_black(stats_black util)
diff --git a/test/unit/util/assert_white.cpp b/test/unit/util/assert_white.cpp
index bab612b62..245ef8aaa 100644
--- a/test/unit/util/assert_white.cpp
+++ b/test/unit/util/assert_white.cpp
@@ -29,7 +29,7 @@ class TestUtilWhite : public TestInternal
 
 TEST_F(TestUtilWhite, Assert)
 {
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(Assert(false), "false");
 #else
   ASSERT_NO_THROW(Assert(false));
@@ -41,7 +41,7 @@ TEST_F(TestUtilWhite, Assert)
 
 TEST_F(TestUtilWhite, AssertArgument)
 {
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_THROW(AssertArgument(false, "x"), AssertArgumentException);
 #else
   ASSERT_NO_THROW(AssertArgument(false, "x"));
diff --git a/test/unit/util/binary_heap_black.cpp b/test/unit/util/binary_heap_black.cpp
index c00aeaeb2..76462b687 100644
--- a/test/unit/util/binary_heap_black.cpp
+++ b/test/unit/util/binary_heap_black.cpp
@@ -60,7 +60,7 @@ TEST_F(TestUtilBlackBinaryHeap, heap_series)
   // First test a heap of 1 element
   ASSERT_EQ(heap.size(), 0u);
   ASSERT_TRUE(heap.empty());
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(heap.top(), "!empty\\(\\)");
   ASSERT_DEATH(heap.pop(), "!empty\\(\\)");
 #endif
@@ -77,7 +77,7 @@ TEST_F(TestUtilBlackBinaryHeap, heap_series)
   ASSERT_NO_THROW(heap.erase(h5));
   ASSERT_TRUE(heap.empty());
   ASSERT_EQ(heap.size(), 0u);
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(heap.top(), "!empty\\(\\)");
   ASSERT_DEATH(heap.pop(), "!empty\\(\\)");
 #endif
@@ -135,7 +135,7 @@ TEST_F(TestUtilBlackBinaryHeap, heap_series)
   ASSERT_TRUE(heap.begin() == heap.end());
   ASSERT_TRUE(heap.empty());
   ASSERT_EQ(heap.size(), 0u);
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(heap.top(), "!empty\\(\\)");
   ASSERT_DEATH(heap.pop(), "!empty\\(\\)");
 #endif
diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp
index 2e266ce58..1ec9c923c 100644
--- a/test/unit/util/boolean_simplification_black.cpp
+++ b/test/unit/util/boolean_simplification_black.cpp
@@ -124,7 +124,7 @@ TEST_F(TestUtilBlackBooleanSimplification, negate)
   out = d_fa.andNode(d_ac).notNode();
   test_nodes_equal(out, BooleanSimplification::negate(in));
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   in = Node();
   ASSERT_THROW(BooleanSimplification::negate(in), AssertArgumentException);
 #endif
@@ -166,7 +166,7 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyClause)
                               << d_hfc << d_ac << d_d.andNode(d_b);
   test_nodes_equal(out, BooleanSimplification::simplifyClause(in));
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   in = d_nodeManager->mkNode(kind::AND, d_a, d_b);
   ASSERT_THROW(BooleanSimplification::simplifyClause(in),
                AssertArgumentException);
@@ -212,7 +212,7 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyHornClause)
         << d_hfc << d_ac << d_d.notNode();
   test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in));
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   in = d_nodeManager->mkNode(kind::OR, d_a, d_b);
   ASSERT_THROW(BooleanSimplification::simplifyHornClause(in),
                AssertArgumentException);
@@ -241,7 +241,7 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyConflict)
                                << d_hfc.orNode(d_ac) << d_d << d_b;
   test_nodes_equal(out, BooleanSimplification::simplifyConflict(in));
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   in = d_nodeManager->mkNode(kind::OR, d_a, d_b);
   ASSERT_THROW(BooleanSimplification::simplifyConflict(in),
                AssertArgumentException);
diff --git a/test/unit/util/check_white.cpp b/test/unit/util/check_white.cpp
index 4909e3a58..d517e4364 100644
--- a/test/unit/util/check_white.cpp
+++ b/test/unit/util/check_white.cpp
@@ -31,7 +31,7 @@ class TestUtilWhiteCheck : public TestInternal
   // This test just checks that this statement compiles.
   std::string terminalCvc4Fatal() const
   {
-    CVC4_FATAL() << "This is a test that confirms that CVC4_FATAL can be a "
+    CVC5_FATAL() << "This is a test that confirms that CVC5_FATAL can be a "
                     "terminal statement in a function that has a non-void "
                     "return type.";
   }
@@ -45,8 +45,8 @@ TEST_F(TestUtilWhiteCheck, check)
 TEST_F(TestUtilWhiteCheck, dcheck)
 {
   Assert(K_ONE == 1) << "always passes";
-#ifndef CVC4_ASSERTIONS
-  Assert(false) << "Will not be compiled in when CVC4_ASSERTIONS off.";
+#ifndef CVC5_ASSERTIONS
+  Assert(false) << "Will not be compiled in when CVC5_ASSERTIONS off.";
 #endif
 }
 
diff --git a/test/unit/util/configuration_black.cpp b/test/unit/util/configuration_black.cpp
index 35bfd4d78..508aa179b 100644
--- a/test/unit/util/configuration_black.cpp
+++ b/test/unit/util/configuration_black.cpp
@@ -27,46 +27,46 @@ class TestUtilBlackConfiguration : public TestInternal
 TEST_F(TestUtilBlackConfiguration, static_flags)
 {
   const bool debug =
-#ifdef CVC4_DEBUG
+#ifdef CVC5_DEBUG
       true;
-#else  /* CVC4_DEBUG */
+#else  /* CVC5_DEBUG */
       false;
-#endif /* CVC4_DEBUG */
+#endif /* CVC5_DEBUG */
 
   const bool tracing =
-#ifdef CVC4_TRACING
+#ifdef CVC5_TRACING
       true;
-#else  /* CVC4_TRACING */
+#else  /* CVC5_TRACING */
       false;
-#endif /* CVC4_TRACING */
+#endif /* CVC5_TRACING */
 
   const bool muzzled =
-#ifdef CVC4_MUZZLE
+#ifdef CVC5_MUZZLE
       true;
-#else  /* CVC4_MUZZLE */
+#else  /* CVC5_MUZZLE */
       false;
-#endif /* CVC4_MUZZLE */
+#endif /* CVC5_MUZZLE */
 
   const bool assertions =
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
       true;
-#else  /* CVC4_ASSERTIONS */
+#else  /* CVC5_ASSERTIONS */
       false;
-#endif /* CVC4_ASSERTIONS */
+#endif /* CVC5_ASSERTIONS */
 
   const bool coverage =
-#ifdef CVC4_COVERAGE
+#ifdef CVC5_COVERAGE
       true;
-#else  /* CVC4_COVERAGE */
+#else  /* CVC5_COVERAGE */
       false;
-#endif /* CVC4_COVERAGE */
+#endif /* CVC5_COVERAGE */
 
   const bool profiling =
-#ifdef CVC4_PROFILING
+#ifdef CVC5_PROFILING
       true;
-#else  /* CVC4_PROFILING */
+#else  /* CVC5_PROFILING */
       false;
-#endif /* CVC4_PROFILING */
+#endif /* CVC5_PROFILING */
 
   ASSERT_EQ(Configuration::isDebugBuild(), debug);
   ASSERT_EQ(Configuration::isTracingBuild(), tracing);
diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp
index e951dd114..09991a6d0 100644
--- a/test/unit/util/output_black.cpp
+++ b/test/unit/util/output_black.cpp
@@ -82,7 +82,7 @@ TEST_F(TestUtilBlackOutput, output)
   Trace.on("foo");
   Trace("foo") << "tracing3";
 
-#ifdef CVC4_MUZZLE
+#ifdef CVC5_MUZZLE
 
   ASSERT_EQ(d_debugStream.str(), "");
   ASSERT_EQ(d_messageStream.str(), "");
@@ -91,32 +91,32 @@ TEST_F(TestUtilBlackOutput, output)
   ASSERT_EQ(d_noticeStream.str(), "");
   ASSERT_EQ(d_traceStream.str(), "");
 
-#else /* CVC4_MUZZLE */
+#else /* CVC5_MUZZLE */
 
-#ifdef CVC4_DEBUG
+#ifdef CVC5_DEBUG
   ASSERT_EQ(d_debugStream.str(), "testing1testing3");
-#else  /* CVC4_DEBUG */
+#else  /* CVC5_DEBUG */
   ASSERT_EQ(d_debugStream.str(), "");
-#endif /* CVC4_DEBUG */
+#endif /* CVC5_DEBUG */
 
   ASSERT_EQ(d_messageStream.str(), "a message");
   ASSERT_EQ(d_warningStream.str(), "bad warning!");
   ASSERT_EQ(d_chatStream.str(), "chatty");
   ASSERT_EQ(d_noticeStream.str(), "note");
 
-#ifdef CVC4_TRACING
+#ifdef CVC5_TRACING
   ASSERT_EQ(d_traceStream.str(), "tracing1tracing3");
-#else  /* CVC4_TRACING */
+#else  /* CVC5_TRACING */
   ASSERT_EQ(d_traceStream.str(), "");
-#endif /* CVC4_TRACING */
+#endif /* CVC5_TRACING */
 
-#endif /* CVC4_MUZZLE */
+#endif /* CVC5_MUZZLE */
 }
 
 TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
 {
   Debug.on("foo");
-#ifndef CVC4_DEBUG
+#ifndef CVC5_DEBUG
   ASSERT_FALSE(Debug.isOn("foo"));
   Debug("foo") << failure() << std::endl;
 #else
@@ -125,7 +125,7 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
   Debug.off("foo");
 
   Trace.on("foo");
-#ifndef CVC4_TRACING
+#ifndef CVC5_TRACING
   ASSERT_FALSE(Trace.isOn("foo"));
   Trace("foo") << failure() << std::endl;
 #else
@@ -133,7 +133,7 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
 #endif
   Trace.off("foo");
 
-#ifdef CVC4_MUZZLE
+#ifdef CVC5_MUZZLE
   ASSERT_FALSE(Debug.isOn("foo"));
   ASSERT_FALSE(Trace.isOn("foo"));
   ASSERT_FALSE(Warning.isOn());
@@ -158,7 +158,7 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
 
 TEST_F(TestUtilBlackOutput, simple_print)
 {
-#ifdef CVC4_MUZZLE
+#ifdef CVC5_MUZZLE
 
   Debug.off("yo");
   Debug("yo") << "foobar";
@@ -194,7 +194,7 @@ TEST_F(TestUtilBlackOutput, simple_print)
   ASSERT_EQ(d_noticeStream.str(), std::string());
   d_noticeStream.str("");
 
-#else /* CVC4_MUZZLE */
+#else /* CVC5_MUZZLE */
 
   Debug.off("yo");
   Debug("yo") << "foobar";
@@ -202,11 +202,11 @@ TEST_F(TestUtilBlackOutput, simple_print)
   d_debugStream.str("");
   Debug.on("yo");
   Debug("yo") << "baz foo";
-#ifdef CVC4_DEBUG
+#ifdef CVC5_DEBUG
   ASSERT_EQ(d_debugStream.str(), std::string("baz foo"));
-#else  /* CVC4_DEBUG */
+#else  /* CVC5_DEBUG */
   ASSERT_EQ(d_debugStream.str(), std::string());
-#endif /* CVC4_DEBUG */
+#endif /* CVC5_DEBUG */
   d_debugStream.str("");
 
   Trace.off("yo");
@@ -215,11 +215,11 @@ TEST_F(TestUtilBlackOutput, simple_print)
   d_traceStream.str("");
   Trace.on("yo");
   Trace("yo") << "baz foo";
-#ifdef CVC4_TRACING
+#ifdef CVC5_TRACING
   ASSERT_EQ(d_traceStream.str(), std::string("baz foo"));
-#else  /* CVC4_TRACING */
+#else  /* CVC5_TRACING */
   ASSERT_EQ(d_traceStream.str(), std::string());
-#endif /* CVC4_TRACING */
+#endif /* CVC5_TRACING */
   d_traceStream.str("");
 
   Warning() << "baz foo";
@@ -238,7 +238,7 @@ TEST_F(TestUtilBlackOutput, simple_print)
   ASSERT_EQ(d_noticeStream.str(), std::string("baz foo"));
   d_noticeStream.str("");
 
-#endif /* CVC4_MUZZLE */
+#endif /* CVC5_MUZZLE */
 }
 }  // namespace test
 }  // namespace cvc5
diff --git a/test/unit/util/real_algebraic_number_black.cpp b/test/unit/util/real_algebraic_number_black.cpp
index 507be5ea0..c130023ca 100644
--- a/test/unit/util/real_algebraic_number_black.cpp
+++ b/test/unit/util/real_algebraic_number_black.cpp
@@ -20,8 +20,8 @@
 namespace cvc5 {
 namespace test {
 
-#ifndef CVC4_POLY_IMP
-#error "This unit test should only be enabled for CVC4_POLY_IMP"
+#ifndef CVC5_POLY_IMP
+#error "This unit test should only be enabled for CVC5_POLY_IMP"
 #endif
 
 class TestUtilBlackRealAlgebraicNumber : public TestInternal
diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp
index 2ee64ab33..c15b0cd47 100644
--- a/test/unit/util/stats_black.cpp
+++ b/test/unit/util/stats_black.cpp
@@ -36,7 +36,7 @@ class TestUtilBlackStats : public TestInternal
 
 TEST_F(TestUtilBlackStats, stats)
 {
-#ifdef CVC4_STATISTICS_ON
+#ifdef CVC5_STATISTICS_ON
   std::string empty, bar = "bar", baz = "baz";
   ReferenceStat<std::string> refStr("stat #1", empty);
   ReferenceStat<std::string> refStr2("refStr2", bar);