From c7ec792a2086c5b92c4a96d18f7cedb293712dfd Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 13 Jul 2020 00:43:45 -0500
Subject: Add support for string/sequence update (#4725)

This adds basic support for string/sequence updating, which has a semantics that is length preserving.
---
 src/theory/strings/word.cpp | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'src/theory/strings/word.cpp')

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>();
+    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();
-- 
cgit v1.2.3