I don't know much about SMT solvers either, but my guess is that "simplification" would be a negligible part of the overall time since usually what people mean by "simplification" doesn't require any sort of search. This might be a premature optimization, especially since I doubt you'll find a ready to use library. On Thu, Apr 2, 2015 at 4:05 PM, Kenneth Adam Miller < kennethadammiller@gmail.com> wrote: > Well, the concern is that equivalent expressions that might arise in our > scenario be more difficult than they need to be. In expression > simplification, we keep the equivalent expression that is produced, > replacing the original. In this way then next time we feed that expression > input, or try to solve on it, we can get results for much less work. > > Am I right? I'm not too too familiar with SMT solvers-it's a different, > highly specialized field, so I just need to use them for my purposes. > > On Thu, Apr 2, 2015 at 3:57 PM, Ashish Agarwal > wrote: > >> > 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? >>>>> >>>> >>>> >>> >> >