diff options
Diffstat (limited to 'test/unit/theory')
23 files changed, 168 insertions, 168 deletions
diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp index ff04adef1..54976c7d7 100644 --- a/test/unit/theory/evaluator_white.cpp +++ b/test/unit/theory/evaluator_white.cpp @@ -24,7 +24,7 @@ #include "theory/rewriter.h" #include "util/rational.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; @@ -156,4 +156,4 @@ TEST_F(TestTheoryWhiteEvaluator, code) } } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/logic_info_white.cpp b/test/unit/theory/logic_info_white.cpp index 56dd062df..0c45cc4ed 100644 --- a/test/unit/theory/logic_info_white.cpp +++ b/test/unit/theory/logic_info_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Unit testing for CVC4::LogicInfo class + ** \brief Unit testing for CVC5::LogicInfo class ** - ** Unit testing for CVC4::LogicInfo class. + ** Unit testing for CVC5::LogicInfo class. **/ #include "base/configuration.h" @@ -19,7 +19,7 @@ #include "test.h" #include "theory/logic_info.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; @@ -544,33 +544,33 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic) LogicInfo info; ASSERT_FALSE(info.isLocked()); - ASSERT_THROW(info.getLogicString(), CVC4::IllegalArgumentException); + ASSERT_THROW(info.getLogicString(), CVC5::IllegalArgumentException); ASSERT_THROW(info.isTheoryEnabled(THEORY_BUILTIN), - CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); ASSERT_THROW(info.isTheoryEnabled(THEORY_BOOL), - CVC4::IllegalArgumentException); - ASSERT_THROW(info.isTheoryEnabled(THEORY_UF), CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); + ASSERT_THROW(info.isTheoryEnabled(THEORY_UF), CVC5::IllegalArgumentException); ASSERT_THROW(info.isTheoryEnabled(THEORY_ARITH), - CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); ASSERT_THROW(info.isTheoryEnabled(THEORY_ARRAYS), - CVC4::IllegalArgumentException); - ASSERT_THROW(info.isTheoryEnabled(THEORY_BV), CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); + ASSERT_THROW(info.isTheoryEnabled(THEORY_BV), CVC5::IllegalArgumentException); ASSERT_THROW(info.isTheoryEnabled(THEORY_DATATYPES), - CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); ASSERT_THROW(info.isTheoryEnabled(THEORY_QUANTIFIERS), - CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_BUILTIN), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_BOOL), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_UF), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_ARITH), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_ARRAYS), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_BV), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_DATATYPES), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isPure(THEORY_QUANTIFIERS), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isQuantified(), CVC4::IllegalArgumentException); - ASSERT_THROW(info.areIntegersUsed(), CVC4::IllegalArgumentException); - ASSERT_THROW(info.areRealsUsed(), CVC4::IllegalArgumentException); - ASSERT_THROW(info.isLinear(), CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_BUILTIN), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_BOOL), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_UF), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_ARITH), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_ARRAYS), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_BV), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_DATATYPES), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isPure(THEORY_QUANTIFIERS), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isQuantified(), CVC5::IllegalArgumentException); + ASSERT_THROW(info.areIntegersUsed(), CVC5::IllegalArgumentException); + ASSERT_THROW(info.areRealsUsed(), CVC5::IllegalArgumentException); + ASSERT_THROW(info.isLinear(), CVC5::IllegalArgumentException); info.lock(); ASSERT_TRUE(info.isLocked()); @@ -598,17 +598,17 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic) ASSERT_TRUE(info.areTranscendentalsUsed()); ASSERT_FALSE(info.isLinear()); - ASSERT_THROW(info.arithOnlyLinear(), CVC4::IllegalArgumentException); - ASSERT_THROW(info.disableIntegers(), CVC4::IllegalArgumentException); - ASSERT_THROW(info.disableQuantifiers(), CVC4::IllegalArgumentException); - ASSERT_THROW(info.disableTheory(THEORY_BV), CVC4::IllegalArgumentException); + ASSERT_THROW(info.arithOnlyLinear(), CVC5::IllegalArgumentException); + ASSERT_THROW(info.disableIntegers(), CVC5::IllegalArgumentException); + ASSERT_THROW(info.disableQuantifiers(), CVC5::IllegalArgumentException); + ASSERT_THROW(info.disableTheory(THEORY_BV), CVC5::IllegalArgumentException); ASSERT_THROW(info.disableTheory(THEORY_DATATYPES), - CVC4::IllegalArgumentException); - ASSERT_THROW(info.enableIntegers(), CVC4::IllegalArgumentException); - ASSERT_THROW(info.disableReals(), CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); + ASSERT_THROW(info.enableIntegers(), CVC5::IllegalArgumentException); + ASSERT_THROW(info.disableReals(), CVC5::IllegalArgumentException); ASSERT_THROW(info.disableTheory(THEORY_ARITH), - CVC4::IllegalArgumentException); - ASSERT_THROW(info.disableTheory(THEORY_UF), CVC4::IllegalArgumentException); + CVC5::IllegalArgumentException); + ASSERT_THROW(info.disableTheory(THEORY_UF), CVC5::IllegalArgumentException); info = info.getUnlockedCopy(); ASSERT_FALSE(info.isLocked()); info.disableTheory(THEORY_STRINGS); @@ -617,7 +617,7 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic) info.arithOnlyLinear(); info.disableIntegers(); info.lock(); - if (CVC4::Configuration::isBuiltWithSymFPU()) + if (CVC5::Configuration::isBuiltWithSymFPU()) { ASSERT_EQ(info.getLogicString(), "SEP_AUFBVFPDTLRA"); } @@ -631,7 +631,7 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic) info.disableQuantifiers(); info.disableTheory(THEORY_BAGS); info.lock(); - if (CVC4::Configuration::isBuiltWithSymFPU()) + if (CVC5::Configuration::isBuiltWithSymFPU()) { ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA"); } @@ -648,7 +648,7 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic) info.enableIntegers(); info.disableReals(); info.lock(); - if (CVC4::Configuration::isBuiltWithSymFPU()) + if (CVC5::Configuration::isBuiltWithSymFPU()) { ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFFPLIA"); } @@ -1371,4 +1371,4 @@ TEST_F(TestTheoryWhiteLogicInfo, comparison) gt(ufHo, "QF_UF"); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp index 0b6bf6500..b87701534 100644 --- a/test/unit/theory/regexp_operation_black.cpp +++ b/test/unit/theory/regexp_operation_black.cpp @@ -27,7 +27,7 @@ #include "theory/strings/regexp_operation.h" #include "theory/strings/skolem_cache.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace theory; @@ -144,4 +144,4 @@ TEST_F(TestTheoryBlackRegexpOperation, star_wildcards) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index fd6e3f3c0..7a85ad13d 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -28,7 +28,7 @@ #include "theory/strings/strings_entail.h" #include "theory/strings/strings_rewriter.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace theory::quantifiers; @@ -85,10 +85,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_length_one) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); - Node aaad = d_nodeManager->mkConst(::CVC4::String("AAAD")); - Node b = d_nodeManager->mkConst(::CVC4::String("B")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD")); + Node aaad = d_nodeManager->mkConst(::CVC5::String("AAAD")); + Node b = d_nodeManager->mkConst(::CVC5::String("B")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node negOne = d_nodeManager->mkConst(Rational(-1)); @@ -149,8 +149,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption) Node zero = d_nodeManager->mkConst(Rational(0)); Node one = d_nodeManager->mkConst(Rational(1)); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); Node slen_y = d_nodeManager->mkNode(kind::STRING_LENGTH, y); Node x_plus_slen_y = d_nodeManager->mkNode(kind::PLUS, x, slen_y); @@ -223,10 +223,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node b = d_nodeManager->mkConst(::CVC4::String("B")); - Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node b = d_nodeManager->mkConst(::CVC5::String("B")); + Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD")); Node negone = d_nodeManager->mkConst(Rational(-1)); Node zero = d_nodeManager->mkConst(Rational(0)); Node one = d_nodeManager->mkConst(Rational(1)); @@ -364,8 +364,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_concat) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); Node zero = d_nodeManager->mkConst(Rational(0)); Node three = d_nodeManager->mkConst(Rational(3)); @@ -431,11 +431,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, length_preserve_rewrite) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); - Node f = d_nodeManager->mkConst(::CVC4::String("F")); - Node gh = d_nodeManager->mkConst(::CVC4::String("GH")); - Node ij = d_nodeManager->mkConst(::CVC4::String("IJ")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD")); + Node f = d_nodeManager->mkConst(::CVC5::String("F")); + Node gh = d_nodeManager->mkConst(::CVC5::String("GH")); + Node ij = d_nodeManager->mkConst(::CVC5::String("IJ")); Node i = d_nodeManager->mkVar("i", intType); Node s = d_nodeManager->mkVar("s", strType); @@ -467,12 +467,12 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); - Node aaad = d_nodeManager->mkConst(::CVC4::String("AAAD")); - Node b = d_nodeManager->mkConst(::CVC4::String("B")); - Node c = d_nodeManager->mkConst(::CVC4::String("C")); - Node ccc = d_nodeManager->mkConst(::CVC4::String("CCC")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD")); + Node aaad = d_nodeManager->mkConst(::CVC5::String("AAAD")); + Node b = d_nodeManager->mkConst(::CVC5::String("B")); + Node c = d_nodeManager->mkConst(::CVC5::String("C")); + Node ccc = d_nodeManager->mkConst(::CVC5::String("CCC")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node negOne = d_nodeManager->mkConst(Rational(-1)); @@ -577,12 +577,12 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node ab = d_nodeManager->mkConst(::CVC4::String("AB")); - Node b = d_nodeManager->mkConst(::CVC4::String("B")); - Node c = d_nodeManager->mkConst(::CVC4::String("C")); - Node d = d_nodeManager->mkConst(::CVC4::String("D")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node ab = d_nodeManager->mkConst(::CVC5::String("AB")); + Node b = d_nodeManager->mkConst(::CVC5::String("B")); + Node c = d_nodeManager->mkConst(::CVC5::String("C")); + Node d = d_nodeManager->mkConst(::CVC5::String("D")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node z = d_nodeManager->mkVar("z", strType); @@ -773,7 +773,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) d_nodeManager->mkConst(String("AZZZB")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("FOO")); + Node res = d_nodeManager->mkConst(::CVC5::String("FOO")); sameNormalForm(t, res); } @@ -790,7 +790,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) d_nodeManager->mkConst(String("ZAZZZBZZB")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZZB")); + Node res = d_nodeManager->mkConst(::CVC5::String("ZFOOZZB")); sameNormalForm(t, res); } @@ -807,7 +807,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) d_nodeManager->mkConst(String("ZAZZZBZAZB")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZAZB")); + Node res = d_nodeManager->mkConst(::CVC5::String("ZFOOZAZB")); sameNormalForm(t, res); } @@ -824,7 +824,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) d_nodeManager->mkConst(String("ZZZ")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("ZZZ")); + Node res = d_nodeManager->mkConst(::CVC5::String("ZZZ")); sameNormalForm(t, res); } @@ -841,7 +841,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) d_nodeManager->mkConst(String("ZZZ")), sigStar, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("FOOZZZ")); + Node res = d_nodeManager->mkConst(::CVC5::String("FOOZZZ")); sameNormalForm(t, res); } @@ -858,7 +858,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re) d_nodeManager->mkConst(String("")), sigStar, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("FOO")); + Node res = d_nodeManager->mkConst(::CVC5::String("FOO")); sameNormalForm(t, res); } } @@ -893,7 +893,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) d_nodeManager->mkConst(String("AZZZB")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("FOO")); + Node res = d_nodeManager->mkConst(::CVC5::String("FOO")); sameNormalForm(t, res); } @@ -910,7 +910,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) d_nodeManager->mkConst(String("ZAZZZBZZB")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZZB")); + Node res = d_nodeManager->mkConst(::CVC5::String("ZFOOZZB")); sameNormalForm(t, res); } @@ -927,7 +927,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) d_nodeManager->mkConst(String("ZAZZZBZAZB")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("ZFOOZFOO")); + Node res = d_nodeManager->mkConst(::CVC5::String("ZFOOZFOO")); sameNormalForm(t, res); } @@ -944,7 +944,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) d_nodeManager->mkConst(String("ZZZ")), re, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("ZZZ")); + Node res = d_nodeManager->mkConst(::CVC5::String("ZZZ")); sameNormalForm(t, res); } @@ -961,7 +961,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) d_nodeManager->mkConst(String("ZZZ")), sigStar, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("FOOFOOFOO")); + Node res = d_nodeManager->mkConst(::CVC5::String("FOOFOOFOO")); sameNormalForm(t, res); } @@ -978,7 +978,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all) d_nodeManager->mkConst(String("")), sigStar, foo); - Node res = d_nodeManager->mkConst(::CVC4::String("")); + Node res = d_nodeManager->mkConst(::CVC5::String("")); sameNormalForm(t, res); } } @@ -988,18 +988,18 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node ab = d_nodeManager->mkConst(::CVC4::String("AB")); - Node b = d_nodeManager->mkConst(::CVC4::String("B")); - Node c = d_nodeManager->mkConst(::CVC4::String("C")); - Node e = d_nodeManager->mkConst(::CVC4::String("E")); - Node h = d_nodeManager->mkConst(::CVC4::String("H")); - Node j = d_nodeManager->mkConst(::CVC4::String("J")); - Node p = d_nodeManager->mkConst(::CVC4::String("P")); - Node abc = d_nodeManager->mkConst(::CVC4::String("ABC")); - Node def = d_nodeManager->mkConst(::CVC4::String("DEF")); - Node ghi = d_nodeManager->mkConst(::CVC4::String("GHI")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node ab = d_nodeManager->mkConst(::CVC5::String("AB")); + Node b = d_nodeManager->mkConst(::CVC5::String("B")); + Node c = d_nodeManager->mkConst(::CVC5::String("C")); + Node e = d_nodeManager->mkConst(::CVC5::String("E")); + Node h = d_nodeManager->mkConst(::CVC5::String("H")); + Node j = d_nodeManager->mkConst(::CVC5::String("J")); + Node p = d_nodeManager->mkConst(::CVC5::String("P")); + Node abc = d_nodeManager->mkConst(::CVC5::String("ABC")); + Node def = d_nodeManager->mkConst(::CVC5::String("DEF")); + Node ghi = d_nodeManager->mkConst(::CVC5::String("GHI")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y); @@ -1356,9 +1356,9 @@ TEST_F(TestTheoryWhiteSequencesRewriter, infer_eqs_from_contains) { TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node b = d_nodeManager->mkConst(::CVC4::String("B")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node b = d_nodeManager->mkConst(::CVC5::String("B")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y); @@ -1400,8 +1400,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_prefix_suffix) { TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node xx = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x); @@ -1437,11 +1437,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext) TypeNode strType = d_nodeManager->stringType(); TypeNode intType = d_nodeManager->integerType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node aaa = d_nodeManager->mkConst(::CVC4::String("AAA")); - Node b = d_nodeManager->mkConst(::CVC4::String("B")); - Node ba = d_nodeManager->mkConst(::CVC4::String("BA")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node aaa = d_nodeManager->mkConst(::CVC5::String("AAA")); + Node b = d_nodeManager->mkConst(::CVC5::String("B")); + Node ba = d_nodeManager->mkConst(::CVC5::String("BA")); Node w = d_nodeManager->mkVar("w", strType); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); @@ -1726,14 +1726,14 @@ TEST_F(TestTheoryWhiteSequencesRewriter, strip_constant_endpoints) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node empty = d_nodeManager->mkConst(::CVC4::String("")); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node ab = d_nodeManager->mkConst(::CVC4::String("AB")); - Node abc = d_nodeManager->mkConst(::CVC4::String("ABC")); - Node abcd = d_nodeManager->mkConst(::CVC4::String("ABCD")); - Node bc = d_nodeManager->mkConst(::CVC4::String("BC")); - Node c = d_nodeManager->mkConst(::CVC4::String("C")); - Node cd = d_nodeManager->mkConst(::CVC4::String("CD")); + Node empty = d_nodeManager->mkConst(::CVC5::String("")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node ab = d_nodeManager->mkConst(::CVC5::String("AB")); + Node abc = d_nodeManager->mkConst(::CVC5::String("ABC")); + Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD")); + Node bc = d_nodeManager->mkConst(::CVC5::String("BC")); + Node c = d_nodeManager->mkConst(::CVC5::String("C")); + Node cd = d_nodeManager->mkConst(::CVC5::String("CD")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); Node n = d_nodeManager->mkVar("n", intType); @@ -1833,7 +1833,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_membership) TypeNode strType = d_nodeManager->stringType(); std::vector<Node> vec_empty; - Node abc = d_nodeManager->mkConst(::CVC4::String("ABC")); + Node abc = d_nodeManager->mkConst(::CVC5::String("ABC")); Node re_abc = d_nodeManager->mkNode(kind::STRING_TO_REGEXP, abc); Node x = d_nodeManager->mkVar("x", strType); @@ -1908,4 +1908,4 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_regexp_concat) } } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/strings_rewriter_white.cpp b/test/unit/theory/strings_rewriter_white.cpp index 93aa1667a..94bf8b581 100644 --- a/test/unit/theory/strings_rewriter_white.cpp +++ b/test/unit/theory/strings_rewriter_white.cpp @@ -24,7 +24,7 @@ #include "theory/rewriter.h" #include "theory/strings/strings_rewriter.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace theory; @@ -41,8 +41,8 @@ TEST_F(TestTheoryWhiteStringsRewriter, rewrite_leq) TypeNode intType = d_nodeManager->integerType(); TypeNode strType = d_nodeManager->stringType(); - Node a = d_nodeManager->mkConst(::CVC4::String("A")); - Node bc = d_nodeManager->mkConst(::CVC4::String("BC")); + Node a = d_nodeManager->mkConst(::CVC5::String("A")); + Node bc = d_nodeManager->mkConst(::CVC5::String("BC")); Node x = d_nodeManager->mkVar("x", strType); Node y = d_nodeManager->mkVar("y", strType); @@ -61,4 +61,4 @@ TEST_F(TestTheoryWhiteStringsRewriter, rewrite_leq) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index d0ed5718e..ac992f5c9 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -24,7 +24,7 @@ #include "theory/theory_engine.h" #include "util/rational.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace theory::arith; @@ -122,4 +122,4 @@ TEST_F(TestTheoryWhiteArith, int_normal_form) ASSERT_EQ(Rewriter::rewrite(Rewriter::rewrite(t)), Rewriter::rewrite(t)); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp index ce6dbc79a..09f5c2ae9 100644 --- a/test/unit/theory/theory_bags_normal_form_white.cpp +++ b/test/unit/theory/theory_bags_normal_form_white.cpp @@ -18,7 +18,7 @@ #include "theory/bags/normal_form.h" #include "theory/strings/type_enumerator.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace kind; @@ -40,7 +40,7 @@ class TestTheoryWhiteBagsNormalForm : public TestSmt std::vector<Node> getNStrings(size_t n) { std::vector<Node> elements(n); - CVC4::theory::strings::StringEnumerator enumerator( + CVC5::theory::strings::StringEnumerator enumerator( d_nodeManager->stringType()); for (size_t i = 0; i < n; i++) @@ -586,4 +586,4 @@ TEST_F(TestTheoryWhiteBagsNormalForm, to_set) ASSERT_EQ(output3, NormalForm::evaluate(input3)); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 987f21fb5..a1cc2761a 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -17,7 +17,7 @@ #include "theory/bags/bags_rewriter.h" #include "theory/strings/type_enumerator.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace kind; @@ -688,4 +688,4 @@ TEST_F(TestTheoryWhiteBagsRewriter, to_set) && response.d_status == REWRITE_AGAIN_FULL); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index 0922a22a4..830169c8b 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -17,7 +17,7 @@ #include "theory/bags/theory_bags_type_rules.h" #include "theory/strings/type_enumerator.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace kind; @@ -33,7 +33,7 @@ class TestTheoryWhiteBagsTypeRule : public TestSmt std::vector<Node> getNStrings(size_t n) { std::vector<Node> elements(n); - CVC4::theory::strings::StringEnumerator enumerator( + CVC5::theory::strings::StringEnumerator enumerator( d_nodeManager->stringType()); for (size_t i = 0; i < n; i++) @@ -110,4 +110,4 @@ TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator) ASSERT_TRUE(d_nodeManager->mkNode(BAG_TO_SET, bag).getType().isSet()); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp index 096013110..ddd43a063 100644 --- a/test/unit/theory/theory_black.cpp +++ b/test/unit/theory/theory_black.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::theory + ** \brief Black box testing of CVC5::theory ** - ** Black box testing of CVC4::theory + ** Black box testing of CVC5::theory **/ #include <sstream> @@ -23,7 +23,7 @@ #include "test_smt.h" #include "theory/rewriter.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace context; @@ -129,4 +129,4 @@ TEST_F(TestTheoryBlack, array_const) ASSERT_TRUE(arr2.isConst()); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index 7888ba52b..247f5428f 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -22,7 +22,7 @@ #include "theory/bv/int_blaster.h" #include "util/bitvector.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace theory; @@ -44,4 +44,4 @@ class TestTheoryWhiteBvIntblaster : public TestSmtNoFinishInit Node d_one; }; } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_bv_rewriter_white.cpp b/test/unit/theory/theory_bv_rewriter_white.cpp index 556785680..c7262117c 100644 --- a/test/unit/theory/theory_bv_rewriter_white.cpp +++ b/test/unit/theory/theory_bv_rewriter_white.cpp @@ -23,7 +23,7 @@ #include "theory/rewriter.h" #include "util/bitvector.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace theory; @@ -81,4 +81,4 @@ TEST_F(TestTheoryWhiteBvRewriter, rewrite_bv_ite) ASSERT_EQ(nr, Rewriter::rewrite(nr)); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index 1447670f3..020c7d0a5 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -25,7 +25,7 @@ #include "theory/theory.h" #include "theory/theory_engine.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace theory::bv; @@ -93,4 +93,4 @@ TEST_F(TestTheoryWhiteBv, mkUmulo) } } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp index e0040e3d3..ff2f3a836 100644 --- a/test/unit/theory/theory_engine_white.cpp +++ b/test/unit/theory/theory_engine_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White box testing of CVC4::theory::Theory. + ** \brief White box testing of CVC5::theory::Theory. ** - ** White box testing of CVC4::theory::Theory. This test creates + ** White box testing of CVC5::theory::Theory. This test creates ** "fake" theory interfaces and injects them into TheoryEngine, so we ** can test TheoryEngine's behavior without relying on independent ** theory behavior. This is done in TheoryEngineWhite::setUp() by @@ -33,7 +33,7 @@ #include "util/integer.h" #include "util/rational.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace expr; @@ -183,4 +183,4 @@ TEST_F(TestTheoryWhiteEngine, rewrite_rules) } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index 81556d33a..fc20d6d73 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -15,7 +15,7 @@ #include "smt/optimization_solver.h" #include "test_smt.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace smt; @@ -136,4 +136,4 @@ TEST_F(TestTheoryWhiteIntOpt, result) std::cout << "Result is :" << r << std::endl; } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp index 942986a7e..715eea5f9 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp @@ -24,7 +24,7 @@ #include "theory/rewriter.h" #include "util/bitvector.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace theory::bv; @@ -452,4 +452,4 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvEqual) ASSERT_EQ(norm_axax[1], a); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index 7b6a73d2c..4ad3f04ef 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -20,7 +20,7 @@ #include "theory/quantifiers/bv_inverter_utils.h" #include "util/result.h" -namespace CVC4 { +namespace CVC5 { using namespace kind; using namespace theory; @@ -1611,4 +1611,4 @@ TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_sext_sgt_false) runTestSext(false, BITVECTOR_SGT); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_sets_type_enumerator_white.cpp b/test/unit/theory/theory_sets_type_enumerator_white.cpp index fdf8e3a5e..adee0c266 100644 --- a/test/unit/theory/theory_sets_type_enumerator_white.cpp +++ b/test/unit/theory/theory_sets_type_enumerator_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White box testing of CVC4::theory::sets::SetsTypeEnumerator + ** \brief White box testing of CVC5::theory::sets::SetsTypeEnumerator ** - ** White box testing of CVC4::theory::sets::SetsTypeEnumerator. (These tests + ** White box testing of CVC5::theory::sets::SetsTypeEnumerator. (These tests ** depends on the ordering that the SetsTypeEnumerator use, so it's a *white-box ** test.) @@ -21,7 +21,7 @@ #include "test_smt.h" #include "theory/sets/theory_sets_type_enumerator.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace kind; @@ -152,4 +152,4 @@ TEST_F(TestTheoryWhiteSetsTypeEnumerator, bv) ASSERT_TRUE(setEnumerator.isFinished()); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp index b6bda5564..22b0a09d6 100644 --- a/test/unit/theory/theory_sets_type_rules_white.cpp +++ b/test/unit/theory/theory_sets_type_rules_white.cpp @@ -16,9 +16,9 @@ #include "test_api.h" #include "test_node.h" -namespace CVC4 { +namespace CVC5 { -using namespace CVC4::api; +using namespace CVC5::api; namespace test { @@ -83,4 +83,4 @@ TEST_F(TestTheoryWhiteSetsTypeRuleInternal, singleton_node) ASSERT_TRUE(n.isConst()); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp index 64ebe2b97..06a86b844 100644 --- a/test/unit/theory/theory_strings_skolem_cache_black.cpp +++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp @@ -20,7 +20,7 @@ #include "util/rational.h" #include "util/string.h" -namespace CVC4 { +namespace CVC5 { using namespace theory::strings; @@ -59,4 +59,4 @@ TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached) } } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_strings_word_white.cpp b/test/unit/theory/theory_strings_word_white.cpp index 5e5c57053..03b9ed4c2 100644 --- a/test/unit/theory/theory_strings_word_white.cpp +++ b/test/unit/theory/theory_strings_word_white.cpp @@ -20,7 +20,7 @@ #include "test_node.h" #include "theory/strings/word.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace theory::strings; @@ -121,4 +121,4 @@ TEST_F(TestTheoryWhiteStringsWord, strings) ASSERT_TRUE(Word::roverlap(aaaaa, aa) == 2); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/theory_white.cpp b/test/unit/theory/theory_white.cpp index 048fac5ac..41abdd6d1 100644 --- a/test/unit/theory/theory_white.cpp +++ b/test/unit/theory/theory_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Black box testing of CVC4::theory::Theory. + ** \brief Black box testing of CVC5::theory::Theory. ** - ** Black box testing of CVC4::theory::Theory. + ** Black box testing of CVC5::theory::Theory. **/ #include <memory> @@ -24,7 +24,7 @@ #include "theory/theory_engine.h" #include "util/resource_manager.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace expr; @@ -109,4 +109,4 @@ TEST_F(TestTheoryWhite, outputChannel) d_outputChannel.d_callHistory.clear(); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp index 538a608e8..2e018f9cf 100644 --- a/test/unit/theory/type_enumerator_white.cpp +++ b/test/unit/theory/type_enumerator_white.cpp @@ -9,9 +9,9 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White box testing of CVC4::theory::TypeEnumerator + ** \brief White box testing of CVC5::theory::TypeEnumerator ** - ** White box testing of CVC4::theory::TypeEnumerator. (These tests depends + ** White box testing of CVC5::theory::TypeEnumerator. (These tests depends ** on the ordering that the TypeEnumerators use, so it's a white-box test.) **/ @@ -25,7 +25,7 @@ #include "test_smt.h" #include "theory/type_enumerator.h" -namespace CVC4 { +namespace CVC5 { using namespace theory; using namespace kind; @@ -332,4 +332,4 @@ TEST_F(TestTheoryWhiteTypeEnumerator, bv) ASSERT_THROW(*++te, NoMoreValuesException); } } // namespace test -} // namespace CVC4 +} // namespace CVC5 |