Make lambda rewriter more robust (#3806)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 24 Feb 2020 15:46:47 +0000 (07:46 -0800)
committerGitHub <noreply@github.com>
Mon, 24 Feb 2020 15:46:47 +0000 (09:46 -0600)
commita431edc5eba8b04812768b475b240725fb07d8c6
treeafcd020e2e58b9a03f0c87b602c01fe0bcd2cc9d
parent6f379f2b83a28995aa77504da1931a598b54bcc0
Make lambda rewriter more robust (#3806)

The lambda rewriter was not robust to the case where the lambda of the
array representation contained a disequality, e.g. `not(x = 1))`. It
would process it as `ite(not(x = 1), true, false)` instead of `ite(x =
1, false, true)`, which meant that it wasn't able to turn it into an
array representation when checking const-ness. Additionally, the
rewriter had issues when the lambda was of the form `ite((= x c1), true,
(= y c2))` (after turning it into an array and then into a lambda)
because it is expecting the false branch of the `ite` to not contain `y`
variables, making it non-constant despite the array being constant. This
commit solves that issue by normalizing `ite(not(c), x, y) ---> ite(c,
y, x)`.
src/theory/booleans/theory_bool_rewriter.cpp
src/theory/builtin/theory_builtin_rewriter.cpp
test/regress/CMakeLists.txt
test/regress/regress0/aufbv/issue3737.smt2 [new file with mode: 0644]