summaryrefslogtreecommitdiff
path: root/src/theory/strings/word.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/word.cpp')
-rw-r--r--src/theory/strings/word.cpp138
1 files changed, 135 insertions, 3 deletions
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());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback