sig
  val tid_of_var :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    'a -> int array
  val reg_of_expr : 'a Expr0.expr -> 'a Cudd.Bdd.t array
  module Bool :
    sig
      type 'a t = 'a Cudd.Bdd.t
      type dt = Cudd.Man.d Expr0.O.Bool.t
      type vt = Cudd.Man.v Expr0.O.Bool.t
      val of_expr : [> `Bool of 'a Expr0.O.Bool.t ] -> 'a Expr0.O.Bool.t
      val to_expr : 'a Expr0.O.Bool.t -> [> `Bool of 'a Expr0.O.Bool.t ]
      val dtrue :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t
      val dfalse :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t
      val of_bool :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        bool -> 'b Expr0.O.Bool.t
      val var :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'a -> 'b Expr0.O.Bool.t
      val dnot :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t
      val dand :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t
      val dor :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t
      val xor :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t
      val nand :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t
      val nor :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t
      val nxor :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t
      val leq :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t
      val eq :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t
      val ite :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t ->
        'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t
      val is_true :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> bool
      val is_false :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> bool
      val is_cst :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> bool
      val is_eq :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t -> bool
      val is_leq :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t -> bool
      val is_and_false :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t -> bool
      val exist :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'a list -> 'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t
      val forall :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'a list -> 'b Expr0.O.Bool.t -> 'b Expr0.O.Bool.t
      val cofactor :
        'a Expr0.O.Bool.t -> 'a Expr0.O.Bool.t -> 'a Expr0.O.Bool.t
      val restrict :
        'a Expr0.O.Bool.t -> 'a Expr0.O.Bool.t -> 'a Expr0.O.Bool.t
      val tdrestrict :
        'a Expr0.O.Bool.t -> 'a Expr0.O.Bool.t -> 'a Expr0.O.Bool.t
      val permute :
        ?memo:Cudd.Memo.t ->
        'a Expr0.O.Bool.t -> int array -> 'a Expr0.O.Bool.t
      val varmap : 'a Expr0.O.Bool.t -> 'a Expr0.O.Bool.t
      val substitute_by_var :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> ('a * 'a) list -> 'b Expr0.O.Bool.t
      val substitute :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t -> ('a * 'b Expr0.expr) list -> 'b Expr0.O.Bool.t
      val print :
        ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        Format.formatter -> 'b Expr0.O.Bool.t -> unit
    end
  module Bint :
    sig
      type 'a t = 'a Int.t
      type dt = Cudd.Man.d Expr0.O.Bint.t
      type vt = Cudd.Man.v Expr0.O.Bint.t
      val of_expr : [> `Bint of 'a Expr0.O.Bint.t ] -> 'a Expr0.O.Bint.t
      val to_expr : 'a Expr0.O.Bint.t -> [> `Bint of 'a Expr0.O.Bint.t ]
      val of_int :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        [> `Bint of bool * int ] -> int -> 'b Expr0.O.Bint.t
      val var :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'a -> 'b Expr0.O.Bint.t
      val ite :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t ->
        'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t
      val neg :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t
      val succ :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t
      val pred :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t
      val add :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t
      val sub :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t
      val mul :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t
      val shift_left :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        int -> 'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t
      val shift_right :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        int -> 'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t
      val scale :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        int -> 'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t
      val zero :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> 'b Expr0.O.Bool.t
      val eq :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t -> 'b Expr0.O.Bool.t
      val eq_int :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> int -> 'b Expr0.O.Bool.t
      val supeq :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t -> 'b Expr0.O.Bool.t
      val supeq_int :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> int -> 'b Expr0.O.Bool.t
      val sup :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> 'b Expr0.O.Bint.t -> 'b Expr0.O.Bool.t
      val sup_int :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> int -> 'b Expr0.O.Bool.t
      val cofactor :
        'a Expr0.O.Bint.t -> 'a Expr0.O.Bool.t -> 'a Expr0.O.Bint.t
      val restrict :
        'a Expr0.O.Bint.t -> 'a Expr0.O.Bool.t -> 'a Expr0.O.Bint.t
      val tdrestrict :
        'a Expr0.O.Bint.t -> 'a Expr0.O.Bool.t -> 'a Expr0.O.Bint.t
      val permute :
        ?memo:Cudd.Memo.t ->
        'a Expr0.O.Bint.t -> int array -> 'a Expr0.O.Bint.t
      val varmap : 'a Expr0.O.Bint.t -> 'a Expr0.O.Bint.t
      val substitute_by_var :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> ('a * 'a) list -> 'b Expr0.O.Bint.t
      val substitute :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> ('a * 'b Expr0.expr) list -> 'b Expr0.O.Bint.t
      val guard_of_int :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> int -> 'b Expr0.O.Bool.t
      val guardints :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bint.t -> ('b Expr0.O.Bool.t * int) list
      val print :
        ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        Format.formatter -> 'b Expr0.O.Bint.t -> unit
    end
  module Benum :
    sig
      type 'a t = 'a Enum.t
      type dt = Cudd.Man.d Expr0.O.Benum.t
      type vt = Cudd.Man.v Expr0.O.Benum.t
      val of_expr : [> `Benum of 'a Expr0.O.Benum.t ] -> 'a Expr0.O.Benum.t
      val to_expr : 'a Expr0.O.Benum.t -> [> `Benum of 'a Expr0.O.Benum.t ]
      val var :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'a -> 'b Expr0.O.Benum.t
      val ite :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Bool.t ->
        'b Expr0.O.Benum.t -> 'b Expr0.O.Benum.t -> 'b Expr0.O.Benum.t
      val eq :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Benum.t -> 'b Expr0.O.Benum.t -> 'b Expr0.O.Bool.t
      val eq_label :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Benum.t -> 'a -> 'b Expr0.O.Bool.t
      val cofactor :
        'a Expr0.O.Benum.t -> 'a Expr0.O.Bool.t -> 'a Expr0.O.Benum.t
      val restrict :
        'a Expr0.O.Benum.t -> 'a Expr0.O.Bool.t -> 'a Expr0.O.Benum.t
      val tdrestrict :
        'a Expr0.O.Benum.t -> 'a Expr0.O.Bool.t -> 'a Expr0.O.Benum.t
      val permute :
        ?memo:Cudd.Memo.t ->
        'a Expr0.O.Benum.t -> int array -> 'a Expr0.O.Benum.t
      val varmap : 'a Expr0.O.Benum.t -> 'a Expr0.O.Benum.t
      val substitute_by_var :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Benum.t -> ('a * 'a) list -> 'b Expr0.O.Benum.t
      val substitute :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Benum.t -> ('a * 'b Expr0.expr) list -> 'b Expr0.O.Benum.t
      val guard_of_label :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Benum.t -> 'a -> 'b Expr0.O.Bool.t
      val guardlabels :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Expr0.O.Benum.t -> ('b Expr0.O.Bool.t * 'a) list
      val print :
        ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        Format.formatter -> 'b Expr0.O.Benum.t -> unit
    end
  val typ_of_expr :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    'b Expr0.t -> [> 'a Env.typ ]
  val var :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    'a -> 'b Expr0.t
  val ite : 'a Expr0.O.Bool.t -> 'a Expr0.t -> 'a Expr0.t -> 'a Expr0.t
  val eq :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    'b Expr0.t -> 'b Expr0.t -> 'b Expr0.O.Bool.t
  val substitute_by_var :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    'b Expr0.t -> ('a * 'a) list -> 'b Expr0.t
  val substitute :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    'b Expr0.t -> ('a * 'b Expr0.t) list -> 'b Expr0.t
  val support :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    'b Expr0.t -> 'a PSette.t
  val support_cond : 'a Cudd.Man.t -> 'a Expr0.t -> 'a Cudd.Bdd.t
  val cube_of_bdd :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    'b Cudd.Bdd.t -> 'b Cudd.Bdd.t
  val tbdd_of_texpr : 'a Expr0.t array -> 'a Cudd.Bdd.t array
  val texpr_of_tbdd :
    'a Expr0.t array -> 'a Cudd.Bdd.t array -> 'a Expr0.t array
  val print :
    ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    Format.formatter -> [< 'b Expr0.t ] -> unit
  val print_minterm :
    ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    Format.formatter -> Cudd.Man.tbool array -> unit
  val print_bdd :
    ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    Format.formatter -> 'b Cudd.Bdd.t -> unit
  val print_idcondb :
    ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    Format.formatter -> int * bool -> unit
  val print_idcond :
    ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    Format.formatter -> int -> unit
  val permutation_of_rename :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    ('a * 'a) list -> int array
  val composition_of_lvarexpr :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    ('a * 'b Expr0.t) list -> 'b Cudd.Bdd.t array
  val composition_of_lvarlexpr :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    'a list -> 'b Expr0.t list -> 'b Cudd.Bdd.t array
  val bddsupport :
    ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
    'a list -> 'b Cudd.Bdd.t
  val varmap : 'a Expr0.t -> 'a Expr0.t
  val permute : ?memo:Cudd.Memo.t -> 'a Expr0.t -> int array -> 'a Expr0.t
  val permute_list :
    ?memo:Cudd.Memo.t -> 'a Expr0.t list -> int array -> 'a Expr0.t list
  val compose :
    ?memo:Cudd.Memo.t -> 'a Expr0.t -> 'a Cudd.Bdd.t array -> 'a Expr0.t
  module Expr :
    sig
      type 'a atom =
          Tbool of 'a * bool
        | Tint of 'a * int list
        | Tenum of 'a * 'a list
      type 'a term =
          Tatom of 'a Expr0.O.Expr.atom
        | Texternal of (int * bool)
        | Tcst of bool
      type 'a conjunction = Conjunction of 'a Expr0.O.Expr.term list | Cfalse
      type 'a disjunction =
          Disjunction of 'a Expr0.O.Expr.conjunction list
        | Dtrue
      val map_atom :
        ('a -> 'b) -> 'a Expr0.O.Expr.atom -> 'b Expr0.O.Expr.atom
      val map_term :
        ('a -> 'b) -> 'a Expr0.O.Expr.term -> 'b Expr0.O.Expr.term
      val map_conjunction :
        ('a -> 'b) ->
        'a Expr0.O.Expr.conjunction -> 'b Expr0.O.Expr.conjunction
      val map_disjunction :
        ('a -> 'b) ->
        'a Expr0.O.Expr.disjunction -> 'b Expr0.O.Expr.disjunction
      val term_of_vint :
        'a -> 'b Int.t -> Reg.Minterm.t -> 'a Expr0.O.Expr.term
      val term_of_venum :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'a -> 'b Enum.t -> Reg.Minterm.t -> 'a Expr0.O.Expr.term
      val term_of_idcondb :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        int * bool -> 'a Expr0.O.Expr.term
      val bool_of_tbool : Cudd.Man.tbool -> bool
      val mand :
        'a Expr0.O.Expr.term list Pervasives.ref ->
        'a Expr0.O.Expr.term -> unit
      val conjunction_of_minterm :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        Cudd.Man.tbool array -> 'a Expr0.O.Expr.conjunction
      val disjunction_of_bdd :
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        'b Cudd.Bdd.t -> 'a Expr0.O.Expr.disjunction
      val print_term :
        ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        Format.formatter -> 'a Expr0.O.Expr.term -> unit
      val print_conjunction :
        ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        Format.formatter -> 'a Expr0.O.Expr.conjunction -> unit
      val print_disjunction :
        ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
        ('a, [> 'a Env.typ ], [> 'a Env.typdef ], 'b, 'c) Env.O.t ->
        Format.formatter -> 'a Expr0.O.Expr.disjunction -> unit
    end
end