Hi Kenneth,

If the expression, that you’re trying to simplify is actually a BAP’s BIL, then there’re some optimizations in the `Bil` module. The most interesting is constant folding and purging unused variables. You can also use fixpoint function to drive the optimization passes. 

In any case, even if it is not a BIL, you can look at BAP’s constant folder class. 

Best wishes

Ivan 

On Apr 2, 2015, at 4:14 PM, Ashish Agarwal <agarwal1975@gmail.com> wrote:

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 <agarwal1975@gmail.com> 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 <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?