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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 4FF09BBC1 for ; Thu, 13 Mar 2008 14:04:55 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ah0BAB/D2EeGnQCBnmdsb2JhbACQcwEBAQEBBgQGBwoYlwU X-IronPort-AV: E=Sophos;i="4.25,493,1199660400"; d="scan'208";a="10221739" Received: from shiva.jussieu.fr ([134.157.0.129]) by mail3-smtp-sop.national.inria.fr with ESMTP; 13 Mar 2008 14:04:55 +0100 Received: from hydrogene.pps.jussieu.fr (hydrogene.pps.jussieu.fr [134.157.168.1]) by shiva.jussieu.fr (8.14.2/jtpda-5.4) with ESMTP id m2DD4MRE019783 for ; Thu, 13 Mar 2008 14:04:45 +0100 (CET) X-Ids:166 Received: from hydrogene.pps.jussieu.fr (localhost.localdomain [127.0.0.1]) by hydrogene.pps.jussieu.fr (8.13.4/jtpda-5.4) with ESMTP id m2DD4LcN008025 for ; Thu, 13 Mar 2008 14:04:21 +0100 Received: (from abate@localhost) by hydrogene.pps.jussieu.fr (8.13.4/8.13.2/Submit) id m2DD4LMN008024 for caml-list@yquem.inria.fr; Thu, 13 Mar 2008 14:04:21 +0100 Date: Thu, 13 Mar 2008 14:04:21 +0100 From: Pietro Abate To: caml-list@yquem.inria.fr Subject: Re: [Caml-list] BDDs in ocaml Message-ID: <20080313130421.GA7714@uranium.pps.jussieu.fr> References: <20080313123446.2F25C8B312@xprdmxin.myway.com> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20080313123446.2F25C8B312@xprdmxin.myway.com> X-Operating-System: GNU/Linux User-Agent: Mutt/1.5.9i X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-3.0 (shiva.jussieu.fr [134.157.0.166]); Thu, 13 Mar 2008 14:04:45 +0100 (CET) X-Virus-Scanned: ClamAV 0.92/6221/Thu Mar 13 11:10:51 2008 on shiva.jussieu.fr X-Virus-Status: Clean X-Miltered: at jchkmail.jussieu.fr with ID 47D9266A.00E by Joe's j-chkmail (http : // j-chkmail dot ensmp dot fr)! X-j-chkmail-Enveloppe: 47D9266A.00E/134.157.168.1/hydrogene.pps.jussieu.fr/hydrogene.pps.jussieu.fr/ X-j-chkmail-Score: MSGID : 47D9266A.00E on jchkmail.jussieu.fr : j-chkmail score : . : R=. U=. O=. B=0.059 -> S=0.059 X-j-chkmail-Status: Ham X-Spam: no; 0.00; bdds:01 ocaml:01 ocaml:01 filliatre:01 lri:01 filliatr:01 publis:01 hash-consing:01 wrote:01 pps:01 caml-list:01 jussieu:01 interfaces:01 binary:02 external:03 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. Ocaml interfaces to external BDD > implementations in other languages (like Cudd) are of no use to me. 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 wasn't able to find it. It would be interesting to repeat their experiments and play with it. :) p