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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id ABF937FCEF for ; Thu, 2 Apr 2015 22:20:08 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of ivg@ieee.org) identity=pra; client-ip=209.85.220.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of ivg@ieee.org designates 209.85.220.48 as permitted sender) identity=mailfrom; client-ip=209.85.220.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.org"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-pa0-f48.google.com) identity=helo; client-ip=209.85.220.48; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="postmaster@mail-pa0-f48.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CmAABXox1VmzDcVdFcgkWBFVyyOQaDN49xhX0CgUxMAQEBAQEBEgEBAQEBBgsLCRQuhB4BAQEDARJnBQsLGC4hEwEFARwGEyKHeQMJCAMCCKksPjGeDA2FMgEBAQEBAQQBAQEBAQEBAQEZCoYFhBt/gkeCMgeDF4EWBZRfhD6BTYEdOoU3hwuCZ4F+NYEVhC1TgkMBAQE X-IPAS-Result: A0CmAABXox1VmzDcVdFcgkWBFVyyOQaDN49xhX0CgUxMAQEBAQEBEgEBAQEBBgsLCRQuhB4BAQEDARJnBQsLGC4hEwEFARwGEyKHeQMJCAMCCKksPjGeDA2FMgEBAQEBAQQBAQEBAQEBAQEZCoYFhBt/gkeCMgeDF4EWBZRfhD6BTYEdOoU3hwuCZ4F+NYEVhC1TgkMBAQE X-IronPort-AV: E=Sophos;i="5.11,512,1422918000"; d="scan'208,217";a="108164466" Received: from mail-pa0-f48.google.com ([209.85.220.48]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 02 Apr 2015 22:20:07 +0200 Received: by pactp5 with SMTP id tp5so94175145pac.1 for ; Thu, 02 Apr 2015 13:20:05 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:content-type:mime-version:subject:from :in-reply-to:date:cc:message-id:references:to; bh=NT0c7N4i6Tig0SqabqODHqWwnIHBhpWT6z+rgtUuub8=; b=UaaQmolg62ZqYZ52SPq63Qb1FIowr6M35DJ+TSXd5bmm/NHc1KtL9EoykqXKgByn2X zG8U0HMgqapNP2sS5NVYPu4a+gk3pO/XhV8faaSk5UIA67ZaUNi1/zqj5rDtAQaVKUlH xggI3wrc0DBEOAVR0HD/lvXKfRm0LEFCAR9m3O2JKxuF6my+WQs7iuKAKiec7yBOBVdG tBMcJMOCo/9vDLzrolwRsKwPAyy+sPTdhxuypVUOst0aBz/YRKDcK5jzDaB9ZuNnxucg ej4K5vd3180wrDuV0jzhC1JFSfCB01NUgRnf7fDs4Idpc6pyFOWRjJDmHOJbMvB3TV6H rOTA== X-Gm-Message-State: ALoCoQmCXsGuX/rh1h/DgVLLMkumzpA2xKn5kZP8DYNvdbmaguANIDNL9S6oW8c5OsNmDxaIEORz X-Received: by 10.70.0.176 with SMTP id 16mr91082273pdf.78.1428006005345; Thu, 02 Apr 2015 13:20:05 -0700 (PDT) Received: from [10.70.105.63] ([38.127.159.5]) by mx.google.com with ESMTPSA id cr1sm6084215pdb.7.2015.04.02.13.20.02 (version=TLSv1 cipher=ECDHE-RSA-RC4-SHA bits=128/128); Thu, 02 Apr 2015 13:20:04 -0700 (PDT) Content-Type: multipart/alternative; boundary="Apple-Mail=_BE3A434E-485B-4F6B-BC45-B5BBF1B6AA41" Mime-Version: 1.0 (Mac OS X Mail 7.3 \(1878.6\)) From: Ivan Gotovchits In-Reply-To: Date: Thu, 2 Apr 2015 16:19:58 -0400 Cc: Kenneth Adam Miller , caml users Message-Id: <40B65243-21FC-4F23-ABE7-711F20CC7370@ieee.org> References: To: Ashish Agarwal X-Mailer: Apple Mail (2.1878.6) Subject: Re: [Caml-list] Mathematical Expression Library --Apple-Mail=_BE3A434E-485B-4F6B-BC45-B5BBF1B6AA41 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=windows-1252 Hi Kenneth, If the expression, that you=92re trying to simplify is actually a BAP=92s B= IL, then there=92re some optimizations in the `Bil` module. The most intere= sting is constant folding and purging unused variables. You can also use fi= xpoint function to drive the optimization passes.=20 In any case, even if it is not a BIL, you can look at BAP=92s constant fold= er class.=20 Best wishes Ivan=20 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 "simplif= ication" would be a negligible part of the overall time since usually what = people mean by "simplification" doesn't require any sort of search. This mi= ght be a premature optimization, especially since I doubt you'll find a rea= dy to use library. >=20 > On Thu, Apr 2, 2015 at 4:05 PM, Kenneth Adam Miller wrote: > Well, the concern is that equivalent expressions that might arise in our = scenario be more difficult than they need to be. In expression simplificati= on, we keep the equivalent expression that is produced, replacing the origi= nal. In this way then next time we feed that expression input, or try to so= lve on it, we can get results for much less work. >=20 > Am I right? I'm not too too familiar with SMT solvers-it's a different, h= ighly specialized field, so I just need to use them for my purposes. >=20 > On Thu, Apr 2, 2015 at 3:57 PM, Ashish Agarwal wr= ote: > > need to simplify expressions before I submit them to SMT solvers >=20 > 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. >=20 > On Thu, Apr 2, 2015 at 3:47 PM, Kenneth Adam Miller wrote: > I predominantly need to simplify expressions before I submit them to SMT = solvers. I'm quite concerned about not reimplementing a difficult and alrea= dy solved problem, and I'm pretty sure that this is part of work of the sol= vers. I'm pretty sure that Z3 provides a simplify function. Would it be bet= ter to cache the result of the simplify function? >=20 > On Thu, Apr 2, 2015 at 3:36 PM, Ashish Agarwal wr= ote: > If you don't find anything else, maybe some of our old code from PADL 201= 0 can 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. >=20 > [1] http://ashishagarwal.org/2010/01/18/automating-mp-transformations/ >=20 >=20 > On Thu, Apr 2, 2015 at 1:16 PM, Kenneth Adam Miller wrote: > Is there a library somewhere where I can represent and simplify simple bi= t operation expressions? Add, subtract, exclusive or, or, and, divide, mult= iply, modulus, composed recursively, and operations on the expression type,= such as simplify? >=20 >=20 >=20 >=20 >=20 --Apple-Mail=_BE3A434E-485B-4F6B-BC45-B5BBF1B6AA41 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=windows-1252 Hi Kenneth,

If the expression, that you=92re trying to simplify is actually a = BAP=92s BIL, then there=92re some optimizations in the `Bil` module. The mo= st interesting is constant folding and purging unused variables. You can al= so use fixpoint function to drive the optimization passes. 
=
In any case, even if it is not a BIL, you can look at BAP=92= s constant folder class. 

Best wishes
Ivan 

On Apr 2, 2015, at 4:14 PM, Ashish Ag= arwal <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 an= y 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 Ada= m Miller <kennethadammiller@gmail.com> wrote:
<= blockquote class=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:1px= #ccc solid;padding-left:1ex">
Well, the concern is that eq= uivalent expressions that might arise in our scenario be more difficult tha= n they need to be. In expression simplification, we keep the equivalent exp= ression that is produced, replacing the original. In this way then next tim= e 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 nee= d to use them for my purposes.

On Thu, A= pr 2, 2015 at 3:57 PM, Ashish Agarwal <agarwal1975@gmail.com> wrote:
>&= nbsp;need to simplify expressi= ons before I submit them to SMT solvers

Why? Is the input language of the solver you're using n= ot rich enough for your needs. The notion of "simplify" can be not so simpl= e depending on the language and your needs.

On Thu, Apr 2, 2015 at 3:= 47 PM, Kenneth Adam Miller <kennethadammiller@gmail.com><= /span> wrote:
I predomin= antly need to simplify expressions before I submit them to SMT solvers. I'm= quite concerned about not reimplementing a difficult and already solved pr= oblem, and I'm pretty sure that this is part of work of the solvers. I'm pr= etty 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 Agarw= al <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 i= t'll be easier to put something together from scratch, assuming you don't c= are about performance or need variables.



<= div class=3D"gmail_quote">On Thu, Apr 2, 2015 at 1:16 PM, Kenneth Adam Mill= er <kennethadammiller@gmail.com> wrote:
Is there a library somewhere where= I can represent and simplify simple bit operation expressions? Add, subtra= ct, exclusive or, or, and, divide, multiply, modulus, composed recursively,= and operations on the expression type, such as simplify?






= --Apple-Mail=_BE3A434E-485B-4F6B-BC45-B5BBF1B6AA41--