signature LIBBDD = 

    (* This is an interface from PolyML to Derek Long's
     libbdd library.  See the manual page bdd.3 for details.

     The libbdd library provides a set of routines for manipulating
     binary decision diagrams (BDDs). Some support is also provided
     for multi-terminal BDDs (MTBDDs).

     libbdd and libmem should be compiled as as shared libraries, and
     placed in a location included in $LD_LIBRARY_PATH 
     *)

sig 
    datatype 'a Option = None | Some of 'a

    eqtype Var  (* variables - a separate ML type *)
    eqtype Bdd  (* bdd *)

    val V : Var -> Bdd (* any variable can be viewed as a bdd *)
    val I : Var -> int (* each variable is represented as an integer *)

    type Bddm (* bdd manager *)

    (* Some routines such as bdd_substitute require a mapping from
    variables to BDDs to operate. This mapping is supplied in the form
    of a variable association which is a set of pairs. The first
    element of each pair is the variable, and the second element is
    the BDD that the variable is associated with. We represent these
    mappings by the ML type Subst. Other routines such as bdd_exists
    require sets of variables. We represent these sets of variables by
    the ML type Assoc *)

    type Assoc 
    type Subst 
    exception Error of string 

    (* 
     In the C library, reorderings functions are 
     passed to bdd_dynamic_reordering.
     The ML datatype Method represents the three options available *)
    datatype Method = SIFT | STABLE_WINDOW | NONE

    val bdd_start : unit -> unit
    (* 
     Loads the shared library. This function must be called before any
     library function -- otherwise functions will fail with Error
     "Library not loaded" 
     *)

  (*******************************************************************

   The remaining functions are curried versions of (most of) the
   library functions, with appropriate ML types.

   The parameters are in the order used by the C library. See bdd.3
   for details.

   *******************************************************************)

  val bdd_init : unit -> Bddm

  val bdd_version : unit -> string (* Get BDD version string *)

  val bdd_quit : Bddm -> unit     

  val bdd_new_var_first : Bddm -> Var
  val bdd_new_var_last : Bddm -> Var
  val bdd_new_var_before : Bddm -> Var -> Var
  val bdd_new_var_after : Bddm -> Var -> Var
  val bdd_var_with_index : Bddm -> int -> Var
  val bdd_var_with_id : Bddm -> int -> Var
  val bdd_one : Bddm -> Bdd
  val bdd_zero : Bddm -> Bdd
  val bdd_and : Bddm -> Bdd -> Bdd -> Bdd
  val bdd_nand : Bddm -> Bdd -> Bdd -> Bdd
  val bdd_or : Bddm -> Bdd -> Bdd -> Bdd
  val bdd_nor : Bddm -> Bdd -> Bdd -> Bdd
  val bdd_xor : Bddm -> Bdd -> Bdd -> Bdd
  val bdd_xnor : Bddm -> Bdd -> Bdd -> Bdd
  val bdd_identity : Bddm -> Bdd -> Bdd
  val bdd_not : Bddm -> Bdd -> Bdd
  val bdd_ite : Bddm -> Bdd -> Bdd -> Bdd -> Bdd
  val bdd_if : Bddm -> Bdd -> Var
  val bdd_then : Bddm -> Bdd -> Bdd
  val bdd_else : Bddm -> Bdd -> Bdd
  (* 
   bdd_if_index 
   not implemented 
   *)
  val bdd_if_id : Bddm -> Bdd -> int
  val bdd_intersects : Bddm -> Bdd -> Bdd -> Bdd
  val bdd_implies : Bddm -> Bdd -> Bdd -> Bdd
  val bdd_new_assoc : Bddm -> Var list -> Assoc
  val bdd_new_subst : Bddm -> (Var * Bdd) list -> Subst 
  (* bdd_new_assoc used to create substitution *)
  val bdd_free_assoc : Bddm -> Assoc -> unit
  val bdd_free_subst : Bddm -> Subst -> unit
  (* bdd_free_assoc used to free a substitution *)  

  (* 
   bdd_temp_assoc 
   bdd_augment_assoc 
   not implemented 
   *)
  val bdd_assoc : Bddm -> Assoc -> unit
  val bdd_subst : Bddm -> Subst -> unit (* bdd_assoc used for substitution *)

  val bdd_exists : Bddm -> Bdd -> Bdd

  val bdd_forall : Bddm -> Bdd -> Bdd
  val bdd_rel_prod : Bddm -> Bdd -> Bdd -> Bdd
  val bdd_compose : Bddm -> Bdd -> Var -> Bdd -> Bdd
  val bdd_substitute : Bddm -> Bdd -> Bdd
  val bdd_reduce : Bddm -> Bdd -> Bdd -> Bdd
  val bdd_cofactor : Bddm -> Bdd -> Bdd -> Bdd
  val bdd_depends_on : Bddm -> Bdd -> Var -> bool
  val bdd_support : Bddm -> Bdd -> Var list
  val bdd_satisfy : Bddm -> Bdd -> Bdd

  val bdd_satisfy_support : Bddm -> Bdd -> Bdd
  val bdd_satisfying_fraction : Bddm -> Bdd -> real
  (* 
   bdd_swap_vars 
   bdd_apply2 
   bdd_apply1 
   not implemented *)
  val bdd_size : Bddm -> Bdd -> bool -> int
  val bdd_size_multiple : Bddm -> Bdd list -> bool -> int
  (* 
   bdd_profile 
   bdd_profile_multiple 
   bdd_function_profile 
   bdd_function_profile_multiple 
   bdd_print_bdd 
   bdd_print_profile
   bdd_print_profile_multiple
   bdd_print_function_profile 
   bdd_dump_bdd
   bdd_undump_bdd
   bdd_type
   not implemented 
   *)
  val bdd_free : Bddm -> Bdd -> unit
  (* 
   bdd_unfree
   bdd_clear_refs 
   not implemented 
   *)
  val bdd_gc : Bddm -> unit
  val bdd_total_size : Bddm -> int
  val bdd_vars : Bddm -> int
  val bdd_cache_ratio : Bddm -> int -> int
  (* 
   bdd_node_limit
   bdd_overflow 
   bdd_overflow_closure
   bdd_abort_closure
   not implemented 
   *)
  val bdd_stats : Bddm -> unit
  val bdd_dynamic_reordering : Bddm -> Method -> unit
  (* See note on type Method above *)
  val bdd_reorder : Bddm -> unit
  
