diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/CMakeLists.txt | 4 | ||||
-rw-r--r-- | test/unit/context/cdlist_black.cpp | 2 | ||||
-rw-r--r-- | test/unit/context/context_black.cpp | 4 | ||||
-rw-r--r-- | test/unit/context/context_mm_black.cpp | 2 | ||||
-rw-r--r-- | test/unit/memory.h | 22 | ||||
-rw-r--r-- | test/unit/node/kind_map_black.cpp | 2 | ||||
-rw-r--r-- | test/unit/node/node_black.cpp | 10 | ||||
-rw-r--r-- | test/unit/node/node_builder_black.cpp | 38 | ||||
-rw-r--r-- | test/unit/node/node_manager_black.cpp | 4 | ||||
-rw-r--r-- | test/unit/node/node_manager_white.cpp | 8 | ||||
-rw-r--r-- | test/unit/parser/parser_black.cpp | 8 | ||||
-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 |
20 files changed, 108 insertions, 108 deletions
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index 0be0b80e1..93ca679f3 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -27,7 +27,7 @@ add_custom_target(units COMMAND ctest --output-on-failure -L "unit" -j${CTEST_NTHREADS} $$ARGS DEPENDS build-units) -set(CVC4_UNIT_TEST_FLAGS_BLACK +set(CVC5_UNIT_TEST_FLAGS_BLACK -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS) @@ -35,7 +35,7 @@ set(CVC4_UNIT_TEST_FLAGS_BLACK macro(cvc4_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 ${CVC4_UNIT_TEST_FLAGS_BLACK}) + target_compile_definitions(${name} PRIVATE ${CVC5_UNIT_TEST_FLAGS_BLACK}) gtest_add_tests(TARGET ${name}) target_link_libraries(${name} PUBLIC main-test) target_link_libraries(${name} PUBLIC GTest::Main) diff --git a/test/unit/context/cdlist_black.cpp b/test/unit/context/cdlist_black.cpp index a3241d058..c944b0722 100644 --- a/test/unit/context/cdlist_black.cpp +++ b/test/unit/context/cdlist_black.cpp @@ -138,7 +138,7 @@ TEST_F(TestContextBlackCDList, empty_iterator) TEST_F(TestContextBlackCDList, out_of_memory) { -#ifndef CVC4_MEMORY_LIMITING_DISABLED +#ifndef CVC5_MEMORY_LIMITING_DISABLED CDList<uint32_t> list(d_context.get()); test::WithLimitedMemory wlm(1); diff --git a/test/unit/context/context_black.cpp b/test/unit/context/context_black.cpp index 0ad830162..ee5140da3 100644 --- a/test/unit/context/context_black.cpp +++ b/test/unit/context/context_black.cpp @@ -91,10 +91,10 @@ TEST_F(TestContextBlack, push_pop) // the interface doesn't declare any exceptions d_context->push(); d_context->pop(); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(d_context->pop(), "Cannot pop below level 0"); ASSERT_DEATH(d_context->pop(), "Cannot pop below level 0"); -#endif /* CVC4_ASSERTIONS */ +#endif /* CVC5_ASSERTIONS */ } TEST_F(TestContextBlack, dtor) diff --git a/test/unit/context/context_mm_black.cpp b/test/unit/context/context_mm_black.cpp index 0f031ef5b..22b15d70d 100644 --- a/test/unit/context/context_mm_black.cpp +++ b/test/unit/context/context_mm_black.cpp @@ -36,7 +36,7 @@ class TestContextBlackMM : public TestInternal TEST_F(TestContextBlackMM, push_pop) { -#ifdef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER +#ifdef CVC5_DEBUG_CONTEXT_MEMORY_MANAGER #warning "Using the debug context memory manager, omitting unit tests" #else // Push, then allocate, then pop diff --git a/test/unit/memory.h b/test/unit/memory.h index 726404e5e..45c65c202 100644 --- a/test/unit/memory.h +++ b/test/unit/memory.h @@ -20,7 +20,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. ** If this is disabled, there will be a function: ** void WarnWithLimitedMemoryDisabledReason() @@ -39,24 +39,24 @@ #include "base/check.h" #include "base/configuration_private.h" -// Conditionally define CVC4_MEMORY_LIMITING_DISABLED. +// Conditionally define CVC5_MEMORY_LIMITING_DISABLED. #ifdef __APPLE__ -# define CVC4_MEMORY_LIMITING_DISABLED 1 -# define CVC4_MEMORY_LIMITING_DISABLED_REASON "setrlimit() is broken on Mac." +#define CVC5_MEMORY_LIMITING_DISABLED 1 +#define CVC5_MEMORY_LIMITING_DISABLED_REASON "setrlimit() is broken on Mac." #else /* __APPLE__ */ // Tests cannot expect bad_alloc to be thrown due to limit memory using // setrlimit when ASAN is enable. ASAN instead aborts on mmap failures. # if IS_ASAN_BUILD -# define CVC4_MEMORY_LIMITING_DISABLED 1 -# define CVC4_MEMORY_LIMITING_DISABLED_REASON "ASAN's mmap failures abort." +#define CVC5_MEMORY_LIMITING_DISABLED 1 +#define CVC5_MEMORY_LIMITING_DISABLED_REASON "ASAN's mmap failures abort." # endif #endif namespace cvc5 { namespace test { -#ifndef CVC4_MEMORY_LIMITING_DISABLED +#ifndef CVC5_MEMORY_LIMITING_DISABLED class WithLimitedMemory { public: WithLimitedMemory() { remember(); } @@ -89,9 +89,9 @@ class WithLimitedMemory { } // namespace test } // namespace cvc5 -// Remove CVC4_MEMORY_LIMITING_DISABLED_REASON if it is defined. -#ifdef CVC4_MEMORY_LIMITING_DISABLED_REASON -#undef CVC4_MEMORY_LIMITING_DISABLED_REASON -#endif /* CVC4_MEMORY_LIMITING_DISABLED_REASON */ +// Remove CVC5_MEMORY_LIMITING_DISABLED_REASON if it is defined. +#ifdef CVC5_MEMORY_LIMITING_DISABLED_REASON +#undef CVC5_MEMORY_LIMITING_DISABLED_REASON +#endif /* CVC5_MEMORY_LIMITING_DISABLED_REASON */ #endif /* __CVC5__TEST__MEMORY_H */ diff --git a/test/unit/node/kind_map_black.cpp b/test/unit/node/kind_map_black.cpp index 7da3e5715..428da7206 100644 --- a/test/unit/node/kind_map_black.cpp +++ b/test/unit/node/kind_map_black.cpp @@ -39,7 +39,7 @@ TEST_F(TestNodeBlackKindMap, simple) ASSERT_TRUE(map.test(AND)); map.reset(AND); ASSERT_FALSE(map.test(AND)); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_THROW(map.set(LAST_KIND), AssertArgumentException); #endif } diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index cfe008ec0..b63541d6c 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -186,7 +186,7 @@ TEST_F(TestNodeBlackNode, operator_not_equals) /* operator[] */ TEST_F(TestNodeBlackNode, operator_square) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS // Basic bounds check on a node w/out children ASSERT_DEATH(Node::null()[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren"); ASSERT_DEATH(Node::null()[0], "i >= 0 && unsigned\\(i\\) < d_nchildren"); @@ -205,7 +205,7 @@ TEST_F(TestNodeBlackNode, operator_square) ASSERT_EQ(tb, ite[1]); ASSERT_EQ(eb, ite[2]); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS // Bounds check on a node with children ASSERT_DEATH(ite == ite[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren"); ASSERT_DEATH(ite == ite[4], "i >= 0 && unsigned\\(i\\) < d_nchildren"); @@ -422,7 +422,7 @@ TEST_F(TestNodeBlackNode, getOperator) ASSERT_EQ(a.getNumChildren(), 0); ASSERT_EQ(f, fa.getOperator()); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(f.getOperator(), "mk == kind::metakind::PARAMETERIZED"); ASSERT_DEATH(a.getOperator(), "mk == kind::metakind::PARAMETERIZED"); #endif @@ -443,7 +443,7 @@ TEST_F(TestNodeBlackNode, getNumChildren) testNaryExpForSize(AND, n); } -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(testNaryExpForSize(AND, 0), "getNumChildren\\(\\) >= " "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)"); @@ -456,7 +456,7 @@ TEST_F(TestNodeBlackNode, getNumChildren) ASSERT_DEATH(testNaryExpForSize(NOT, 2), "getNumChildren\\(\\) <= " "kind::metakind::getMaxArityForKind\\(getKind\\(\\)\\)"); -#endif /* CVC4_ASSERTIONS */ +#endif /* CVC5_ASSERTIONS */ } TEST_F(TestNodeBlackNode, iterator) diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp index 2b8ef7a04..fbf2b9108 100644 --- a/test/unit/node/node_builder_black.cpp +++ b/test/unit/node/node_builder_black.cpp @@ -55,7 +55,7 @@ TEST_F(TestNodeBlackNodeBuilder, ctors) /* Default size tests. */ NodeBuilder def; ASSERT_EQ(def.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(def.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif @@ -65,7 +65,7 @@ TEST_F(TestNodeBlackNodeBuilder, ctors) NodeBuilder from_nm(d_nodeManager.get()); ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(from_nm.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif @@ -77,7 +77,7 @@ TEST_F(TestNodeBlackNodeBuilder, ctors) /* Copy constructors */ NodeBuilder copy(def); ASSERT_EQ(copy.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(copy.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif } @@ -100,7 +100,7 @@ TEST_F(TestNodeBlackNodeBuilder, getKind) ASSERT_EQ(noKind.getKind(), PLUS); Node n = noKind; -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(noKind.getKind(), "!isUsed\\(\\)"); #endif @@ -115,7 +115,7 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren) Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode)); NodeBuilder nb; -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif @@ -126,7 +126,7 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren) ASSERT_EQ(nb.getNumChildren(), 4u); nb.clear(); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif @@ -139,7 +139,7 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren) nb << x << x << x; ASSERT_EQ(nb.getNumChildren(), 6u); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(nb << PLUS, "getKind\\(\\) == kind::UNDEFINED_KIND"); Node n = nb; ASSERT_DEATH(nb.getNumChildren(), "!isUsed\\(\\)"); @@ -154,7 +154,7 @@ TEST_F(TestNodeBlackNodeBuilder, operator_square) Node i_2 = d_nodeManager->mkConst(true); Node i_K = d_nodeManager->mkNode(NOT, i_0); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(arr[-1], "index out of range"); ASSERT_DEATH(arr[0], "index out of range"); #endif @@ -184,7 +184,7 @@ TEST_F(TestNodeBlackNodeBuilder, operator_square) } ASSERT_EQ(arr[K], i_K); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS Node n = arr; ASSERT_DEATH(arr[0], "!isUsed\\(\\)"); #endif @@ -194,7 +194,7 @@ TEST_F(TestNodeBlackNodeBuilder, clear) { NodeBuilder nb; ASSERT_EQ(nb.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif @@ -205,7 +205,7 @@ TEST_F(TestNodeBlackNodeBuilder, clear) nb.clear(); ASSERT_EQ(nb.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif @@ -221,14 +221,14 @@ TEST_F(TestNodeBlackNodeBuilder, clear) push_back(nb, K); nb.clear(); ASSERT_EQ(nb.getKind(), UNDEFINED_KIND); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND"); #endif } TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS NodeBuilder spec(d_specKind); ASSERT_DEATH(spec << PLUS, "can't redefine the Kind of a NodeBuilder"); #endif @@ -246,20 +246,20 @@ TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind) nb << d_nodeManager->mkConst(true) << d_nodeManager->mkConst(false); nb.clear(PLUS); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS Node n; ASSERT_DEATH(n = nb, "Nodes with kind PLUS must have at least 2 children"); nb.clear(PLUS); #endif -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(nb << PLUS, "can't redefine the Kind of a NodeBuilder"); #endif NodeBuilder testRef; ASSERT_EQ((testRef << d_specKind).getKind(), d_specKind); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS NodeBuilder testTwo; ASSERT_DEATH(testTwo << d_specKind << PLUS, "can't redefine the Kind of a NodeBuilder"); @@ -284,7 +284,7 @@ TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node) ASSERT_EQ(nb.getKind(), d_specKind); ASSERT_EQ(nb.getNumChildren(), K); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS Node n = nb; ASSERT_DEATH(nb << n, "!isUsed\\(\\)"); #endif @@ -317,7 +317,7 @@ TEST_F(TestNodeBlackNodeBuilder, append) d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t)); Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y)); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(d_nodeManager->mkNode(XOR, y, x, x), "Nodes with kind XOR must have at most 2 children"); #endif @@ -380,7 +380,7 @@ TEST_F(TestNodeBlackNodeBuilder, operator_node_cast) ASSERT_EQ(nexplicit.getKind(), d_specKind); ASSERT_EQ(nexplicit.getNumChildren(), K); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(Node blah = implicit, "!isUsed\\(\\)"); #endif } diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp index 6ad6f583c..a2d25c8d8 100644 --- a/test/unit/node/node_manager_black.cpp +++ b/test/unit/node/node_manager_black.cpp @@ -302,7 +302,7 @@ TEST_F(TestNodeBlackNodeManager, mkPredicateType) /* This test is only valid if assertions are enabled. */ TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType()); ASSERT_DEATH(d_nodeManager->mkNode(AND, x), "Nodes with kind AND must have at least 2 children"); @@ -312,7 +312,7 @@ TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children) /* This test is only valid if assertions are enabled. */ TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS std::vector<Node> vars; const uint32_t max = metakind::getMaxArityForKind(AND); TypeNode boolType = d_nodeManager->booleanType(); diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp index a13e76d03..986eac870 100644 --- a/test/unit/node/node_manager_white.cpp +++ b/test/unit/node/node_manager_white.cpp @@ -46,9 +46,9 @@ TEST_F(TestNodeWhiteNodeManager, oversized_node_builder) ASSERT_NO_THROW(nb.realloc(15)); ASSERT_NO_THROW(nb.realloc(25)); ASSERT_NO_THROW(nb.realloc(256)); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(nb.realloc(100), "toSize > d_nvMaxChildren"); -#endif /* CVC4_ASSERTIONS */ +#endif /* CVC5_ASSERTIONS */ ASSERT_NO_THROW(nb.realloc(257)); ASSERT_NO_THROW(nb.realloc(4000)); ASSERT_NO_THROW(nb.realloc(20000)); @@ -56,9 +56,9 @@ TEST_F(TestNodeWhiteNodeManager, oversized_node_builder) ASSERT_NO_THROW(nb.realloc(65535)); ASSERT_NO_THROW(nb.realloc(65536)); ASSERT_NO_THROW(nb.realloc(67108863)); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS ASSERT_DEATH(nb.realloc(67108863), "toSize > d_nvMaxChildren"); -#endif /* CVC4_ASSERTIONS */ +#endif /* CVC5_ASSERTIONS */ } TEST_F(TestNodeWhiteNodeManager, topological_sort) diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp index 5b695030e..27d008228 100644 --- a/test/unit/parser/parser_black.cpp +++ b/test/unit/parser/parser_black.cpp @@ -238,7 +238,7 @@ TEST_F(TestParserBlackCvCParser, good_inputs) TEST_F(TestParserBlackCvCParser, bad_inputs) { // competition builds don't do any checking -#ifndef CVC4_COMPETITION_MODE +#ifndef CVC5_COMPETITION_MODE tryBadInput("ASSERT;"); // no args tryBadInput("QUERY"); tryBadInput("CHECKSAT"); @@ -278,7 +278,7 @@ TEST_F(TestParserBlackCvCParser, good_exprs) TEST_F(TestParserBlackCvCParser, bad_exprs) { // competition builds don't do any checking -#ifndef CVC4_COMPETITION_MODE +#ifndef CVC5_COMPETITION_MODE tryBadInput("a AND"); // wrong arity tryBadInput("AND(a,b)"); // not infix tryBadInput("(OR (AND a b) c)"); // not infix @@ -326,7 +326,7 @@ TEST_F(TestParserBlackSmt2Parser, good_inputs) TEST_F(TestParserBlackSmt2Parser, bad_inputs) { // competition builds don't do any checking -#ifndef CVC4_COMPETITION_MODE +#ifndef CVC5_COMPETITION_MODE // no arguments tryBadInput("(assert)"); // illegal character in symbol @@ -366,7 +366,7 @@ TEST_F(TestParserBlackSmt2Parser, good_exprs) TEST_F(TestParserBlackSmt2Parser, bad_exprs) { // competition builds don't do any checking -#ifndef CVC4_COMPETITION_MODE +#ifndef CVC5_COMPETITION_MODE tryBadExpr("(and)"); // wrong arity tryBadExpr("(and a b"); // no closing paren tryBadExpr("(a and b)"); // infix 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); |