Excellent guess! Thank you once again! On Thu, Apr 2, 2015 at 4:19 PM, Ivan Gotovchits wrote: > 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 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 >> 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? >>>>>> >>>>> >>>>> >>>> >>> >> > >