(* 
   bdd_new_var_block
   bdd_new_var_blockreorderable
   mtbdd_*  (* ie all mtbdd operations *)

   bdd_overflow_closure
   bdd_abort_closure
   not implemented 
   *)
end

functor LIBBDD () :LIBBDD =
struct
local open CInterface
in
datatype 'a Option = None | Some of 'a
exception Error of string
val bddlib = ref(None : dylib Option)
fun bdd_start() = bddlib := Some (CInterface.load_lib ("libbdd.so"));
fun get s = let fun getLib None = raise (Error "Library not loaded")
		  |getLib (Some theLibrary) = theLibrary
	    in
		load_sym (getLib (!bddlib)) s
	    end;

datatype Var   = Var of int
datatype Bdd   = Bdd of int
datatype Bddm  = Bddm of vol
datatype Assoc = Assoc of int
datatype Subst = Subst of int

fun V (Var v) = Bdd v
fun I (Var v) = v

val (fromCbool,toCbool,_) = breakConversion BOOL
fun notNULL v = fromCbool v

val VAR = mkConversion (Var o fromClong) (fn (Var b) => toClong b) (Cpointer Cvoid);
val BDD = mkConversion (Bdd o fromClong) (fn (Bdd b) => toClong b) (Cpointer Cvoid);
val BDDM = mkConversion Bddm (fn (Bddm m) => m) (Cpointer Cvoid);
val ASSOC = mkConversion (Assoc o fromCint) (fn (Assoc n) => toCint n) Cint
val SUBST = mkConversion (Subst o fromCint) (fn (Subst n) => toCint n) Cint
val PAIR = STRUCT2(VAR,BDD)

