summaryrefslogtreecommitdiff
path: root/src/theory/strings/rewrites.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-07-13 00:43:45 -0500
committerGitHub <noreply@github.com>2020-07-12 22:43:45 -0700
commitc7ec792a2086c5b92c4a96d18f7cedb293712dfd (patch)
treec88ebf889cb2f6aa6678154e1984bbe60a5b92b9 /src/theory/strings/rewrites.h
parent090d8bc3c31404140856e51d2cc5a5aa1335b3b3 (diff)
Add support for string/sequence update (#4725)
This adds basic support for string/sequence updating, which has a semantics that is length preserving.
Diffstat (limited to 'src/theory/strings/rewrites.h')
-rw-r--r--src/theory/strings/rewrites.h5
1 files changed, 5 insertions, 0 deletions
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,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback