google test: theory: Migrate theory_strings_word_white. (#6003)

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 790857d86c5371950742cbd5d2769047d19d0aa1..0d24da50be52ede05a22b037853d72d2dded6291 100644 (file)
--- 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 (file)
index 0000000..ef55880
--- /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 <iostream>
+#include <memory>
+#include <vector>
+
+#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<Node> 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 (file)
index ce432d3..0000000
--- 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 <cxxtest/TestSuite.h>
-#include <iostream>
-#include <memory>
-#include <vector>
-
-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<Node> 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;
-};