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
