From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <markus.weissmann@in.tum.de>
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 4F1C77FCCB
	for <caml-list@sympa.inria.fr>; Tue,  7 Apr 2015 08:37:07 +0200 (CEST)
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  markus.weissmann@in.tum.de) identity=pra;
  client-ip=131.159.0.8;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="markus.weissmann@in.tum.de";
  x-sender="markus.weissmann@in.tum.de";
  x-conformance=sidf_compatible
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  markus.weissmann@in.tum.de) identity=mailfrom;
  client-ip=131.159.0.8;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="markus.weissmann@in.tum.de";
  x-sender="markus.weissmann@in.tum.de";
  x-conformance=sidf_compatible
Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender
  authenticity information available from domain of
  postmaster@mail-out1.informatik.tu-muenchen.de)
  identity=helo; client-ip=131.159.0.8;
  receiver=mail2-smtp-roc.national.inria.fr;
  envelope-from="markus.weissmann@in.tum.de";
  x-sender="postmaster@mail-out1.informatik.tu-muenchen.de";
  x-conformance=sidf_compatible
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: A0CnAADJeSNVnAgAn4Ncg1pcgxXCKoYBAoEoTAEBAQEBARIBAQEBAQgLCQkULoQfAQUjDwEFUQQHGAICJgICVwYbiCe0VpZcDCCBIYoIhQAWglKBRQWUYIdkhTqNQ4QTPDEBgkIBAQE
X-IPAS-Result: A0CnAADJeSNVnAgAn4Ncg1pcgxXCKoYBAoEoTAEBAQEBARIBAQEBAQgLCQkULoQfAQUjDwEFUQQHGAICJgICVwYbiCe0VpZcDCCBIYoIhQAWglKBRQWUYIdkhTqNQ4QTPDEBgkIBAQE
X-IronPort-AV: E=Sophos;i="5.11,536,1422918000"; 
   d="scan'208";a="131873307"
Received: from mail-out1.informatik.tu-muenchen.de ([131.159.0.8])
  by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 07 Apr 2015 08:37:06 +0200
Received: from webmail.in.tum.de (localhost [127.0.0.1])
	by vmwebmail1.informatik.tu-muenchen.de (Postfix) with ESMTP id BF59F2402CF
	for <caml-list@inria.fr>; Tue,  7 Apr 2015 08:37:05 +0200 (CEST)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8;
 format=flowed
Content-Transfer-Encoding: 8bit
Date: Tue, 07 Apr 2015 08:37:05 +0200
From: =?UTF-8?Q?Markus_Wei=C3=9Fmann?= <markus.weissmann@in.tum.de>
To: <caml-list@inria.fr>
In-Reply-To: <CAK7rcp_+02ZbrmocUXkJaE0wrO72=2huWAbssG3sxsnWkBio=g@mail.gmail.com>
References: <CAK7rcp_+02ZbrmocUXkJaE0wrO72=2huWAbssG3sxsnWkBio=g@mail.gmail.com>
Message-ID: <981a73893459ff720b3cc5e25fd9ab54@in.tum.de>
X-Sender: markus.weissmann@in.tum.de
User-Agent: Roundcube Webmail/0.8.1
Subject: Re: [Caml-list] Mathematical Expression Library

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 
the 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 bit
> operation expressions? Add, subtract, exclusive or, or, and, divide,
> multiply, modulus, composed recursively, and operations on the 
> expression
> type, such as simplify?

-- 
Markus Weißmann, M.Sc.
Technische Universität München
Institut für Informatik
Boltzmannstr. 3
D-85748 Garching
Germany
http://wwwknoll.in.tum.de/