If I may, "simplifications" on the
formula (eliminating dead variables and constant folding for
example) is completely unimportant. Z3 is going to do it for you.
The actual shape of your formula is much more important and you
should care of that when generating your formula (while you still
have semantic informations), not after it's done.
Le 02/04/2015 21:47, Kenneth Adam Miller a écrit :
I predominantly need to simplify expressions before
I submit them to SMT solvers. I'm quite concerned about not
reimplementing a difficult and already solved problem, and I'm
pretty sure that this is part of work of the solvers. I'm pretty
sure that Z3 provides a simplify function. Would it be better to
cache the result of the simplify function?