sig
  module Output :
    sig
      type bnode = BIte of int * int * bool * int | BTrue
      type 'a bdd = {
        cond : int PSette.t Pervasives.ref;
        mutable bdef : (int, Bdd.Output.bnode) PMappe.t;
        bhash : ('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, 'Bdd.Output.vnode) PMappe.t;
        lhash : ('a, unit) PHashhe.t;
        vhash : ('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, Bdd.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 -> 'Bdd.Output.bdd
      val signid_of_bdd : 'Bdd.Output.bdd -> 'Cudd.Bdd.t -> bool * int
      val make_vdd :
        compare:'Cudd.PWeakke.compare ->
        cond:int PSette.t Pervasives.ref -> 'Bdd.Output.vdd
      val make_mtbdd :
        table:'Cudd.Mtbdd.table ->
        cond:int PSette.t Pervasives.ref ->
        'Cudd.Mtbdd.unique Bdd.Output.vdd
      val make_mtbddc :
        table:'Cudd.Mtbddc.table ->
        cond:int PSette.t Pervasives.ref ->
        'Cudd.Mtbddc.unique Bdd.Output.vdd
      val id_of_vdd : 'Bdd.Output.vdd -> 'Cudd.Vdd.t -> int
      val iter_cond_ordered :
        int PSette.t -> 'Cudd.Man.t -> (int -> unit) -> unit
      val iter_bdef_ordered :
        'Bdd.Output.bdd -> (int -> Bdd.Output.bnode -> unit) -> unit
      val iter_vdef_ordered :
        'Bdd.Output.vdd -> (int -> 'Bdd.Output.vnode -> unit) -> unit
    end
  module Normalform :
    sig
      type 'a conjunction = Conjunction of 'a list | Cfalse
      type 'a disjunction = Disjunction of 'a list | Dtrue
      type 'a cnf = 'Bdd.Normalform.disjunction Bdd.Normalform.conjunction
      type 'a dnf = '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 : 'Bdd.Normalform.conjunction
      val conjunction_true : 'Bdd.Normalform.conjunction
      val disjunction_false : 'Bdd.Normalform.disjunction
      val disjunction_true : 'Bdd.Normalform.disjunction
      val cnf_false : 'Bdd.Normalform.cnf
      val cnf_true : 'Bdd.Normalform.cnf
      val dnf_false : 'Bdd.Normalform.dnf
      val dnf_true : 'Bdd.Normalform.dnf
      val conjunction_and :
        ?merge:('a list -> 'a list -> 'a list) ->
        'Bdd.Normalform.conjunction ->
        'Bdd.Normalform.conjunction -> 'Bdd.Normalform.conjunction
      val disjunction_or :
        ?merge:('a list -> 'a list -> 'a list) ->
        'Bdd.Normalform.disjunction ->
        'Bdd.Normalform.disjunction -> 'Bdd.Normalform.disjunction
      val conjunction_and_term :
        'Bdd.Normalform.conjunction -> '-> 'Bdd.Normalform.conjunction
      val disjunction_or_term :
        'Bdd.Normalform.disjunction -> '-> 'Bdd.Normalform.disjunction
      val minterm_of_tree :
        ?compare:'PHashhe.compare ->
        ('a, 'b) Bdd.Normalform.tree ->
        (('a * bool) Bdd.Normalform.dnf * 'b) list
      val rev_map_conjunction :
        ('-> 'b) ->
        'Bdd.Normalform.conjunction -> 'Bdd.Normalform.conjunction
      val rev_map_disjunction :
        ('-> 'b) ->
        'Bdd.Normalform.disjunction -> 'Bdd.Normalform.disjunction
      val rev_map2_conjunction :
        ('-> '-> 'c) ->
        'Bdd.Normalform.conjunction ->
        'Bdd.Normalform.conjunction -> 'Bdd.Normalform.conjunction
      val rev_map2_disjunction :
        ('-> '-> 'c) ->
        'Bdd.Normalform.disjunction ->
        'Bdd.Normalform.disjunction -> 'Bdd.Normalform.disjunction
      val map_conjunction :
        ('-> 'b) ->
        'Bdd.Normalform.conjunction -> 'Bdd.Normalform.conjunction
      val map_disjunction :
        ('-> 'b) ->
        'Bdd.Normalform.disjunction -> 'Bdd.Normalform.disjunction
      val map_cnf :
        ('-> 'b) -> 'Bdd.Normalform.cnf -> 'Bdd.Normalform.cnf
      val map_dnf :
        ('-> 'b) -> 'Bdd.Normalform.dnf -> 'Bdd.Normalform.dnf
      val map_tree :
        ('-> 'c) ->
        ('-> '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 -> '-> unit) ->
        Format.formatter -> '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 -> '-> unit) ->
        Format.formatter -> '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 -> '-> unit) ->
        Format.formatter -> '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 -> '-> unit) ->
        Format.formatter -> 'Bdd.Normalform.dnf -> unit
      val print_tree_minterm :
        ?compare:'PHashhe.compare ->
        (Format.formatter -> ('b * bool) Bdd.Normalform.dnf -> unit) ->
        (Format.formatter -> '-> unit) ->
        Format.formatter -> ('b, 'a) Bdd.Normalform.tree -> unit
      val print_tree :
        (Format.formatter -> '-> unit) ->
        (Format.formatter -> '-> unit) ->
        Format.formatter -> ('a, 'b) Bdd.Normalform.tree -> unit
    end
  module Reg :
    sig
      type 'a t = 'Cudd.Bdd.t array
      type dt = Cudd.Man.d Bdd.Reg.t
      type vt = Cudd.Man.v Bdd.Reg.t
      val lnot : 'Bdd.Reg.t -> 'Bdd.Reg.t
      val shift_left :
        'Cudd.Man.t -> int -> 'Bdd.Reg.t -> 'Bdd.Reg.t * 'Cudd.Bdd.t
      val shift_right :
        'Cudd.Man.t -> int -> 'Bdd.Reg.t -> 'Bdd.Reg.t * 'Cudd.Bdd.t
      val shift_right_logical :
        'Cudd.Man.t -> int -> 'Bdd.Reg.t -> 'Bdd.Reg.t * 'Cudd.Bdd.t
      val extend :
        'Cudd.Man.t -> signed:bool -> int -> 'Bdd.Reg.t -> 'Bdd.Reg.t
      val succ :
        'Cudd.Man.t -> 'Bdd.Reg.t -> 'Bdd.Reg.t * 'Cudd.Bdd.t
      val pred :
        'Cudd.Man.t -> 'Bdd.Reg.t -> 'Bdd.Reg.t * 'Cudd.Bdd.t
      val add :
        'Cudd.Man.t ->
        'Bdd.Reg.t ->
        'Bdd.Reg.t -> 'Bdd.Reg.t * 'Cudd.Bdd.t * 'Cudd.Bdd.t
      val sub :
        'Cudd.Man.t ->
        'Bdd.Reg.t ->
        'Bdd.Reg.t -> 'Bdd.Reg.t * 'Cudd.Bdd.t * 'Cudd.Bdd.t
      val neg : 'Bdd.Reg.t -> 'Bdd.Reg.t
      val scale : int -> 'Bdd.Reg.t -> 'Bdd.Reg.t
      val mul : 'Bdd.Reg.t -> 'Bdd.Reg.t -> 'Bdd.Reg.t
      val ite : 'Cudd.Bdd.t -> 'Bdd.Reg.t -> 'Bdd.Reg.t -> 'Bdd.Reg.t
      val is_cst : 'Bdd.Reg.t -> bool
      val zero : 'Cudd.Man.t -> 'Bdd.Reg.t -> 'Cudd.Bdd.t
      val equal :
        'Cudd.Man.t -> 'Bdd.Reg.t -> 'Bdd.Reg.t -> 'Cudd.Bdd.t
      val greatereq :
        'Cudd.Man.t -> 'Bdd.Reg.t -> 'Bdd.Reg.t -> 'Cudd.Bdd.t
      val greater :
        'Cudd.Man.t -> 'Bdd.Reg.t -> 'Bdd.Reg.t -> 'Cudd.Bdd.t
      val highereq :
        'Cudd.Man.t -> 'Bdd.Reg.t -> 'Bdd.Reg.t -> 'Cudd.Bdd.t
      val higher :
        'Cudd.Man.t -> 'Bdd.Reg.t -> 'Bdd.Reg.t -> 'Cudd.Bdd.t
      val min_size : int -> int
      val of_int : 'Cudd.Man.t -> int -> int -> 'Bdd.Reg.t
      val to_int : signed:bool -> 'Bdd.Reg.t -> int
      val equal_int : 'Cudd.Man.t -> 'Bdd.Reg.t -> int -> 'Cudd.Bdd.t
      val greatereq_int :
        'Cudd.Man.t -> 'Bdd.Reg.t -> int -> 'Cudd.Bdd.t
      val greater_int : 'Cudd.Man.t -> 'Bdd.Reg.t -> int -> 'Cudd.Bdd.t
      val highereq_int :
        'Cudd.Man.t -> 'Bdd.Reg.t -> int -> 'Cudd.Bdd.t
      val higher_int : 'Cudd.Man.t -> 'Bdd.Reg.t -> int -> 'Cudd.Bdd.t
      module Minterm :
        sig
          type t = Cudd.Man.tbool array
          val is_indet : Bdd.Reg.Minterm.t -> bool
          val of_int : int -> int -> Bdd.Reg.Minterm.t
          val to_int : signed:bool -> Bdd.Reg.Minterm.t -> int
          val iter : (Bdd.Reg.Minterm.t -> unit) -> Bdd.Reg.Minterm.t -> unit
          val map : (Bdd.Reg.Minterm.t -> 'a) -> Bdd.Reg.Minterm.t -> 'a list
        end
      val guard_of_minterm :
        'Cudd.Man.t -> 'Bdd.Reg.t -> Bdd.Reg.Minterm.t -> 'Cudd.Bdd.t
      val guard_of_int :
        'Cudd.Man.t -> 'Bdd.Reg.t -> int -> 'Cudd.Bdd.t
      val guardints :
        'Cudd.Man.t ->
        signed:bool -> 'Bdd.Reg.t -> ('Cudd.Bdd.t * int) list
      val cofactor : 'Bdd.Reg.t -> 'Cudd.Bdd.t -> 'Bdd.Reg.t
      val restrict : 'Bdd.Reg.t -> 'Cudd.Bdd.t -> 'Bdd.Reg.t
      val tdrestrict : 'Bdd.Reg.t -> 'Cudd.Bdd.t -> 'Bdd.Reg.t
      val print :
        (Format.formatter -> int -> unit) ->
        Format.formatter -> 'Bdd.Reg.t -> unit
      val print_minterm :
        signed:bool ->
        (Format.formatter -> 'Cudd.Bdd.t -> unit) ->
        Format.formatter -> 'Bdd.Reg.t -> unit
      val permute :
        ?memo:Cudd.Memo.t -> 'Bdd.Reg.t -> int array -> 'Bdd.Reg.t
      val varmap : 'Bdd.Reg.t -> 'Bdd.Reg.t
      val vectorcompose :
        ?memo:Cudd.Memo.t ->
        'Cudd.Bdd.t array -> 'Bdd.Reg.t -> 'Bdd.Reg.t
    end
  module Env :
    sig
      exception Bddindex
      type 'a typdef = [ `Benum of 'a array ]
      type 'a typ = [ `Benum of '| `Bint of bool * int | `Bool ]
      type 'a symbol = {
        compare : '-> '-> int;
        marshal : '-> string;
        unmarshal : string -> 'a;
        mutable print : Format.formatter -> '-> unit;
      }
      type ('a, 'b, 'c, 'd, 'e) t0 = {
        mutable cudd : 'Cudd.Man.t;
        mutable typdef : ('a, 'c) PMappe.t;
        mutable vartyp : ('a, 'b) PMappe.t;
        mutable bddindex0 : int;
        mutable bddsize : int;
        mutable bddindex : int;
        mutable bddincr : int;
        mutable idcondvar : (int, 'a) PMappe.t;
        mutable vartid : ('a, int array) PMappe.t;
        mutable varset : ('a, 'Cudd.Bdd.t) PMappe.t;
        mutable print_external_idcondb :
          Format.formatter -> int * bool -> unit;
        mutable ext : 'e;
        symbol : 'Bdd.Env.symbol;
        copy_ext : '-> 'e;
      }
      module O :
        sig
          type ('a, 'b, 'c, 'd, 'e) t = ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0
            constraint 'b = [> 'Bdd.Env.typ ]
            constraint 'c = [> 'Bdd.Env.typdef ]
          val make :
            symbol:'Bdd.Env.symbol ->
            copy_ext:('-> 'e) ->
            ?bddindex0:int ->
            ?bddsize:int ->
            ?relational:bool ->
            'Cudd.Man.t ->
            '->
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t
          val print :
            (Format.formatter -> ([> 'Bdd.Env.typ ] as 'b) -> unit) ->
            (Format.formatter -> ([> 'Bdd.Env.typdef ] as 'c) -> unit) ->
            (Format.formatter -> '-> unit) ->
            Format.formatter -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> unit
        end
      type ('a, 'd) t =
          ('a, 'Bdd.Env.typ, 'Bdd.Env.typdef, 'd, unit) Bdd.Env.O.t
      val print_typ :
        (Format.formatter -> '-> unit) ->
        Format.formatter -> [> 'Bdd.Env.typ ] -> unit
      val print_typdef :
        (Format.formatter -> '-> unit) ->
        Format.formatter -> [> 'Bdd.Env.typdef ] -> unit
      val print_tid : Format.formatter -> int array -> unit
      val print_idcondb :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        Format.formatter -> int * bool -> unit
      val print_order :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        Format.formatter -> unit
      val print :
        Format.formatter ->
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        unit
      val marshal : '-> string
      val unmarshal : string -> 'a
      val make_symbol :
        ?compare:('-> '-> int) ->
        ?marshal:('-> string) ->
        ?unmarshal:(string -> 'a) ->
        (Format.formatter -> '-> unit) -> 'Bdd.Env.symbol
      val string_symbol : string Bdd.Env.symbol
      val make :
        symbol:'Bdd.Env.symbol ->
        ?bddindex0:int ->
        ?bddsize:int ->
        ?relational:bool -> 'Cudd.Man.t -> ('a, 'd) Bdd.Env.t
      val make_string :
        ?bddindex0:int ->
        ?bddsize:int ->
        ?relational:bool -> 'Cudd.Man.t -> (string, 'd) Bdd.Env.t
      val copy :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
      val mem_typ :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        '-> bool
      val mem_var :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        '-> bool
      val mem_label :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        '-> bool
      val typdef_of_typ :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ] as 'b, 'd, 'e)
        Bdd.Env.O.t -> '-> 'b
      val typ_of_var :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ], 'd, 'e)
        Bdd.Env.O.t -> '-> 'b
      val vars :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'PSette.t
      val labels :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'PSette.t
      val add_typ_with :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ] as 'b, 'd, 'e)
        Bdd.Env.O.t -> '-> '-> unit
      val add_vars_with :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ], 'd, 'e)
        Bdd.Env.O.t -> ('a * 'b) list -> int array option
      val remove_vars_with :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'a list -> int array option
      val rename_vars_with :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        ('a * 'a) list -> int array option
      val add_typ :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t -> '-> '-> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
      val add_vars :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t -> ('a * 'b) list -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
      val remove_vars :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t -> 'a list -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
      val rename_vars :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t -> ('a * 'a) list -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
      val add_var_with :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ], 'd, 'e)
        Bdd.Env.O.t -> '-> '-> unit
      val iter_ordered :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        ('-> int array -> unit) -> unit
      val is_leq :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> bool
      val is_eq :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> bool
      val shift :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t -> int -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
      val lce :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t ->
        ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t
      val permutation12 :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> int array
      val permutation21 :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> int array
      type 'a change = {
        intro : int array option;
        remove : ('Cudd.Bdd.t * int array) option;
      }
      val compute_change :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t -> ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t -> 'Bdd.Env.change
      val notfound :
        ('a, Format.formatter, unit, 'b) Pervasives.format4 -> 'a
      type ('a, 'b) value = { env : 'a; val0 : 'b; }
      val make_value :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t ->
        '-> (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value
      val get_env : ('a, 'b) Bdd.Env.value -> 'a
      val get_val0 : ('a, 'b) Bdd.Env.value -> 'b
      val extend_environment :
        ('-> int array -> 'f) ->
        (('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd,
          'e)
         Bdd.Env.O.t, 'f)
        Bdd.Env.value ->
        ('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value
      val compare_idb : int * bool -> int * bool -> int
      val permutation :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        int array
      val permute_with :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        int array -> unit
      val normalize_with :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        int array
      val check_normalized :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        bool
      val compose_permutation : int array -> int array -> int array
      val compose_opermutation :
        int array option -> int array option -> int array option
      val permutation_of_offset : int -> int -> int array
      val check_var :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        '-> unit
      val check_lvar :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'a list -> unit
      val check_value :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value -> unit
      val check_value2 :
        (('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd,
          'e)
         Bdd.Env.O.t, 'f)
        Bdd.Env.value ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value -> unit
      val check_value3 :
        (('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd,
          'e)
         Bdd.Env.O.t, 'f)
        Bdd.Env.value ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'h) Bdd.Env.value -> unit
      val check_lvarvalue :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t ->
        ('a * (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value) list ->
        ('a * 'f) list
      val check_lvalue :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value list -> 'f list
      val check_ovalue :
        ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd, 'e)
        Bdd.Env.O.t ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value option ->
        'f option
      val mapunop :
        ('-> 'g) ->
        (('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd,
          'e)
         Bdd.Env.O.t, 'f)
        Bdd.Env.value -> (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value
      val mapbinop :
        ('-> '-> 'h) ->
        (('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd,
          'e)
         Bdd.Env.O.t, 'f)
        Bdd.Env.value ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'h) Bdd.Env.value
      val mapbinope :
        (('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd,
          'e)
         Bdd.Env.O.t -> '-> '-> 'h) ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'f) Bdd.Env.value ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'h) Bdd.Env.value
      val mapterop :
        ('-> '-> '-> 'i) ->
        (('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'c, 'd,
          'e)
         Bdd.Env.O.t, 'f)
        Bdd.Env.value ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'g) Bdd.Env.value ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'h) Bdd.Env.value ->
        (('a, 'b, 'c, 'd, 'e) Bdd.Env.O.t, 'i) Bdd.Env.value
    end
  module Int :
    sig
      type 'a t = { signed : bool; reg : 'Cudd.Bdd.t array; }
      type dt = Cudd.Man.d Bdd.Int.t
      type vt = Cudd.Man.v Bdd.Int.t
      exception Typing of string
      val extend : 'Cudd.Man.t -> int -> 'Bdd.Int.t -> 'Bdd.Int.t
      val neg : 'Bdd.Int.t -> 'Bdd.Int.t
      val succ : 'Bdd.Int.t -> 'Bdd.Int.t
      val pred : 'Bdd.Int.t -> 'Bdd.Int.t
      val add : 'Bdd.Int.t -> 'Bdd.Int.t -> 'Bdd.Int.t
      val sub : 'Bdd.Int.t -> 'Bdd.Int.t -> 'Bdd.Int.t
      val mul : 'Bdd.Int.t -> 'Bdd.Int.t -> 'Bdd.Int.t
      val shift_left : int -> 'Bdd.Int.t -> 'Bdd.Int.t
      val shift_right : int -> 'Bdd.Int.t -> 'Bdd.Int.t
      val scale : int -> 'Bdd.Int.t -> 'Bdd.Int.t
      val ite : 'Cudd.Bdd.t -> 'Bdd.Int.t -> 'Bdd.Int.t -> 'Bdd.Int.t
      val is_cst : 'Bdd.Int.t -> bool
      val zero : 'Cudd.Man.t -> 'Bdd.Int.t -> 'Cudd.Bdd.t
      val equal :
        'Cudd.Man.t -> 'Bdd.Int.t -> 'Bdd.Int.t -> 'Cudd.Bdd.t
      val greatereq :
        'Cudd.Man.t -> 'Bdd.Int.t -> 'Bdd.Int.t -> 'Cudd.Bdd.t
      val greater :
        'Cudd.Man.t -> 'Bdd.Int.t -> 'Bdd.Int.t -> 'Cudd.Bdd.t
      val of_int : 'Cudd.Man.t -> bool -> int -> int -> 'Bdd.Int.t
      val to_int : 'Bdd.Int.t -> int
      val equal_int : 'Cudd.Man.t -> 'Bdd.Int.t -> int -> 'Cudd.Bdd.t
      val greatereq_int :
        'Cudd.Man.t -> 'Bdd.Int.t -> int -> 'Cudd.Bdd.t
      val greater_int : 'Cudd.Man.t -> 'Bdd.Int.t -> int -> 'Cudd.Bdd.t
      module Minterm :
        sig
          val iter :
            signed:bool -> (int -> unit) -> Bdd.Reg.Minterm.t -> unit
          val map :
            signed:bool -> (int -> 'a) -> Bdd.Reg.Minterm.t -> 'a list
        end
      val guard_of_int :
        'Cudd.Man.t -> 'Bdd.Int.t -> int -> 'Cudd.Bdd.t
      val guardints :
        'Cudd.Man.t -> 'Bdd.Int.t -> ('Cudd.Bdd.t * int) list
      val cofactor : 'Bdd.Int.t -> 'Cudd.Bdd.t -> 'Bdd.Int.t
      val restrict : 'Bdd.Int.t -> 'Cudd.Bdd.t -> 'Bdd.Int.t
      val tdrestrict : 'Bdd.Int.t -> 'Cudd.Bdd.t -> 'Bdd.Int.t
      val print :
        (Format.formatter -> int -> unit) ->
        Format.formatter -> 'Bdd.Int.t -> unit
      val print_minterm :
        (Format.formatter -> 'Cudd.Bdd.t -> unit) ->
        Format.formatter -> 'Bdd.Int.t -> unit
      val permute :
        ?memo:Cudd.Memo.t -> 'Bdd.Int.t -> int array -> 'Bdd.Int.t
      val varmap : 'Bdd.Int.t -> 'Bdd.Int.t
      val vectorcompose :
        ?memo:Cudd.Memo.t ->
        'Cudd.Bdd.t array -> 'Bdd.Int.t -> 'Bdd.Int.t
    end
  module Enum :
    sig
      type 'a typ = [ `Benum of 'a ]
      type 'a typdef = [ `Benum of 'a array ]
      type 'a t = { typ : string; reg : 'Bdd.Reg.t; }
      type dt = Cudd.Man.d Bdd.Enum.t
      type vt = Cudd.Man.v Bdd.Enum.t
      val of_label :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        '-> 'Bdd.Enum.t
      val is_cst : 'Bdd.Enum.t -> bool
      val to_code : 'Bdd.Enum.t -> int
      val to_label :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'Bdd.Enum.t -> 'a
      val equal_label :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'Bdd.Enum.t -> '-> 'Cudd.Bdd.t
      val equal :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'Bdd.Enum.t -> 'Bdd.Enum.t -> 'Cudd.Bdd.t
      val ite :
        'Cudd.Bdd.t -> 'Bdd.Enum.t -> 'Bdd.Enum.t -> 'Bdd.Enum.t
      val guard_of_label :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'Bdd.Enum.t -> '-> 'Cudd.Bdd.t
      val guardlabels :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        'Bdd.Enum.t -> ('Cudd.Bdd.t * 'a) list
      val cofactor : 'Bdd.Enum.t -> 'Cudd.Bdd.t -> 'Bdd.Enum.t
      val restrict : 'Bdd.Enum.t -> 'Cudd.Bdd.t -> 'Bdd.Enum.t
      val tdrestrict : 'Bdd.Enum.t -> 'Cudd.Bdd.t -> 'Bdd.Enum.t
      val print :
        (Format.formatter -> int -> unit) ->
        Format.formatter -> 'Bdd.Enum.t -> unit
      val print_minterm :
        (Format.formatter -> 'Cudd.Bdd.t -> unit) ->
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        Format.formatter -> 'Bdd.Enum.t -> unit
      val size_of_typ :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        '-> int
      val maxcode_of_typ :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        '-> int
      val mem_typcode :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        '-> int -> bool
      val labels_of_typ :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        '-> 'a array
      val code_of_label :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        '-> int
      val label_of_typcode :
        ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e) Bdd.Env.O.t ->
        '-> int -> 'a
      module Minterm :
        sig
          val iter :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> '-> ('-> unit) -> Bdd.Reg.Minterm.t -> unit
          val map :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> '-> ('-> 'f) -> Bdd.Reg.Minterm.t -> 'f list
        end
      val permute :
        ?memo:Cudd.Memo.t -> 'Bdd.Enum.t -> int array -> 'Bdd.Enum.t
      val varmap : 'Bdd.Enum.t -> 'Bdd.Enum.t
      val vectorcompose :
        ?memo:Cudd.Memo.t ->
        'Cudd.Bdd.t array -> 'Bdd.Enum.t -> 'Bdd.Enum.t
    end
  module Cond :
    sig
      type ('a, 'b, 'c, 'd) t = {
        symbol : 'Bdd.Env.symbol;
        compare_cond : '-> '-> int;
        negate_cond : '-> '-> 'c;
        support_cond : '-> '-> 'PSette.t;
        mutable print_cond : '-> Format.formatter -> '-> unit;
        mutable cudd : 'Cudd.Man.t;
        mutable bddindex0 : int;
        mutable bddsize : int;
        mutable bddindex : int;
        mutable bddincr : int;
        mutable condidb : ('c, int * bool) PDMappe.t;
        mutable supp : 'Cudd.Bdd.t;
        mutable careset : 'Cudd.Bdd.t;
      }
      val print :
        '-> Format.formatter -> ('a, 'b, 'c, 'd) Bdd.Cond.t -> unit
      val make :
        symbol:'Bdd.Env.symbol ->
        compare_cond:('-> '-> int) ->
        negate_cond:('-> '-> 'c) ->
        support_cond:('-> '-> 'PSette.t) ->
        print_cond:('-> Format.formatter -> '-> unit) ->
        ?bddindex0:int ->
        ?bddsize:int -> 'Cudd.Man.t -> ('a, 'b, 'c, 'd) Bdd.Cond.t
      val copy : ('a, 'b, 'c, 'd) Bdd.Cond.t -> ('a, 'b, 'c, 'd) Bdd.Cond.t
      val permutation : ('a, 'b, 'c, 'd) Bdd.Cond.t -> int array
      val permute_with : ('a, 'b, 'c, 'd) Bdd.Cond.t -> int array -> unit
      val normalize_with : ('a, 'b, 'c, 'd) Bdd.Cond.t -> int array
      val reduce_with : ('a, 'b, 'c, 'd) Bdd.Cond.t -> 'Cudd.Bdd.t -> unit
      val clear : ('a, 'b, 'c, 'd) Bdd.Cond.t -> unit
      val check_normalized : '-> ('a, 'b, 'c, 'd) Bdd.Cond.t -> bool
      val cond_of_idb : ('a, 'b, 'c, 'd) Bdd.Cond.t -> int * bool -> 'c
      val idb_of_cond : '-> ('b, 'a, 'c, 'd) Bdd.Cond.t -> '-> int * bool
      val compute_careset :
        ('a, 'b, 'c, 'd) Bdd.Cond.t -> normalized:bool -> unit
      val is_leq :
        ('a, 'b, 'c, 'd) Bdd.Cond.t -> ('a, 'b, 'c, 'd) Bdd.Cond.t -> bool
      val is_eq :
        ('a, 'b, 'c, 'd) Bdd.Cond.t -> ('a, 'b, 'c, 'd) Bdd.Cond.t -> bool
      val shift :
        ('a, 'b, 'c, 'd) Bdd.Cond.t -> int -> ('a, 'b, 'c, 'd) Bdd.Cond.t
      val lce :
        ('a, 'b, 'c, 'd) Bdd.Cond.t ->
        ('a, 'b, 'c, 'd) Bdd.Cond.t -> ('a, 'b, 'c, 'd) Bdd.Cond.t
      val permutation12 :
        ('a, 'b, 'c, 'd) Bdd.Cond.t ->
        ('a, 'b, 'c, 'd) Bdd.Cond.t -> int array
      val permutation21 :
        ('a, 'b, 'c, 'd) Bdd.Cond.t ->
        ('a, 'b, 'c, 'd) Bdd.Cond.t -> int array
      type ('a, 'b) value = { cond : 'a; val1 : 'b; }
      val make_value : '-> '-> ('a, 'b) Bdd.Cond.value
      val get_cond : ('a, 'b) Bdd.Cond.value -> 'a
      val get_val1 : ('a, 'b) Bdd.Cond.value -> 'b
      val get_env : ('a, ('b, 'c) Bdd.Env.value) Bdd.Cond.value -> 'b
      val get_val0 : ('a, ('b, 'c) Bdd.Env.value) Bdd.Cond.value -> 'c
    end
  module Decompose :
    sig
      type vdd = bool Cudd.Vdd.t
      val vdd_of_bdd : Cudd.Bdd.vt -> bool Cudd.Vdd.t
      val bdd_of_vdd : bool Cudd.Vdd.t -> Cudd.Bdd.vt
      type typ = Bool | Cond | Other
      type info = {
        mutable minlevelbool : int;
        mutable maxlevelbool : int;
        mutable minlevelcond : int;
        mutable maxlevelcond : int;
        varlevel : int array;
        levelvar : int array;
        vartyp : Bdd.Decompose.typ array;
        leveltyp : Bdd.Decompose.typ array;
      }
      val make_info :
        ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
        ('f, 'g, 'h, 'i) Bdd.Cond.t -> Bdd.Decompose.info
      val split_level :
        Cudd.Bdd.vt -> int -> (Cudd.Bdd.vt * Cudd.Bdd.vt) list
      val splitpermutation_of_envcond :
        ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
        ('f, 'g, 'h, 'i) Bdd.Cond.t ->
        [ `BoolCond | `CondBool ] -> int * (int array * int array) option
      val split_bdd :
        ?memo1:Cudd.Memo.t ->
        ?memo2:Cudd.Memo.t ->
        int * (int array * int array) option ->
        Cudd.Bdd.vt -> (Cudd.Bdd.vt * Cudd.Bdd.vt) list
      val cube_split :
        ('a, 'b, 'c, 'd) Bdd.Cond.t ->
        'Cudd.Bdd.t -> 'Cudd.Bdd.t * 'Cudd.Bdd.t
      val decompose_bdd_boolcond :
        ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
        ('f, 'g, 'h, 'i) Bdd.Cond.t ->
        Cudd.Bdd.vt -> (Cudd.Bdd.vt * Cudd.Bdd.vt) list
      val decompose_bdd_condbool :
        ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
        ('f, 'g, 'h, 'i) Bdd.Cond.t ->
        Cudd.Bdd.vt -> (Cudd.Bdd.vt * Cudd.Bdd.vt) list
      val decompose_dd_treecondbool :
        ?careset:'Cudd.Bdd.t ->
        topvar:('-> int) ->
        support:('-> 'Cudd.Bdd.t) ->
        cofactor:('-> 'Cudd.Bdd.t -> 'b) ->
        ('d, 'e, 'f, 'g, 'h) Bdd.Env.t0 ->
        ('i, 'j, 'k, 'a) Bdd.Cond.t -> '-> (int, 'b) Bdd.Normalform.tree
      val decompose_bdd_treecondbool :
        ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
        ('f, 'g, 'h, 'i) Bdd.Cond.t ->
        'Cudd.Bdd.t -> (int, 'Cudd.Bdd.t) Bdd.Normalform.tree
      val decompose_vdd_treecondbool :
        ?careset:Cudd.Bdd.vt ->
        ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
        ('f, 'g, 'h, Cudd.Man.v) Bdd.Cond.t ->
        'Cudd.Vdd.t -> (int, 'Cudd.Vdd.t) Bdd.Normalform.tree
      val decompose_tbdd_tvdd_treecondbool :
        ?careset:Cudd.Bdd.vt ->
        ('a, 'b, 'c, 'd, 'e) Bdd.Env.t0 ->
        ('f, 'g, 'h, Cudd.Man.v) Bdd.Cond.t ->
        Cudd.Bdd.vt array * 'Cudd.Vdd.t array ->
        (int, Cudd.Bdd.vt array * 'Cudd.Vdd.t array) Bdd.Normalform.tree
      val conjunction_of_minterm :
        ?first:int ->
        ?last:int ->
        (int * bool -> 'a) ->
        Cudd.Man.tbool array -> 'Bdd.Normalform.conjunction
      val dnf_of_bdd :
        ?first:int ->
        ?last:int ->
        (int * bool -> 'a) -> 'Cudd.Bdd.t -> 'Bdd.Normalform.dnf
      val descend :
        cudd:'Cudd.Man.t ->
        maxdepth:int ->
        nocare:('-> bool) ->
        cube_of_down:('-> 'Cudd.Bdd.t) ->
        cofactor:('-> 'Cudd.Bdd.t -> 'a) ->
        select:('-> int) ->
        terminal:(depth:int ->
                  newcube:'Cudd.Bdd.t ->
                  cube:'Cudd.Bdd.t -> down:'-> 'b option) ->
        ite:(depth:int ->
             newcube:'Cudd.Bdd.t ->
             cond:int -> dthen:'b option -> delse:'b option -> 'b option) ->
        down:'-> 'b option
      val select_cond : 'Cudd.Bdd.t -> int
      val select_cond_bdd :
        ('a, 'b, 'c, 'd) Bdd.Cond.t -> 'Cudd.Bdd.t -> int
      val bdd_support_cond :
        ('a, 'b, 'c, 'd) Bdd.Cond.t -> 'Cudd.Bdd.t -> 'Cudd.Bdd.t
      val vdd_support_cond :
        ('a, 'b, 'c, Cudd.Man.v) Bdd.Cond.t -> 'Cudd.Vdd.t -> Cudd.Bdd.vt
      val tbdd_tvdd_support_cond :
        ('a, 'b, 'c, Cudd.Man.v) Bdd.Cond.t ->
        Cudd.Bdd.vt array * 'Cudd.Vdd.t array -> Cudd.Bdd.vt
      val tbdd_tvdd_cofactor :
        Cudd.Bdd.vt array * 'Cudd.Vdd.t array ->
        Cudd.Bdd.vt -> Cudd.Bdd.vt array * 'Cudd.Vdd.t array
    end
  module Expr0 :
    sig
      type 'a t =
          [ `Benum of 'Bdd.Enum.t
          | `Bint of 'Bdd.Int.t
          | `Bool of 'Cudd.Bdd.t ]
      type 'a expr = 'Bdd.Expr0.t
      type dt = Cudd.Man.d Bdd.Expr0.t
      type vt = Cudd.Man.v Bdd.Expr0.t
      module Bool :
        sig
          type 'a t = 'Cudd.Bdd.t
          type dt = Cudd.Man.d Bdd.Expr0.Bool.t
          type vt = Cudd.Man.v Bdd.Expr0.Bool.t
          val of_expr : 'Bdd.Expr0.expr -> 'Bdd.Expr0.Bool.t
          val to_expr : 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.expr
          val dtrue : ('a, 'b) Bdd.Env.t -> 'Bdd.Expr0.Bool.t
          val dfalse : ('a, 'b) Bdd.Env.t -> 'Bdd.Expr0.Bool.t
          val of_bool : ('a, 'b) Bdd.Env.t -> bool -> 'Bdd.Expr0.Bool.t
          val var : ('a, 'b) Bdd.Env.t -> '-> 'Bdd.Expr0.Bool.t
          val dnot :
            ('a, 'b) Bdd.Env.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val dand :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val dor :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val xor :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val nand :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val nor :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val nxor :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val leq :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val eq :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val ite :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val is_true : ('a, 'b) Bdd.Env.t -> 'Bdd.Expr0.Bool.t -> bool
          val is_false : ('a, 'b) Bdd.Env.t -> 'Bdd.Expr0.Bool.t -> bool
          val is_cst : ('a, 'b) Bdd.Env.t -> 'Bdd.Expr0.Bool.t -> bool
          val is_eq :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> bool
          val is_leq :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> bool
          val is_and_false :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> bool
          val exist :
            ('a, 'b) Bdd.Env.t ->
            'a list -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val forall :
            ('a, 'b) Bdd.Env.t ->
            'a list -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val cofactor :
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val restrict :
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val tdrestrict :
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val permute :
            ?memo:Cudd.Memo.t ->
            'Bdd.Expr0.Bool.t -> int array -> 'Bdd.Expr0.Bool.t
          val varmap : 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bool.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t -> ('a * 'a) list -> 'Bdd.Expr0.Bool.t
          val substitute :
            ?memo:Cudd.Memo.t ->
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t ->
            ('a * 'Bdd.Expr0.expr) list -> 'Bdd.Expr0.Bool.t
          val print :
            ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
            ('a, 'b) Bdd.Env.t ->
            Format.formatter -> 'Bdd.Expr0.Bool.t -> unit
        end
      module Bint :
        sig
          type 'a t = 'Bdd.Int.t
          type dt = Cudd.Man.d Bdd.Expr0.Bint.t
          type vt = Cudd.Man.v Bdd.Expr0.Bint.t
          val of_expr : 'Bdd.Expr0.expr -> 'Bdd.Expr0.Bint.t
          val to_expr : 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.expr
          val of_int :
            ('a, 'b) Bdd.Env.t ->
            [ `Bint of bool * int ] -> int -> 'Bdd.Expr0.Bint.t
          val var : ('a, 'b) Bdd.Env.t -> '-> 'Bdd.Expr0.Bint.t
          val ite :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t ->
            'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t
          val neg :
            ('a, 'b) Bdd.Env.t -> 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t
          val succ :
            ('a, 'b) Bdd.Env.t -> 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t
          val pred :
            ('a, 'b) Bdd.Env.t -> 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t
          val add :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t
          val sub :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t
          val mul :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t
          val shift_left :
            ('a, 'b) Bdd.Env.t ->
            int -> 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t
          val shift_right :
            ('a, 'b) Bdd.Env.t ->
            int -> 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t
          val scale :
            ('a, 'b) Bdd.Env.t ->
            int -> 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t
          val zero :
            ('a, 'b) Bdd.Env.t -> 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bool.t
          val eq :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bool.t
          val eq_int :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bint.t -> int -> 'Bdd.Expr0.Bool.t
          val supeq :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bool.t
          val supeq_int :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bint.t -> int -> 'Bdd.Expr0.Bool.t
          val sup :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bool.t
          val sup_int :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bint.t -> int -> 'Bdd.Expr0.Bool.t
          val cofactor :
            'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bint.t
          val restrict :
            'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bint.t
          val tdrestrict :
            'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Bint.t
          val permute :
            ?memo:Cudd.Memo.t ->
            'Bdd.Expr0.Bint.t -> int array -> 'Bdd.Expr0.Bint.t
          val varmap : 'Bdd.Expr0.Bint.t -> 'Bdd.Expr0.Bint.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bint.t -> ('a * 'a) list -> 'Bdd.Expr0.Bint.t
          val substitute :
            ?memo:Cudd.Memo.t ->
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bint.t ->
            ('a * 'Bdd.Expr0.expr) list -> 'Bdd.Expr0.Bint.t
          val guard_of_int :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bint.t -> int -> 'Bdd.Expr0.Bool.t
          val guardints :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bint.t -> ('Bdd.Expr0.Bool.t * int) list
          val print :
            ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
            ('a, 'b) Bdd.Env.t ->
            Format.formatter -> 'Bdd.Expr0.Bint.t -> unit
        end
      module Benum :
        sig
          type 'a t = 'Bdd.Enum.t
          type dt = Cudd.Man.d Bdd.Expr0.Benum.t
          type vt = Cudd.Man.v Bdd.Expr0.Benum.t
          val of_expr : 'Bdd.Expr0.expr -> 'Bdd.Expr0.Benum.t
          val to_expr : 'Bdd.Expr0.Benum.t -> 'Bdd.Expr0.expr
          val var : ('a, 'b) Bdd.Env.t -> '-> 'Bdd.Expr0.Benum.t
          val ite :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t ->
            'Bdd.Expr0.Benum.t ->
            'Bdd.Expr0.Benum.t -> 'Bdd.Expr0.Benum.t
          val eq :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Benum.t ->
            'Bdd.Expr0.Benum.t -> 'Bdd.Expr0.Bool.t
          val eq_label :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Benum.t -> '-> 'Bdd.Expr0.Bool.t
          val cofactor :
            'Bdd.Expr0.Benum.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Benum.t
          val restrict :
            'Bdd.Expr0.Benum.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Benum.t
          val tdrestrict :
            'Bdd.Expr0.Benum.t ->
            'Bdd.Expr0.Bool.t -> 'Bdd.Expr0.Benum.t
          val permute :
            ?memo:Cudd.Memo.t ->
            'Bdd.Expr0.Benum.t -> int array -> 'Bdd.Expr0.Benum.t
          val varmap : 'Bdd.Expr0.Benum.t -> 'Bdd.Expr0.Benum.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Benum.t -> ('a * 'a) list -> 'Bdd.Expr0.Benum.t
          val substitute :
            ?memo:Cudd.Memo.t ->
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Benum.t ->
            ('a * 'Bdd.Expr0.expr) list -> 'Bdd.Expr0.Benum.t
          val guard_of_label :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Benum.t -> '-> 'Bdd.Expr0.Bool.t
          val guardlabels :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Benum.t -> ('Bdd.Expr0.Bool.t * 'a) list
          val print :
            ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
            ('a, 'b) Bdd.Env.t ->
            Format.formatter -> 'Bdd.Expr0.Benum.t -> unit
        end
      val typ_of_expr :
        ('a, 'b) Bdd.Env.t -> 'Bdd.Expr0.t -> 'Bdd.Env.typ
      val var : ('a, 'b) Bdd.Env.t -> '-> 'Bdd.Expr0.t
      val ite :
        'Bdd.Expr0.Bool.t ->
        'Bdd.Expr0.t -> 'Bdd.Expr0.t -> 'Bdd.Expr0.t
      val eq :
        ('a, 'b) Bdd.Env.t ->
        'Bdd.Expr0.t -> 'Bdd.Expr0.t -> 'Bdd.Expr0.Bool.t
      val substitute_by_var :
        ?memo:Cudd.Memo.t ->
        ('a, 'b) Bdd.Env.t ->
        'Bdd.Expr0.t -> ('a * 'a) list -> 'Bdd.Expr0.t
      val substitute_by_var_list :
        ?memo:Cudd.Memo.t ->
        ('a, 'b) Bdd.Env.t ->
        'Bdd.Expr0.t list -> ('a * 'a) list -> 'Bdd.Expr0.t list
      val substitute :
        ?memo:Cudd.Memo.t ->
        ('a, 'b) Bdd.Env.t ->
        'Bdd.Expr0.t -> ('a * 'Bdd.Expr0.t) list -> 'Bdd.Expr0.t
      val substitute_list :
        ?memo:Cudd.Memo.t ->
        ('a, 'b) Bdd.Env.t ->
        'Bdd.Expr0.t list ->
        ('a * 'Bdd.Expr0.t) list -> 'Bdd.Expr0.t list
      val cofactor : 'Bdd.Expr0.t -> 'Cudd.Bdd.t -> 'Bdd.Expr0.t
      val restrict : 'Bdd.Expr0.t -> 'Cudd.Bdd.t -> 'Bdd.Expr0.t
      val tdrestrict : 'Bdd.Expr0.t -> 'Cudd.Bdd.t -> 'Bdd.Expr0.t
      val support : ('a, 'b) Bdd.Env.t -> 'Bdd.Expr0.t -> 'PSette.t
      val support_cond : 'Cudd.Man.t -> 'Bdd.Expr0.t -> 'Cudd.Bdd.t
      val cube_of_bdd : ('a, 'b) Bdd.Env.t -> 'Cudd.Bdd.t -> 'Cudd.Bdd.t
      val print :
        ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
        ('a, 'b) Bdd.Env.t -> Format.formatter -> 'Bdd.Expr0.t -> unit
      val print_minterm :
        ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
        ('a, 'b) Bdd.Env.t ->
        Format.formatter -> Cudd.Man.tbool array -> unit
      val print_bdd :
        ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
        ('a, 'b) Bdd.Env.t -> Format.formatter -> 'Cudd.Bdd.t -> unit
      val print_idcondb :
        ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
        ('a, 'b) Bdd.Env.t -> Format.formatter -> int * bool -> unit
      val print_idcond :
        ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
        ('a, 'b) Bdd.Env.t -> Format.formatter -> int -> unit
      module O :
        sig
          val tid_of_var :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> '-> int array
          val reg_of_expr : 'Bdd.Expr0.expr -> 'Cudd.Bdd.t array
          module Bool :
            sig
              type 'd t = 'Cudd.Bdd.t
              type dt = Cudd.Man.d Bdd.Expr0.O.Bool.t
              type vt = Cudd.Man.v Bdd.Expr0.O.Bool.t
              val of_expr :
                [> `Bool of 'Bdd.Expr0.O.Bool.t ] -> 'Bdd.Expr0.O.Bool.t
              val to_expr :
                'Bdd.Expr0.O.Bool.t -> [> `Bool of 'Bdd.Expr0.O.Bool.t ]
              val dtrue :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> 'Bdd.Expr0.O.Bool.t
              val dfalse :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> 'Bdd.Expr0.O.Bool.t
              val of_bool :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> bool -> 'Bdd.Expr0.O.Bool.t
              val var :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> '-> 'Bdd.Expr0.O.Bool.t
              val dnot :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> 'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val dand :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val dor :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val xor :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val nand :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val nor :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val nxor :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val leq :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val eq :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val ite :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val is_true :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> 'Bdd.Expr0.O.Bool.t -> bool
              val is_false :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> 'Bdd.Expr0.O.Bool.t -> bool
              val is_cst :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> 'Bdd.Expr0.O.Bool.t -> bool
              val is_eq :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t -> bool
              val is_leq :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t -> bool
              val is_and_false :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t -> bool
              val exist :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'a list -> 'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val forall :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'a list -> 'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val cofactor :
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val restrict :
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val tdrestrict :
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val permute :
                ?memo:Cudd.Memo.t ->
                'Bdd.Expr0.O.Bool.t -> int array -> 'Bdd.Expr0.O.Bool.t
              val varmap : 'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bool.t
              val substitute_by_var :
                ?memo:Cudd.Memo.t ->
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t ->
                ('a * 'a) list -> 'Bdd.Expr0.O.Bool.t
              val substitute :
                ?memo:Cudd.Memo.t ->
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t ->
                ('a * 'Bdd.Expr0.expr) list -> 'Bdd.Expr0.O.Bool.t
              val print :
                ?print_external_idcondb:(Format.formatter ->
                                         int * bool -> unit) ->
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                Format.formatter -> 'Bdd.Expr0.O.Bool.t -> unit
            end
          module Bint :
            sig
              type 'd t = 'Bdd.Int.t
              type dt = Cudd.Man.d Bdd.Expr0.O.Bint.t
              type vt = Cudd.Man.v Bdd.Expr0.O.Bint.t
              val of_expr :
                [> `Bint of 'Bdd.Expr0.O.Bint.t ] -> 'Bdd.Expr0.O.Bint.t
              val to_expr :
                'Bdd.Expr0.O.Bint.t -> [> `Bint of 'Bdd.Expr0.O.Bint.t ]
              val of_int :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                [> `Bint of bool * int ] -> int -> 'Bdd.Expr0.O.Bint.t
              val var :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> '-> 'Bdd.Expr0.O.Bint.t
              val ite :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Bint.t ->
                'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bint.t
              val neg :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> 'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bint.t
              val succ :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> 'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bint.t
              val pred :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> 'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bint.t
              val add :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bint.t ->
                'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bint.t
              val sub :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bint.t ->
                'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bint.t
              val mul :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bint.t ->
                'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bint.t
              val shift_left :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                int -> 'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bint.t
              val shift_right :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                int -> 'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bint.t
              val scale :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                int -> 'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bint.t
              val zero :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> 'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bool.t
              val eq :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bint.t ->
                'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bool.t
              val eq_int :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bint.t -> int -> 'Bdd.Expr0.O.Bool.t
              val supeq :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bint.t ->
                'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bool.t
              val supeq_int :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bint.t -> int -> 'Bdd.Expr0.O.Bool.t
              val sup :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bint.t ->
                'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bool.t
              val sup_int :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bint.t -> int -> 'Bdd.Expr0.O.Bool.t
              val cofactor :
                'Bdd.Expr0.O.Bint.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bint.t
              val restrict :
                'Bdd.Expr0.O.Bint.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bint.t
              val tdrestrict :
                'Bdd.Expr0.O.Bint.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Bint.t
              val permute :
                ?memo:Cudd.Memo.t ->
                'Bdd.Expr0.O.Bint.t -> int array -> 'Bdd.Expr0.O.Bint.t
              val varmap : 'Bdd.Expr0.O.Bint.t -> 'Bdd.Expr0.O.Bint.t
              val substitute_by_var :
                ?memo:Cudd.Memo.t ->
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bint.t ->
                ('a * 'a) list -> 'Bdd.Expr0.O.Bint.t
              val substitute :
                ?memo:Cudd.Memo.t ->
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bint.t ->
                ('a * 'Bdd.Expr0.expr) list -> 'Bdd.Expr0.O.Bint.t
              val guard_of_int :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bint.t -> int -> 'Bdd.Expr0.O.Bool.t
              val guardints :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bint.t -> ('Bdd.Expr0.O.Bool.t * int) list
              val print :
                ?print_external_idcondb:(Format.formatter ->
                                         int * bool -> unit) ->
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                Format.formatter -> 'Bdd.Expr0.O.Bint.t -> unit
            end
          module Benum :
            sig
              type 'd t = 'Bdd.Enum.t
              type dt = Cudd.Man.d Bdd.Expr0.O.Benum.t
              type vt = Cudd.Man.v Bdd.Expr0.O.Benum.t
              val of_expr :
                [> `Benum of 'Bdd.Expr0.O.Benum.t ] ->
                'Bdd.Expr0.O.Benum.t
              val to_expr :
                'Bdd.Expr0.O.Benum.t ->
                [> `Benum of 'Bdd.Expr0.O.Benum.t ]
              val var :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> '-> 'Bdd.Expr0.O.Benum.t
              val ite :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Bool.t ->
                'Bdd.Expr0.O.Benum.t ->
                'Bdd.Expr0.O.Benum.t -> 'Bdd.Expr0.O.Benum.t
              val eq :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Benum.t ->
                'Bdd.Expr0.O.Benum.t -> 'Bdd.Expr0.O.Bool.t
              val eq_label :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Benum.t -> '-> 'Bdd.Expr0.O.Bool.t
              val cofactor :
                'Bdd.Expr0.O.Benum.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Benum.t
              val restrict :
                'Bdd.Expr0.O.Benum.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Benum.t
              val tdrestrict :
                'Bdd.Expr0.O.Benum.t ->
                'Bdd.Expr0.O.Bool.t -> 'Bdd.Expr0.O.Benum.t
              val permute :
                ?memo:Cudd.Memo.t ->
                'Bdd.Expr0.O.Benum.t -> int array -> 'Bdd.Expr0.O.Benum.t
              val varmap : 'Bdd.Expr0.O.Benum.t -> 'Bdd.Expr0.O.Benum.t
              val substitute_by_var :
                ?memo:Cudd.Memo.t ->
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Benum.t ->
                ('a * 'a) list -> 'Bdd.Expr0.O.Benum.t
              val substitute :
                ?memo:Cudd.Memo.t ->
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Benum.t ->
                ('a * 'Bdd.Expr0.expr) list -> 'Bdd.Expr0.O.Benum.t
              val guard_of_label :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Benum.t -> '-> 'Bdd.Expr0.O.Bool.t
              val guardlabels :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.O.Benum.t -> ('Bdd.Expr0.O.Bool.t * 'a) list
              val print :
                ?print_external_idcondb:(Format.formatter ->
                                         int * bool -> unit) ->
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                Format.formatter -> 'Bdd.Expr0.O.Benum.t -> unit
            end
          val typ_of_expr :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> 'Bdd.Expr0.t -> [> 'Bdd.Env.typ ]
          val var :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> '-> 'Bdd.Expr0.t
          val ite :
            'Bdd.Expr0.O.Bool.t ->
            'Bdd.Expr0.t -> 'Bdd.Expr0.t -> 'Bdd.Expr0.t
          val eq :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t ->
            'Bdd.Expr0.t -> 'Bdd.Expr0.t -> 'Bdd.Expr0.O.Bool.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> 'Bdd.Expr0.t -> ('a * 'a) list -> 'Bdd.Expr0.t
          val substitute_by_var_list :
            ?memo:Cudd.Memo.t ->
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t ->
            'Bdd.Expr0.t list -> ('a * 'a) list -> 'Bdd.Expr0.t list
          val substitute :
            ?memo:Cudd.Memo.t ->
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t ->
            'Bdd.Expr0.t -> ('a * 'Bdd.Expr0.t) list -> 'Bdd.Expr0.t
          val substitute_list :
            ?memo:Cudd.Memo.t ->
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t ->
            'Bdd.Expr0.t list ->
            ('a * 'Bdd.Expr0.t) list -> 'Bdd.Expr0.t list
          val support :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> 'Bdd.Expr0.t -> 'PSette.t
          val support_cond : 'Cudd.Man.t -> 'Bdd.Expr0.t -> 'Cudd.Bdd.t
          val cube_of_bdd :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> 'Cudd.Bdd.t -> 'Cudd.Bdd.t
          val tbdd_of_texpr : 'Bdd.Expr0.t array -> 'Cudd.Bdd.t array
          val texpr_of_tbdd :
            'Bdd.Expr0.t array ->
            'Cudd.Bdd.t array -> 'Bdd.Expr0.t array
          val print :
            ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> Format.formatter -> [< 'Bdd.Expr0.t ] -> unit
          val print_minterm :
            ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> Format.formatter -> Cudd.Man.tbool array -> unit
          val print_bdd :
            ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> Format.formatter -> 'Cudd.Bdd.t -> unit
          val print_idcondb :
            ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> Format.formatter -> int * bool -> unit
          val print_idcond :
            ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> Format.formatter -> int -> unit
          val permutation_of_rename :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> ('a * 'a) list -> int array
          val composition_of_lvarexpr :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> ('a * 'Bdd.Expr0.t) list -> 'Cudd.Bdd.t array
          val composition_of_lvarlexpr :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t ->
            'a list -> 'Bdd.Expr0.t list -> 'Cudd.Bdd.t array
          val bddsupport :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> 'a list -> 'Cudd.Bdd.t
          val varmap : 'Bdd.Expr0.t -> 'Bdd.Expr0.t
          val permute :
            ?memo:Cudd.Memo.t ->
            'Bdd.Expr0.t -> int array -> 'Bdd.Expr0.t
          val compose :
            ?memo:Cudd.Memo.t ->
            'Bdd.Expr0.t -> 'Cudd.Bdd.t array -> 'Bdd.Expr0.t
          val permute_list :
            ?memo:Cudd.Memo.t ->
            'Bdd.Expr0.t list -> int array -> 'Bdd.Expr0.t list
          val compose_list :
            ?memo:Cudd.Memo.t ->
            'Bdd.Expr0.t list -> 'Cudd.Bdd.t array -> 'Bdd.Expr0.t list
          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 'Bdd.Expr0.O.Expr.atom
                | Texternal of (int * bool)
                | Tcst of bool
              val map_atom :
                ('-> 'b) ->
                'Bdd.Expr0.O.Expr.atom -> 'Bdd.Expr0.O.Expr.atom
              val map_term :
                ('-> 'b) ->
                'Bdd.Expr0.O.Expr.term -> 'Bdd.Expr0.O.Expr.term
              val term_of_vint :
                '->
                'Bdd.Int.t -> Bdd.Reg.Minterm.t -> 'Bdd.Expr0.O.Expr.term
              val term_of_venum :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                '->
                'Bdd.Enum.t ->
                Bdd.Reg.Minterm.t -> 'Bdd.Expr0.O.Expr.term
              val term_of_idcondb :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t -> int * bool -> 'Bdd.Expr0.O.Expr.term
              val bool_of_tbool : Cudd.Man.tbool -> bool
              val mand :
                'Bdd.Expr0.O.Expr.term list Pervasives.ref ->
                'Bdd.Expr0.O.Expr.term -> unit
              val conjunction_of_minterm :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                Cudd.Man.tbool array ->
                'Bdd.Expr0.O.Expr.term Bdd.Normalform.conjunction
              val dnf_of_bdd :
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                'Cudd.Bdd.t -> 'Bdd.Expr0.O.Expr.term Bdd.Normalform.dnf
              val print_term :
                ?print_external_idcondb:(Format.formatter ->
                                         int * bool -> unit) ->
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                Format.formatter -> 'Bdd.Expr0.O.Expr.term -> unit
              val print_conjunction :
                ?print_external_idcondb:(Format.formatter ->
                                         int * bool -> unit) ->
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                Format.formatter ->
                'Bdd.Expr0.O.Expr.term Bdd.Normalform.conjunction -> unit
              val print_dnf :
                ?print_external_idcondb:(Format.formatter ->
                                         int * bool -> unit) ->
                ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
                Bdd.Env.O.t ->
                Format.formatter ->
                'Bdd.Expr0.O.Expr.term Bdd.Normalform.dnf -> unit
            end
        end
    end
  module Expr1 :
    sig
      type ('a, 'b) t = (('a, 'b) Bdd.Env.t, 'Bdd.Expr0.t) Bdd.Env.value
      type ('a, 'b) expr = ('a, 'b) Bdd.Expr1.t
      type 'a dt = ('a, Cudd.Man.d) Bdd.Expr1.t
      type 'a vt = ('a, Cudd.Man.v) Bdd.Expr1.t
      module Bool :
        sig
          type ('a, 'b) t = (('a, 'b) Bdd.Env.t, 'Cudd.Bdd.t) Bdd.Env.value
          type 'a dt = ('a, Cudd.Man.d) Bdd.Expr1.Bool.t
          type 'a vt = ('a, Cudd.Man.v) Bdd.Expr1.Bool.t
          val of_expr0 :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val get_env : ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Env.t
          val to_expr0 : ('a, 'b) Bdd.Expr1.Bool.t -> 'Bdd.Expr0.Bool.t
          val of_expr : ('a, 'b) Bdd.Expr1.expr -> ('a, 'b) Bdd.Expr1.Bool.t
          val to_expr : ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.expr
          val extend_environment :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val dtrue : ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val dfalse : ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val of_bool :
            ('a, 'b) Bdd.Env.t -> bool -> ('a, 'b) Bdd.Expr1.Bool.t
          val var : ('a, 'b) Bdd.Env.t -> '-> ('a, 'b) Bdd.Expr1.Bool.t
          val dnot : ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val dand :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val dor :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val xor :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val nand :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val nor :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val nxor :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val eq :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val leq :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val ite :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val is_true : ('a, 'b) Bdd.Expr1.Bool.t -> bool
          val is_false : ('a, 'b) Bdd.Expr1.Bool.t -> bool
          val is_cst : ('a, 'b) Bdd.Expr1.Bool.t -> bool
          val is_eq :
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t -> bool
          val is_leq :
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t -> bool
          val is_inter_false :
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t -> bool
          val exist :
            'a list -> ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val forall :
            'a list -> ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val cofactor :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val restrict :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val tdrestrict :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a * 'a) list -> ('a, 'b) Bdd.Expr1.Bool.t
          val substitute :
            ?memo:Cudd.Memo.t ->
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a * ('a, 'b) Bdd.Expr1.expr) list -> ('a, 'b) Bdd.Expr1.Bool.t
          val print : Format.formatter -> ('a, 'b) Bdd.Expr1.Bool.t -> unit
        end
      module Bint :
        sig
          type ('a, 'b) t = (('a, 'b) Bdd.Env.t, 'Bdd.Int.t) Bdd.Env.value
          type 'a dt = ('a, Cudd.Man.d) Bdd.Expr1.Bint.t
          type 'a vt = ('a, Cudd.Man.v) Bdd.Expr1.Bint.t
          val of_expr0 :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val get_env : ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Env.t
          val to_expr0 : ('a, 'b) Bdd.Expr1.Bint.t -> 'Bdd.Expr0.Bint.t
          val of_expr : ('a, 'b) Bdd.Expr1.expr -> ('a, 'b) Bdd.Expr1.Bint.t
          val to_expr : ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.expr
          val extend_environment :
            ('a, 'b) Bdd.Expr1.Bint.t ->
            ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val of_int :
            ('a, 'b) Bdd.Env.t ->
            [ `Bint of bool * int ] -> int -> ('a, 'b) Bdd.Expr1.Bint.t
          val var : ('a, 'b) Bdd.Env.t -> '-> ('a, 'b) Bdd.Expr1.Bint.t
          val neg : ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val succ : ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val pred : ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val add :
            ('a, 'b) Bdd.Expr1.Bint.t ->
            ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val sub :
            ('a, 'b) Bdd.Expr1.Bint.t ->
            ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val mul :
            ('a, 'b) Bdd.Expr1.Bint.t ->
            ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val shift_left :
            int -> ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val shift_right :
            int -> ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val scale :
            int -> ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val ite :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Bint.t ->
            ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val zero : ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val eq :
            ('a, 'b) Bdd.Expr1.Bint.t ->
            ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val supeq :
            ('a, 'b) Bdd.Expr1.Bint.t ->
            ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val sup :
            ('a, 'b) Bdd.Expr1.Bint.t ->
            ('a, 'b) Bdd.Expr1.Bint.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val eq_int :
            ('a, 'b) Bdd.Expr1.Bint.t -> int -> ('a, 'b) Bdd.Expr1.Bool.t
          val supeq_int :
            ('a, 'b) Bdd.Expr1.Bint.t -> int -> ('a, 'b) Bdd.Expr1.Bool.t
          val sup_int :
            ('a, 'b) Bdd.Expr1.Bint.t -> int -> ('a, 'b) Bdd.Expr1.Bool.t
          val cofactor :
            ('a, 'b) Bdd.Expr1.Bint.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val restrict :
            ('a, 'b) Bdd.Expr1.Bint.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val tdrestrict :
            ('a, 'b) Bdd.Expr1.Bint.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Bint.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            ('a, 'b) Bdd.Expr1.Bint.t ->
            ('a * 'a) list -> ('a, 'b) Bdd.Expr1.Bint.t
          val substitute :
            ?memo:Cudd.Memo.t ->
            ('a, 'b) Bdd.Expr1.Bint.t ->
            ('a * ('a, 'b) Bdd.Expr1.expr) list -> ('a, 'b) Bdd.Expr1.Bint.t
          val guard_of_int :
            ('a, 'b) Bdd.Expr1.Bint.t -> int -> ('a, 'b) Bdd.Expr1.Bool.t
          val guardints :
            ('a, 'b) Bdd.Expr1.Bint.t ->
            (('a, 'b) Bdd.Expr1.Bool.t * int) list
          val print : Format.formatter -> ('a, 'b) Bdd.Expr1.Bint.t -> unit
        end
      module Benum :
        sig
          type ('a, 'b) t = (('a, 'b) Bdd.Env.t, 'Bdd.Enum.t) Bdd.Env.value
          type 'a dt = ('a, Cudd.Man.d) Bdd.Expr1.Benum.t
          type 'a vt = ('a, Cudd.Man.v) Bdd.Expr1.Benum.t
          val of_expr0 :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.Benum.t -> ('a, 'b) Bdd.Expr1.Benum.t
          val get_env : ('a, 'b) Bdd.Expr1.Benum.t -> ('a, 'b) Bdd.Env.t
          val to_expr0 : ('a, 'b) Bdd.Expr1.Benum.t -> 'Bdd.Expr0.Benum.t
          val of_expr : ('a, 'b) Bdd.Expr1.expr -> ('a, 'b) Bdd.Expr1.Benum.t
          val to_expr : ('a, 'b) Bdd.Expr1.Benum.t -> ('a, 'b) Bdd.Expr1.expr
          val extend_environment :
            ('a, 'b) Bdd.Expr1.Benum.t ->
            ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Expr1.Benum.t
          val var : ('a, 'b) Bdd.Env.t -> '-> ('a, 'b) Bdd.Expr1.Benum.t
          val ite :
            ('a, 'b) Bdd.Expr1.Bool.t ->
            ('a, 'b) Bdd.Expr1.Benum.t ->
            ('a, 'b) Bdd.Expr1.Benum.t -> ('a, 'b) Bdd.Expr1.Benum.t
          val eq :
            ('a, 'b) Bdd.Expr1.Benum.t ->
            ('a, 'b) Bdd.Expr1.Benum.t -> ('a, 'b) Bdd.Expr1.Bool.t
          val eq_label :
            ('a, 'b) Bdd.Expr1.Benum.t -> '-> ('a, 'b) Bdd.Expr1.Bool.t
          val cofactor :
            ('a, 'b) Bdd.Expr1.Benum.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Benum.t
          val restrict :
            ('a, 'b) Bdd.Expr1.Benum.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Benum.t
          val tdrestrict :
            ('a, 'b) Bdd.Expr1.Benum.t ->
            ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.Benum.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            ('a, 'b) Bdd.Expr1.Benum.t ->
            ('a * 'a) list -> ('a, 'b) Bdd.Expr1.Benum.t
          val substitute :
            ?memo:Cudd.Memo.t ->
            ('a, 'b) Bdd.Expr1.Benum.t ->
            ('a * ('a, 'b) Bdd.Expr1.expr) list -> ('a, 'b) Bdd.Expr1.Benum.t
          val guard_of_label :
            ('a, 'b) Bdd.Expr1.Benum.t -> '-> ('a, 'b) Bdd.Expr1.Bool.t
          val guardlabels :
            ('a, 'b) Bdd.Expr1.Benum.t ->
            (('a, 'b) Bdd.Expr1.Bool.t * 'a) list
          val print : Format.formatter -> ('a, 'b) Bdd.Expr1.Benum.t -> unit
        end
      val typ_of_expr : ('a, 'b) Bdd.Expr1.t -> 'Bdd.Env.typ
      val make : ('a, 'b) Bdd.Env.t -> 'Bdd.Expr0.t -> ('a, 'b) Bdd.Expr1.t
      val of_expr0 :
        ('a, 'b) Bdd.Env.t -> 'Bdd.Expr0.t -> ('a, 'b) Bdd.Expr1.t
      val get_env : ('a, 'b) Bdd.Expr1.t -> ('a, 'b) Bdd.Env.t
      val to_expr0 : ('a, 'b) Bdd.Expr1.t -> 'Bdd.Expr0.t
      val extend_environment :
        ('a, 'b) Bdd.Expr1.t -> ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Expr1.t
      val var : ('a, 'b) Bdd.Env.t -> '-> ('a, 'b) Bdd.Expr1.t
      val ite :
        ('a, 'b) Bdd.Expr1.Bool.t ->
        ('a, 'b) Bdd.Expr1.t -> ('a, 'b) Bdd.Expr1.t -> ('a, 'b) Bdd.Expr1.t
      val eq :
        ('a, 'b) Bdd.Expr1.t ->
        ('a, 'b) Bdd.Expr1.t -> ('a, 'b) Bdd.Expr1.Bool.t
      val substitute_by_var :
        ?memo:Cudd.Memo.t ->
        ('a, 'b) Bdd.Expr1.t -> ('a * 'a) list -> ('a, 'b) Bdd.Expr1.t
      val substitute_by_var_list :
        ?memo:Cudd.Memo.t ->
        ('a, 'b) Bdd.Expr1.t list ->
        ('a * 'a) list -> ('a, 'b) Bdd.Expr1.t list
      val substitute :
        ?memo:Cudd.Memo.t ->
        ('a, 'b) Bdd.Expr1.t ->
        ('a * ('a, 'b) Bdd.Expr1.t) list -> ('a, 'b) Bdd.Expr1.t
      val substitute_list :
        ?memo:Cudd.Memo.t ->
        ('a, 'b) Bdd.Expr1.t list ->
        ('a * ('a, 'b) Bdd.Expr1.t) list -> ('a, 'b) Bdd.Expr1.t list
      val support : ('a, 'b) Bdd.Expr1.t -> 'PSette.t
      val support_cond : ('a, 'b) Bdd.Expr1.t -> 'Cudd.Bdd.t
      val cofactor :
        ('a, 'b) Bdd.Expr1.t ->
        ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.t
      val restrict :
        ('a, 'b) Bdd.Expr1.t ->
        ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.t
      val tdrestrict :
        ('a, 'b) Bdd.Expr1.t ->
        ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Expr1.t
      val print : Format.formatter -> ('a, 'b) Bdd.Expr1.t -> unit
      module List :
        sig
          type ('a, 'b) t =
              (('a, 'b) Bdd.Env.t, 'Bdd.Expr0.t list) Bdd.Env.value
          type 'a dt = ('a, Cudd.Man.d) Bdd.Expr1.List.t
          type 'a vt = ('a, Cudd.Man.v) Bdd.Expr1.List.t
          val of_lexpr0 :
            ('a, 'b) Bdd.Env.t ->
            'Bdd.Expr0.t list -> ('a, 'b) Bdd.Expr1.List.t
          val get_env : ('a, 'b) Bdd.Expr1.List.t -> ('a, 'b) Bdd.Env.t
          val to_lexpr0 : ('a, 'b) Bdd.Expr1.List.t -> 'Bdd.Expr0.t list
          val of_lexpr :
            ('a, 'b) Bdd.Env.t ->
            ('a, 'b) Bdd.Expr1.expr list -> ('a, 'b) Bdd.Expr1.List.t
          val to_lexpr :
            ('a, 'b) Bdd.Expr1.List.t -> ('a, 'b) Bdd.Expr1.expr list
          val extend_environment :
            ('a, 'b) Bdd.Expr1.List.t ->
            ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Expr1.List.t
          val print :
            ?first:(unit, Format.formatter, unit) Pervasives.format ->
            ?sep:(unit, Format.formatter, unit) Pervasives.format ->
            ?last:(unit, Format.formatter, unit) Pervasives.format ->
            Format.formatter -> ('a, 'b) Bdd.Expr1.List.t -> unit
        end
      module O :
        sig
          type ('a, 'b, 'c) t = ('b, 'Bdd.Expr0.t) Bdd.Env.value
            constraint 'b =
              ('a, [> 'Bdd.Env.typ ] as 'd, [> 'Bdd.Env.typdef ] as 'e,
               'c, 'f)
              Bdd.Env.O.t
          type ('a, 'b, 'c) expr = ('a, 'b, 'c) Bdd.Expr1.O.t
            constraint 'b =
              ('a, [> 'Bdd.Env.typ ] as 'd, [> 'Bdd.Env.typdef ] as 'e,
               'c, 'f)
              Bdd.Env.O.t
          type ('a, 'b) dt = ('a, 'b, Cudd.Man.d) Bdd.Expr1.O.t
            constraint 'b =
              ('a, [> 'Bdd.Env.typ ] as 'c, [> 'Bdd.Env.typdef ] as 'd,
               Cudd.Man.d, 'e)
              Bdd.Env.O.t
          type ('a, 'b) vt = ('a, 'b, Cudd.Man.v) Bdd.Expr1.O.t
            constraint 'b =
              ('a, [> 'Bdd.Env.typ ] as 'c, [> 'Bdd.Env.typdef ] as 'd,
               Cudd.Man.v, 'e)
              Bdd.Env.O.t
          module Bool :
            sig
              type ('a, 'b, 'c) t = ('b, 'Cudd.Bdd.t) Bdd.Env.value
                constraint 'b =
                  ('a, [> 'Bdd.Env.typ ] as 'd,
                   [> 'Bdd.Env.typdef ] as 'e, 'c, 'f)
                  Bdd.Env.O.t
              type ('a, 'b) dt = ('a, 'b, Cudd.Man.d) Bdd.Expr1.O.Bool.t
                constraint 'b =
                  ('a, [> 'Bdd.Env.typ ] as 'c,
                   [> 'Bdd.Env.typdef ] as 'd, Cudd.Man.d, 'e)
                  Bdd.Env.O.t
              type ('a, 'b) vt = ('a, 'b, Cudd.Man.v) Bdd.Expr1.O.Bool.t
                constraint 'b =
                  ('a, [> 'Bdd.Env.typ ] as 'c,
                   [> 'Bdd.Env.typdef ] as 'd, Cudd.Man.v, 'e)
                  Bdd.Env.O.t
              val of_expr0 :
                ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
                 'c, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val get_env :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t -> ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t
              val to_expr0 :
                ('a,
                 ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t -> 'Bdd.Expr0.Bool.t
              val of_expr :
                (('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, [> `Bool of 'Cudd.Bdd.t ])
                Bdd.Env.value ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val to_expr :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                (('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t,
                 [> `Bool of 'Cudd.Bdd.t ])
                Bdd.Env.value
              val extend_environment :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val dtrue :
                ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
                 'c, 'e)
                Bdd.Env.O.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val dfalse :
                ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
                 'c, 'e)
                Bdd.Env.O.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val of_bool :
                ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
                 'c, 'e)
                Bdd.Env.O.t ->
                bool ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val var :
                ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
                 'c, 'e)
                Bdd.Env.O.t ->
                '->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val dnot :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val dand :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val dor :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val xor :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val nand :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val nor :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val nxor :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val eq :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val leq :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val ite :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val is_true :
                ('a,
                 ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t -> bool
              val is_false :
                ('a,
                 ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t -> bool
              val is_cst :
                ('a,
                 ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t -> bool
              val is_eq :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                bool
              val is_leq :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                bool
              val is_inter_false :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                bool
              val exist :
                'a list ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val forall :
                'a list ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val cofactor :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val restrict :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val tdrestrict :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val substitute_by_var :
                ?memo:Cudd.Memo.t ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a * 'a) list ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val substitute :
                ?memo:Cudd.Memo.t ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a *
                 ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.expr)
                list ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val print :
                Format.formatter ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t -> unit
            end
          module Bint :
            sig
              type ('a, 'b, 'c) t = ('b, 'Bdd.Int.t) Bdd.Env.value
                constraint 'b =
                  ('a, [> 'Bdd.Env.typ ] as 'd,
                   [> 'Bdd.Env.typdef ] as 'e, 'c, 'f)
                  Bdd.Env.O.t
              type ('a, 'b, 'c) dt = ('a, 'b, Cudd.Man.d) Bdd.Expr1.O.Bint.t
                constraint 'b =
                  ('a, [> 'Bdd.Env.typ ] as 'd,
                   [> 'Bdd.Env.typdef ] as 'e, Cudd.Man.d, 'f)
                  Bdd.Env.O.t
              type ('a, 'b, 'c) vt = ('a, 'b, Cudd.Man.v) Bdd.Expr1.O.Bint.t
                constraint 'b =
                  ('a, [> 'Bdd.Env.typ ] as 'd,
                   [> 'Bdd.Env.typdef ] as 'e, Cudd.Man.v, 'f)
                  Bdd.Env.O.t
              val of_expr0 :
                ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
                 'c, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val get_env :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t -> ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t
              val to_expr0 :
                ('a,
                 ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t -> 'Bdd.Expr0.Bint.t
              val of_expr :
                (('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, [> `Bint of 'Bdd.Int.t ])
                Bdd.Env.value ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val to_expr :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                (('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t,
                 [> `Bint of 'Bdd.Int.t ])
                Bdd.Env.value
              val extend_environment :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val of_int :
                ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
                 'c, 'e)
                Bdd.Env.O.t ->
                [ `Bint of bool * int ] ->
                int ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val var :
                ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
                 'c, 'e)
                Bdd.Env.O.t ->
                '->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val neg :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val succ :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val pred :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val add :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val sub :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val mul :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val shift_left :
                int ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val shift_right :
                int ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val scale :
                int ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val ite :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val zero :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val eq :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val supeq :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val sup :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val eq_int :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                int ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val supeq_int :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                int ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val sup_int :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                int ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val cofactor :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val restrict :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val tdrestrict :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val substitute_by_var :
                ?memo:Cudd.Memo.t ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a * 'a) list ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val substitute :
                ?memo:Cudd.Memo.t ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                ('a *
                 ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.expr)
                list ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bint.t
              val guard_of_int :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                int ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val guardints :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t ->
                (('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                 Bdd.Expr1.O.Bool.t * int)
                list
              val print :
                Format.formatter ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bint.t -> unit
            end
          module Benum :
            sig
              type ('a, 'b, 'c) t = ('b, 'Bdd.Enum.t) Bdd.Env.value
                constraint 'b =
                  ('a, [> 'Bdd.Env.typ ] as 'd,
                   [> 'Bdd.Env.typdef ] as 'e, 'c, 'f)
                  Bdd.Env.O.t
              type ('a, 'b) dt = ('a, 'b, Cudd.Man.d) Bdd.Expr1.O.Benum.t
                constraint 'b =
                  ('a, [> 'Bdd.Env.typ ] as 'c,
                   [> 'Bdd.Env.typdef ] as 'd, Cudd.Man.d, 'e)
                  Bdd.Env.O.t
              type ('a, 'b) vt = ('a, 'b, Cudd.Man.v) Bdd.Expr1.O.Benum.t
                constraint 'b =
                  ('a, [> 'Bdd.Env.typ ] as 'c,
                   [> 'Bdd.Env.typdef ] as 'd, Cudd.Man.v, 'e)
                  Bdd.Env.O.t
              val of_expr0 :
                ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
                 'c, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.Benum.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t
              val get_env :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t -> ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t
              val to_expr0 :
                ('a,
                 ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t -> 'Bdd.Expr0.Benum.t
              val of_expr :
                (('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, [> `Benum of 'Bdd.Enum.t ])
                Bdd.Env.value ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t
              val to_expr :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t ->
                (('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t,
                 [> `Benum of 'Bdd.Enum.t ])
                Bdd.Env.value
              val extend_environment :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t ->
                ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t
              val var :
                ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
                 'c, 'e)
                Bdd.Env.O.t ->
                '->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t
              val ite :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t
              val eq :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val eq_label :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t ->
                '->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val cofactor :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t
              val restrict :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t
              val tdrestrict :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t
              val substitute_by_var :
                ?memo:Cudd.Memo.t ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t ->
                ('a * 'a) list ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t
              val substitute :
                ?memo:Cudd.Memo.t ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t ->
                ('a *
                 ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.expr)
                list ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t
              val guard_of_label :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t ->
                '->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
              val guardlabels :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t ->
                (('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c)
                 Bdd.Expr1.O.Bool.t * 'a)
                list
              val print :
                Format.formatter ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.Benum.t -> unit
            end
          val typ_of_expr :
            ('a,
             ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t -> 'Bdd.Env.typ
          val make :
            ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd, 'c,
             'e)
            Bdd.Env.O.t ->
            'Bdd.Expr0.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.expr
          val of_expr0 :
            ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd, 'c,
             'e)
            Bdd.Env.O.t ->
            'Bdd.Expr0.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.expr
          val get_env :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t -> ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t
          val to_expr0 :
            ('a,
             ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t -> 'Bdd.Expr0.t
          val extend_environment :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t ->
            ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t
          val var :
            ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd, 'c,
             'e)
            Bdd.Env.O.t ->
            '-> ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t
          val ite :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.Bool.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t
          val eq :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
          val substitute_by_var :
            ?memo:Cudd.Memo.t ->
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t ->
            ('a * 'a) list ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t
          val substitute_by_var_list :
            ?memo:Cudd.Memo.t ->
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t list ->
            ('a * 'a) list ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t list
          val substitute :
            ?memo:Cudd.Memo.t ->
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t ->
            ('a * ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t)
            list -> ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t
          val substitute_list :
            ?memo:Cudd.Memo.t ->
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t list ->
            ('a * ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t)
            list ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t list
          val support :
            ('a,
             ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t -> 'PSette.t
          val support_cond :
            ('a,
             ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t -> 'Cudd.Bdd.t
          val cofactor :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t
          val restrict :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t
          val tdrestrict :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t
          val print :
            Format.formatter ->
            ('a,
             ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.t -> unit
          module List :
            sig
              type ('a, 'b, 'c) t = ('b, 'Bdd.Expr0.t list) Bdd.Env.value
                constraint 'b =
                  ('a, [> 'Bdd.Env.typ ] as 'd,
                   [> 'Bdd.Env.typdef ] as 'e, 'c, 'f)
                  Bdd.Env.O.t
              type ('a, 'b) dt = ('a, 'b, Cudd.Man.d) Bdd.Expr1.O.List.t
                constraint 'b =
                  ('a, [> 'Bdd.Env.typ ] as 'c,
                   [> 'Bdd.Env.typdef ] as 'd, Cudd.Man.d, 'e)
                  Bdd.Env.O.t
              type ('a, 'b) vt = ('a, 'b, Cudd.Man.v) Bdd.Expr1.O.List.t
                constraint 'b =
                  ('a, [> 'Bdd.Env.typ ] as 'c,
                   [> 'Bdd.Env.typdef ] as 'd, Cudd.Man.v, 'e)
                  Bdd.Env.O.t
              val of_lexpr0 :
                ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
                 'c, 'e)
                Bdd.Env.O.t ->
                'Bdd.Expr0.t list ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.List.t
              val get_env :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.List.t -> ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t
              val to_lexpr0 :
                ('a,
                 ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.List.t -> 'Bdd.Expr0.t list
              val of_lexpr :
                ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
                 'c, 'e)
                Bdd.Env.O.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.expr
                list ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.List.t
              val to_lexpr :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.List.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.expr
                list
              val extend_environment :
                ('a,
                 ('a, [> 'Bdd.Env.typ ] as 'b,
                  [> 'Bdd.Env.typdef ] as 'd, 'c, 'e)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.List.t ->
                ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t ->
                ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.List.t
              val print :
                ?first:(unit, Format.formatter, unit) Pervasives.format ->
                ?sep:(unit, Format.formatter, unit) Pervasives.format ->
                ?last:(unit, Format.formatter, unit) Pervasives.format ->
                Format.formatter ->
                ('a,
                 ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
                 Bdd.Env.O.t, 'c)
                Bdd.Expr1.O.List.t -> unit
            end
        end
    end
  module Domain0 :
    sig
      type 'a t = 'Bdd.Expr0.Bool.t
      type dt = Cudd.Man.d Bdd.Domain0.t
      type vt = Cudd.Man.v Bdd.Domain0.t
      val size : 'Bdd.Domain0.t -> int
      val print :
        ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
        ('a, 'b) Bdd.Env.t -> Format.formatter -> 'Bdd.Domain0.t -> unit
      val bottom : ('a, 'b) Bdd.Env.t -> 'Bdd.Domain0.t
      val top : ('a, 'b) Bdd.Env.t -> 'Bdd.Domain0.t
      val is_bottom : ('a, 'b) Bdd.Env.t -> 'Bdd.Domain0.t -> bool
      val is_top : ('a, 'b) Bdd.Env.t -> 'Bdd.Domain0.t -> bool
      val is_leq :
        ('a, 'b) Bdd.Env.t -> 'Bdd.Domain0.t -> 'Bdd.Domain0.t -> bool
      val is_eq :
        ('a, 'b) Bdd.Env.t -> 'Bdd.Domain0.t -> 'Bdd.Domain0.t -> bool
      val is_variable_unconstrained :
        ('a, 'b) Bdd.Env.t -> 'Bdd.Domain0.t -> '-> bool
      val meet :
        ('a, 'b) Bdd.Env.t ->
        'Bdd.Domain0.t -> 'Bdd.Domain0.t -> 'Bdd.Domain0.t
      val join :
        ('a, 'b) Bdd.Env.t ->
        'Bdd.Domain0.t -> 'Bdd.Domain0.t -> 'Bdd.Domain0.t
      val meet_condition :
        ('a, 'b) Bdd.Env.t ->
        'Bdd.Domain0.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Domain0.t
      val assign_lexpr :
        ?relational:bool ->
        ?nodependency:bool ->
        ('a, 'b) Bdd.Env.t ->
        'Bdd.Domain0.t ->
        'a list -> 'Bdd.Expr0.expr list -> 'Bdd.Domain0.t
      val substitute_lexpr :
        ('a, 'b) Bdd.Env.t ->
        'Bdd.Domain0.t ->
        'a list -> 'Bdd.Expr0.expr list -> 'Bdd.Domain0.t
      val forget_list :
        ('a, 'b) Bdd.Env.t -> 'Bdd.Domain0.t -> 'a list -> 'Bdd.Domain0.t
      module O :
        sig
          val print :
            ?print_external_idcondb:(Format.formatter -> int * bool -> unit) ->
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> Format.formatter -> 'Bdd.Domain0.t -> unit
          val bottom :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> 'Bdd.Domain0.t
          val top :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> 'Bdd.Domain0.t
          val is_bottom :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> 'Bdd.Domain0.t -> bool
          val is_top :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> 'Bdd.Domain0.t -> bool
          val is_leq :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> 'Bdd.Domain0.t -> 'Bdd.Domain0.t -> bool
          val is_eq :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> 'Bdd.Domain0.t -> 'Bdd.Domain0.t -> bool
          val is_variable_unconstrained :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> 'Bdd.Domain0.t -> '-> bool
          val meet :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t ->
            'Bdd.Domain0.t -> 'Bdd.Domain0.t -> 'Bdd.Domain0.t
          val join :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t ->
            'Bdd.Domain0.t -> 'Bdd.Domain0.t -> 'Bdd.Domain0.t
          val meet_condition :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t ->
            'Bdd.Domain0.t -> 'Bdd.Expr0.Bool.t -> 'Bdd.Domain0.t
          val assign_lexpr :
            ?relational:bool ->
            ?nodependency:bool ->
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t ->
            'Bdd.Domain0.t ->
            'a list -> 'Bdd.Expr0.expr list -> 'Bdd.Domain0.t
          val substitute_lexpr :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t ->
            'Bdd.Domain0.t ->
            'a list -> 'Bdd.Expr0.expr list -> 'Bdd.Domain0.t
          val forget_list :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t -> 'Bdd.Domain0.t -> 'a list -> 'Bdd.Domain0.t
          module Asssub :
            sig
              val sort :
                int array ->
                'Cudd.Bdd.t array -> int array * 'Cudd.Bdd.t array
              val is_equal :
                'Cudd.Bdd.t array -> 'Cudd.Bdd.t array -> bool
              val post :
                'Cudd.Bdd.t ->
                int array -> 'Cudd.Bdd.t array -> 'Cudd.Bdd.t
              val postcondition :
                'Cudd.Bdd.t -> 'Cudd.Bdd.t array -> 'Cudd.Bdd.t
            end
          val relation_supp_compose_of_lvarlexpr :
            ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'd, 'e)
            Bdd.Env.O.t ->
            'a list ->
            'Bdd.Expr0.expr list ->
            'Cudd.Bdd.t * 'Cudd.Bdd.t * 'Cudd.Bdd.t array
          val apply_change :
            'Bdd.Domain0.t -> 'Bdd.Env.change -> 'Bdd.Domain0.t
        end
    end
  module Domain1 :
    sig
      type ('a, 'b) t = ('a, 'b) Bdd.Expr1.Bool.t
      type 'a dt = ('a, Cudd.Man.d) Bdd.Domain1.t
      type 'a vt = ('a, Cudd.Man.v) Bdd.Domain1.t
      val of_domain0 :
        ('a, 'b) Bdd.Env.t -> 'Bdd.Domain0.t -> ('a, 'b) Bdd.Domain1.t
      val get_env : ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Env.t
      val to_domain0 : ('a, 'b) Bdd.Domain1.t -> 'Bdd.Domain0.t
      val of_expr1 : ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Domain1.t
      val to_expr1 : ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Expr1.Bool.t
      val size : ('a, 'b) Bdd.Domain1.t -> int
      val print : Format.formatter -> ('a, 'b) Bdd.Domain1.t -> unit
      val bottom : ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Domain1.t
      val top : ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Domain1.t
      val is_bottom : ('a, 'b) Bdd.Domain1.t -> bool
      val is_top : ('a, 'b) Bdd.Domain1.t -> bool
      val is_leq : ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Domain1.t -> bool
      val is_eq : ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Domain1.t -> bool
      val is_variable_unconstrained : ('a, 'b) Bdd.Domain1.t -> '-> bool
      val meet :
        ('a, 'b) Bdd.Domain1.t ->
        ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Domain1.t
      val join :
        ('a, 'b) Bdd.Domain1.t ->
        ('a, 'b) Bdd.Domain1.t -> ('a, 'b) Bdd.Domain1.t
      val meet_condition :
        ('a, 'b) Bdd.Domain1.t ->
        ('a, 'b) Bdd.Expr1.Bool.t -> ('a, 'b) Bdd.Domain1.t
      val assign_lexpr :
        ?relational:bool ->
        ?nodependency:bool ->
        ('a, 'b) Bdd.Domain1.t ->
        'a list -> ('a, 'b) Bdd.Expr1.t list -> ('a, 'b) Bdd.Domain1.t
      val assign_listexpr :
        ?relational:bool ->
        ?nodependency:bool ->
        ('a, 'b) Bdd.Domain1.t ->
        'a list -> ('a, 'b) Bdd.Expr1.List.t -> ('a, 'b) Bdd.Domain1.t
      val substitute_lexpr :
        ('a, 'b) Bdd.Domain1.t ->
        'a list -> ('a, 'b) Bdd.Expr1.t list -> ('a, 'b) Bdd.Domain1.t
      val substitute_listexpr :
        ('a, 'b) Bdd.Domain1.t ->
        'a list -> ('a, 'b) Bdd.Expr1.List.t -> ('a, 'b) Bdd.Domain1.t
      val forget_list :
        ('a, 'b) Bdd.Domain1.t -> 'a list -> ('a, 'b) Bdd.Domain1.t
      val change_environment :
        ('a, 'b) Bdd.Domain1.t ->
        ('a, 'b) Bdd.Env.t -> ('a, 'b) Bdd.Domain1.t
      val rename :
        ('a, 'b) Bdd.Domain1.t -> ('a * 'a) list -> ('a, 'b) Bdd.Domain1.t
      module O :
        sig
          val check_value :
            ('-> int array -> 'a) ->
            (('b, [> 'Bdd.Env.typ ] as 'c, [> 'Bdd.Env.typdef ] as 'd,
              'e, 'f)
             Bdd.Env.O.t, 'a)
            Bdd.Env.value -> ('b, 'c, 'd, 'e, 'f) Bdd.Env.O.t -> 'a
          val check_lvalue :
            ('-> int array -> 'a) ->
            (('b, [> 'Bdd.Env.typ ] as 'c, [> 'Bdd.Env.typdef ] as 'd,
              'e, 'f)
             Bdd.Env.O.t, 'a)
            Bdd.Env.value list -> ('b, 'c, 'd, 'e, 'f) Bdd.Env.O.t -> 'a list
          type ('a, 'b, 'c) t = ('a, 'b, 'c) Bdd.Expr1.O.Bool.t
            constraint 'b =
              ('a, [> 'Bdd.Env.typ ] as 'd, [> 'Bdd.Env.typdef ] as 'e,
               'c, 'f)
              Bdd.Env.O.t
          type ('a, 'b) dt = ('a, 'b, Cudd.Man.d) Bdd.Domain1.O.t
            constraint 'b =
              ('a, [> 'Bdd.Env.typ ] as 'c, [> 'Bdd.Env.typdef ] as 'd,
               Cudd.Man.d, 'e)
              Bdd.Env.O.t
          type ('a, 'b) vt = ('a, 'b, Cudd.Man.v) Bdd.Domain1.O.t
            constraint 'b =
              ('a, [> 'Bdd.Env.typ ] as 'c, [> 'Bdd.Env.typdef ] as 'd,
               Cudd.Man.v, 'e)
              Bdd.Env.O.t
          val of_domain0 :
            ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd, 'c,
             'e)
            Bdd.Env.O.t ->
            'Bdd.Domain0.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
          val get_env :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t -> ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t
          val to_domain0 :
            ('a,
             ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t -> 'Bdd.Domain0.t
          val of_expr1 :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Expr1.O.Bool.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
          val to_expr1 :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t
          val size :
            ('a,
             ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t -> int
          val print :
            Format.formatter ->
            ('a,
             ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t -> unit
          val bottom :
            ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd, 'c,
             'e)
            Bdd.Env.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
          val top :
            ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd, 'c,
             'e)
            Bdd.Env.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
          val is_bottom :
            ('a,
             ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t -> bool
          val is_top :
            ('a,
             ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t -> bool
          val is_leq :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t ->
            bool
          val is_eq :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t ->
            bool
          val is_variable_unconstrained :
            ('a,
             ('a, [> 'Bdd.Env.typ ], [> 'Bdd.Env.typdef ], 'c, 'b)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t -> '-> bool
          val meet :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
          val join :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
          val meet_condition :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.Bool.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
          val assign_lexpr :
            ?relational:bool ->
            ?nodependency:bool ->
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t ->
            'a list ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t list ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
          val assign_listexpr :
            ?relational:bool ->
            ?nodependency:bool ->
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t ->
            'a list ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.List.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
          val substitute_lexpr :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t ->
            'a list ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.t list ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
          val substitute_listexpr :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t ->
            'a list ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Expr1.O.List.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
          val forget_list :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t ->
            'a list ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
          val change_environment :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t ->
            ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
          val rename :
            ('a,
             ('a, [> 'Bdd.Env.typ ] as 'b, [> 'Bdd.Env.typdef ] as 'd,
              'c, 'e)
             Bdd.Env.O.t, 'c)
            Bdd.Domain1.O.t ->
            ('a * 'a) list ->
            ('a, ('a, 'b, 'd, 'c, 'e) Bdd.Env.O.t, 'c) Bdd.Domain1.O.t
        end
    end
end