diff options
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/base_solver.cpp | 5 | ||||
-rw-r--r-- | src/theory/strings/kinds | 6 | ||||
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 6 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.h | 10 | ||||
-rw-r--r-- | src/theory/strings/type_enumerator.cpp | 4 | ||||
-rw-r--r-- | src/theory/strings/word.cpp | 85 |
6 files changed, 54 insertions, 62 deletions
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 952f26691..00658d08b 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -95,10 +95,7 @@ void BaseSolver::checkInit() Node oval = prev.isConst() ? n : prev; Assert(oval.getKind() == SEQ_UNIT); s = oval[0]; - t = cchars[0] - .getConst<ExprSequence>() - .getSequence() - .getVec()[0]; + t = cchars[0].getConst<Sequence>().getVec()[0]; // oval is congruent (ignored) in this context d_congruent.insert(oval); } diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 96ba82a44..21a435152 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -76,9 +76,9 @@ enumerator SEQUENCE_TYPE \ "theory/strings/type_enumerator.h" constant CONST_SEQUENCE \ - ::CVC4::ExprSequence \ - ::CVC4::ExprSequenceHashFunction \ - "expr/expr_sequence.h" \ + ::CVC4::Sequence \ + ::CVC4::SequenceHashFunction \ + "expr/sequence.h" \ "a sequence of characters" operator SEQ_UNIT 1 "a sequence of length one" diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index bb0fa1d97..110864c3b 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -3237,10 +3237,10 @@ Node SequencesRewriter::rewriteSeqUnit(Node node) NodeManager* nm = NodeManager::currentNM(); if (node[0].isConst()) { - std::vector<Expr> seq; - seq.push_back(node[0].toExpr()); + std::vector<Node> seq; + seq.push_back(node[0]); TypeNode stype = node[0].getType(); - Node ret = nm->mkConst(ExprSequence(stype.toType(), seq)); + Node ret = nm->mkConst(Sequence(stype, seq)); return returnRewrite(node, ret, Rewrite::SEQ_UNIT_EVAL); } return node; diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 192b4fd34..78b925ebe 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -20,7 +20,6 @@ #ifndef CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H #define CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H -#include "expr/expr_sequence.h" #include "expr/sequence.h" namespace CVC4 { @@ -330,8 +329,7 @@ class ConstSequenceTypeRule bool check) { Assert(n.getKind() == kind::CONST_SEQUENCE); - return nodeManager->mkSequenceType( - n.getConst<ExprSequence>().getSequence().getType()); + return nodeManager->mkSequenceType(n.getConst<Sequence>().getType()); } }; @@ -364,9 +362,9 @@ struct SequenceProperties { Assert(type.isSequence()); // empty sequence - std::vector<Expr> seq; - return NodeManager::currentNM()->mkConst(ExprSequence( - SequenceType(type.getSequenceElementType().toType()), seq)); + std::vector<Node> seq; + return NodeManager::currentNM()->mkConst( + Sequence(type.getSequenceElementType(), seq)); } }; /* struct SequenceProperties */ diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp index afedaed5c..ae88f63f7 100644 --- a/src/theory/strings/type_enumerator.cpp +++ b/src/theory/strings/type_enumerator.cpp @@ -211,7 +211,7 @@ bool SeqEnumLen::increment() void SeqEnumLen::mkCurr() { - std::vector<Expr> seq; + std::vector<Node> seq; const std::vector<unsigned>& data = d_witer->getData(); for (unsigned i : data) { @@ -220,7 +220,7 @@ void SeqEnumLen::mkCurr() } // make sequence from seq d_curr = NodeManager::currentNM()->mkConst( - ExprSequence(d_type.getSequenceElementType().toType(), seq)); + Sequence(d_type.getSequenceElementType(), seq)); } StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep) diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index fec567733..49221409e 100644 --- a/src/theory/strings/word.cpp +++ b/src/theory/strings/word.cpp @@ -32,9 +32,9 @@ Node Word::mkEmptyWord(TypeNode tn) } else if (tn.isSequence()) { - std::vector<Expr> seq; + std::vector<Node> seq; return NodeManager::currentNM()->mkConst( - ExprSequence(tn.getSequenceElementType().toType(), seq)); + Sequence(tn.getSequenceElementType(), seq)); } Unimplemented(); return Node::null(); @@ -59,20 +59,17 @@ Node Word::mkWordFlatten(const std::vector<Node>& xs) } else if (k == CONST_SEQUENCE) { - std::vector<Expr> seq; + std::vector<Node> seq; TypeNode tn = xs[0].getType(); for (TNode x : xs) { Assert(x.getType() == tn); - const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); const std::vector<Node>& vecc = sx.getVec(); - for (const Node& c : vecc) - { - seq.push_back(c.toExpr()); - } + seq.insert(seq.end(), vecc.begin(), vecc.end()); } return NodeManager::currentNM()->mkConst( - ExprSequence(tn.getSequenceElementType().toType(), seq)); + Sequence(tn.getSequenceElementType(), seq)); } Unimplemented(); return Node::null(); @@ -87,7 +84,7 @@ size_t Word::getLength(TNode x) } else if (k == CONST_SEQUENCE) { - return x.getConst<ExprSequence>().getSequence().size(); + return x.getConst<Sequence>().size(); } Unimplemented() << "Word::getLength on " << x; return 0; @@ -113,12 +110,12 @@ std::vector<Node> Word::getChars(TNode x) } else if (k == CONST_SEQUENCE) { - Type t = x.getConst<ExprSequence>().getType(); - const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + TypeNode t = x.getConst<Sequence>().getType(); + const Sequence& sx = x.getConst<Sequence>(); const std::vector<Node>& vec = sx.getVec(); for (const Node& v : vec) { - ret.push_back(nm->mkConst(ExprSequence(t, {v.toExpr()}))); + ret.push_back(nm->mkConst(Sequence(t, {v}))); } return ret; } @@ -141,8 +138,8 @@ bool Word::strncmp(TNode x, TNode y, std::size_t 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(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); return sx.strncmp(sy, n); } Unimplemented(); @@ -162,8 +159,8 @@ bool Word::rstrncmp(TNode x, TNode y, std::size_t 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(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); return sx.rstrncmp(sy, n); } Unimplemented(); @@ -183,8 +180,8 @@ std::size_t Word::find(TNode x, TNode y, std::size_t 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(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); return sx.find(sy, start); } Unimplemented(); @@ -204,8 +201,8 @@ std::size_t Word::rfind(TNode x, TNode y, std::size_t 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(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); return sx.rfind(sy, start); } Unimplemented(); @@ -225,8 +222,8 @@ bool Word::hasPrefix(TNode x, TNode y) else if (k == CONST_SEQUENCE) { Assert(y.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); return sx.hasPrefix(sy); } Unimplemented(); @@ -246,8 +243,8 @@ bool Word::hasSuffix(TNode x, TNode y) else if (k == CONST_SEQUENCE) { Assert(y.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); return sx.hasSuffix(sy); } Unimplemented(); @@ -271,11 +268,11 @@ Node Word::replace(TNode x, TNode y, TNode t) { 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(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); + const Sequence& st = t.getConst<Sequence>(); Sequence res = sx.replace(sy, st); - return nm->mkConst(res.toExprSequence()); + return nm->mkConst(res); } Unimplemented(); return Node::null(); @@ -291,9 +288,9 @@ Node Word::substr(TNode x, std::size_t i) } else if (k == CONST_SEQUENCE) { - const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); Sequence res = sx.substr(i); - return nm->mkConst(res.toExprSequence()); + return nm->mkConst(res); } Unimplemented(); return Node::null(); @@ -309,9 +306,9 @@ Node Word::substr(TNode x, std::size_t i, std::size_t j) } else if (k == CONST_SEQUENCE) { - const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); Sequence res = sx.substr(i, j); - return nm->mkConst(res.toExprSequence()); + return nm->mkConst(res); } Unimplemented(); return Node::null(); @@ -330,9 +327,9 @@ Node Word::suffix(TNode x, std::size_t i) } else if (k == CONST_SEQUENCE) { - const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); Sequence res = sx.suffix(i); - return nm->mkConst(res.toExprSequence()); + return nm->mkConst(res); } Unimplemented(); return Node::null(); @@ -351,8 +348,8 @@ bool Word::noOverlapWith(TNode x, TNode y) else if (k == CONST_SEQUENCE) { Assert(y.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); return sx.noOverlapWith(sy); } Unimplemented(); @@ -372,8 +369,8 @@ std::size_t Word::overlap(TNode x, TNode y) else if (k == CONST_SEQUENCE) { Assert(y.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); return sx.overlap(sy); } Unimplemented(); @@ -393,8 +390,8 @@ std::size_t Word::roverlap(TNode x, TNode y) else if (k == CONST_SEQUENCE) { Assert(y.getKind() == CONST_SEQUENCE); - const Sequence& sx = x.getConst<ExprSequence>().getSequence(); - const Sequence& sy = y.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); + const Sequence& sy = y.getConst<Sequence>(); return sx.roverlap(sy); } Unimplemented(); @@ -410,7 +407,7 @@ bool Word::isRepeated(TNode x) } else if (k == CONST_SEQUENCE) { - return x.getConst<ExprSequence>().getSequence().isRepeated(); + return x.getConst<Sequence>().isRepeated(); } Unimplemented(); return false; @@ -454,12 +451,12 @@ Node Word::reverse(TNode x) } else if (k == CONST_SEQUENCE) { - const Sequence& sx = x.getConst<ExprSequence>().getSequence(); + const Sequence& sx = x.getConst<Sequence>(); const std::vector<Node>& vecc = sx.getVec(); std::vector<Node> vecr(vecc.begin(), vecc.end()); std::reverse(vecr.begin(), vecr.end()); Sequence res(sx.getType(), vecr); - return nm->mkConst(res.toExprSequence()); + return nm->mkConst(res); } Unimplemented(); return Node::null(); |