Add support for string/sequence update (#4725)

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

1 files changed, 17 insertions, 0 deletions

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;