From c7ec792a2086c5b92c4a96d18f7cedb293712dfd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 13 Jul 2020 00:43:45 -0500 Subject: [PATCH] Add support for string/sequence update (#4725) This adds basic support for string/sequence updating, which has a semantics that is length preserving. --- src/api/cvc4cpp.cpp | 4 ++ src/api/cvc4cppkind.h | 39 ++++++++++-- src/expr/sequence.cpp | 22 +++++++ src/expr/sequence.h | 2 + src/parser/smt2/smt2.cpp | 2 + src/printer/smt2/smt2_printer.cpp | 2 + src/theory/evaluator.cpp | 17 ++++++ src/theory/strings/extf_solver.cpp | 12 ++-- src/theory/strings/kinds | 2 + src/theory/strings/rewrites.cpp | 5 ++ src/theory/strings/rewrites.h | 5 ++ src/theory/strings/sequences_rewriter.cpp | 52 +++++++++++++++- src/theory/strings/sequences_rewriter.h | 6 ++ src/theory/strings/term_registry.cpp | 2 +- src/theory/strings/theory_strings.cpp | 1 + .../strings/theory_strings_preprocess.cpp | 59 +++++++++++++++++++ .../strings/theory_strings_type_rules.h | 32 ++++++++++ src/theory/strings/word.cpp | 22 +++++++ src/theory/strings/word.h | 3 + src/util/string.cpp | 31 ++++++++-- src/util/string.h | 2 + test/regress/CMakeLists.txt | 4 ++ test/regress/regress1/strings/update-ex1.smt2 | 8 +++ test/regress/regress1/strings/update-ex2.smt2 | 9 +++ test/regress/regress2/strings/update-ex3.smt2 | 13 ++++ .../regress2/strings/update-ex4-seq.smt2 | 11 ++++ 26 files changed, 351 insertions(+), 16 deletions(-) create mode 100644 test/regress/regress1/strings/update-ex1.smt2 create mode 100644 test/regress/regress1/strings/update-ex2.smt2 create mode 100644 test/regress/regress2/strings/update-ex3.smt2 create mode 100644 test/regress/regress2/strings/update-ex4-seq.smt2 diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 319257ac7..550dd760b 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -256,6 +256,7 @@ const static std::unordered_map s_kinds{ {STRING_IN_REGEXP, CVC4::Kind::STRING_IN_REGEXP}, {STRING_LENGTH, CVC4::Kind::STRING_LENGTH}, {STRING_SUBSTR, CVC4::Kind::STRING_SUBSTR}, + {STRING_UPDATE, CVC4::Kind::STRING_UPDATE}, {STRING_CHARAT, CVC4::Kind::STRING_CHARAT}, {STRING_CONTAINS, CVC4::Kind::STRING_STRCTN}, {STRING_INDEXOF, CVC4::Kind::STRING_STRIDOF}, @@ -294,6 +295,7 @@ const static std::unordered_map s_kinds{ {SEQ_CONCAT, CVC4::Kind::STRING_CONCAT}, {SEQ_LENGTH, CVC4::Kind::STRING_LENGTH}, {SEQ_EXTRACT, CVC4::Kind::STRING_SUBSTR}, + {SEQ_UPDATE, CVC4::Kind::STRING_UPDATE}, {SEQ_AT, CVC4::Kind::STRING_CHARAT}, {SEQ_CONTAINS, CVC4::Kind::STRING_STRCTN}, {SEQ_INDEXOF, CVC4::Kind::STRING_STRIDOF}, @@ -542,6 +544,7 @@ const static std::unordered_map {CVC4::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP}, {CVC4::Kind::STRING_LENGTH, STRING_LENGTH}, {CVC4::Kind::STRING_SUBSTR, STRING_SUBSTR}, + {CVC4::Kind::STRING_UPDATE, STRING_UPDATE}, {CVC4::Kind::STRING_CHARAT, STRING_CHARAT}, {CVC4::Kind::STRING_STRCTN, STRING_CONTAINS}, {CVC4::Kind::STRING_STRIDOF, STRING_INDEXOF}, @@ -1408,6 +1411,7 @@ Kind Term::getKindHelper() const case CVC4::Kind::STRING_CONCAT: return SEQ_CONCAT; case CVC4::Kind::STRING_LENGTH: return SEQ_LENGTH; case CVC4::Kind::STRING_SUBSTR: return SEQ_EXTRACT; + case CVC4::Kind::STRING_UPDATE: return SEQ_UPDATE; case CVC4::Kind::STRING_CHARAT: return SEQ_AT; case CVC4::Kind::STRING_STRCTN: return SEQ_CONTAINS; case CVC4::Kind::STRING_STRIDOF: return SEQ_INDEXOF; diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 1f23d0e8d..9e1ce3ecf 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -1971,6 +1971,21 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& children) */ STRING_SUBSTR, + /** + * String update. + * Updates a string s by replacing its context starting at an index with t. + * If the start index is negative, the start index is greater than the + * length of the string, the result is s. Otherwise, the length of the + * original string is preserved. + * Parameters: 3 + * -[1]: Term of sort String + * -[2]: Term of sort Integer (index i) + * -[3]: Term of sort String (replacement string t) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector& children) + */ + STRING_UPDATE, /** * String character at. * Returns the character at index i from a string s. If the index is negative @@ -2365,11 +2380,26 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector& children) */ SEQ_EXTRACT, + /** + * Sequence update. + * Updates a sequence s by replacing its context starting at an index with t. + * If the start index is negative, the start index is greater than the + * length of the sequence, the result is s. Otherwise, the length of the + * original sequence is preserved. + * Parameters: 3 + * -[1]: Term of sort Sequence + * -[2]: Term of sort Integer (index i) + * -[3]: Term of sort Sequence (replacement sequence t) + * Create with: + * mkTerm(Kind kind, Term child1, Term child2, Term child3) + * mkTerm(Kind kind, const std::vector& children) + */ + SEQ_UPDATE, /** * Sequence element at. * Returns the element at index i from a sequence s. If the index is negative - * or the index is greater or equal to the length of the sequence, the result is the - * empty sequence. Otherwise the result is a sequence of length 1. + * or the index is greater or equal to the length of the sequence, the result + * is the empty sequence. Otherwise the result is a sequence of length 1. * Parameters: 2 * -[1]: Term of sequence sort (string s) * -[2]: Term of sort Integer (index i) @@ -2405,8 +2435,9 @@ enum CVC4_PUBLIC Kind : int32_t SEQ_INDEXOF, /** * Sequence replace. - * Replaces the first occurrence of a sequence s2 in a sequence s1 with sequence s3. If s2 does not - * appear in s1, s1 is returned unmodified. Parameters: 3 + * Replaces the first occurrence of a sequence s2 in a sequence s1 with + * sequence s3. If s2 does not appear in s1, s1 is returned unmodified. + * Parameters: 3 * -[1]: Term of sort Sequence (sequence s1) * -[2]: Term of sort Sequence (sequence s2) * -[3]: Term of sort Sequence (sequence s3) diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp index 816b894e0..9ae19660b 100644 --- a/src/expr/sequence.cpp +++ b/src/expr/sequence.cpp @@ -280,6 +280,28 @@ bool Sequence::hasSuffix(const Sequence& y) const return true; } +Sequence Sequence::update(size_t i, const Sequence& t) const +{ + Assert(d_type == t.d_type); + if (i < size()) + { + std::vector vec(d_seq.begin(), d_seq.begin() + i); + size_t remNum = size() - i; + size_t tnum = t.d_seq.size(); + if (tnum >= remNum) + { + vec.insert(vec.end(), t.d_seq.begin(), t.d_seq.begin() + remNum); + } + else + { + vec.insert(vec.end(), t.d_seq.begin(), t.d_seq.end()); + vec.insert(vec.end(), d_seq.begin() + i + tnum, d_seq.end()); + } + return Sequence(getType(), vec); + } + return *this; +} + Sequence Sequence::replace(const Sequence& s, const Sequence& t) const { Assert(getType() == s.getType()); diff --git a/src/expr/sequence.h b/src/expr/sequence.h index c3b710592..5a037752f 100644 --- a/src/expr/sequence.h +++ b/src/expr/sequence.h @@ -83,6 +83,8 @@ class Sequence bool hasPrefix(const Sequence& y) const; /** Returns true if y is a suffix of this */ bool hasSuffix(const Sequence& y) const; + /** Replace the character at index i in this sequence with t */ + Sequence update(size_t i, const Sequence& t) const; /** Replace the first occurrence of s in this sequence with t */ Sequence replace(const Sequence& s, const Sequence& t) const; /** Return the subsequence of this sequence starting at index i */ diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ec2009cc3..2e17d812c 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -164,6 +164,7 @@ void Smt2::addStringOperators() { addOperator(api::STRING_REPLACE_RE_ALL, "str.replace_re_all"); if (!strictModeEnabled()) { + addOperator(api::STRING_UPDATE, "str.update"); addOperator(api::STRING_TOLOWER, "str.tolower"); addOperator(api::STRING_TOUPPER, "str.toupper"); addOperator(api::STRING_REV, "str.rev"); @@ -171,6 +172,7 @@ void Smt2::addStringOperators() { addOperator(api::SEQ_CONCAT, "seq.++"); addOperator(api::SEQ_LENGTH, "seq.len"); addOperator(api::SEQ_EXTRACT, "seq.extract"); + addOperator(api::SEQ_UPDATE, "seq.update"); addOperator(api::SEQ_AT, "seq.at"); addOperator(api::SEQ_CONTAINS, "seq.contains"); addOperator(api::SEQ_INDEXOF, "seq.indexof"); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 10357904a..3eedee600 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -629,6 +629,7 @@ void Smt2Printer::toStream(std::ostream& out, } case kind::STRING_LENGTH: case kind::STRING_SUBSTR: + case kind::STRING_UPDATE: case kind::STRING_CHARAT: case kind::STRING_STRCTN: case kind::STRING_STRIDOF: @@ -1195,6 +1196,7 @@ static string smtKindString(Kind k, Variant v) case kind::STRING_CONCAT: return "str.++"; case kind::STRING_LENGTH: return "str.len"; case kind::STRING_SUBSTR: return "str.substr" ; + case kind::STRING_UPDATE: return "str.update"; case kind::STRING_STRCTN: return "str.contains" ; case kind::STRING_CHARAT: return "str.at" ; case kind::STRING_STRIDOF: return "str.indexof" ; diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index 852dede78..7a4940328 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -507,6 +507,23 @@ EvalResult Evaluator::evalInternal( break; } + case kind::STRING_UPDATE: + { + const String& s = results[currNode[0]].d_str; + Integer s_len(s.size()); + Integer i = results[currNode[1]].d_rat.getNumerator(); + const String& t = results[currNode[2]].d_str; + + if (i.strictlyNegative() || i >= s_len) + { + results[currNode] = EvalResult(s); + } + else + { + results[currNode] = EvalResult(s.update(i.toUnsignedInt(), t)); + } + break; + } case kind::STRING_CHARAT: { const String& s = results[currNode[0]].d_str; diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 4ee2f4919..9b1b0e6dd 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -51,6 +51,7 @@ ExtfSolver::ExtfSolver(context::Context* c, d_reduced(u) { d_extt.addFunctionKind(kind::STRING_SUBSTR); + d_extt.addFunctionKind(kind::STRING_UPDATE); d_extt.addFunctionKind(kind::STRING_STRIDOF); d_extt.addFunctionKind(kind::STRING_ITOS); d_extt.addFunctionKind(kind::STRING_STOI); @@ -183,11 +184,12 @@ bool ExtfSolver::doReduction(int effort, Node n) else if (k != kind::STRING_TO_CODE) { NodeManager* nm = NodeManager::currentNM(); - Assert(k == STRING_SUBSTR || k == STRING_STRCTN || k == STRING_STRIDOF - || k == STRING_ITOS || k == STRING_STOI || k == STRING_STRREPL - || k == STRING_STRREPLALL || k == STRING_REPLACE_RE - || k == STRING_REPLACE_RE_ALL || k == STRING_LEQ - || k == STRING_TOLOWER || k == STRING_TOUPPER || k == STRING_REV); + Assert(k == STRING_SUBSTR || k == STRING_UPDATE || k == STRING_STRCTN + || k == STRING_STRIDOF || k == STRING_ITOS || k == STRING_STOI + || k == STRING_STRREPL || k == STRING_STRREPLALL + || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL + || k == STRING_LEQ || k == STRING_TOLOWER || k == STRING_TOUPPER + || k == STRING_REV); std::vector new_nodes; Node res = d_preproc.simplify(n, new_nodes); Assert(res != n); diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 21a435152..226dcbd17 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -16,6 +16,7 @@ operator STRING_CONCAT 2: "string concat (N-ary)" operator STRING_IN_REGEXP 2 "membership" operator STRING_LENGTH 1 "string length" operator STRING_SUBSTR 3 "string substr" +operator STRING_UPDATE 3 "string update" operator STRING_CHARAT 2 "string charat" operator STRING_STRCTN 2 "string contains" operator STRING_LT 2 "string less than" @@ -141,6 +142,7 @@ typerule REGEXP_SIGMA "SimpleTypeRule" typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule typerule STRING_LENGTH ::CVC4::theory::strings::StringStrToIntTypeRule typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule +typerule STRING_UPDATE ::CVC4::theory::strings::StringUpdateTypeRule typerule STRING_CHARAT ::CVC4::theory::strings::StringAtTypeRule typerule STRING_STRCTN ::CVC4::theory::strings::StringRelationTypeRule typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule diff --git a/src/theory/strings/rewrites.cpp b/src/theory/strings/rewrites.cpp index 68b510de6..6ea467ae9 100644 --- a/src/theory/strings/rewrites.cpp +++ b/src/theory/strings/rewrites.cpp @@ -139,6 +139,11 @@ const char* toString(Rewrite r) case Rewrite::SS_START_NEG: return "SS_START_NEG"; case Rewrite::SS_STRIP_END_PT: return "SS_STRIP_END_PT"; case Rewrite::SS_STRIP_START_PT: return "SS_STRIP_START_PT"; + case Rewrite::UPD_EVAL: return "UPD_EVAL"; + case Rewrite::UPD_EMPTYSTR: return "UPD_EMPTYSTR"; + case Rewrite::UPD_CONST_INDEX_MAX_OOB: return "UPD_CONST_INDEX_MAX_OOB"; + case Rewrite::UPD_CONST_INDEX_NEG: return "UPD_CONST_INDEX_NEG"; + case Rewrite::UPD_CONST_INDEX_OOB: return "UPD_CONST_INDEX_OOB"; case Rewrite::STOI_CONCAT_NONNUM: return "STOI_CONCAT_NONNUM"; case Rewrite::STOI_EVAL: return "STOI_EVAL"; case Rewrite::STR_CONV_CONST: return "STR_CONV_CONST"; diff --git a/src/theory/strings/rewrites.h b/src/theory/strings/rewrites.h index ccbdbc0cd..bc5de3a8a 100644 --- a/src/theory/strings/rewrites.h +++ b/src/theory/strings/rewrites.h @@ -142,6 +142,11 @@ enum class Rewrite : uint32_t SS_START_NEG, SS_STRIP_END_PT, SS_STRIP_START_PT, + UPD_EVAL, + UPD_EMPTYSTR, + UPD_CONST_INDEX_MAX_OOB, + UPD_CONST_INDEX_NEG, + UPD_CONST_INDEX_OOB, STOI_CONCAT_NONNUM, STOI_EVAL, STR_CONV_CONST, diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 110864c3b..292960e6a 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -570,9 +570,11 @@ Node SequencesRewriter::rewriteLength(Node node) return returnRewrite(node, retNode, Rewrite::LEN_REPL_INV); } } - else if (nk0 == STRING_TOLOWER || nk0 == STRING_TOUPPER || nk0 == STRING_REV) + else if (nk0 == STRING_TOLOWER || nk0 == STRING_TOUPPER || nk0 == STRING_REV + || nk0 == STRING_UPDATE) { // len( f( x ) ) == len( x ) where f is tolower, toupper, or rev. + // len( update( x, n, y ) ) = len( x ) Node retNode = nm->mkNode(STRING_LENGTH, node[0][0]); return returnRewrite(node, retNode, Rewrite::LEN_CONV_INV); } @@ -1406,6 +1408,10 @@ RewriteResponse SequencesRewriter::postRewrite(TNode node) { retNode = rewriteSubstr(node); } + else if (nk == kind::STRING_UPDATE) + { + retNode = rewriteUpdate(node); + } else if (nk == kind::STRING_STRCTN) { retNode = rewriteContains(node); @@ -1800,6 +1806,50 @@ Node SequencesRewriter::rewriteSubstr(Node node) return node; } +Node SequencesRewriter::rewriteUpdate(Node node) +{ + Assert(node.getKind() == kind::STRING_UPDATE); + Node s = node[0]; + if (s.isConst()) + { + if (Word::isEmpty(s)) + { + return returnRewrite(node, s, Rewrite::UPD_EMPTYSTR); + } + // rewriting for constant arguments + if (node[1].isConst()) + { + CVC4::Rational rMaxInt(String::maxSize()); + if (node[1].getConst() > rMaxInt) + { + // start beyond the maximum size of strings + // thus, it must be beyond the end point of this string + return returnRewrite(node, s, Rewrite::UPD_CONST_INDEX_MAX_OOB); + } + else if (node[1].getConst().sgn() < 0) + { + // start before the beginning of the string + return returnRewrite(node, s, Rewrite::UPD_CONST_INDEX_NEG); + } + uint32_t start = + node[1].getConst().getNumerator().toUnsignedInt(); + size_t len = Word::getLength(s); + if (start >= len) + { + // start beyond the end of the string + return returnRewrite(node, s, Rewrite::UPD_CONST_INDEX_OOB); + } + if (node[2].isConst()) + { + Node ret = Word::update(s, start, node[2]); + return returnRewrite(node, ret, Rewrite::UPD_EVAL); + } + } + } + + return node; +} + Node SequencesRewriter::rewriteContains(Node node) { Assert(node.getKind() == kind::STRING_STRCTN); diff --git a/src/theory/strings/sequences_rewriter.h b/src/theory/strings/sequences_rewriter.h index 8da672cb5..3251579ff 100644 --- a/src/theory/strings/sequences_rewriter.h +++ b/src/theory/strings/sequences_rewriter.h @@ -170,6 +170,12 @@ class SequencesRewriter : public TheoryRewriter * Returns the rewritten form of node. */ Node rewriteSubstr(Node node); + /** rewrite update + * This is the entry point for post-rewriting terms node of the form + * str.update( s, i1, i2 ) + * Returns the rewritten form of node. + */ + Node rewriteUpdate(Node node); /** rewrite contains * This is the entry point for post-rewriting terms node of the form * str.contains( t, s ) diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index d21cf069d..0b80db2ee 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -140,7 +140,7 @@ void TermRegistry::preRegisterTerm(TNode n) || k == STRING_STRREPL || k == STRING_STRREPLALL || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL || k == STRING_STRCTN || k == STRING_LEQ || k == STRING_TOLOWER - || k == STRING_TOUPPER || k == STRING_REV) + || k == STRING_TOUPPER || k == STRING_REV || k == STRING_UPDATE) { std::stringstream ss; ss << "Term of kind " << k diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 942c8d216..150ea8977 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -86,6 +86,7 @@ TheoryStrings::TheoryStrings(context::Context* c, d_equalityEngine.addFunctionKind(kind::STRING_STRCTN); d_equalityEngine.addFunctionKind(kind::STRING_LEQ); d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR); + d_equalityEngine.addFunctionKind(kind::STRING_UPDATE); d_equalityEngine.addFunctionKind(kind::STRING_ITOS); d_equalityEngine.addFunctionKind(kind::STRING_STOI); d_equalityEngine.addFunctionKind(kind::STRING_STRIDOF); diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index af946567b..a752958b2 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -114,6 +114,65 @@ Node StringsPreprocess::reduce(Node t, // Thus, substr( s, n, m ) = skt retNode = skt; } + else if (t.getKind() == kind::STRING_UPDATE) + { + // processing term: update( s, n, r ) + Node s = t[0]; + Node n = t[1]; + Node r = t[2]; + Node skt = sc->mkSkolemCached(t, SkolemCache::SK_PURIFY, "sst"); + Node ls = nm->mkNode(STRING_LENGTH, s); + // start point is greater than or equal zero + Node c1 = nm->mkNode(GEQ, n, zero); + // start point is less than end of string + Node c2 = nm->mkNode(GT, ls, n); + Node cond = nm->mkNode(AND, c1, c2); + + // substr(r,0,|s|-n) + Node lens = nm->mkNode(STRING_LENGTH, s); + Node rs; + if (r.isConst() && Word::getLength(r) == 1) + { + // optimization: don't need to take substring for single characters, due + // to guard on where it is used in the reduction below. + rs = r; + } + else + { + rs = nm->mkNode(STRING_SUBSTR, r, zero, nm->mkNode(MINUS, lens, n)); + } + Node rslen = nm->mkNode(STRING_LENGTH, rs); + Node nsuf = nm->mkNode(PLUS, n, rslen); + // substr(s, n, len(substr(r,0,|s|-n))), which is used for formalizing the + // purification variable sk3 below. + Node ssubstr = nm->mkNode(STRING_SUBSTR, s, n, rslen); + + Node sk1 = sc->mkSkolemCached(s, n, SkolemCache::SK_PREFIX, "sspre"); + Node sk2 = + sc->mkSkolemCached(s, nsuf, SkolemCache::SK_SUFFIX_REM, "sssufr"); + Node sk3 = sc->mkSkolemCached(ssubstr, SkolemCache::SK_PURIFY, "ssubstr"); + Node a1 = skt.eqNode(nm->mkNode(STRING_CONCAT, sk1, rs, sk2)); + Node a2 = s.eqNode(nm->mkNode(STRING_CONCAT, sk1, sk3, sk2)); + // length of first skolem is second argument + Node a3 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n); + + Node b1 = nm->mkNode(AND, a1, a2, a3); + Node b2 = skt.eqNode(s); + Node lemma = nm->mkNode(ITE, cond, b1, b2); + + // assert: + // IF n >=0 AND n < len( s ) + // THEN: skt = sk1 ++ substr(r,0,len(s)-n) ++ sk2 AND + // s = sk1 ++ sk3 ++ sk2 AND + // len( sk1 ) = n + // ELSE: skt = s + // We use an optimization where r is used instead of substr(r,0,len(s)-n) + // if r is a constant of length one. + asserts.push_back(lemma); + + // Thus, str.update( s, n, r ) = skt + retNode = skt; + } else if (t.getKind() == kind::STRING_STRIDOF) { // processing term: indexof( x, y, n ) diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 78b925ebe..12ddb8a3d 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -95,6 +95,38 @@ class StringSubstrTypeRule } }; +class StringUpdateTypeRule +{ + public: + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) + { + TypeNode t = n[0].getType(check); + if (check) + { + if (!t.isStringLike()) + { + throw TypeCheckingExceptionPrivate( + n, "expecting a string-like term in update"); + } + TypeNode t2 = n[1].getType(check); + if (!t2.isInteger()) + { + throw TypeCheckingExceptionPrivate( + n, "expecting an integer start term in update"); + } + t2 = n[2].getType(check); + if (!t2.isStringLike()) + { + throw TypeCheckingExceptionPrivate( + n, "expecting an string-like replace term in update"); + } + } + return t; + } +}; + class StringAtTypeRule { public: diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index 49221409e..63e3f1dba 100644 --- a/src/theory/strings/word.cpp +++ b/src/theory/strings/word.cpp @@ -251,6 +251,28 @@ bool Word::hasSuffix(TNode x, TNode y) return false; } +Node Word::update(TNode x, std::size_t i, TNode t) +{ + NodeManager* nm = NodeManager::currentNM(); + Kind k = x.getKind(); + if (k == CONST_STRING) + { + Assert(t.getKind() == CONST_STRING); + String sx = x.getConst(); + String st = t.getConst(); + return nm->mkConst(String(sx.update(i, st))); + } + else if (k == CONST_SEQUENCE) + { + Assert(t.getKind() == CONST_SEQUENCE); + const Sequence& sx = x.getConst(); + const Sequence& st = t.getConst(); + Sequence res = sx.update(i, st); + return nm->mkConst(res); + } + Unimplemented(); + return Node::null(); +} Node Word::replace(TNode x, TNode y, TNode t) { NodeManager* nm = NodeManager::currentNM(); diff --git a/src/theory/strings/word.h b/src/theory/strings/word.h index 3b15b763a..bace06bfb 100644 --- a/src/theory/strings/word.h +++ b/src/theory/strings/word.h @@ -80,6 +80,9 @@ class Word /** Returns true if y is a suffix of x */ static bool hasSuffix(TNode x, TNode y); + /** Replace the character at index n in x with t */ + static Node update(TNode x, std::size_t n, TNode t); + /** Replace the first occurrence of y in x with t */ static Node replace(TNode x, TNode y, TNode t); diff --git a/src/util/string.cpp b/src/util/string.cpp index abe3b01e7..44c4d3e4b 100644 --- a/src/util/string.cpp +++ b/src/util/string.cpp @@ -401,10 +401,31 @@ bool String::hasSuffix(const String& y) const return true; } +String String::update(std::size_t i, const String& t) const +{ + if (i < size()) + { + std::vector vec(d_str.begin(), d_str.begin() + i); + size_t remNum = size() - i; + size_t tnum = t.d_str.size(); + if (tnum >= remNum) + { + vec.insert(vec.end(), t.d_str.begin(), t.d_str.begin() + remNum); + } + else + { + vec.insert(vec.end(), t.d_str.begin(), t.d_str.end()); + vec.insert(vec.end(), d_str.begin() + i + tnum, d_str.end()); + } + return String(vec); + } + return *this; +} + String String::replace(const String &s, const String &t) const { std::size_t ret = find(s); if (ret != std::string::npos) { - std::vector vec; + std::vector vec; vec.insert(vec.begin(), d_str.begin(), d_str.begin() + ret); vec.insert(vec.end(), t.d_str.begin(), t.d_str.end()); vec.insert(vec.end(), d_str.begin() + ret + s.size(), d_str.end()); @@ -416,16 +437,16 @@ String String::replace(const String &s, const String &t) const { String String::substr(std::size_t i) const { Assert(i <= size()); - std::vector ret_vec; - std::vector::const_iterator itr = d_str.begin() + i; + std::vector ret_vec; + std::vector::const_iterator itr = d_str.begin() + i; ret_vec.insert(ret_vec.end(), itr, d_str.end()); return String(ret_vec); } String String::substr(std::size_t i, std::size_t j) const { Assert(i + j <= size()); - std::vector ret_vec; - std::vector::const_iterator itr = d_str.begin() + i; + std::vector ret_vec; + std::vector::const_iterator itr = d_str.begin() + i; ret_vec.insert(ret_vec.end(), itr, itr + j); return String(ret_vec); } diff --git a/src/util/string.h b/src/util/string.h index 700291aeb..ca458232f 100644 --- a/src/util/string.h +++ b/src/util/string.h @@ -139,6 +139,8 @@ class CVC4_PUBLIC String { bool hasPrefix(const String& y) const; /** Returns true if y is a suffix of this */ bool hasSuffix(const String& y) const; + /** Replace the character at index i in this string with t */ + String update(std::size_t i, const String& t) const; /** Replace the first occurrence of s in this string with t */ String replace(const String& s, const String& t) const; /** Return the substring of this string starting at index i */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index dd48b1fff..c5048ae63 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1871,6 +1871,8 @@ set(regress_1_tests regress1/strings/timeout-no-resp.smt2 regress1/strings/type002.smt2 regress1/strings/type003.smt2 + regress1/strings/update-ex1.smt2 + regress1/strings/update-ex2.smt2 regress1/strings/username_checker_min.smt2 regress1/sygus-abduct-ex1-grammar.smt2 regress1/sygus-abduct-test.smt2 @@ -2113,6 +2115,8 @@ set(regress_2_tests regress2/strings/replaceall-diffrange.smt2 regress2/strings/replaceall-len-c.smt2 regress2/strings/small-1.smt2 + regress2/strings/update-ex3.smt2 + regress2/strings/update-ex4-seq.smt2 regress2/sygus/DRAGON_1.lus.sy regress2/sygus/MPwL_d1s3.sy regress2/sygus/array_sum_dd.sy diff --git a/test/regress/regress1/strings/update-ex1.smt2 b/test/regress/regress1/strings/update-ex1.smt2 new file mode 100644 index 000000000..deff4b6c2 --- /dev/null +++ b/test/regress/regress1/strings/update-ex1.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_SLIA) +(set-option :strings-exp true) +(set-info :status sat) +(declare-fun s () String) + +(assert (not (= (str.substr (str.update "AAAAAA" 1 s) 5 1) "A"))) + +(check-sat) diff --git a/test/regress/regress1/strings/update-ex2.smt2 b/test/regress/regress1/strings/update-ex2.smt2 new file mode 100644 index 000000000..dedba68b2 --- /dev/null +++ b/test/regress/regress1/strings/update-ex2.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_SLIA) +(set-option :strings-exp true) +(set-info :status unsat) +(declare-fun s () String) + +(assert (not (= (str.substr (str.update "AAAAAA" 1 s) 5 1) "A"))) +(assert (< (str.len s) 3)) + +(check-sat) diff --git a/test/regress/regress2/strings/update-ex3.smt2 b/test/regress/regress2/strings/update-ex3.smt2 new file mode 100644 index 000000000..e21a2f445 --- /dev/null +++ b/test/regress/regress2/strings/update-ex3.smt2 @@ -0,0 +1,13 @@ +(set-logic QF_SLIA) +(set-option :strings-exp true) +(set-info :status sat) +(declare-fun s () String) +(declare-fun x () Int) +(declare-fun y () Int) + +(assert (= s (str.update (str.update "ABCDEFG" x "ZZZ") y "X"))) +(assert (not (str.contains s "B"))) +(assert (not (str.contains s "D"))) +(assert (not (str.contains s "G"))) + +(check-sat) diff --git a/test/regress/regress2/strings/update-ex4-seq.smt2 b/test/regress/regress2/strings/update-ex4-seq.smt2 new file mode 100644 index 000000000..d28df8534 --- /dev/null +++ b/test/regress/regress2/strings/update-ex4-seq.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_SLIA) +(set-option :strings-exp true) +(set-info :status sat) +(declare-fun s () (Seq Int)) +(declare-fun x () Int) + +(assert (= s (seq.++ (seq.unit 0) (seq.unit 1) (seq.unit 7) (seq.unit 3) (seq.unit 4) (seq.unit 5)))) + +(assert (not (= s (seq.update s x (seq.unit x))))) + +(check-sat) -- 2.30.2