sig
  type 'a conjunction = Conjunction of 'a list | Cfalse
  type 'a disjunction = Disjunction of 'a list | Dtrue
  type 'a cnf = 'a Bdd.Normalform.disjunction Bdd.Normalform.conjunction
  type 'a dnf = 'a Bdd.Normalform.conjunction Bdd.Normalform.disjunction
  type ('a, 'b) tree = ('a * bool) list * ('a, 'b) Bdd.Normalform.decision
  and ('a, 'b) decision =
      Leaf of 'b
    | Ite of 'a * ('a, 'b) Bdd.Normalform.tree * ('a, 'b) Bdd.Normalform.tree
  val conjunction_false : 'a Bdd.Normalform.conjunction
  val conjunction_true : 'a Bdd.Normalform.conjunction
  val disjunction_false : 'a Bdd.Normalform.disjunction
  val disjunction_true : 'a Bdd.Normalform.disjunction
  val cnf_false : 'a Bdd.Normalform.cnf
  val cnf_true : 'a Bdd.Normalform.cnf
  val dnf_false : 'a Bdd.Normalform.dnf
  val dnf_true : 'a Bdd.Normalform.dnf
  val conjunction_and :
    ?merge:('a list -> 'a list -> 'a list) ->
    'a Bdd.Normalform.conjunction ->
    'a Bdd.Normalform.conjunction -> 'a Bdd.Normalform.conjunction
  val disjunction_or :
    ?merge:('a list -> 'a list -> 'a list) ->
    'a Bdd.Normalform.disjunction ->
    'a Bdd.Normalform.disjunction -> 'a Bdd.Normalform.disjunction
  val conjunction_and_term :
    'a Bdd.Normalform.conjunction -> 'a -> 'a Bdd.Normalform.conjunction
  val disjunction_or_term :
    'a Bdd.Normalform.disjunction -> 'a -> 'a Bdd.Normalform.disjunction
  val minterm_of_tree :
    ?compare:'b PHashhe.compare ->
    ('a, 'b) Bdd.Normalform.tree ->
    (('a * bool) Bdd.Normalform.dnf * 'b) list
  val rev_map_conjunction :
    ('a -> 'b) ->
    'a Bdd.Normalform.conjunction -> 'b Bdd.Normalform.conjunction
  val rev_map_disjunction :
    ('a -> 'b) ->
    'a Bdd.Normalform.disjunction -> 'b Bdd.Normalform.disjunction
  val rev_map2_conjunction :
    ('a -> 'b -> 'c) ->
    'a Bdd.Normalform.conjunction ->
    'b Bdd.Normalform.conjunction -> 'c Bdd.Normalform.conjunction
  val rev_map2_disjunction :
    ('a -> 'b -> 'c) ->
    'a Bdd.Normalform.disjunction ->
    'b Bdd.Normalform.disjunction -> 'c Bdd.Normalform.disjunction
  val map_conjunction :
    ('a -> 'b) ->
    'a Bdd.Normalform.conjunction -> 'b Bdd.Normalform.conjunction
  val map_disjunction :
    ('a -> 'b) ->
    'a Bdd.Normalform.disjunction -> 'b Bdd.Normalform.disjunction
  val map_cnf : ('a -> 'b) -> 'a Bdd.Normalform.cnf -> 'b Bdd.Normalform.cnf
  val map_dnf : ('a -> 'b) -> 'a Bdd.Normalform.dnf -> 'b Bdd.Normalform.dnf
  val map_tree :
    ('a -> 'c) ->
    ('b -> 'd) ->
    ('a, 'b) Bdd.Normalform.tree -> ('c, 'd) Bdd.Normalform.tree
  val print_conjunction :
    ?firstconj:(unit, Format.formatter, unit) Pervasives.format ->
    ?sepconj:(unit, Format.formatter, unit) Pervasives.format ->
    ?lastconj:(unit, Format.formatter, unit) Pervasives.format ->
    (Format.formatter -> 'a -> unit) ->
    Format.formatter -> 'a Bdd.Normalform.conjunction -> unit
  val print_disjunction :
    ?firstdisj:(unit, Format.formatter, unit) Pervasives.format ->
    ?sepdisj:(unit, Format.formatter, unit) Pervasives.format ->
    ?lastdisj:(unit, Format.formatter, unit) Pervasives.format ->
    (Format.formatter -> 'a -> unit) ->
    Format.formatter -> 'a Bdd.Normalform.disjunction -> unit
  val print_cnf :
    ?firstconj:(unit, Format.formatter, unit) Pervasives.format ->
    ?sepconj:(unit, Format.formatter, unit) Pervasives.format ->
    ?lastconj:(unit, Format.formatter, unit) Pervasives.format ->
    ?firstdisj:(unit, Format.formatter, unit) Pervasives.format ->
    ?sepdisj:(unit, Format.formatter, unit) Pervasives.format ->
    ?lastdisj:(unit, Format.formatter, unit) Pervasives.format ->
    (Format.formatter -> 'a -> unit) ->
    Format.formatter -> 'a Bdd.Normalform.cnf -> unit
  val print_dnf :
    ?firstdisj:(unit, Format.formatter, unit) Pervasives.format ->
    ?sepdisj:(unit, Format.formatter, unit) Pervasives.format ->
    ?lastdisj:(unit, Format.formatter, unit) Pervasives.format ->
    ?firstconj:(unit, Format.formatter, unit) Pervasives.format ->
    ?sepconj:(unit, Format.formatter, unit) Pervasives.format ->
    ?lastconj:(unit, Format.formatter, unit) Pervasives.format ->
    (Format.formatter -> 'a -> unit) ->
    Format.formatter -> 'a Bdd.Normalform.dnf -> unit
  val print_tree_minterm :
    ?compare:'a PHashhe.compare ->
    (Format.formatter -> ('b * bool) Bdd.Normalform.dnf -> unit) ->
    (Format.formatter -> 'a -> unit) ->
    Format.formatter -> ('b, 'a) Bdd.Normalform.tree -> unit
  val print_tree :
    (Format.formatter -> 'a -> unit) ->
    (Format.formatter -> 'b -> unit) ->
    Format.formatter -> ('a, 'b) Bdd.Normalform.tree -> unit
end