## Simplifying long and messy expressions using Mathematica and Z3

... 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/dennis714/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)
s.add(exp1!=exp2)
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.

→ [list of blog posts, my twitter/facebook]

##### The page last updated on 02-July-2017