sig
  type ('a, 'k) node
  type ('a, 'k) mem
  val init : ('a -> int) -> ('a -> 'a -> bool) -> ('a, 'k) Bdd.mem
  val constant : ('a, 'k) Bdd.mem -> 'a -> ('a, 'k) Bdd.node
  val unary :
    ('b, 'k) Bdd.mem -> ('a -> 'b) -> ('a, 'k) Bdd.node -> ('b, 'k) Bdd.node
  val binary :
    ('c, 'k) Bdd.mem ->
    ('a -> 'b -> 'c) ->
    ('a, 'k) Bdd.node -> ('b, 'k) Bdd.node -> ('c, 'k) Bdd.node
  val hide :
    ('a, 'k) Bdd.mem ->
    'k ->
    (('a, 'k) Bdd.node -> ('a, 'k) Bdd.node -> ('a, 'k) Bdd.node) ->
    ('a, 'k) Bdd.node -> ('a, 'k) Bdd.node
  val walk :
    ((('a, 'k) Bdd.node -> unit) -> ('a, 'k) Bdd.node -> unit) ->
    ('a, 'k) Bdd.node -> unit
  val partial_apply :
    ('a, 'k) Bdd.mem ->
    ('k -> bool option) -> ('a, 'k) Bdd.node -> ('a, 'k) Bdd.node
  type ('a, 'k) unifier =
      (('k * bool) list -> 'a -> 'a -> unit) ->
      ('a, 'k) Bdd.node -> ('a, 'k) Bdd.node -> unit
  val unify_naive : bool -> ('a, 'k) Bdd.unifier
  val unify_dsf : bool -> ('a, 'k) Bdd.unifier
  type key = char
  type formula = (bool, Bdd.key) Bdd.node
  val neg : Bdd.formula -> Bdd.formula
  val dsj : Bdd.formula -> Bdd.formula -> Bdd.formula
  val cnj : Bdd.formula -> Bdd.formula -> Bdd.formula
  val xor : Bdd.formula -> Bdd.formula -> Bdd.formula
  val iff : Bdd.formula -> Bdd.formula -> Bdd.formula
  val bot : Bdd.formula
  val top : Bdd.formula
  val var : Bdd.key -> Bdd.formula
  val rav : Bdd.key -> Bdd.formula
  val witness : (bool, 'k) Bdd.node -> ('k * bool) list
  val times :
    ('a, 'k) Bdd.mem ->
    ('a, 'k) Bdd.node ->
    (bool, 'k) Bdd.node -> ('a, 'k) Bdd.node -> ('a, 'k) Bdd.node
  val print_formula : int -> Bdd.formula Common.formatter
  type ('a, 'k) descr = private
      V of 'a
    | N of 'k * ('a, 'k) Bdd.node * ('a, 'k) Bdd.node
  val head : ('a, 'k) Bdd.node -> ('a, 'k) Bdd.descr
  val tag : ('a, 'k) Bdd.node -> int
  val hash : ('a, 'k) Bdd.node -> int
  val node :
    ('a, 'k) Bdd.mem ->
    'k -> ('a, 'k) Bdd.node -> ('a, 'k) Bdd.node -> ('a, 'k) Bdd.node
  val reset_caches : unit -> unit
end