sig
  type bnode = BIte of int * int * bool * int | BTrue
  type 'a bdd = {
    cond : int PSette.t Pervasives.ref;
    mutable bdef : (int, Output.bnode) PMappe.t;
    bhash : ('a Cudd.Bdd.t, int) Hashhe.t;
    mutable blastid : int;
  }
  type 'a vnode = VIte of int * int * int | VCst of 'a
  type 'a vdd = {
    cond : int PSette.t Pervasives.ref;
    mutable vdef : (int, 'a Output.vnode) PMappe.t;
    lhash : ('a, unit) PHashhe.t;
    vhash : ('a Cudd.Vdd.t, int) Hashhe.t;
    mutable vlastid : int;
  }
  type anode = AIte of int * int * int | ACst of float
  type add = {
    cond : int PSette.t Pervasives.ref;
    mutable adef : (int, Output.anode) PMappe.t;
    mutable lset : float Sette.t;
    ahash : (Cudd.Add.t, int) Hashhe.t;
    mutable alastid : int;
  }
  val make_bdd : cond:int PSette.t Pervasives.ref -> 'a Output.bdd
  val signid_of_bdd : 'a Output.bdd -> 'a Cudd.Bdd.t -> bool * int
  val make_vdd :
    compare:'a Cudd.PWeakke.compare ->
    cond:int PSette.t Pervasives.ref -> 'a Output.vdd
  val make_mtbdd :
    table:'a Cudd.Mtbdd.table ->
    cond:int PSette.t Pervasives.ref -> 'a Cudd.Mtbdd.unique Output.vdd
  val make_mtbddc :
    table:'a Cudd.Mtbddc.table ->
    cond:int PSette.t Pervasives.ref -> 'a Cudd.Mtbddc.unique Output.vdd
  val id_of_vdd : 'a Output.vdd -> 'a Cudd.Vdd.t -> int
  val iter_cond_ordered :
    int PSette.t -> 'a Cudd.Man.t -> (int -> unit) -> unit
  val iter_bdef_ordered :
    'a Output.bdd -> (int -> Output.bnode -> unit) -> unit
  val iter_vdef_ordered :
    'a Output.vdd -> (int -> 'a Output.vnode -> unit) -> unit
end