From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 2BD04BBC1 for ; Thu, 13 Mar 2008 21:17:54 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ah0DANYo2UeBrw8Eh2dsb2JhbACQdAEBAQgKKZgy X-IronPort-AV: E=Sophos;i="4.25,495,1199660400"; d="scan'208";a="23739945" Received: from ext.lri.fr ([129.175.15.4]) by mail4-smtp-sop.national.inria.fr with ESMTP; 13 Mar 2008 21:17:54 +0100 Received: from localhost (localhost [127.0.0.1]) by ext.lri.fr (Postfix) with ESMTP id C2BEEA4687; Thu, 13 Mar 2008 21:17:53 +0100 (CET) X-Virus-Scanned: Debian amavisd-new at lri.fr Received: from ext.lri.fr ([127.0.0.1]) by localhost (ext.lri.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id Ys4-mLvCz4eF; Thu, 13 Mar 2008 21:17:53 +0100 (CET) Received: from [192.168.0.10] (mry91-1-82-229-156-20.fbx.proxad.net [82.229.156.20]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (No client certificate requested) by ext.lri.fr (Postfix) with ESMTP id 70599A4683; Thu, 13 Mar 2008 21:17:53 +0100 (CET) Message-ID: <47D98BF0.4070005@lri.fr> Date: Thu, 13 Mar 2008 21:17:52 +0100 From: =?ISO-8859-1?Q?Jean-Christophe_Filli=E2tre?= User-Agent: Thunderbird 1.5.0.14ubu (X11/20080306) MIME-Version: 1.0 To: Pietro Abate Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] BDDs in ocaml References: <20080313123446.2F25C8B312@xprdmxin.myway.com> <20080313130421.GA7714@uranium.pps.jussieu.fr> In-Reply-To: <20080313130421.GA7714@uranium.pps.jussieu.fr> X-Enigmail-Version: 0.94.2.0 OpenPGP: url=http://www.lri.fr/~filliatr/mykey.asc Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Spam: no; 0.00; filliatre:01 filliatre:01 lri:01 bdds:01 ocaml:01 ocaml:01 lri:01 filliatr:01 publis:01 hash-consing:01 filliatr:01 wrote:01 wrote:01 caml-list:01 lazy:02 Pietro Abate a écrit : > On Thu, Mar 13, 2008 at 08:34:46AM -0400, sasha mal wrote: >> I wonder whether anyone has a BDD (binary decision diagram) >> implementation in ocaml. > > have a look at this paper for a non-optimized bdd implementation from > Jean-Christophe Filliatre. > http://www.lri.fr/~filliatr/ftp/publis/hash-consing2.ps.gz > > I don't know if the full source code is avalaible. I wrote the code by that time, but I was too lazy to package it. Here it is: http://www.lri.fr/~filliatr/ftp/ocaml/bdd/ Hope this helps, -- Jean-Christophe