search

trailofbits / manticore

Symbolic execution tool
https://blog.trailofbits.com/2017/04/27/manticore-symbolic-execution-for-humans/
GNU Affero General Public License v3.0
3.68k stars 472 forks source link

Add boolean simplifications #2563

Closed Boyan-MILANOV closed 2 years ago

Boyan-MILANOV commented 2 years ago

This PR adds the following simplification patterns on constraints that we often encounter within MATE:

!(a||b) -> !a && !b
!(a&&b) -> !a || !b
a == True -> a
a == False -> !a
1*a -> a
Boyan-MILANOV commented 2 years ago

Ready for review now. I've added tests for all new simplifications. The additions are minimal despite the long commit history.