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 971C17FCEF for ; Thu, 2 Apr 2015 21:58:13 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of agarwal1975@gmail.com) identity=pra; client-ip=209.85.212.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="agarwal1975@gmail.com"; x-sender="agarwal1975@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of agarwal1975@gmail.com designates 209.85.212.182 as permitted sender) identity=mailfrom; client-ip=209.85.212.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="agarwal1975@gmail.com"; x-sender="agarwal1975@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-wi0-f182.google.com) identity=helo; client-ip=209.85.212.182; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="agarwal1975@gmail.com"; x-sender="postmaster@mail-wi0-f182.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AOAgAOnh1VlLbUVdFcgkWBFVwFgxCyYY9xhX0CgUUHTAEBAQEBARIBAQEBBwsLCRIwQQKDWwEBAQMBEhEdARsdAQMBCwYFBAcNKgICIQEBEQEFARwGEwgah3gBAwkIDak+PjGLOIFrgneNJwoZJw1UhF4BAQEBBgEBAQEBFwEFDosbgkeCMgeCaIFFBZRfhD6BTYEdOoxCgmeBfhIjgQwJhC0iMYJDAQEB X-IPAS-Result: A0AOAgAOnh1VlLbUVdFcgkWBFVwFgxCyYY9xhX0CgUUHTAEBAQEBARIBAQEBBwsLCRIwQQKDWwEBAQMBEhEdARsdAQMBCwYFBAcNKgICIQEBEQEFARwGEwgah3gBAwkIDak+PjGLOIFrgneNJwoZJw1UhF4BAQEBBgEBAQEBFwEFDosbgkeCMgeCaIFFBZRfhD6BTYEdOoxCgmeBfhIjgQwJhC0iMYJDAQEB X-IronPort-AV: E=Sophos;i="5.11,512,1422918000"; d="scan'208";a="131372797" Received: from mail-wi0-f182.google.com ([209.85.212.182]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 02 Apr 2015 21:58:13 +0200 Received: by wibgn9 with SMTP id gn9so118046332wib.1 for ; Thu, 02 Apr 2015 12:58:13 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=lVZ+CGwXJPtD0NLGTs4IvpqIlcobB5KJDh9x3SQxcbw=; b=FVB0wMo1nrcMrFilNOhdkiND9bxnLV5WzZIyB2HKTH38Dg+439+n95e+KvpUwlVZvL OpLATxSbqE+jlqwDPxrVqPAWGL1257xmPI4MSTkkv83OizDhH3gceKiVirwhu00t+ugo HFq4vvDyJdTAo57SJZWsur6YgDkA7uWQVQMPQKfkTttCDlc+Ntag4Wj+yiwDQcza+npR pWmzfqSXeEbJp6dEqUpOJ/WYKEdr0CpKHbMQwvFaQQDiCfYoXNJp2kjGOvC6mNpldTvf Pp9lFjqLwmtR+oJYVy9QsCXoHoDQgA4wRsdZwC8Wq0Cycw1TUMrSAWUsYunAOFNDGE+X YQmg== X-Received: by 10.180.104.33 with SMTP id gb1mr27338931wib.33.1428004692930; Thu, 02 Apr 2015 12:58:12 -0700 (PDT) MIME-Version: 1.0 Received: by 10.27.45.17 with HTTP; Thu, 2 Apr 2015 12:57:52 -0700 (PDT) In-Reply-To: References: From: Ashish Agarwal Date: Thu, 2 Apr 2015 15:57:52 -0400 Message-ID: To: Kenneth Adam Miller Cc: caml users Content-Type: multipart/alternative; boundary=f46d0442678e75b50b0512c3409b Subject: Re: [Caml-list] Mathematical Expression Library --f46d0442678e75b50b0512c3409b Content-Type: text/plain; charset=UTF-8 > 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? >>> >> >> > --f46d0442678e75b50b0512c3409b Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
>=C2=A0nee= d 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 "simpl= ify" can be not so simple depending on the language and your needs.

O= n Thu, Apr 2, 2015 at 3:47 PM, Kenneth Adam Miller <kennethadamm= iller@gmail.com> wrote:
I predominantly need to simplify expressions before I submit = them to SMT solvers. I'm quite concerned about not reimplementing a dif= ficult and already solved problem, and I'm pretty sure that this is par= t of work of the solvers. I'm pretty sure that Z3 provides a simplify f= unction. Would it be better to cache the result of the simplify function?

=
On Thu, Apr 2, 2015 at 3:36 PM, Ashish Agarwal <= span dir=3D"ltr"><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&= #39;ll be easier to put something together from scratch, assuming you don&#= 39;t care about performance or need variables.



On Thu, Apr 2, 2015 at 1:16 PM, Kennet= h Adam Miller <kennethadammiller@gmail.com> wrote:=
Is there a library some= where where I can represent and simplify simple bit operation expressions? = Add, subtract, exclusive or, or, and, divide, multiply, modulus, composed r= ecursively, and operations on the expression type, such as simplify?



--f46d0442678e75b50b0512c3409b--