[Caml-list] Mathematical Expression Library

[Caml-list] Mathematical Expression Library

[Kenneth Adam Miller]

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

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: 264 bytes --]

Re: [Caml-list] Mathematical Expression Library

[Ashish Agarwal]

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

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: 1097 bytes --]

Re: [Caml-list] Mathematical Expression Library

[Kenneth Adam Miller]

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

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: 1897 bytes --]

Re: [Caml-list] Mathematical Expression Library

[Ashish Agarwal]

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

> 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: 2746 bytes --]

Re: [Caml-list] Mathematical Expression Library

[Kenneth Adam Miller]

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

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: 3689 bytes --]

Re: [Caml-list] Mathematical Expression Library

[Ashish Agarwal]

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

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: 4444 bytes --]

Re: [Caml-list] Mathematical Expression Library

[Ivan Gotovchits]

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

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: 5270 bytes --]

Re: [Caml-list] Mathematical Expression Library

[Kenneth Adam Miller]

[-- 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 --]

Re: [Caml-list] Mathematical Expression Library

[Drup]

[-- 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 --]

Re: [Caml-list] Mathematical Expression Library

[Drup]

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


> Can you also explain in more depth your justification of Z3 doing 
> expression simplification on my behalf for anything submitted? That 
> was also my guess, but I didn't have that substantiated before my 
> colleagues, so I wanted to be thorough.
Knowledge of Z3, I guess ? It calls the simplification function (which 
is exposed as Z3.Expr.simplify in the ml-ng bindings) before solving. 
It's a bit more complicated when in the so-called "interactive" mode but 
still doing it. Note that the function is still useful when printing the 
formula for debugging purposes.

>
>     Shape?? I don't know what you mean.
>
I mean that, for a solver like Z3, two encodings of the same problem can 
result in different results (between UNSAT and UNKNOWN, in particular) 
and can result, and that's more sneaky, in completely different 
performance profiles. Solvers (and Z3 in particular) uses heuristics to 
know which branches to solve first so it's rather guess-y.

You mostly notice that when trying them though, it's rather pointless to 
try to guess in advance, since it's very implementation-sensible.

>
>     In any case, my plan was to use OCamlgraph and some hash-consing
>     to construct correspondingly equivalent semantics, then reason
>     about it in a distributed fashion.
>
If you are looking to encode an SSA control flow graph in Z3's SMT, I 
have the code to do that. I could extract it and get it into shape. It's 
based on llvm's IR, but It should be fairly reusable. Tell me if you are 
interested.



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

Re: [Caml-list] Mathematical Expression Library

[Markus Weißmann]

Just for completeness sake: There is also the "boolean expression 
simplifier" [1] library implementing the Quine-McCluskey algorithm (and 
friends) in pure OCaml.
I'd guess that a decent SMT solver will solve the "raw" expression much 
faster than running it through the simplifier and then solving it (with 
the same solver).

regards
Markus

[1] http://bes.forge.ocamlcore.org/

On 2015-04-02 19:16, Kenneth Adam Miller 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?

-- 
Markus Weißmann, M.Sc.
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
http://wwwknoll.in.tum.de/

Re: [Caml-list] Mathematical Expression Library

[Kenneth Adam Miller]

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

Thank you!

On Tue, Apr 7, 2015 at 2:37 AM, Markus Weißmann <markus.weissmann@in.tum.de>
wrote:

> Just for completeness sake: There is also the "boolean expression
> simplifier" [1] library implementing the Quine-McCluskey algorithm (and
> friends) in pure OCaml.
> I'd guess that a decent SMT solver will solve the "raw" expression much
> faster than running it through the simplifier and then solving it (with the
> same solver).
>
> regards
> Markus
>
> [1] http://bes.forge.ocamlcore.org/
>
>
> On 2015-04-02 19:16, Kenneth Adam Miller 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?
>>
>
> --
> Markus Weißmann, M.Sc.
> Technische Universität München
> Institut für Informatik
> Boltzmannstr. 3
> D-85748 Garching
> Germany
> http://wwwknoll.in.tum.de/
>
>
> --
> Caml-list mailing list.  Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>

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