diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-13 00:43:45 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-12 22:43:45 -0700 |
| commit | c7ec792a2086c5b92c4a96d18f7cedb293712dfd (patch) | |
| tree | c88ebf889cb2f6aa6678154e1984bbe60a5b92b9 /src/theory/strings/extf_solver.cpp | |
| parent | 090d8bc3c31404140856e51d2cc5a5aa1335b3b3 (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/extf_solver.cpp')
| -rw-r--r-- | src/theory/strings/extf_solver.cpp | 12 |
1 files changed, 7 insertions, 5 deletions
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<Node> new_nodes; Node res = d_preproc.simplify(n, new_nodes); Assert(res != n); |