diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-10-19 17:44:12 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-19 19:44:12 -0500 |
| commit | 96c6ec71ccdde72c6cbc850df94c8965cda8d7db (patch) | |
| tree | 511d4d38af86ed097b88d62d0454c31bd2465d9f /src/theory/strings/extf_solver.cpp | |
| parent | 5a2f629f138f31e27965ede4884284437e30e801 (diff) | |
Expand `seq.nth` lazily (#5287)
Our first support for seq.nth eliminated it eagerly during expandDefinitions.
This PR changes that, by eliminating it lazily, as done with other extended string operators.
Diffstat (limited to 'src/theory/strings/extf_solver.cpp')
| -rw-r--r-- | src/theory/strings/extf_solver.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 88edaeff7..53cd92ac2 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -65,6 +65,7 @@ ExtfSolver::ExtfSolver(SolverState& s, d_extt.addFunctionKind(kind::STRING_TOUPPER); d_extt.addFunctionKind(kind::STRING_REV); d_extt.addFunctionKind(kind::SEQ_UNIT); + d_extt.addFunctionKind(kind::SEQ_NTH); d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -188,7 +189,7 @@ bool ExtfSolver::doReduction(int effort, Node n) NodeManager* nm = NodeManager::currentNM(); 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_STRREPL || k == STRING_STRREPLALL || k == SEQ_NTH || k == STRING_REPLACE_RE || k == STRING_REPLACE_RE_ALL || k == STRING_LEQ || k == STRING_TOLOWER || k == STRING_TOUPPER || k == STRING_REV); |