summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/strings/sequences_rewriter.cpp6
-rw-r--r--src/theory/strings/word.cpp138
-rw-r--r--src/theory/strings/word.h4
3 files changed, 141 insertions, 7 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<Node> 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<Node> 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<Node> 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<Expr> 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<unsigned> vec;
- return nm->mkConst(String(vec));
+ return NodeManager::currentNM()->mkConst(String(vec));
}
Unimplemented();
return Node::null();
}
-Node Word::mkWord(const std::vector<Node>& xs)
+Node Word::mkWordFlatten(const std::vector<Node>& xs)
{
Assert(!xs.empty());
NodeManager* nm = NodeManager::currentNM();
@@ -61,6 +67,22 @@ Node Word::mkWord(const std::vector<Node>& xs)
}
return nm->mkConst(String(vec));
}
+ else if (k == CONST_SEQUENCE)
+ {
+ std::vector<Expr> seq;
+ TypeNode tn = xs[0].getType();
+ for (TNode x : xs)
+ {
+ Assert(x.getType() == tn);
+ const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+ const std::vector<Node>& 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<String>().size();
}
+ else if (k == CONST_SEQUENCE)
+ {
+ return x.getConst<ExprSequence>().getSequence().size();
+ }
Unimplemented();
return 0;
}
@@ -111,6 +137,13 @@ bool Word::strncmp(TNode x, TNode y, std::size_t n)
String sy = y.getConst<String>();
return sx.strncmp(sy, n);
}
+ else if (k == CONST_SEQUENCE)
+ {
+ Assert(y.getKind() == CONST_SEQUENCE);
+ const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+ const Sequence& sy = y.getConst<ExprSequence>().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<String>();
return sx.rstrncmp(sy, n);
}
+ else if (k == CONST_SEQUENCE)
+ {
+ Assert(y.getKind() == CONST_SEQUENCE);
+ const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+ const Sequence& sy = y.getConst<ExprSequence>().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<String>();
return sx.find(sy, start);
}
+ else if (k == CONST_SEQUENCE)
+ {
+ Assert(y.getKind() == CONST_SEQUENCE);
+ const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+ const Sequence& sy = y.getConst<ExprSequence>().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<String>();
return sx.rfind(sy, start);
}
+ else if (k == CONST_SEQUENCE)
+ {
+ Assert(y.getKind() == CONST_SEQUENCE);
+ const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+ const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+ return sx.rfind(sy, start);
+ }
Unimplemented();
return 0;
}
@@ -167,6 +221,13 @@ bool Word::hasPrefix(TNode x, TNode y)
String sy = y.getConst<String>();
return sx.hasPrefix(sy);
}
+ else if (k == CONST_SEQUENCE)
+ {
+ Assert(y.getKind() == CONST_SEQUENCE);
+ const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+ const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+ return sx.hasPrefix(sy);
+ }
Unimplemented();
return false;
}
@@ -181,6 +242,13 @@ bool Word::hasSuffix(TNode x, TNode y)
String sy = y.getConst<String>();
return sx.hasSuffix(sy);
}
+ else if (k == CONST_SEQUENCE)
+ {
+ Assert(y.getKind() == CONST_SEQUENCE);
+ const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+ const Sequence& sy = y.getConst<ExprSequence>().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<String>();
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<ExprSequence>().getSequence();
+ const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+ const Sequence& st = t.getConst<ExprSequence>().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<String>();
return nm->mkConst(String(sx.substr(i)));
}
+ else if (k == CONST_SEQUENCE)
+ {
+ const Sequence& sx = x.getConst<ExprSequence>().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<String>();
return nm->mkConst(String(sx.substr(i, j)));
}
+ else if (k == CONST_SEQUENCE)
+ {
+ const Sequence& sx = x.getConst<ExprSequence>().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<String>();
return nm->mkConst(String(sx.suffix(i)));
}
+ else if (k == CONST_SEQUENCE)
+ {
+ const Sequence& sx = x.getConst<ExprSequence>().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<String>();
return sx.noOverlapWith(sy);
}
+ else if (k == CONST_SEQUENCE)
+ {
+ Assert(y.getKind() == CONST_SEQUENCE);
+ const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+ const Sequence& sy = y.getConst<ExprSequence>().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<String>();
return sx.overlap(sy);
}
+ else if (k == CONST_SEQUENCE)
+ {
+ Assert(y.getKind() == CONST_SEQUENCE);
+ const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+ const Sequence& sy = y.getConst<ExprSequence>().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<String>();
return sx.roverlap(sy);
}
+ else if (k == CONST_SEQUENCE)
+ {
+ Assert(y.getKind() == CONST_SEQUENCE);
+ const Sequence& sx = x.getConst<ExprSequence>().getSequence();
+ const Sequence& sy = y.getConst<ExprSequence>().getSequence();
+ return sx.roverlap(sy);
+ }
Unimplemented();
return 0;
}
+bool Word::isRepeated(TNode x)
+{
+ Kind k = x.getKind();
+ if (k == CONST_STRING)
+ {
+ return x.getConst<String>().isRepeated();
+ }
+ else if (k == CONST_SEQUENCE)
+ {
+ return x.getConst<ExprSequence>().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<Node>& xs);
+ static Node mkWordFlatten(const std::vector<Node>& 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback