diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-24 16:21:45 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-24 16:21:45 -0600 |
commit | b0fa6b29a1e15b231547eab147b49f2883a139de (patch) | |
tree | 6aa77261ea9d53d945d93b8847acade934a1a914 /test | |
parent | 9fbe415992986d33d09b3b9e5049ebc22d20790a (diff) |
Utilities for words (#3797)
This adds a utility file for handling operations over constant "words" (this will eventually generalize string or sequence constants). This is work towards CVC4/cvc4-projects#23.
Also improves documentation in regexp.h.
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/theory/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/theory/theory_strings_word_white.h | 149 |
2 files changed, 150 insertions, 0 deletions
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 02ca5d8b5..f20088ad1 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -10,5 +10,6 @@ cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory) cvc4_add_unit_test_white(theory_strings_rewriter_white theory) cvc4_add_unit_test_white(theory_strings_skolem_cache_black 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.h b/test/unit/theory/theory_strings_word_white.h new file mode 100644 index 000000000..d84df7836 --- /dev/null +++ b/test/unit/theory/theory_strings_word_white.h @@ -0,0 +1,149 @@ +/********************* */ +/*! \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-2019 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(opts); + d_smt = new SmtEngine(d_em); + d_scope = new SmtScope(d_smt); + + d_nm = NodeManager::currentNM(); + } + + 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")); + + TS_ASSERT(Word::mkEmptyWord(kind::CONST_STRING) == empty); + + std::vector<Node> vec; + vec.push_back(abc); + Node abcMk = Word::mkWord(vec); + TS_ASSERT_EQUALS(abc, abcMk); + vec.push_back(a); + Node abcaMk = Word::mkWord(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; +}; |