From: Aina Niemetz Date: Mon, 1 Mar 2021 09:00:46 +0000 (-0800) Subject: google test: theory: Migrate theory_strings_word_white. (#6003) X-Git-Tag: cvc5-1.0.0~2192 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bccce83987c0e3d3c1c829fe324cae534b292c87;p=cvc5.git google test: theory: Migrate theory_strings_word_white. (#6003) --- diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 790857d86..0d24da50b 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -26,6 +26,6 @@ cvc4_add_cxx_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_cxx_unit_test_white(theory_strings_skolem_cache_black theory) -cvc4_add_cxx_unit_test_white(theory_strings_word_white 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) diff --git a/test/unit/theory/theory_strings_word_white.cpp b/test/unit/theory/theory_strings_word_white.cpp new file mode 100644 index 000000000..ef5588020 --- /dev/null +++ b/test/unit/theory/theory_strings_word_white.cpp @@ -0,0 +1,124 @@ +/********************* */ +/*! \file theory_strings_word_white.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Unit tests for the strings word utilities + **/ + +#include +#include +#include + +#include "expr/node.h" +#include "test_node.h" +#include "theory/strings/word.h" + +namespace CVC4 { + +using namespace theory; +using namespace theory::strings; + +namespace test { + +class TestTheoryWhiteStringsWord : public TestNode +{ +}; + +TEST_F(TestTheoryWhiteStringsWord, strings) +{ + Node empty = d_nodeManager->mkConst(String("")); + Node a = d_nodeManager->mkConst(String("a")); + Node b = d_nodeManager->mkConst(String("b")); + Node aa = d_nodeManager->mkConst(String("aa")); + Node aaaaa = d_nodeManager->mkConst(String("aaaaa")); + Node abc = d_nodeManager->mkConst(String("abc")); + Node bbc = d_nodeManager->mkConst(String("bbc")); + Node cac = d_nodeManager->mkConst(String("cac")); + Node abca = d_nodeManager->mkConst(String("abca")); + + TypeNode stringType = d_nodeManager->stringType(); + ASSERT_TRUE(Word::mkEmptyWord(stringType) == empty); + + std::vector vec; + vec.push_back(abc); + Node abcMk = Word::mkWordFlatten(vec); + ASSERT_EQ(abc, abcMk); + vec.push_back(a); + Node abcaMk = Word::mkWordFlatten(vec); + ASSERT_EQ(abca, abcaMk); + + ASSERT_TRUE(Word::getLength(empty) == 0); + ASSERT_TRUE(Word::getLength(aaaaa) == 5); + + ASSERT_TRUE(Word::isEmpty(empty)); + ASSERT_FALSE(Word::isEmpty(a)); + + ASSERT_TRUE(Word::find(empty, empty) == 0); + ASSERT_TRUE(Word::find(a, empty) == 0); + ASSERT_TRUE(Word::find(empty, empty, 1) == std::string::npos); + ASSERT_TRUE(Word::find(cac, a, 0) == 1); + ASSERT_TRUE(Word::find(cac, abc) == std::string::npos); + + ASSERT_TRUE(Word::rfind(aaaaa, empty) == 0); + ASSERT_TRUE(Word::rfind(aaaaa, a) == 0); + ASSERT_TRUE(Word::rfind(abca, abc, 1) == 1); + + ASSERT_TRUE(Word::hasPrefix(empty, empty)); + ASSERT_TRUE(Word::hasPrefix(a, empty)); + ASSERT_TRUE(Word::hasPrefix(aaaaa, a)); + ASSERT_FALSE(Word::hasPrefix(abca, b)); + ASSERT_FALSE(Word::hasPrefix(empty, a)); + + ASSERT_TRUE(Word::hasSuffix(empty, empty)); + ASSERT_TRUE(Word::hasSuffix(a, empty)); + ASSERT_TRUE(Word::hasSuffix(a, a)); + ASSERT_FALSE(Word::hasSuffix(abca, b)); + ASSERT_FALSE(Word::hasSuffix(empty, abc)); + + ASSERT_EQ(bbc, Word::replace(abc, a, b)); + ASSERT_EQ(aaaaa, Word::replace(aaaaa, b, a)); + ASSERT_EQ(aa, Word::replace(a, empty, a)); + + ASSERT_EQ(empty, Word::substr(a, 1)); + ASSERT_EQ(empty, Word::substr(empty, 0)); + ASSERT_EQ(a, Word::substr(abca, 3)); + + ASSERT_EQ(a, Word::substr(abc, 0, 1)); + ASSERT_EQ(aa, Word::substr(aaaaa, 3, 2)); + + ASSERT_EQ(a, Word::prefix(a, 1)); + ASSERT_EQ(empty, Word::prefix(empty, 0)); + ASSERT_EQ(a, Word::prefix(aaaaa, 1)); + + ASSERT_EQ(a, Word::suffix(a, 1)); + ASSERT_EQ(empty, Word::suffix(empty, 0)); + ASSERT_EQ(aa, Word::suffix(aaaaa, 2)); + + ASSERT_FALSE(Word::noOverlapWith(abc, empty)); + ASSERT_TRUE(Word::noOverlapWith(cac, aa)); + ASSERT_FALSE(Word::noOverlapWith(cac, abc)); + ASSERT_TRUE(Word::noOverlapWith(cac, b)); + ASSERT_FALSE(Word::noOverlapWith(cac, a)); + ASSERT_FALSE(Word::noOverlapWith(abca, a)); + + ASSERT_TRUE(Word::overlap(abc, empty) == 0); + ASSERT_TRUE(Word::overlap(aaaaa, abc) == 1); + ASSERT_TRUE(Word::overlap(cac, abc) == 0); + ASSERT_TRUE(Word::overlap(empty, abc) == 0); + ASSERT_TRUE(Word::overlap(aaaaa, aa) == 2); + + ASSERT_TRUE(Word::roverlap(abc, empty) == 0); + ASSERT_TRUE(Word::roverlap(aaaaa, abc) == 0); + ASSERT_TRUE(Word::roverlap(cac, abc) == 1); + ASSERT_TRUE(Word::roverlap(empty, abc) == 0); + ASSERT_TRUE(Word::roverlap(aaaaa, aa) == 2); +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/theory/theory_strings_word_white.h b/test/unit/theory/theory_strings_word_white.h deleted file mode 100644 index ce432d385..000000000 --- a/test/unit/theory/theory_strings_word_white.h +++ /dev/null @@ -1,150 +0,0 @@ -/********************* */ -/*! \file theory_strings_word_white.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Unit tests for the strings word utilities - **/ - -#include "expr/node.h" -#include "expr/node_manager.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/strings/word.h" - -#include -#include -#include -#include - -using namespace CVC4; -using namespace CVC4::smt; -using namespace CVC4::theory; -using namespace CVC4::theory::strings; - -class TheoryStringsWordWhite : public CxxTest::TestSuite -{ - public: - TheoryStringsWordWhite() {} - - void setUp() override - { - Options opts; - opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); - d_em = new ExprManager; - d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_nm, &opts); - d_scope = new SmtScope(d_smt); - - } - - void tearDown() override - { - delete d_scope; - delete d_smt; - delete d_em; - } - - void testStrings() - { - Node empty = d_nm->mkConst(String("")); - Node a = d_nm->mkConst(String("a")); - Node b = d_nm->mkConst(String("b")); - Node aa = d_nm->mkConst(String("aa")); - Node aaaaa = d_nm->mkConst(String("aaaaa")); - Node abc = d_nm->mkConst(String("abc")); - Node bbc = d_nm->mkConst(String("bbc")); - Node cac = d_nm->mkConst(String("cac")); - Node abca = d_nm->mkConst(String("abca")); - - TypeNode stringType = d_nm->stringType(); - TS_ASSERT(Word::mkEmptyWord(stringType) == empty); - - std::vector vec; - vec.push_back(abc); - Node abcMk = Word::mkWordFlatten(vec); - TS_ASSERT_EQUALS(abc, abcMk); - vec.push_back(a); - Node abcaMk = Word::mkWordFlatten(vec); - TS_ASSERT_EQUALS(abca, abcaMk); - - TS_ASSERT(Word::getLength(empty) == 0); - TS_ASSERT(Word::getLength(aaaaa) == 5); - - TS_ASSERT(Word::isEmpty(empty)); - TS_ASSERT(!Word::isEmpty(a)); - - TS_ASSERT(Word::find(empty, empty) == 0); - TS_ASSERT(Word::find(a, empty) == 0); - TS_ASSERT(Word::find(empty, empty, 1) == std::string::npos); - TS_ASSERT(Word::find(cac, a, 0) == 1); - TS_ASSERT(Word::find(cac, abc) == std::string::npos); - - TS_ASSERT(Word::rfind(aaaaa, empty) == 0); - TS_ASSERT(Word::rfind(aaaaa, a) == 0); - TS_ASSERT(Word::rfind(abca, abc, 1) == 1); - - TS_ASSERT(Word::hasPrefix(empty, empty)); - TS_ASSERT(Word::hasPrefix(a, empty)); - TS_ASSERT(Word::hasPrefix(aaaaa, a)); - TS_ASSERT(!Word::hasPrefix(abca, b)); - TS_ASSERT(!Word::hasPrefix(empty, a)); - - TS_ASSERT(Word::hasSuffix(empty, empty)); - TS_ASSERT(Word::hasSuffix(a, empty)); - TS_ASSERT(Word::hasSuffix(a, a)); - TS_ASSERT(!Word::hasSuffix(abca, b)); - TS_ASSERT(!Word::hasSuffix(empty, abc)); - - TS_ASSERT_EQUALS(bbc, Word::replace(abc, a, b)); - TS_ASSERT_EQUALS(aaaaa, Word::replace(aaaaa, b, a)); - TS_ASSERT_EQUALS(aa, Word::replace(a, empty, a)); - - TS_ASSERT_EQUALS(empty, Word::substr(a, 1)); - TS_ASSERT_EQUALS(empty, Word::substr(empty, 0)); - TS_ASSERT_EQUALS(a, Word::substr(abca, 3)); - - TS_ASSERT_EQUALS(a, Word::substr(abc, 0, 1)); - TS_ASSERT_EQUALS(aa, Word::substr(aaaaa, 3, 2)); - - TS_ASSERT_EQUALS(a, Word::prefix(a, 1)); - TS_ASSERT_EQUALS(empty, Word::prefix(empty, 0)); - TS_ASSERT_EQUALS(a, Word::prefix(aaaaa, 1)); - - TS_ASSERT_EQUALS(a, Word::suffix(a, 1)); - TS_ASSERT_EQUALS(empty, Word::suffix(empty, 0)); - TS_ASSERT_EQUALS(aa, Word::suffix(aaaaa, 2)); - - TS_ASSERT(!Word::noOverlapWith(abc, empty)); - TS_ASSERT(Word::noOverlapWith(cac, aa)); - TS_ASSERT(!Word::noOverlapWith(cac, abc)); - TS_ASSERT(Word::noOverlapWith(cac, b)); - TS_ASSERT(!Word::noOverlapWith(cac, a)); - TS_ASSERT(!Word::noOverlapWith(abca, a)); - - TS_ASSERT(Word::overlap(abc, empty) == 0); - TS_ASSERT(Word::overlap(aaaaa, abc) == 1); - TS_ASSERT(Word::overlap(cac, abc) == 0); - TS_ASSERT(Word::overlap(empty, abc) == 0); - TS_ASSERT(Word::overlap(aaaaa, aa) == 2); - - TS_ASSERT(Word::roverlap(abc, empty) == 0); - TS_ASSERT(Word::roverlap(aaaaa, abc) == 0); - TS_ASSERT(Word::roverlap(cac, abc) == 1); - TS_ASSERT(Word::roverlap(empty, abc) == 0); - TS_ASSERT(Word::roverlap(aaaaa, aa) == 2); - } - - private: - ExprManager* d_em; - SmtEngine* d_smt; - SmtScope* d_scope; - - NodeManager* d_nm; -};