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 2F3867FCEF for ; Thu, 2 Apr 2015 21:47:48 +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: A0AQAgCYmx1VlKvWVdFcg1pQDAWDELJhj3GFfQKBRQdMAQEBAQEBEgEBAQEHCwsJEjBBAoNbAQEBAwESER0BGx0BAwELBgUEBw0qAgIhAQERAQUBHAYTIod4AQMJCA2pQD4xiziBa4J3jSYKGScNVIReAQEBAQEBBAEBAQEBARYBBQ6LG4JHgjIHgmiBRQWUX4Q+gU2BV4xChGUSI4EMCYQtIjGCQwEBAQ X-IPAS-Result: A0AQAgCYmx1VlKvWVdFcg1pQDAWDELJhj3GFfQKBRQdMAQEBAQEBEgEBAQEHCwsJEjBBAoNbAQEBAwESER0BGx0BAwELBgUEBw0qAgIhAQERAQUBHAYTIod4AQMJCA2pQD4xiziBa4J3jSYKGScNVIReAQEBAQEBBAEBAQEBARYBBQ6LG4JHgjIHgmiBRQWUX4Q+gU2BV4xChGUSI4EMCYQtIjGCQwEBAQ X-IronPort-AV: E=Sophos;i="5.11,512,1422918000"; d="scan'208";a="131371589" 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 21:47:47 +0200 Received: by obvd1 with SMTP id d1so145442170obv.0 for ; Thu, 02 Apr 2015 12:47:46 -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=EOjr8i7OXQYBmBBzRGZmrh3F3PbVz7MfP2aFHQ9yorE=; b=POMp3Zw04OO+tRCzbiTpxUKhRhCIR9MCqIfZIY+UeY6wUkprYB4EqvTwhPqBxK5Pxx gSrrAI0Rjd8JmoQHmpbKA+ZyiC1TtLQEtWbM8qX66a2HgJUantvHRlf/HfnEwpsUgQLO ZgqS4IlBI9a+bOdn9BCOfj/GJzSVYQjTSi024SDbNr7zz3GT0VTFpObgCTW4m07yizVx 23ZdU2UI/GISHfESLl2CngTbCN9TAQcLRQQ7W72rstAHXUwWHAZYKznJ40GR6oZg99AH ZfefNFE1JBJz4g4MLV7BMFjDersKBBeXrWJ/huUj5Zah8S42MICi86wEEJoOyTHL1Mw2 /9Fw== MIME-Version: 1.0 X-Received: by 10.182.74.166 with SMTP id u6mr48776119obv.68.1428004066223; Thu, 02 Apr 2015 12:47:46 -0700 (PDT) Received: by 10.202.185.8 with HTTP; Thu, 2 Apr 2015 12:47:46 -0700 (PDT) In-Reply-To: References: Date: Thu, 2 Apr 2015 15:47:46 -0400 Message-ID: From: Kenneth Adam Miller To: Ashish Agarwal Cc: caml users Content-Type: multipart/alternative; boundary=001a11c1f2321aec460512c31b50 Subject: Re: [Caml-list] Mathematical Expression Library --001a11c1f2321aec460512c31b50 Content-Type: text/plain; charset=UTF-8 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? >> > > --001a11c1f2321aec460512c31b50 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
I predominantly need to simplify expressions before I subm= it 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 simplif= y function. Would it be better to cache the result of the simplify function= ?

On Thu, Ap= r 2, 2015 at 3:36 PM, Ashish Agarwal <agarwal1975@gmail.com> wrote:
If you don&#= 39;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 tog= ether from scratch, assuming you don't care about performance or need v= ariables.


<= br>
On Thu, Apr 2, 2015 at 1:16 PM, Kenneth Adam = Miller <kennethadammiller@gmail.com> wrote:
Is there a library somewhere w= here I can represent and simplify simple bit operation expressions? Add, su= btract, exclusive or, or, and, divide, multiply, modulus, composed recursiv= ely, and operations on the expression type, such as simplify?


--001a11c1f2321aec460512c31b50--