projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5a2f629) | patch
Expand `seq.nth` lazily (#5287)
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 20 Oct 2020 00:44:12 +0000 (17:44 -0700)
committerGitHub <noreply@github.com>
Tue, 20 Oct 2020 00:44:12 +0000 (19:44 -0500)
commit96c6ec71ccdde72c6cbc850df94c8965cda8d7db
tree511d4d38af86ed097b88d62d0454c31bd2465d9ftree
parent5a2f629f138f31e27965ede4884284437e30e801commit | 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.
src/theory/strings/extf_solver.cpp diff | blob | history
src/theory/strings/sequences_rewriter.cpp diff | blob | history
src/theory/strings/term_registry.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history
src/theory/strings/theory_strings_utils.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/seq/seq-nth-undef-unsat.smt2 [new file with mode: 0644] blob
test/regress/regress0/seq/seq-nth-undef.smt2 [deleted file] blob | history
test/regress/regress0/seq/seq-nth.smt2 diff | blob | history
test/regress/regress0/seq/seq-types.smt2 [new file with mode: 0644] blob