sig
  type cond = CondDD.cond
  type typ = CondDD.typ
  type typdef = CondDD.typdef
  type expr =
      [ `Arith of ArithDD.t
      | `Benum of Bddenum.t
      | `Bint of Bddint.t
      | `Bool of Bdd.t ]
  type leaf = [ `Arith of Arith.expr ]
  class type db =
    object
      method add_typ : Var.t -> Formula.typdef -> unit
      method add_var : Var.t -> Formula.typ -> unit
      method bddincr : int
      method bddindex : int
      method careset : Bdd.t
      method cond : CondDD.DHashCond.t
      method cond_of_idb : int * bool -> Formula.cond
      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_careset : Bdd.t -> unit
      method set_idcondvar : Var.t MappeI.t -> unit
      method set_print_external_idcondb :
        (Format.formatter -> int * bool -> unit) -> unit
      method set_typdef : Formula.typdef 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 : Formula.typ Var.Map.t -> unit
      method typ_of_var : Var.t -> Formula.typ
      method typdef : Formula.typdef Var.Map.t
      method typdef_of_typ : Var.t -> Formula.typdef
      method var_of_idcond : int -> Var.t
      method varinfo : Bddvar.info Var.Map.t
      method varset : Bdd.t Var.Map.t
      method vartyp : Formula.typ Var.Map.t
    end
  class make_db : Manager.t -> CondDD.db
  val typ_of_expr : Formula.expr -> Formula.typ
  val print_cond : Format.formatter -> Formula.cond -> unit
  val print_typ : Format.formatter -> Formula.typ -> unit
  val print_typdef : Format.formatter -> Formula.typdef -> unit
  val print_expr : #db -> Format.formatter -> expr -> unit
  val print_bdd : #db -> Format.formatter -> Bdd.t -> unit
  val print_db : Format.formatter -> #Formula.db -> unit
  module Bool :
    sig
      type t = Bdd.t
      val of_expr : Formula.expr -> Formula.Bool.t
      val to_expr : Formula.Bool.t -> Formula.expr
      val dtrue : #Formula.db -> Formula.Bool.t
      val dfalse : #Formula.db -> Formula.Bool.t
      val of_bool : #Formula.db -> bool -> Formula.Bool.t
      val var : #Formula.db -> Var.t -> Formula.Bool.t
      val dnot : #Formula.db -> Formula.Bool.t -> Formula.Bool.t
      val dand :
        #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
      val dor :
        #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
      val xor :
        #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
      val nand :
        #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
      val nor :
        #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
      val nxor :
        #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
      val eq :
        #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
      val ite :
        #Formula.db ->
        Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t -> Formula.Bool.t
      val is_included_in :
        ?sem:bool -> #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> bool
      val is_inter_empty :
        ?sem:bool -> #Formula.db -> Formula.Bool.t -> Formula.Bool.t -> bool
      val exists :
        ?sem:bool ->
        #Formula.db -> Var.t list -> Formula.Bool.t -> Formula.Bool.t
      val forall :
        ?sem:bool ->
        #Formula.db -> Var.t list -> Formula.Bool.t -> Formula.Bool.t
      val print : #Formula.db -> Format.formatter -> Formula.Bool.t -> unit
    end
  module Bint :
    sig
      type t = Bddint.t
      val of_expr : Formula.expr -> Formula.Bint.t
      val to_expr : Formula.Bint.t -> Formula.expr
      val of_int :
        #Formula.db -> [> `Tbint of bool * int ] -> int -> Formula.Bint.t
      val var : #Formula.db -> Var.t -> Formula.Bint.t
      val neg : #Formula.db -> Formula.Bint.t -> Formula.Bint.t
      val succ : #Formula.db -> Formula.Bint.t -> Formula.Bint.t
      val pred : #Formula.db -> Formula.Bint.t -> Formula.Bint.t
      val add :
        #Formula.db -> Formula.Bint.t -> Formula.Bint.t -> Formula.Bint.t
      val sub :
        #Formula.db -> Formula.Bint.t -> Formula.Bint.t -> Formula.Bint.t
      val shift_left : #Formula.db -> int -> Formula.Bint.t -> Formula.Bint.t
      val shift_right :
        #Formula.db -> int -> Formula.Bint.t -> Formula.Bint.t
      val scale : #Formula.db -> int -> Formula.Bint.t -> Formula.Bint.t
      val ite :
        #Formula.db ->
        Bdd.t -> Formula.Bint.t -> Formula.Bint.t -> Formula.Bint.t
      val zero : #Formula.db -> Formula.Bint.t -> Bdd.t
      val eq : #Formula.db -> Formula.Bint.t -> Formula.Bint.t -> Bdd.t
      val eq_int : #Formula.db -> Formula.Bint.t -> int -> Bdd.t
      val supeq : #Formula.db -> Formula.Bint.t -> Formula.Bint.t -> Bdd.t
      val supeq_int : #Formula.db -> Formula.Bint.t -> int -> Bdd.t
      val sup : #Formula.db -> Formula.Bint.t -> Formula.Bint.t -> Bdd.t
      val print : #Formula.db -> Format.formatter -> Formula.Bint.t -> unit
    end
  module Benum :
    sig
      type t = Bddenum.t
      val of_expr : Formula.expr -> Formula.Benum.t
      val to_expr : Formula.Benum.t -> Formula.expr
      val var : #Formula.db -> Var.t -> Formula.Benum.t
      val ite :
        #Formula.db ->
        Bdd.t -> Formula.Benum.t -> Formula.Benum.t -> Formula.Benum.t
      val eq : #Formula.db -> Formula.Benum.t -> Formula.Benum.t -> Bdd.t
      val eq_label : #Formula.db -> Formula.Benum.t -> Var.t -> Bdd.t
      val print : #Formula.db -> Format.formatter -> Formula.Benum.t -> unit
    end
  module Arith :
    sig
      type t = ArithDD.t
      val of_expr : [> `Arith of Formula.Arith.t ] -> Formula.Arith.t
      val to_expr : Formula.Arith.t -> [> `Arith of Formula.Arith.t ]
      val var : #Formula.db -> Var.t -> Formula.Arith.t
      val cst : Mpqf.t -> Formula.Arith.t
      val add :
        #Formula.db -> Formula.Arith.t -> Formula.Arith.t -> Formula.Arith.t
      val mul :
        #Formula.db -> Formula.Arith.t -> Formula.Arith.t -> Formula.Arith.t
      val sub :
        #Formula.db -> Formula.Arith.t -> Formula.Arith.t -> Formula.Arith.t
      val div :
        #Formula.db -> Formula.Arith.t -> Formula.Arith.t -> Formula.Arith.t
      val gmod :
        #Formula.db -> Formula.Arith.t -> Formula.Arith.t -> Formula.Arith.t
      val other :
        #Formula.db -> Var.t -> Formula.Arith.t list -> Formula.Arith.t
      val negate : #Formula.db -> Formula.Arith.t -> Formula.Arith.t
      val ite :
        #Formula.db ->
        Bdd.t -> Formula.Arith.t -> Formula.Arith.t -> Formula.Arith.t
      val condition :
        #Formula.db -> Arith.Condition.typ -> Formula.Arith.t -> Bdd.t
      val supeq : #Formula.db -> Formula.Arith.t -> Bdd.t
      val sup : #Formula.db -> Formula.Arith.t -> Bdd.t
      val eq : #Formula.db -> Formula.Arith.t -> Bdd.t
      val substitute_expr :
        #Formula.db ->
        Arith.expr ->
        [> `Arith of Formula.Arith.t ] Var.Map.t -> Formula.Arith.t
      val substitute_cond :
        #Formula.db ->
        Arith.Condition.t ->
        [> `Arith of Formula.Arith.t ] Var.Map.t -> Bdd.t
      val print : #Formula.db -> Format.formatter -> Formula.Arith.t -> unit
    end
  val eq : #Formula.db -> Formula.expr -> Formula.expr -> Formula.Bool.t
  val ite :
    #Formula.db ->
    Formula.Bool.t -> Formula.expr -> Formula.expr -> Formula.expr
  val compose_of_substitution :
    #Formula.db ->
    Formula.expr Var.Map.t -> Bdd.t array option * Formula.expr Var.Map.t
  val substitute :
    #Formula.db -> Formula.expr -> Formula.expr Var.Map.t -> Formula.expr
  val var : #Formula.db -> Var.t -> Formula.expr
  val cofactor : Formula.expr -> Bdd.t -> Formula.expr
  val tdrestrict : Formula.expr -> Bdd.t -> Formula.expr
  val support_cond : #Formula.db -> Formula.expr -> Bdd.t
  val vectorsupport_cond : #Formula.db -> Formula.expr list -> Bdd.t
  val support : #Formula.db -> Formula.expr -> Var.Set.t
  val print_expr : #Formula.db -> Format.formatter -> Formula.expr -> unit
  val print_bdd : #Formula.db -> Format.formatter -> Bdd.t -> unit
  val cleanup : #Formula.db -> SetteI.t -> Formula.expr list -> unit
end