Re: [Caml-list] Mathematical Expression Library

[Drup <drupyog+caml@zoho.com>]

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

If I may, "simplifications" on the formula (eliminating dead variables 
and constant folding for example) is completely unimportant. Z3 is going 
to do it for you.

The actual shape of your formula is much more important and you should 
care of that when generating your formula (while you still have semantic 
informations), not after it's done.

Le 02/04/2015 21:47, Kenneth Adam Miller a écrit :
> 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 
> <mailto: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 <mailto: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: 3540 bytes --]