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 2C1D47FCEF for ; Thu, 2 Apr 2015 23:41:46 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of drupyog+caml@zoho.com) identity=pra; client-ip=74.201.84.155; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="drupyog+caml@zoho.com"; x-sender="drupyog+caml@zoho.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of drupyog+caml@zoho.com designates 74.201.84.155 as permitted sender) identity=mailfrom; client-ip=74.201.84.155; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="drupyog+caml@zoho.com"; x-sender="drupyog+caml@zoho.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@sender1.zohomail.com) identity=helo; client-ip=74.201.84.155; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="drupyog+caml@zoho.com"; x-sender="postmaster@sender1.zohomail.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0CjAAActh1Vm5tUyUpcg1pcgxXCVIV9AoFMTAEBAQEBARIBAQEBAQYLCwkULoQfAQUjIAE0AQIOCxgJFggDAgIJAwIBAgEPJREGAQwBBQIBAYgWAQMBBAwECbROcIRoAo0mIigNGIUaAQEBAQEFAQEBAQEBARQHiymCR4IyB4JogUWRdYJvhD6BTYEdOliEX4cLgmeDSIQTbYJDAQEB X-IPAS-Result: A0CjAAActh1Vm5tUyUpcg1pcgxXCVIV9AoFMTAEBAQEBARIBAQEBAQYLCwkULoQfAQUjIAE0AQIOCxgJFggDAgIJAwIBAgEPJREGAQwBBQIBAYgWAQMBBAwECbROcIRoAo0mIigNGIUaAQEBAQEFAQEBAQEBARQHiymCR4IyB4JogUWRdYJvhD6BTYEdOliEX4cLgmeDSIQTbYJDAQEB X-IronPort-AV: E=Sophos;i="5.11,513,1422918000"; d="scan'208,217";a="108172672" Received: from sender1.zohomail.com ([74.201.84.155]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-MD5; 02 Apr 2015 23:41:42 +0200 DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=zapps768; d=zoho.com; h=message-id:date:from:user-agent:mime-version:to:cc:subject:references:in-reply-to:content-type; b=p7X4pqbUzyPTobE5WHpVnCm6gLaX3TPoV9/tcGVOhJ7Lpdesmoo+pgnMfw6NKl3DKV98vQlRzFgG 3pvzB6X6IieOgU9F8nljm/qe1JB1+I/nIf0N9IedNaMromh9Hxni Received: from [192.168.1.8] (did75-8-82-228-42-129.fbx.proxad.net [82.228.42.129]) by mx.zohomail.com with SMTPS id 1428010896588272.11643313933405; Thu, 2 Apr 2015 14:41:36 -0700 (PDT) Message-ID: <551DB78D.1040705@zoho.com> Date: Thu, 02 Apr 2015 23:41:33 +0200 From: Drup User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.5.0 MIME-Version: 1.0 To: Kenneth Adam Miller , Ashish Agarwal CC: caml users References: In-Reply-To: Content-Type: multipart/alternative; boundary="------------060506060009080009030501" Subject: Re: [Caml-list] Mathematical Expression Library This is a multi-part message in MIME format. --------------060506060009080009030501 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit If I may, "simplifications" on the formula (eliminating dead variables and constant folding for example) is completely unimportant. Z3 is going to do it for you. The actual shape of your formula is much more important and you should care of that when generating your formula (while you still have semantic informations), not after it's done. Le 02/04/2015 21:47, Kenneth Adam Miller a écrit : > 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 > > > 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? > > > --------------060506060009080009030501 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 8bit
If I may, "simplifications" on the formula (eliminating dead variables and constant folding for example) is completely unimportant. Z3 is going to do it for you.

The actual shape of your formula is much more important and you should care of that when generating your formula (while you still have semantic informations), not after it's done.

Le 02/04/2015 21:47, Kenneth Adam Miller a écrit :
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 <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'll be easier to put something together from scratch, assuming you don't care 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, subtract, exclusive or, or, and, divide, multiply, modulus, composed recursively, and operations on the expression type, such as simplify?



--------------060506060009080009030501--