val (fromCvar, toCvar, Cvar) = breakConversion VAR
val (fromCbdd, toCbdd, Cbdd) = breakConversion BDD
val (fromCbddm, toCbddm, Cbddm) = breakConversion BDDM

fun bdd_vars m = call1 (get "bdd_vars") (BDDM) LONG m

fun bdd_init () = call0 (get "bdd_init") () BDDM ()

fun bdd_version () = call0 (get "bdd_version") () STRING ()

fun bdd_quit m = call1 (get "bdd_quit") (BDDM) VOID m

fun bdd_new_var_first m = call1 (get "bdd_new_var_first") (BDDM) VAR m
fun bdd_new_var_last m = call1 (get "bdd_new_var_last") (BDDM) VAR m
fun bdd_new_var_before m v = call2 (get "bdd_new_var_before") (BDDM, VAR) VAR (m,v)
fun bdd_new_var_after m v = call2 (get "bdd_new_var_after") (BDDM, VAR) VAR (m,v)

fun bdd_var_with_id m i = call2 (get "bdd_var_with_id") (BDDM, LONG) VAR (m,i)

fun bdd_one m  = call1 (get "bdd_one")  (BDDM) BDD m
fun bdd_zero m = call1 (get "bdd_zero") (BDDM) BDD m

fun bdd_and m f g = call3 (get "bdd_and") (BDDM,BDD,BDD) BDD (m,f,g)
fun bdd_nand m f g = call3 (get "bdd_nand") (BDDM,BDD,BDD) BDD (m,f,g)
fun bdd_or m f g = call3 (get "bdd_or") (BDDM,BDD,BDD) BDD (m,f,g)
fun bdd_nor m f g = call3 (get "bdd_nor") (BDDM,BDD,BDD) BDD (m,f,g)
fun bdd_xor m f g = call3 (get "bdd_xor") (BDDM,BDD,BDD) BDD (m,f,g)
fun bdd_xnor m f g = call3 (get "bdd_xnor") (BDDM,BDD,BDD) BDD (m,f,g)
fun bdd_identity m f = call2 (get "bdd_identity") (BDDM,BDD) BDD (m,f)

fun bdd_not m f = call2 (get "bdd_not") (BDDM,BDD) BDD (m,f)

fun bdd_ite m f g h = call4 (get "bdd_ite") (BDDM,BDD,BDD,BDD) BDD (m,f,g,h)

fun bdd_if m f = call2 (get "bdd_if") (BDDM,BDD) VAR (m,f)
fun bdd_then m f = call2 (get "bdd_then") (BDDM,BDD) BDD (m,f)
fun bdd_else m f = call2 (get "bdd_else") (BDDM,BDD) BDD (m,f)
fun bdd_if_id m f = call2 (get "bdd_if_id") (BDDM,BDD) LONG (m,f) 
fun bdd_intersects m f g = call3 (get "bdd_intersects") (BDDM,BDD,BDD) BDD (m,f,g)
fun bdd_implies m f g = call3 (get "bdd_implies") (BDDM,BDD,BDD) BDD (m,f,g)

(* assoc in C is created from an array of pointers to variables *)
(* we deal with lists of variables                              *)

fun fill CONV =
    let val (fromCtype, toCtype, Ctype) = breakConversion CONV
    fun f p [] = (assign Ctype p (toCbool false))
      | f p (x :: xs) = (assign Ctype p (toCtype x);
			 f (offset 1 Ctype p) xs
			 )
    in f end

fun extract CONV =
    let val (fromCtype, toCtype, Ctype) = breakConversion CONV
    fun e p = 
    if notNULL p then
	fromCtype p :: e (offset 1 Ctype p)
    else
	[]
    in e end

fun block CONV n =     
    let val (fromCtype, toCtype, Ctype) = breakConversion CONV
    in 
	alloc (n+1) Ctype 
    end;

fun LIST CONV =
    let fun length [] = 0 | length (_:: xs) = 1 + length xs;
	val (_,_, Ctype) = breakConversion CONV
	fun fromClist v = extract CONV v
	fun toClist  xs =
	    let val p = block CONV (length xs)
	    in fill CONV p xs; p end
    in
	mkConversion (fromClist o deref) (address o toClist) (Cpointer Ctype)
    end;

