Re: [Caml-list] Mathematical Expression Library

[Kenneth Adam Miller <kennethadammiller@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 3319 bytes --]

Excellent guess! Thank you once again!

On Thu, Apr 2, 2015 at 4:19 PM, Ivan Gotovchits <ivg@ieee.org> 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 <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?
>>>>>>
>>>>>
>>>>>
>>>>
>>>
>>
>
>

[-- Attachment #2: Type: text/html, Size: 5612 bytes --]