search

GaloisInc / what4

Symbolic formula representation and solver interaction library
155 stars 13 forks source link

Guard mux-pushing simplifications behind option #256

Closed RyanGlScott closed 6 months ago

RyanGlScott commented 9 months ago

Add pushMuxOps and pushMuxOpsOption. If this option is enabled, What4 will push certain ExprBuilder operations (e.g., zext) down to the branches of ite expressions. In some (but not all) circumstances, this can result in operations that are easier for SMT solvers to reason about.

kquick commented 6 months ago

To be clear, Macaw isn't yet making use of the new behavior, and by the time Macaw bumps its What4 submodule, the new behavior will be guarded behind an opt-in flag. As a result, Macaw's behavior won't change unless it specifically opts into the new behavior. (Indeed, this was the whole point of guarding this behavior behind a flag, as the new behavior proved problematic for certain use cases, such as in certain SAW proofs.)

Exactly the situation I was hoping for. We probably discussed this back then but I subsequently forgot. Thanks for the confirmation.