fun bdd_new_assoc m a = 
    call3 (get "bdd_new_assoc") (BDDM, LIST VAR, INT) ASSOC (m,a,0)
   
fun bdd_free_assoc m a = call2 (get "bdd_free_assoc") (BDDM,ASSOC) VOID (m,a)

fun bdd_assoc m a = call2 (get "bdd_assoc") (BDDM,ASSOC) VOID (m,a)

fun length [] = 0 | length (_ :: t) = 1 + length t;

fun bdd_new_subst m a = 
    call3 (get "bdd_new_assoc") (BDDM, LIST PAIR, INT) SUBST (m,a,length a)

fun bdd_free_subst m a = call2 (get "bdd_free_assoc") (BDDM,SUBST) VOID (m,a)

fun bdd_subst m a = call2 (get "bdd_assoc") (BDDM,SUBST) VOID (m,a)


fun bdd_exists m f  = call2 (get "bdd_exists") (BDDM,BDD) BDD (m,f)
fun bdd_forall m f  = call2 (get "bdd_forall") (BDDM,BDD) BDD (m,f)
fun bdd_rel_prod m f g = call3 (get "bdd_rel_prod") (BDDM,BDD,BDD) BDD (m,f,g)

fun bdd_compose m f g h = call4 (get "bdd_compose") (BDDM,BDD,VAR,BDD) BDD (m,f,g,h)
fun bdd_substitute m f = call2 (get "bdd_substitute") (BDDM,BDD) BDD (m,f)
fun bdd_reduce m f g = call3 (get "bdd_reduce") (BDDM,BDD,BDD) BDD (m,f,g)
fun bdd_cofactor m f g = call3 (get "bdd_cofactor") (BDDM,BDD,BDD) BDD (m,f,g)
fun bdd_depends_on m f v = call3 (get "bdd_depends_on") (BDDM,BDD,VAR) BOOL (m,f,v)

fun bdd_support m f = 
    let	val table = block VAR (bdd_vars m + 1)
    in 
	call3 (get "bdd_support") (BDDM, BDD, POINTER) VOID (m, f, address table);
	extract VAR table
    end

fun bdd_satisfy m f  = call2 (get "bdd_satisfy") (BDDM, BDD) BDD (m,f) 
fun bdd_satisfy_support m f  = call2 (get "bdd_satisfy_support") (BDDM, BDD) BDD (m,f) 

fun bdd_satisfying_fraction m f =call2 (get "bdd_satisfying_fraction") (BDDM,BDD) DOUBLE (m,f) 

fun bdd_total_size m  = call1 (get "bdd_total_size") (BDDM) LONG (m) ;
fun bdd_size m f b = call3 (get "bdd_size") (BDDM,BDD,BOOL) LONG (m,f,b) ;
fun bdd_size_multiple m fs b = call3 (get "bdd_size_multiple") (BDDM,LIST BDD,BOOL) LONG (m,fs,b) ;

fun bdd_free m f = call2 (get "bdd_free") (BDDM, BDD) VOID (m,f) 

fun bdd_stats m =  call1 (get "bdd_stats") (BDDM) VOID m

datatype Method = SIFT | STABLE_WINDOW | NONE

local
   fun method SIFT          = volOfSym (get "bdd_reorder_sift")
     | method STABLE_WINDOW = volOfSym (get "bdd_reorder_stable_window3")
     | method NONE          = toCbool false (*volOfSym (get "bdd_reorder_none")*)
in
    fun bdd_dynamic_reordering m r =
	call2 (get "bdd_dynamic_reordering") (BDDM, POINTER) VOID (m, method r)
end
 
fun bdd_gc m = call1 (get "bdd_gc") (BDDM) VOID m
fun bdd_reorder m = call1 (get "bdd_reorder") (BDDM) VOID m
fun bdd_var_with_index m i =  call2 (get "bdd_var_with_index") (BDDM, LONG) VAR (m,i) 
fun bdd_cache_ratio m i =  call2 (get "bdd_cache_ratio") (BDDM, INT) INT (m,i) 

end

end;