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?

On Thu, Apr 2, 2015 at 3:36 PM, Ashish Agarwal <agarwal1975@gmail.com>
wrote:

> If you don't find anything else, maybe some of our old code from PADL 2010
> can help as a starting point [1]. Probably it'll be easier to put something
> together from scratch, assuming you don't care about performance or need
> variables.
>
> [1] http://ashishagarwal.org/2010/01/18/automating-mp-transformations/
>
>
> On Thu, Apr 2, 2015 at 1:16 PM, Kenneth Adam Miller <
> kennethadammiller@gmail.com> wrote:
>
>> Is there a library somewhere where I can represent and simplify simple
>> bit operation expressions? Add, subtract, exclusive or, or, and, divide,
>> multiply, modulus, composed recursively, and operations on the expression
>> type, such as simplify?
>>
>
>