sig
  type expr = [ `Benum of Bddenum.t | `Bint of Bddint.t | `Bool of Bdd.t ]
  type typdef = [ `Benum of Var.t array | `Bint of bool * int ]
  type typ = [ `Benum of Var.t | `Bint of bool * int | `Bool ]
  type info = { tid : int array; var : Bddvar.expr; }
  class type ['a, 'b] db =
    object
      constraint 'a = [> Bddvar.typ ]
      constraint 'b = [> typdef ]
      val mutable v_bddincr : int
      val mutable v_bddindex : int
      val mutable v_idcondvar : Var.t MappeI.t
      val v_manager : Manager.t
      val mutable v_print_external_idcondb :
        Format.formatter -> int * bool -> unit
      val mutable v_typdef : 'b Var.Map.t
      val mutable v_varinfo : Bddvar.info Var.Map.t
      val mutable v_varset : Bdd.t Var.Map.t
      val mutable v_vartyp : 'a Var.Map.t
      method private add_label : Var.t -> 'a -> unit
      method add_typ : Var.t -> 'b -> unit
      method add_var : Var.t -> 'a -> unit
      method bddincr : int
      method bddindex : int
      method idcondvar : Var.t MappeI.t
      method manager : Manager.t
      method mem_typ : Var.t -> bool
      method mem_var : Var.t -> bool
      method print_external_idcondb : Format.formatter -> int * bool -> unit
      method print_order : Format.formatter -> unit
      method set_bddincr : int -> unit
      method set_bddindex : int -> unit
      method set_idcondvar : Var.t MappeI.t -> unit
      method set_print_external_idcondb :
        (Format.formatter -> int * bool -> unit) -> unit
      method set_typdef : 'b Var.Map.t -> unit
      method set_varinfo : Bddvar.info Var.Map.t -> unit
      method set_varset : Bdd.t Var.Map.t -> unit
      method set_vartyp : 'a Var.Map.t -> unit
      method typ_of_var : Var.t -> 'a
      method typdef : 'b Var.Map.t
      method typdef_of_typ : Var.t -> 'b
      method var_of_idcond : int -> Var.t
      method varinfo : Bddvar.info Var.Map.t
      method varset : Bdd.t Var.Map.t
      method vartyp : 'a Var.Map.t
    end
  class ['a, 'b] make_db :
    Manager.t ->
    object
      constraint 'a = [> Bddvar.typ ]
      constraint 'b = [> Bddvar.typdef ]
      val mutable v_bddincr : int
      val mutable v_bddindex : int
      val mutable v_idcondvar : Var.t MappeI.t
      val v_manager : Manager.t
      val mutable v_print_external_idcondb :
        Format.formatter -> int * bool -> unit
      val mutable v_typdef : 'b Var.Map.t
      val mutable v_varinfo : info Var.Map.t
      val mutable v_varset : Bdd.t Var.Map.t
      val mutable v_vartyp : 'a Var.Map.t
      method private add_label : Var.t -> 'a -> unit
      method add_typ : Var.t -> 'b -> unit
      method add_var : Var.t -> 'a -> unit
      method bddincr : int
      method bddindex : int
      method idcondvar : Var.t MappeI.t
      method manager : Manager.t
      method mem_typ : Var.t -> bool
      method mem_var : Var.t -> bool
      method print_external_idcondb : Format.formatter -> int * bool -> unit
      method print_order : Format.formatter -> unit
      method set_bddincr : int -> unit
      method set_bddindex : int -> unit
      method set_idcondvar : Var.t MappeI.t -> unit
      method set_print_external_idcondb :
        (Format.formatter -> int * bool -> unit) -> unit
      method set_typdef : 'b Var.Map.t -> unit
      method set_varinfo : info Var.Map.t -> unit
      method set_varset : Bdd.t Var.Map.t -> unit
      method set_vartyp : 'a Var.Map.t -> unit
      method typ_of_var : Var.t -> 'a
      method typdef : 'b Var.Map.t
      method typdef_of_typ : Var.t -> 'b
      method var_of_idcond : int -> Var.t
      method varinfo : info Var.Map.t
      method varset : Bdd.t Var.Map.t
      method vartyp : 'a Var.Map.t
    end
  val typ_of_expr : Bddvar.expr -> [> Bddvar.typ ]
  val var :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db -> Var.t -> Bddvar.expr
  val ite : Bdd.t -> Bddvar.expr -> Bddvar.expr -> Bddvar.expr
  val rename :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Bddvar.expr -> (Var.t * Var.t) list -> Bddvar.expr
  val substitute :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Bddvar.expr -> (Var.t * Bddvar.expr) list -> Bddvar.expr
  val exist :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Bddvar.expr -> Var.t list -> Bddvar.expr
  val forall :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Bddvar.expr -> Var.t list -> Bddvar.expr
  val cofactor : Bddvar.expr -> Bdd.t -> Bddvar.expr
  val tdrestrict : Bddvar.expr -> Bdd.t -> Bddvar.expr
  val support_cond :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db -> Bddvar.expr -> Bdd.t
  val vectorsupport_cond :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Bddvar.expr array -> Bdd.t
  val cube_of_bdd :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db -> Bdd.t -> Bdd.t
  val iter_ordered :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    (Var.t -> Bddvar.info -> unit) -> unit
  val print_db :
    Format.formatter ->
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db -> unit
  val print_typ : Format.formatter -> Bddvar.typ -> unit
  val print_typdef : Format.formatter -> Bddvar.typdef -> unit
  val print_expr :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Format.formatter -> Bddvar.expr -> unit
  val print_minterm :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Format.formatter -> Manager.tbool array -> unit
  val print_bdd :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Format.formatter -> Bdd.t -> unit
  val print_idd :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    (Format.formatter -> int -> unit) -> Format.formatter -> Idd.t -> unit
  val print_idcondb :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Format.formatter -> int * bool -> unit
  val print_idcond :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Format.formatter -> int -> unit
  val print_info : Format.formatter -> Bddvar.info -> unit
  val permutation_of_rename :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    (Var.t * Var.t) list -> int array
  val composition_of_substitution :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    (Var.t * Bddvar.expr) list -> Bdd.t array
  val bddsupport :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db -> Var.t list -> Bdd.t
  val permute : Bddvar.expr -> int array -> Bddvar.expr
  val compose : Bddvar.expr -> Bdd.t array -> Bddvar.expr
  val mem_id :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db -> int -> bool
  val varinfo_of_id :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    int -> Var.t * Bddvar.info
  val print_id :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
    Format.formatter -> int -> unit
  val info_of_var :
    ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db -> Var.t -> Bddvar.info
  val reg_of_expr : Bddvar.expr -> Bdd.t array
  module Expr :
    sig
      type atom =
          Tbool of Var.t * bool
        | Tint of Var.t * int list
        | Tenum of Var.t * Var.t list
      type term =
          Tatom of Bddvar.Expr.atom
        | Texternal of int * bool
        | Tcst of bool
      type conjunction = Conjunction of Bddvar.Expr.term list | Cfalse
      type disjunction = Disjunction of Bddvar.Expr.conjunction list | Dtrue
      val term_of_vint :
        Var.t -> Bddint.t -> Bddreg.Minterm.t -> Bddvar.Expr.term
      val term_of_venum :
        ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
        Var.t -> Bddenum.t -> Bddreg.Minterm.t -> Bddvar.Expr.term
      val term_of_idcondb :
        ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
        MappeI.key * bool -> Bddvar.Expr.term
      val bool_of_tbool : Manager.tbool -> bool
      val mand :
        Bddvar.Expr.term list Pervasives.ref -> Bddvar.Expr.term -> unit
      val conjunction_of_minterm :
        ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
        Manager.tbool array -> Bddvar.Expr.conjunction
      val disjunction_of_bdd :
        ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
        Bdd.t -> Bddvar.Expr.disjunction
      val print_term :
        ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
        Format.formatter -> Bddvar.Expr.term -> unit
      val print_conjunction :
        ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
        Format.formatter -> Bddvar.Expr.conjunction -> unit
      val print_disjunction :
        ([> Bddvar.typ ], [> Bddvar.typdef ]) #Bddvar.db ->
        Format.formatter -> Bddvar.Expr.disjunction -> unit
    end
end