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.4 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 552CDBBC1 for ; Fri, 14 Mar 2008 06:41:14 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqkBAAat2UfD3aJ+h2dsb2JhbACQewEBAQgKKZgwAQ X-IronPort-AV: E=Sophos;i="4.25,499,1199660400"; d="scan'208";a="8378785" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 14 Mar 2008 06:41:14 +0100 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m2E5fDJY030519 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Fri, 14 Mar 2008 06:41:14 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqkBAAat2UfD3aJ+h2dsb2JhbACQewEBAQgKKZgwAQ X-IronPort-AV: E=Sophos;i="4.25,499,1199660400"; d="scan'208";a="8378784" Received: from ns-quad.ibisc.univ-evry.fr ([195.221.162.126]) by mail2-smtp-roc.national.inria.fr with ESMTP; 14 Mar 2008 06:41:13 +0100 Received: by ns-quad.ibisc.univ-evry.fr (Postfix, from userid 2067) id 138B5BF089; Fri, 14 Mar 2008 06:41:13 +0100 (CET) Date: Fri, 14 Mar 2008 06:41:13 +0100 From: Olivier Michel To: Berke Durak Cc: sasha.mal@excite.com, caml-list List Subject: Re: [Caml-list] BDDs in ocaml Message-ID: <20080314054112.GC24937@lami.univ-evry.fr> Reply-To: michel@ibisc.univ-evry.fr References: <20080313123446.2F25C8B312@xprdmxin.myway.com> <47D928C3.2010105@exalead.com> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: <47D928C3.2010105@exalead.com> User-Agent: Mutt/1.5.13 (2006-08-11) X-Miltered: at concorde with ID 47DA0FF9.001 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; univ-evry:01 bdds:01 ocaml:01 0100,:01 berke:01 durak:01 ocaml:01 viewcvs:01 univ-evry:01 val:01 evry:01 edos:98 fre:98 wrote:01 wrote:01 On Thu, Mar 13, 2008 at 02:14:43PM +0100, Berke Durak wrote: > sasha mal a écrit : > >Dear all, > > > > > > > >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. > > > > > > Hello, > > There is one small BDD module written by Xavier Leroy for an experimental > SAT-solver > during the EDOS project: > > https://gforge.inria.fr/plugins/scmsvn/viewcvs.php/xlsat/?root=sodiac > > Hello, I once wrote in the 90s a (RO)BDD implementation in caml-light (the translation to Ocaml should not be a big deal though) for the development of the declarative data-parallel language 8,5. The sources (unfortunately with comments in French, but they are pretty much straightforward!) are available here: http://www.ibisc.univ-evry.fr/~michel/BDD/ Regards, Olivier MICHEL. -- Olivier MICHEL Email : michel@ibisc.univ-evry.fr Universite d'Evry Val d'Essonne http : www.ibisc.univ-evry.fr/~michel Lab. IBISC - LIS project http : mgs.ibisc.univ-evry.fr FRE 3190 of CNRS and Genopole Phone : +33 (0)1.60.87.39.10 523, place des terrasses de l'agora Fax : +33 (0)1.60.87.37.89 91000 Evry - FRANCE