From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 425307FCF0 for ; Thu, 2 Apr 2015 22:22:02 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of kennethadammiller@gmail.com) identity=pra; client-ip=209.85.214.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="kennethadammiller@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of kennethadammiller@gmail.com designates 209.85.214.171 as permitted sender) identity=mailfrom; client-ip=209.85.214.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="kennethadammiller@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ob0-f171.google.com) identity=helo; client-ip=209.85.214.171; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="postmaster@mail-ob0-f171.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0C6AADPox1VlKvWVdFcgkWBFVwFgxCyYY9xhX0CgUUHTAEBAQEBARIBAQEBBwsLCRIwhB4BAQEDARIRHQEbHQEDAQsGBQsDCioCAiEBAREBBQEcBhMih3gBAwkIDaksPjGLOIFrgneNJwoZJw1UhF4BAQEBBgEBAQEBFwEFDoocf4JHgjIHgmiBRQWUX4Q+gU2BHTqMQoJngX4SI4EMCYQtIjGCQwEBAQ X-IPAS-Result: A0C6AADPox1VlKvWVdFcgkWBFVwFgxCyYY9xhX0CgUUHTAEBAQEBARIBAQEBBwsLCRIwhB4BAQEDARIRHQEbHQEDAQsGBQsDCioCAiEBAREBBQEcBhMih3gBAwkIDaksPjGLOIFrgneNJwoZJw1UhF4BAQEBBgEBAQEBFwEFDoocf4JHgjIHgmiBRQWUX4Q+gU2BHTqMQoJngX4SI4EMCYQtIjGCQwEBAQ X-IronPort-AV: E=Sophos;i="5.11,512,1422918000"; d="scan'208";a="131376259" Received: from mail-ob0-f171.google.com ([209.85.214.171]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 02 Apr 2015 22:22:01 +0200 Received: by obbgh1 with SMTP id gh1so138906825obb.1 for ; Thu, 02 Apr 2015 13:21:59 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=7BGDYMYnyaE3DgiQvWSrvKb2sBHuZq+kDH0/r/EB1C4=; b=Uj0/s6Gk3PRfcxv3YRwkF44ZUMZXK/H2/v0JrKwzqFTiEm4bvQtR1OWbqwPA7/OqRW q5k+oKDKLpu5PC8iXjuj3alf496aaS4dZ9Ct8ydUyhpV7u10GzgYBPf3iNkWnRpoHUf2 Je3sq+RWtWbJlvcO1wo+Bg1OX28SAdcX1LqvHsX8s1i25s1vMvJjfMWLfLd5w5JcHdbO SUhlbOZPfrkPIeD1qLs9eJ7rKNjLO/7ISN1PamyEZ/zFN5PKL+AUKf86XvNDQ/DJRw5Y Ry2QRjWFrzAb7tnODfKhcI0MAlzfzn8xNhKOz4PkodnKUVbDy6NTUqaREj/bgjGBEfN1 etZw== MIME-Version: 1.0 X-Received: by 10.182.131.130 with SMTP id om2mr693017obb.70.1428006119827; Thu, 02 Apr 2015 13:21:59 -0700 (PDT) Received: by 10.202.185.8 with HTTP; Thu, 2 Apr 2015 13:21:59 -0700 (PDT) In-Reply-To: <40B65243-21FC-4F23-ABE7-711F20CC7370@ieee.org> References: <40B65243-21FC-4F23-ABE7-711F20CC7370@ieee.org> Date: Thu, 2 Apr 2015 16:21:59 -0400 Message-ID: From: Kenneth Adam Miller To: Ivan Gotovchits Cc: Ashish Agarwal , caml users Content-Type: multipart/alternative; boundary=089e01634b90826c510512c395ea Subject: Re: [Caml-list] Mathematical Expression Library --089e01634b90826c510512c395ea Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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=E2=80=99re trying to simplify is actually a B= AP=E2=80=99s BIL, > then there=E2=80=99re some optimizations in the `Bil` module. The most in= teresting > is constant folding and purging unused variables. You can also use fixpoi= nt > function to drive the optimization passes. > > In any case, even if it is not a BIL, you can look at BAP=E2=80=99s const= ant > 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 expressi= on >> 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. Wou= ld 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 perfor= mance >>>>> 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, a= nd, >>>>>> divide, multiply, modulus, composed recursively, and operations on t= he >>>>>> expression type, such as simplify? >>>>>> >>>>> >>>>> >>>> >>> >> > > --089e01634b90826c510512c395ea Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
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=E2=80=99re trying to simplify is actually a BAP= =E2=80=99s BIL, then there=E2=80=99re some optimizations in the `Bil` modul= e. The most interesting is constant folding and purging unused variables. Y= ou can also use fixpoint function to drive the optimization passes.=C2=A0

In any case, even if it is not a BIL, you can look = at BAP=E2=80=99s constant folder class.=C2=A0

Best= wishes
Ivan=C2=A0=

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

I don't know much about SMT solvers eit= her, but my guess is that "simplification" would be a negligible = part of the overall time since usually what people mean by "simplifica= tion" doesn't require any sort of search. This might be a prematur= e optimization, especially since I doubt you'll find a ready to use lib= rary.

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 simpl= ification, we keep the equivalent expression that is produced, replacing th= e original. In this way then next time we feed that expression input, or tr= y 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 diffe= rent, highly specialized field, so I just need to use them for my purposes.=

On Thu, Apr 2, 2015 at 3:57 PM, Ashish Agarwal <<= a href=3D"mailto:agarwal1975@gmail.com" target=3D"_blank">agarwal1975@gmail= .com> wrote:
>=C2=A0need to sim= plify 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 "simpli= fy" can be not so simple depending on the language and your needs.

On Thu, Apr 2, 2015 at 3:47 PM, Kenneth Adam Miller &l= t;kennetha= dammiller@gmail.com> wrote:
I predominantly need to simplify expressions before I sub= mit 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 simpli= fy function. Would it be better to cache the result of the simplify functio= n?

On T= hu, Apr 2, 2015 at 3:36 PM, Ashish Agarwal <agarwal1975@gmail.com&= gt; wrote:
If you= don't find anything else, maybe some of our old code from PADL 2010 ca= n help as a starting point [1]. Probably it'll be easier to put somethi= ng together from scratch, assuming you don't care about performance or = need variables.


On Thu, Apr 2, 2015 at 1:16 PM, Kenneth Adam Miller <= kennethada= mmiller@gmail.com> wrote:
<= div dir=3D"ltr">Is there a library somewhere where I can represent and simp= lify simple bit operation expressions? Add, subtract, exclusive or, or, and= , divide, multiply, modulus, composed recursively, and operations on the ex= pression type, such as simplify?







--089e01634b90826c510512c395ea--