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 4F9CD7FCEF for ; Thu, 2 Apr 2015 22:05:12 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of kennethadammiller@gmail.com) identity=pra; client-ip=209.85.214.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="kennethadammiller@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of kennethadammiller@gmail.com designates 209.85.214.169 as permitted sender) identity=mailfrom; client-ip=209.85.214.169; receiver=mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ob0-f169.google.com) identity=helo; client-ip=209.85.214.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="postmaster@mail-ob0-f169.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0C0AAD4nx1Vm6nWVdFcgkWBFVAMBYMQsmGPcYV9AoFFB0wBAQEBAQESAQEBAQEGCwsJFC6EHgEBAQMBEhEdARsdAQMMBgULDSoCAiEBAREBBQEcBhMih3gBAwkIDak3PjGLOIFrgneNKAoZJw1UhF4BAQEBAQEEAQEBAQEBFgEFDosbgkeCMgeCaIFFBZRfhD6BTYEdOoxCgmeBfhIjgQwJhC0iMYJDAQEB X-IPAS-Result: A0C0AAD4nx1Vm6nWVdFcgkWBFVAMBYMQsmGPcYV9AoFFB0wBAQEBAQESAQEBAQEGCwsJFC6EHgEBAQMBEhEdARsdAQMMBgULDSoCAiEBAREBBQEcBhMih3gBAwkIDak3PjGLOIFrgneNKAoZJw1UhF4BAQEBAQEEAQEBAQEBFgEFDosbgkeCMgeCaIFFBZRfhD6BTYEdOoxCgmeBfhIjgQwJhC0iMYJDAQEB X-IronPort-AV: E=Sophos;i="5.11,512,1422918000"; d="scan'208";a="108162670" Received: from mail-ob0-f169.google.com ([209.85.214.169]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 02 Apr 2015 22:05:11 +0200 Received: by obvd1 with SMTP id d1so146103014obv.0 for ; Thu, 02 Apr 2015 13:05:09 -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=vp4vg41ZC8o4PbIvAkMVE9Ol9kYXxTCI9O5FZV5RmoY=; b=CRtGIPz13p2S+qoHp5R71cZCkquPihJW/TJpeS7IDtrpD3MXjkmx7FTOZmK2Q2ptwy 93H6Kz7p3PLVYbAt7O7xk7FMzjt+3kA7pPVFctWK2Vv2aBHbjNBFfxs1TN+QaUEM3Vd1 tZQ84foioTt4BKK2iHCdNgthlkV30AzaKGj3hN6eTjws75wvaxtnCZGIKhtD9JaOUQIW 7wPS1ArZjuC2nQa2S8filosDi5yGpvZsOg0dwazrS+u9elTA0njasF6dvyjaLnxsXz39 202WZvWREAwLpW1lUXqVMBUGxPjEvlW97HqwLp3b901b3a/TUumOXK9cQByd3nWoaYIe DFPA== MIME-Version: 1.0 X-Received: by 10.60.133.144 with SMTP id pc16mr38267341oeb.0.1428005109758; Thu, 02 Apr 2015 13:05:09 -0700 (PDT) Received: by 10.202.185.8 with HTTP; Thu, 2 Apr 2015 13:05:09 -0700 (PDT) In-Reply-To: References: Date: Thu, 2 Apr 2015 16:05:09 -0400 Message-ID: From: Kenneth Adam Miller To: Ashish Agarwal Cc: caml users Content-Type: multipart/alternative; boundary=047d7b4728664e01040512c359da Subject: Re: [Caml-list] Mathematical Expression Library --047d7b4728664e01040512c359da Content-Type: text/plain; charset=UTF-8 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 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 >> 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? >>>> >>> >>> >> > --047d7b4728664e01040512c359da Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Well, the concern is that equivalent expressions that migh= t arise in our scenario be more difficult than they need to be. In expressi= on simplification, we keep the equivalent expression that is produced, repl= acing the original. In this way then next time we feed that expression inpu= t, 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 p= urposes.

On Thu, Apr 2, 2015 at 3:57 PM, Ashish Agarwal <agarwal1975@gmail.c= om> wrote:
>=C2=A0ne= ed to simplify expressions before I submit them to SMT solvers
<= span style=3D"font-size:12.8000001907349px">
Why? Is the input language of th= e solver you're using not rich enough for your needs. The notion of &qu= ot;simplify" can be not so simple depending on the language and your n= eeds.

On Thu, Apr 2, 2015 at 3:47= PM, Kenneth Adam Miller <kennethadammiller@gmail.com> wrote:
I predominan= tly 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 bette= r 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 anythin= g else, maybe some of our old code from PADL 2010 can help as a starting po= int [1]. Probably it'll be easier to put something together from scratc= h, assuming you don't care about performance or need variables.




--047d7b4728664e01040512c359da--