Send `nth(unit(...), ...)` terms to array solver (#7983)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 25 Jan 2022 17:46:20 +0000 (09:46 -0800)
committerGitHub <noreply@github.com>
Tue, 25 Jan 2022 17:46:20 +0000 (17:46 +0000)
commit0f15ebaeaa34b52e6bd3268cfc5cf411cad4a21f
tree6d35dba799f1a7faaeaae892cb252f6808b89e9d
parentb022fb999107870c07fad71944d916cfb6332f41
Send `nth(unit(...), ...)` terms to array solver (#7983)

This commit changes our policy of which terms we send to the array core
solver. Previously, we were not sending nth terms that
were applied to unit sequences. This was incorrect, because for example
the split STRINGS_ARRAY_EQ_SPLIT has to be applied to nth of units,
too, to guarantee model soundness: For example, if we have a disequality
nth(t1, i) != nth(unit(v), i), then we have to reason about the
(dis)equality of t1 and unit(v), because of the UF for the
out-of-bounds case of nth (i.e., we have to reason that Uf(t1, i) != Uf(unit(v), i), which requires t1 != unit(v)). Splitting on t1 = unit(v) is done by STRINGS_ARRAY_EQ_SPLIT.
src/theory/strings/array_solver.cpp
test/regress/CMakeLists.txt
test/regress/regress0/seq/nth-unit.smt2 [new file with mode: 0644]