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 03B077FCCB for ; Tue, 7 Apr 2015 16:16:30 +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.180; 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.180 as permitted sender) identity=mailfrom; client-ip=209.85.214.180; 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-f180.google.com) identity=helo; client-ip=209.85.214.180; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="kennethadammiller@gmail.com"; x-sender="postmaster@mail-ob0-f180.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: A0AAAQD55SNVm7TWVdFcg1pcBYMQsheOGIIFhX0CgSUHTAEBAQEBARIBAQEBAQYLCwkULoQeAQEBAwESER0BGxILAQMBCwYFBAcNDR0CAiIBEQEFAQoSBhMIChCHcwEDCQgNqQo+MYs4gWuCdowRChknAwpUhEsBAQEBAQEBAwEBAQEBAQEBFAEFDosdhHgEB4JogUUFhRAKiUmGCYYPgVeROhIjgQwJgX2CMCIxAYJCAQEB X-IPAS-Result: A0AAAQD55SNVm7TWVdFcg1pcBYMQsheOGIIFhX0CgSUHTAEBAQEBARIBAQEBAQYLCwkULoQeAQEBAwESER0BGxILAQMBCwYFBAcNDR0CAiIBEQEFAQoSBhMIChCHcwEDCQgNqQo+MYs4gWuCdowRChknAwpUhEsBAQEBAQEBAwEBAQEBAQEBFAEFDosdhHgEB4JogUUFhRAKiUmGCYYPgVeROhIjgQwJgX2CMCIxAYJCAQEB X-IronPort-AV: E=Sophos;i="5.11,538,1422918000"; d="scan'208";a="108637177" Received: from mail-ob0-f180.google.com ([209.85.214.180]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 07 Apr 2015 16:16:29 +0200 Received: by obbgh1 with SMTP id gh1so87736722obb.1 for ; Tue, 07 Apr 2015 07:16:27 -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=thwHc6wxGzcf17qXNSWZ1J9wQrfkqdwLQ6W0KixBOzk=; b=BLIZ1/CDgmHiVly54h8qmo2qeCB5XuJFle6biYplssy600UYn7+1QBAGV1TnNKmljB YpICdKOmAaTvJ4En/Sp1UkXLiMKiHuGYuXJxvjTcVrbqn8zpDJz9f4f0XV3Gvr2wNLSV H2WUeCYvoSjQ48sOADcgZAuQkQDwsPmbh/xROUYwlrU/xkOL3KtyjvhIQMf1S9dxuVEs Mv1jLn3smPvIQsZ0TUo+bHuZL+aLVQtrXP3eYP+wJrMljxtejvL5gbRy7Fcc2et1JXWu KUmo12Y/4kpMUKrJF1sSx3nJkNAPzIHrYVoLqSpxfxLvU+3umnIZPSyH7IdZe4406MH2 XF9A== MIME-Version: 1.0 X-Received: by 10.182.75.133 with SMTP id c5mr13641375obw.26.1428416176475; Tue, 07 Apr 2015 07:16:16 -0700 (PDT) Received: by 10.202.185.8 with HTTP; Tue, 7 Apr 2015 07:16:16 -0700 (PDT) In-Reply-To: <981a73893459ff720b3cc5e25fd9ab54@in.tum.de> References: <981a73893459ff720b3cc5e25fd9ab54@in.tum.de> Date: Tue, 7 Apr 2015 10:16:16 -0400 Message-ID: From: Kenneth Adam Miller To: =?UTF-8?Q?Markus_Wei=C3=9Fmann?= Cc: caml users Content-Type: multipart/alternative; boundary=089e0158aa64ca57160513230e53 Subject: Re: [Caml-list] Mathematical Expression Library --089e0158aa64ca57160513230e53 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Thank you! On Tue, Apr 7, 2015 at 2:37 AM, Markus Wei=C3=9Fmann wrote: > Just for completeness sake: There is also the "boolean expression > simplifier" [1] library implementing the Quine-McCluskey algorithm (and > friends) in pure OCaml. > I'd guess that a decent SMT solver will solve the "raw" expression much > faster than running it through the simplifier and then solving it (with t= he > same solver). > > regards > Markus > > [1] http://bes.forge.ocamlcore.org/ > > > On 2015-04-02 19:16, Kenneth Adam Miller wrote: > >> Is there a library somewhere where I can represent and simplify simple b= it >> operation expressions? Add, subtract, exclusive or, or, and, divide, >> multiply, modulus, composed recursively, and operations on the expression >> type, such as simplify? >> > > -- > Markus Wei=C3=9Fmann, M.Sc. > Technische Universit=C3=A4t M=C3=BCnchen > Institut f=C3=BCr Informatik > Boltzmannstr. 3 > D-85748 Garching > Germany > http://wwwknoll.in.tum.de/ > > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > --089e0158aa64ca57160513230e53 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Thank you!

On Tue, Apr 7, 2015 at 2:37 AM, Markus Wei=C3=9Fmann <markus.weissmann@in.tum.de> wrote:
Just for completeness sake: There is also the "boolean e= xpression simplifier" [1] library implementing the Quine-McCluskey alg= orithm (and friends) in pure OCaml.
I'd guess that a decent SMT solver will solve the "raw" expre= ssion much faster than running it through the simplifier and then solving i= t (with the same solver).

regards
Markus

[1] http://be= s.forge.ocamlcore.org/

On 2015-04-02 19:16, Kenneth Adam Miller wrote:
Is there a library somewhere where I can represent and simplify simple bit<= br> operation expressions? Add, subtract, exclusive or, or, and, divide,
multiply, modulus, composed recursively, and operations on the expression type, such as simplify?

--
Markus Wei=C3=9Fmann, M.Sc.
Technische Universit=C3=A4t M=C3=BCnchen
Institut f=C3=BCr Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
http://wwwknoll.in= .tum.de/


--
Caml-list mailing list.=C2=A0 Subscription management and archives:
ht= tps://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners<= /a>
Bug reports: http://caml.inria.fr/bin/caml-bugs

--089e0158aa64ca57160513230e53--