From 30673d6ce9a5a1444b33fb11367914df0399e824 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 1 Jun 2020 09:14:23 -0500 Subject: Incorporate sequences into the word interface (#4543) Also renames a function mkWord -> mkWordFlatten. --- src/theory/strings/sequences_rewriter.cpp | 6 +- src/theory/strings/word.cpp | 138 ++++++++++++++++++++++++++- src/theory/strings/word.h | 4 +- test/unit/theory/theory_strings_word_white.h | 4 +- 4 files changed, 143 insertions(+), 9 deletions(-) diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 55d58b860..4f74d7c15 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -264,7 +264,7 @@ Node SequencesRewriter::rewriteStrEqualityExt(Node node) // Add a constant string to the side with more `cn`s to restore // the difference in number of `cn`s std::vector vec(diff, cn); - trimmed[j].push_back(Word::mkWord(vec)); + trimmed[j].push_back(Word::mkWordFlatten(vec)); } } @@ -602,7 +602,7 @@ Node SequencesRewriter::rewriteConcat(Node node) std::vector wvec; wvec.push_back(preNode); wvec.push_back(tmpNode[0]); - preNode = Word::mkWord(wvec); + preNode = Word::mkWordFlatten(wvec); node_vec.push_back(preNode); } else @@ -644,7 +644,7 @@ Node SequencesRewriter::rewriteConcat(Node node) std::vector vec; vec.push_back(preNode); vec.push_back(tmpNode); - preNode = Word::mkWord(vec); + preNode = Word::mkWordFlatten(vec); } } } diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index e9ab2652e..3f6a9de32 100644 --- a/src/theory/strings/word.cpp +++ b/src/theory/strings/word.cpp @@ -14,6 +14,7 @@ #include "theory/strings/word.h" +#include "expr/sequence.h" #include "util/string.h" using namespace CVC4::kind; @@ -28,23 +29,28 @@ Node Word::mkEmptyWord(TypeNode tn) { return mkEmptyWord(CONST_STRING); } + else if (tn.isSequence()) + { + std::vector seq; + return NodeManager::currentNM()->mkConst( + ExprSequence(tn.getSequenceElementType().toType(), seq)); + } Unimplemented(); return Node::null(); } Node Word::mkEmptyWord(Kind k) { - NodeManager* nm = NodeManager::currentNM(); if (k == CONST_STRING) { std::vector vec; - return nm->mkConst(String(vec)); + return NodeManager::currentNM()->mkConst(String(vec)); } Unimplemented(); return Node::null(); } -Node Word::mkWord(const std::vector& xs) +Node Word::mkWordFlatten(const std::vector& xs) { Assert(!xs.empty()); NodeManager* nm = NodeManager::currentNM(); @@ -61,6 +67,22 @@ Node Word::mkWord(const std::vector& xs) } return nm->mkConst(String(vec)); } + else if (k == CONST_SEQUENCE) + { + std::vector seq; + TypeNode tn = xs[0].getType(); + for (TNode x : xs) + { + Assert(x.getType() == tn); + const Sequence& sx = x.getConst().getSequence(); + const std::vector& vecc = sx.getVec(); + for (const Node& c : vecc) + { + seq.push_back(c.toExpr()); + } + } + return NodeManager::currentNM()->mkConst(ExprSequence(tn.toType(), seq)); + } Unimplemented(); return Node::null(); } @@ -72,6 +94,10 @@ size_t Word::getLength(TNode x) { return x.getConst().size(); } + else if (k == CONST_SEQUENCE) + { + return x.getConst().getSequence().size(); + } Unimplemented(); return 0; } @@ -111,6 +137,13 @@ bool Word::strncmp(TNode x, TNode y, std::size_t n) String sy = y.getConst(); return sx.strncmp(sy, n); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst().getSequence(); + const Sequence& sy = y.getConst().getSequence(); + return sx.strncmp(sy, n); + } Unimplemented(); return false; } @@ -125,6 +158,13 @@ bool Word::rstrncmp(TNode x, TNode y, std::size_t n) String sy = y.getConst(); return sx.rstrncmp(sy, n); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst().getSequence(); + const Sequence& sy = y.getConst().getSequence(); + return sx.rstrncmp(sy, n); + } Unimplemented(); return false; } @@ -139,6 +179,13 @@ std::size_t Word::find(TNode x, TNode y, std::size_t start) String sy = y.getConst(); return sx.find(sy, start); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst().getSequence(); + const Sequence& sy = y.getConst().getSequence(); + return sx.find(sy, start); + } Unimplemented(); return 0; } @@ -153,6 +200,13 @@ std::size_t Word::rfind(TNode x, TNode y, std::size_t start) String sy = y.getConst(); return sx.rfind(sy, start); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst().getSequence(); + const Sequence& sy = y.getConst().getSequence(); + return sx.rfind(sy, start); + } Unimplemented(); return 0; } @@ -167,6 +221,13 @@ bool Word::hasPrefix(TNode x, TNode y) String sy = y.getConst(); return sx.hasPrefix(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst().getSequence(); + const Sequence& sy = y.getConst().getSequence(); + return sx.hasPrefix(sy); + } Unimplemented(); return false; } @@ -181,6 +242,13 @@ bool Word::hasSuffix(TNode x, TNode y) String sy = y.getConst(); return sx.hasSuffix(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst().getSequence(); + const Sequence& sy = y.getConst().getSequence(); + return sx.hasSuffix(sy); + } Unimplemented(); return false; } @@ -198,6 +266,16 @@ Node Word::replace(TNode x, TNode y, TNode t) String st = t.getConst(); return nm->mkConst(String(sx.replace(sy, st))); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + Assert(t.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst().getSequence(); + const Sequence& sy = y.getConst().getSequence(); + const Sequence& st = t.getConst().getSequence(); + Sequence res = sx.replace(sy, st); + return nm->mkConst(res.toExprSequence()); + } Unimplemented(); return Node::null(); } @@ -210,6 +288,12 @@ Node Word::substr(TNode x, std::size_t i) String sx = x.getConst(); return nm->mkConst(String(sx.substr(i))); } + else if (k == CONST_SEQUENCE) + { + const Sequence& sx = x.getConst().getSequence(); + Sequence res = sx.substr(i); + return nm->mkConst(res.toExprSequence()); + } Unimplemented(); return Node::null(); } @@ -222,6 +306,12 @@ Node Word::substr(TNode x, std::size_t i, std::size_t j) String sx = x.getConst(); return nm->mkConst(String(sx.substr(i, j))); } + else if (k == CONST_SEQUENCE) + { + const Sequence& sx = x.getConst().getSequence(); + Sequence res = sx.substr(i, j); + return nm->mkConst(res.toExprSequence()); + } Unimplemented(); return Node::null(); } @@ -237,6 +327,12 @@ Node Word::suffix(TNode x, std::size_t i) String sx = x.getConst(); return nm->mkConst(String(sx.suffix(i))); } + else if (k == CONST_SEQUENCE) + { + const Sequence& sx = x.getConst().getSequence(); + Sequence res = sx.suffix(i); + return nm->mkConst(res.toExprSequence()); + } Unimplemented(); return Node::null(); } @@ -251,6 +347,13 @@ bool Word::noOverlapWith(TNode x, TNode y) String sy = y.getConst(); return sx.noOverlapWith(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst().getSequence(); + const Sequence& sy = y.getConst().getSequence(); + return sx.noOverlapWith(sy); + } Unimplemented(); return false; } @@ -265,6 +368,13 @@ std::size_t Word::overlap(TNode x, TNode y) String sy = y.getConst(); return sx.overlap(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst().getSequence(); + const Sequence& sy = y.getConst().getSequence(); + return sx.overlap(sy); + } Unimplemented(); return 0; } @@ -279,10 +389,32 @@ std::size_t Word::roverlap(TNode x, TNode y) String sy = y.getConst(); return sx.roverlap(sy); } + else if (k == CONST_SEQUENCE) + { + Assert(y.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst().getSequence(); + const Sequence& sy = y.getConst().getSequence(); + return sx.roverlap(sy); + } Unimplemented(); return 0; } +bool Word::isRepeated(TNode x) +{ + Kind k = x.getKind(); + if (k == CONST_STRING) + { + return x.getConst().isRepeated(); + } + else if (k == CONST_SEQUENCE) + { + return x.getConst().getSequence().isRepeated(); + } + Unimplemented(); + return false; +} + Node Word::splitConstant(TNode x, TNode y, size_t& index, bool isRev) { Assert(x.isConst() && y.isConst()); diff --git a/src/theory/strings/word.h b/src/theory/strings/word.h index b84ea6874..ad1d9bc74 100644 --- a/src/theory/strings/word.h +++ b/src/theory/strings/word.h @@ -37,7 +37,7 @@ class Word static Node mkEmptyWord(Kind k); /** make word from constants in (non-empty) vector vec */ - static Node mkWord(const std::vector& xs); + static Node mkWordFlatten(const std::vector& xs); /** Return the length of word x */ static size_t getLength(TNode x); @@ -139,6 +139,8 @@ class Word * Notice that x.overlap(y) = y.roverlap(x) */ static std::size_t roverlap(TNode x, TNode y); + /** Return true if word x is a repetition of the same character */ + static bool isRepeated(TNode x); /** Split constant * * This returns the suffix remainder (resp. prefix remainder when isRev is diff --git a/test/unit/theory/theory_strings_word_white.h b/test/unit/theory/theory_strings_word_white.h index d84df7836..6b594d904 100644 --- a/test/unit/theory/theory_strings_word_white.h +++ b/test/unit/theory/theory_strings_word_white.h @@ -67,10 +67,10 @@ class TheoryStringsWordWhite : public CxxTest::TestSuite std::vector vec; vec.push_back(abc); - Node abcMk = Word::mkWord(vec); + Node abcMk = Word::mkWordFlatten(vec); TS_ASSERT_EQUALS(abc, abcMk); vec.push_back(a); - Node abcaMk = Word::mkWord(vec); + Node abcaMk = Word::mkWordFlatten(vec); TS_ASSERT_EQUALS(abca, abcaMk); TS_ASSERT(Word::getLength(empty) == 0); -- cgit v1.2.3