Add support for string/sequence update (#4725)

This adds basic support for string/sequence updating, which has a semantics that is length preserving.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 319257ac7d62522af5df2b8a5c8b6ad727f1c5a6..550dd760bd2f516a43dbdc3c3c53505ffab1aa90 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -256,6 +256,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> 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<Kind, CVC4::Kind, KindHashFunction> 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, Kind, CVC4::kind::KindHashFunction>
         {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 1f23d0e8d0b5f60483fd62df3f5761910501a6df..9e1ce3ecf7892d58dc4106950d014a51caa7669c 100644 (file)
--- 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<Term>& 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<Term>& 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<Term>& 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<Term>& 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 816b894e060e0e04cfbf92d7cf30ae49de5382d6..9ae19660be43b2ea5c1f7b05cc9e345fceef2a82 100644 (file)
--- 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<Node> 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 c3b7105921fede9e89ab18241e027a14d113b1f6..5a037752fda8b15709ff019c1a4364b4b3532a45 100644 (file)
--- 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 ec2009cc36799fb5d014d1e1cf10aba990a7c7f3..2e17d812c32318e148c9a33e1c1edc1a7946e35b 100644 (file)
--- 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 10357904a21c3a21993e65e7e853dd077ab711df..3eedee600702efae6f0d7838ad173bec684b72e2 100644 (file)
--- 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 852dede78723e7f0926154150951404fec325009..7a4940328fec68e03e15824d3220cb252d91d195 100644 (file)
--- 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 4ee2f4919bc357e70339f32b8451a32f0cdb6bc2..9b1b0e6dd747261993df5861c54d56624170e2bf 100644 (file)
--- 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<Node> 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 21a435152f496f5858c57a8e8e7809aa14b845ee..226dcbd1779e5f4c5c1d5e768b34c78ecc62e3cb 100644 (file)
--- 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<RRegExp>"
 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 68b510de6717138765998b906783a7ab6f82470d..6ea467ae9a64f1c490febe4c8405942c8f9fd27d 100644 (file)
--- 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 ccbdbc0cdff5efa4632f03c014670e721398eaec..bc5de3a8a6b417f827beab70f54db3ce7444063d 100644 (file)
--- 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 110864c3b20186ce7376b299b51c30bc8613a46d..292960e6a4c94d650b51d45716c8674d6ba9883c 100644 (file)
--- 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<Rational>() > 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<Rational>().sgn() < 0)
+      {
+        // start before the beginning of the string
+        return returnRewrite(node, s, Rewrite::UPD_CONST_INDEX_NEG);
+      }
+      uint32_t start =
+          node[1].getConst<Rational>().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 8da672cb559318ea8a705a3340f0f5455af62492..3251579ff0ec6bf1d596864c92f53acf5fe737ff 100644 (file)
--- 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 d21cf069d86c73cf90a81153a096322cf51b53ad..0b80db2ee1aa4fafbea9a8ea18e63446d3af0fec 100644 (file)
--- 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 942c8d216e50e36e6bb72104640d5d57cb1a6729..150ea89774dceb3725755b296ece481e8b925b09 100644 (file)
--- 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 af946567bbe17d8ac9cc951091819d33b62bfd7b..a752958b2397bae224ace36ef0584e17910c97f8 100644 (file)
--- 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 78b925ebe84092b7b8968a7c023cb9b5fa97d453..12ddb8a3dd667fc8801c35cb1767d5db70d90a11 100644 (file)
--- 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 49221409e5c4921b8458595a12c0b56c456fa634..63e3f1dba83af821dc8169fc67f58bff06698a5d 100644 (file)
--- 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>();
+    String st = t.getConst<String>();
+    return nm->mkConst(String(sx.update(i, st)));
+  }
+  else if (k == CONST_SEQUENCE)
+  {
+    Assert(t.getKind() == CONST_SEQUENCE);
+    const Sequence& sx = x.getConst<Sequence>();
+    const Sequence& st = t.getConst<Sequence>();
+    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 3b15b763ab679f0658187b7d426d43b4d31b2e87..bace06bfb5abc4ffa1a2b2ed652c5774b76b85d7 100644 (file)
--- 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 abe3b01e7449fefed4b0f0782ef13c266e98abab..44c4d3e4b21238aa5984c46b9ff64fcfcba80ca6 100644 (file)
--- 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<unsigned> 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<unsigned int> vec;
+    std::vector<unsigned> 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<unsigned int> ret_vec;
-  std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
+  std::vector<unsigned> ret_vec;
+  std::vector<unsigned>::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<unsigned int> ret_vec;
-  std::vector<unsigned int>::const_iterator itr = d_str.begin() + i;
+  std::vector<unsigned> ret_vec;
+  std::vector<unsigned>::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 700291aebdeea9fb8a67a7fddf3cdb417924430a..ca458232f832b9f244d26020fe9f21ce7956b34b 100644 (file)
--- 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 dd48b1ffff16a55208b492716f9c14756c0c9d20..c5048ae63583f89d34611db9b1ead8f48def58ba 100644 (file)
--- 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 (file)
index 0000000..deff4b6
--- /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 (file)
index 0000000..dedba68
--- /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 (file)
index 0000000..e21a2f4
--- /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 (file)
index 0000000..d28df85
--- /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)