Article View: fa.caml
Article #113Re: [Caml-list] [ANN] Boolean expression simplifier library
From: "Markus W. Weißmann"
Date: Thu, 19 Apr 2012 14:55
Date: Thu, 19 Apr 2012 14:55
60 lines
4462 bytes
4462 bytes
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/ -- Caml-list mailing list. Subscription management and archives: https://sympa-roc.inria.fr/wws/info/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://caml.inria.fr/bin/caml-bugs
Technical Details
Message-ID:
<fa.YJGOs31ZzNwOPuQot2xs4vXV5Ik@ifi.uio.no>Path:
arc1-ca.pugleaf.net!h15ni141837bkw.0!nntp.google.com!news1.google.com!news.glorb.com!uio.no!nntp.uio.no!.POSTED!not-for-mailReferences:
<fa.fAw41xsBYTYJoeFiCdsHBUoKOYA@ifi.uio.no> <fa.E019rOq25021XLEIFfo7TZM44Pk@ifi.uio.no>Show Full Headers
Complete Article Headers
X-Google-Thread: ff861,b7c03ba90cedb70b
X-Google-NewGroupId: yes
X-Google-Attributes: gidc0fe4b917e,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII
Received: by 10.204.151.211 with SMTP id d19mr258461bkw.6.1334847334167;
Thu, 19 Apr 2012 07:55:34 -0700 (PDT)
Path: arc1-ca.pugleaf.net!h15ni141837bkw.0!nntp.google.com!news1.google.com!news.glorb.com!uio.no!nntp.uio.no!.POSTED!not-for-mail
From: "Markus W. Weißmann" <markus.weissmann@in.tum.de>
Newsgroups: fa.caml
Subject: Re: [Caml-list] [ANN] Boolean expression simplifier library
Date: Thu, 19 Apr 2012 14:55:33 UTC
Organization: Internet mailing list
Lines: 61
Message-ID: <fa.YJGOs31ZzNwOPuQot2xs4vXV5Ik@ifi.uio.no>
References: <fa.fAw41xsBYTYJoeFiCdsHBUoKOYA@ifi.uio.no> <fa.E019rOq25021XLEIFfo7TZM44Pk@ifi.uio.no>
NNTP-Posting-Host: mail-jess.uio.no
Mime-Version: 1.0 (Apple Message framework v1257)
X-Trace: readme.uio.no 1334847333 16951 129.240.7.9 (19 Apr 2012 14:55:33 GMT)
X-Complaints-To: abuse@uio.no
NNTP-Posting-Date: Thu, 19 Apr 2012 14:55:33 +0000 (UTC)
To: Caml Mailing List <caml-list@inria.fr>
X-IronPort-AV: E=Sophos;i="4.75,446,1330902000";
d="scan'208";a="154753092"
X-Authentication-Warning: walapai.inria.fr: sympa set sender to caml-list-owner@inria.fr using -f
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"
In-Reply-To: <4F8F62D5.3040802@riken.jp>
X-Mailer: Apple Mail (2.1257)
X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q3JEtD9o022057
X-Sequence: 3939
List-Id: <caml-list.inria.fr>
List-Archive: <https://sympa-roc.inria.fr/wws/arc/caml-list>
List-Help: <mailto:sympa@inria.fr?subject=help>
List-Owner: <mailto:caml-list-request@inria.fr>
List-Post: <mailto:caml-list@inria.fr>
List-Subscribe: <mailto:sympa@inria.fr?subject=subscribe%20caml-list>
List-Unsubscribe: <mailto:sympa@inria.fr?subject=unsubscribe%20caml-list>
Original-Date: Thu, 19 Apr 2012 16:54:56 +0200
Original-Message-Id: <55A4844B-BA31-4EF9-95FF-E9D20A569A96@in.tum.de>
Original-References: <063785FB-EC33-4350-BCDA-FB450D87FEAD@in.tum.de> <4F8F62D5.3040802@riken.jp>
Content-Type: text/plain; charset=iso-8859-1
Content-Transfer-Encoding: 8bit