diff options
Diffstat (limited to 'test/unit/util')
-rw-r--r-- | test/unit/util/CMakeLists.txt | 4 | ||||
-rw-r--r-- | test/unit/util/assert_white.cpp | 4 | ||||
-rw-r--r-- | test/unit/util/binary_heap_black.cpp | 6 | ||||
-rw-r--r-- | test/unit/util/boolean_simplification_black.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/check_white.cpp | 6 | ||||
-rw-r--r-- | test/unit/util/configuration_black.cpp | 36 | ||||
-rw-r--r-- | test/unit/util/output_black.cpp | 42 | ||||
-rw-r--r-- | test/unit/util/real_algebraic_number_black.cpp | 4 | ||||
-rw-r--r-- | test/unit/util/stats_black.cpp | 2 |
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); |