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 A08B77FCEF for ; Thu, 2 Apr 2015 22:15:03 +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.181; 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.181 as permitted sender) identity=mailfrom; client-ip=209.85.212.181; 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-f181.google.com) identity=helo; client-ip=209.85.212.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="agarwal1975@gmail.com"; x-sender="postmaster@mail-wi0-f181.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0C6AAC6oh1VlLXUVdFcgkWBFVwFgxCyYY9xhX0CgUUHTAEBAQEBARIBAQEBBwsLCRIwhB4BAQEDARIRHQEbHQEDAQsGBQsNKgICIQEBEQEFARwGEyKHeAEDCQgNqTE+MYs4gWuCd40oChknDVSEXgEBAQEGAQEBAQEXAQUOixuCR4IyB4JogUUFlF+EPoFNgR06jEKCZ4F+EiOBDAmELSIxgkMBAQE X-IPAS-Result: A0C6AAC6oh1VlLXUVdFcgkWBFVwFgxCyYY9xhX0CgUUHTAEBAQEBARIBAQEBBwsLCRIwhB4BAQEDARIRHQEbHQEDAQsGBQsNKgICIQEBEQEFARwGEyKHeAEDCQgNqTE+MYs4gWuCd40oChknDVSEXgEBAQEGAQEBAQEXAQUOixuCR4IyB4JogUUFlF+EPoFNgR06jEKCZ4F+EiOBDAmELSIxgkMBAQE X-IronPort-AV: E=Sophos;i="5.11,512,1422918000"; d="scan'208";a="131375149" Received: from mail-wi0-f181.google.com ([209.85.212.181]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 02 Apr 2015 22:15:03 +0200 Received: by wibgn9 with SMTP id gn9so118502751wib.1 for ; Thu, 02 Apr 2015 13:15:03 -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=mNMAvnbsRIBPmgTCKf4UBu6EACBDLfR0s2UIDKn3QRc=; b=rU9tqTYi3gi//vxlNEgsDHdyTF03GdNougTySanAikqWlea06o1xXJdBwR4YEdi7Py yA5g8wFazLFER0mDK3uW8n/Oaidu2v08ys/SOkDLxgXWKJWoSztDblUAVISMCZEXlQ5d rKkZxWRocnECAY8lxafJgrcLcVMKVmBERWnqFttfQ5rphQ6QAmq0gXn9QolzrYLCkYcQ zZZ4xjoQ85y/XR24wVWFf8SuekNavequ7zkpLtOeqhNdQP194PMhGw0YUUTMlamvRNtc eA8w6ZD6jwOOuqsSbKX5LtGjMaiSQFEu5jRtatrlldVSzwtBA1c4NH0t2JY7Hei1dE52 aMbQ== X-Received: by 10.181.8.76 with SMTP id di12mr27734173wid.75.1428005702997; Thu, 02 Apr 2015 13:15:02 -0700 (PDT) MIME-Version: 1.0 Received: by 10.27.45.17 with HTTP; Thu, 2 Apr 2015 13:14:42 -0700 (PDT) In-Reply-To: References: From: Ashish Agarwal Date: Thu, 2 Apr 2015 16:14:42 -0400 Message-ID: To: Kenneth Adam Miller Cc: caml users Content-Type: multipart/alternative; boundary=001a1135f0aaaa1b040512c37cf5 Subject: Re: [Caml-list] Mathematical Expression Library --001a1135f0aaaa1b040512c37cf5 Content-Type: text/plain; charset=UTF-8 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 > 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? >>>>> >>>> >>>> >>> >> > --001a1135f0aaaa1b040512c37cf5 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
I don't know much about SMT solvers either, but my gue= ss is that "simplification" would be a negligible part of the ove= rall time since usually what people mean by "simplification" does= n'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 a= t 4:05 PM, Kenneth Adam Miller <kennethadammiller@gmail.com&= gt; 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 k= eep 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 i= t, we can get results for much less work.

Am I right? I&= #39;m not too too familiar with SMT solvers-it's a different, highly sp= ecialized field, so I just need to use them for my purposes.

On Thu, Apr 2, 2015 at 3:57 PM, Ashish Agarwal <ag= arwal1975@gmail.com> wrote:
>=C2=A0need to simplify expressions before I submit them to SMT solvers=

<= div>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 expr= essions before I submit them to SMT solvers. I'm quite concerned about = not reimplementing a difficult and already solved problem, and I'm pret= ty 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 <a= garwal1975@gmail.com> wrote:
If you don't find anything else, maybe some of our o= ld 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 c= are about performance or need variables.


=
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, s= ubtract, exclusive or, or, and, divide, multiply, modulus, composed recursi= vely, and operations on the expression type, such as simplify?





--001a1135f0aaaa1b040512c37cf5--