(* Zero-suppressed BDDs, headers.
   Copyright (C) 2008 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

datatype ''form zbdd = Z | I | N of ''form * ''form zbdd * ''form zbdd;
(* Z = empty set;
 I = {empty set};
 N (x, F0, F1) = {{x} U c | c in F0} U F1
 *)

extern val ZBDDmake : ''form -> ''form zbdd;

extern val ZBDDops : (''form * ''form -> bool) ->
	   |[subset1 : ''form zbdd * ''form -> ''form zbdd,
	     (* subset1 (F,x) returns the zbdd of all c such that x in c *)
	     subset0 : ''form zbdd * ''form -> ''form zbdd,
	     (* subset0 (F,x) returns the zbdd of all c such that x not in c *)
	     union : ''form zbdd * ''form zbdd -> ''form zbdd,
	     (* union (F0,F1) computes the union of F0 and F1 *)
	     ]|;
