> need to simplify expressions before I submit them to SMT solvers Why? Is the input language of the solver you're using not rich enough for your needs. The notion of "simplify" can be not so simple depending on the language and your needs. On Thu, Apr 2, 2015 at 3:47 PM, Kenneth Adam Miller < kennethadammiller@gmail.com> wrote: > 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 > 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? >>> >> >> >