Module Cudd

module Cudd: sig .. end

An Ocaml interface to the CUDD BDD library.

type bdd

Abstract type for BDDs. BDDs are automatically referenced at creation and dereferenced with garbage collecting.

val init : int -> unit

Initialization of CUDD. Should be called with the number of variables you plan to use. Reordering is automatically activated.

val bdd_true : unit -> bdd

val bdd_false : unit -> bdd

val bdd_not : bdd -> bdd

val bddAnd : bdd -> bdd -> bdd

val bddOr : bdd -> bdd -> bdd

val ithVar : int -> bdd

val bddExistAbstract : bdd -> bdd -> bdd

val bddUnivAbstract : bdd -> bdd -> bdd

val bddAndAbstract : bdd -> bdd -> bdd -> bdd

val make_cube : int list -> bdd

val bddSwapVariables : bdd -> int array -> int array -> bdd

val bddVectorCompose : bdd -> bdd array -> bdd

Warning: this function will cause a core dump if the biggest index of the array is not as big as the biggest variable in the bdd

val equal : bdd -> bdd -> bool

val output_file : string -> bdd -> unit

val bddRestrict : bdd -> bdd -> bdd

val value : bdd -> int

return 1 if the bdd is the constant true, 0 for the constant false, and -1 if it is not constant

val t : bdd -> bdd

then child of a node

else child of a node

val e : bdd -> bdd

val nodeReadIndex : bdd -> int

val isComplement : bdd -> bool

val isConstant : bdd -> bool

val id : bdd -> nativeint