Reorder ITE rewrites (#6723)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 9 Jun 2021 19:53:31 +0000 (12:53 -0700)
committerGitHub <noreply@github.com>
Wed, 9 Jun 2021 19:53:31 +0000 (19:53 +0000)
commit10e9d697e5ac14f921215b2847bd9bc9c035215e
treed5621d35271a7ae39ea1542d9722dfabee4404ad
parent181a175839e3af50a8cf7f80adf635fe612aeaba
Reorder ITE rewrites (#6723)

Fixes #6717. Commit 11c1fba added some
new rewrites for ITE. Due to the new rewrites taking precedence over
existing rewrites, it could happen that some of the previous rewrites
did not apply anymore even though they would have further simplified the
ITE. In the example from the issue, (ite c c true) was rewritten to
(or (not T) T) instead of (ite T true true) and then true. The
commit fixes the issue by moving rewrites resulting in
conjunctions/disjunctions to the end.
src/theory/booleans/theory_bool_rewriter.cpp
test/regress/CMakeLists.txt
test/regress/regress0/bool/issue6717-ite-rewrite.smt2 [new file with mode: 0644]