projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5cd2630) | patch
Improve `STRINGS_ARRAY_UPDATE_BOUND` inference (#8123)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 18 Feb 2022 21:10:25 +0000 (13:10 -0800)
committerGitHub <noreply@github.com>
Fri, 18 Feb 2022 21:10:25 +0000 (21:10 +0000)
commit12fe80eff81db3d7b13cbd785061429b1c49c522
tree553a2264299f6aef3d448832e173a5a14418450atree
parent5cd263060e0b1e23937aaa2fa978794dbe81aee6commit | diff
Improve `STRINGS_ARRAY_UPDATE_BOUND` inference (#8123)

This changes the `STRINGS_ARRAY_UPDATE_BOUND` inference to explicitly
include the disequality between the term before and after the update if
the update has an effect. This is an optimization that prevents us from
splitting on that (dis-)equality later on.
src/theory/strings/array_core_solver.cpp diff | blob | history