From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q3JEtD9o022057 for ; Thu, 19 Apr 2012 16:55:13 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ah8DAOgmkE+DnwAImWdsb2JhbABDgxyuJiIBAQEBAQgLCxsnggkBAQMBAX4LCxguVwYuh28FBAe6cI9aYwSXAYRijTA X-IronPort-AV: E=Sophos;i="4.75,446,1330902000"; d="scan'208";a="154752960" Received: from mail-out1.informatik.tu-muenchen.de ([131.159.0.8]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/ADH-AES256-SHA; 19 Apr 2012 16:54:58 +0200 Received: from [172.16.1.4] (178-27-27-49-dynip.superkabel.de [178.27.27.49]) (using TLSv1 with cipher AES128-SHA (128/128 bits)) (No client certificate requested) by mail.in.tum.de (Postfix) with ESMTPSA id 1C784240931 for ; Thu, 19 Apr 2012 16:54:57 +0200 (CEST) Content-Type: text/plain; charset=iso-8859-1 Mime-Version: 1.0 (Apple Message framework v1257) From: =?iso-8859-1?Q?=22Markus_W=2E_Wei=DFmann=22?= In-Reply-To: <4F8F62D5.3040802@riken.jp> Date: Thu, 19 Apr 2012 16:54:56 +0200 Message-Id: <55A4844B-BA31-4EF9-95FF-E9D20A569A96@in.tum.de> References: <063785FB-EC33-4350-BCDA-FB450D87FEAD@in.tum.de> <4F8F62D5.3040802@riken.jp> To: Caml Mailing List X-Mailer: Apple Mail (2.1257) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q3JEtD9o022057 Subject: Re: [Caml-list] [ANN] Boolean expression simplifier library Hello, On 19 Apr 2012, at 02:56, Francois Berenger wrote: > I'm curious, what is it used for? > > Is it for people doing proof checkers or things like this? > Like that, yes: We successfully use it for reducing the size of programs we want to perform model checking on. My concrete target are industrial robot systems [1]. I even tried to integrate it into a compiler to reduce the size of right-hand-side boolean expression; unfortunately for small expressions the normalization (that occurs during minimization) often made the results less optimal than just some heuristic rewriting rules. Generally speaking you would use it for optimizing the execution time of boolean expressions; I would guess that the biggest user base of similar implementations are electrical engineers designing circuit boards. Regards -Markus [1] http://www6.in.tum.de/Main/Publications/Weissmann2011.pdf > On 04/19/2012 07:26 AM, "Markus W. Weißmann" wrote: >> Hi, >> >> I'd like to announce the first public release of the 'boolean expression simplifier' library "bes". >> It is an implementation of several algorithms for minimizing boolean expressions similar to the espresso solver [1] -- though in OCaml. >> The source code is available on ocamlforge under the new bsd license: >> >> http://bes.forge.ocamlcore.org/ >> >> It comes with a simple front-end program for reading and simplifying expressions in DFA from text files. >> Students trying to verify their Karnaugh Veitch map solutions rejoice! ;) >> >> >> Regards >> >> -Markus >> >> [1] http://embedded.eecs.berkeley.edu/pubs/downloads/espresso/index.htm >> > -- 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/