## Simplifying long and messy expressions using Mathematica and Z3

(The following text has been copypasted to the SAT/SMT by example.)

... which can be results of Hex-Rays and/or manual rewriting.

I've added to my RE4B book about Wolfram Mathematica capabilities to minimize expressions: https://github.com/DennisYurichev/RE-for-beginners/blob/cd85356051937e87f90967cc272248084808223b/other/hexrays_EN.tex#L412.

Today I stumbled upon this Hex-Rays output:

if ( ( x != 7 || y!=0 ) && (x < 6 || x > 7) )
{
...
};


Both Mathematica and Z3 (using "simplify" command) can't make it shorter, but I've got gut feeling, that it's somewhat redundant.

Let's take a look at the right part of the expression. If $x$ must be less than 6 OR greater than 7, that it can hold any value except 6 AND 7, right? So I can rewrite this manually:

if ( ( x != 7 || y!=0 ) && x != 6 && x != 7) )
{
...
};


This is what Mathematica can simplify:

In[]:= BooleanMinimize[(x != 7 || y != 0) && (x != 6 && x != 7)]
Out[]:= x != 6 && x != 7


$y$ gets reduced.

But am I really right? And why Mathematica and Z3 didn't simplify this at first place?

I can use Z3 to prove that these expressions are equal to each other:

#!/usr/bin/env python

from z3 import *

x=Int('x')
y=Int('y')

s=Solver()

exp1=And(Or(x!=7, y!=0), Or(x<6, x>7))
exp2=And(x!=6, x!=7)

print simplify(exp1) # no luck

print s.check()
print s.model()


Z3 can't find counterexample, so it says "unsat", meaning, these expressions are equal to each other. So I've rewritten this expression in my code, tests has been passed, etc.

Yes, using both Mathematica and Z3 is overkill, and this is basic boolean algebra, but after ~10 hours of sitting at a computer you can make really dumb mistakes, and additional proof your piece of code is correct is never unwanted.

My other notes about SAT/SMT: https://yurichev.com/writings/SAT_SMT_draft-EN.pdf.