sig
  type typ = [ `Benum of Var.t | `Bint of bool * int | `Bool | `Int | `Real ]
  type typdef = Bddvar.typdef
  type cond = [ `Arith of Arith.Condition.t ]
  type ('a, 'b) ddexpr = Leaf of 'a | Mtbdd of 'b
  module HashCond :
    sig
      type key = cond
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val map : (key -> 'a -> 'b) -> 'a t -> 'b t
      val length : 'a t -> int
      val print :
        ?first:(unit, Format.formatter, unit) format ->
        ?sep:(unit, Format.formatter, unit) format ->
        ?last:(unit, Format.formatter, unit) format ->
        ?firstbind:(unit, Format.formatter, unit) format ->
        ?sepbind:(unit, Format.formatter, unit) format ->
        ?lastbind:(unit, Format.formatter, unit) format ->
        (Format.formatter -> key -> unit) ->
        (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
    end
  module DHashCond :
    sig
      module HashX :
        sig
          type key = cond
          type 'a t = 'a HashCond.t
          val create : int -> 'a t
          val clear : 'a t -> unit
          val copy : 'a t -> 'a t
          val add : 'a t -> key -> 'a -> unit
          val remove : 'a t -> key -> unit
          val find : 'a t -> key -> 'a
          val find_all : 'a t -> key -> 'a list
          val replace : 'a t -> key -> 'a -> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val map : (key -> 'a -> 'b) -> 'a t -> 'b t
          val length : 'a t -> int
          val print :
            ?first:(unit, Format.formatter, unit) format ->
            ?sep:(unit, Format.formatter, unit) format ->
            ?last:(unit, Format.formatter, unit) format ->
            ?firstbind:(unit, Format.formatter, unit) format ->
            ?sepbind:(unit, Format.formatter, unit) format ->
            ?lastbind:(unit, Format.formatter, unit) format ->
            (Format.formatter -> key -> unit) ->
            (Format.formatter -> 'a -> unit) ->
            Format.formatter -> 'a t -> unit
        end
      module HashY :
        sig
          type key = int * bool
          type 'a t = 'a HashheIB.t
          val create : int -> 'a t
          val clear : 'a t -> unit
          val copy : 'a t -> 'a t
          val add : 'a t -> key -> 'a -> unit
          val remove : 'a t -> key -> unit
          val find : 'a t -> key -> 'a
          val find_all : 'a t -> key -> 'a list
          val replace : 'a t -> key -> 'a -> unit
          val mem : 'a t -> key -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val map : (key -> 'a -> 'b) -> 'a t -> 'b t
          val length : 'a t -> int
          val print :
            ?first:(unit, Format.formatter, unit) format ->
            ?sep:(unit, Format.formatter, unit) format ->
            ?last:(unit, Format.formatter, unit) format ->
            ?firstbind:(unit, Format.formatter, unit) format ->
            ?sepbind:(unit, Format.formatter, unit) format ->
            ?lastbind:(unit, Format.formatter, unit) format ->
            (Format.formatter -> key -> unit) ->
            (Format.formatter -> 'a -> unit) ->
            Format.formatter -> 'a t -> unit
        end
      type x = HashX.key
      type y = HashY.key
      type t
      val clear : t -> unit
      val create : int -> t
      val add : t -> x -> y -> unit
      val y_of_x : t -> x -> y
      val x_of_y : t -> y -> x
      val removex : t -> x -> unit
      val removey : t -> y -> unit
      val memx : t -> x -> bool
      val memy : t -> y -> bool
      val iter : t -> (x -> y -> unit) -> unit
      val fold : t -> 'a -> (x -> y -> 'a -> 'a) -> 'a
      val cardinal : t -> int
      val print :
        ?first:(unit, Format.formatter, unit) format ->
        ?sep:(unit, Format.formatter, unit) format ->
        ?last:(unit, Format.formatter, unit) format ->
        ?firstbind:(unit, Format.formatter, unit) format ->
        ?sepbind:(unit, Format.formatter, unit) format ->
        ?lastbind:(unit, Format.formatter, unit) format ->
        (Format.formatter -> x -> unit) ->
        (Format.formatter -> y -> unit) -> Format.formatter -> t -> unit
    end
  class type db =
    object
      val mutable v_bddincr : int
      val mutable v_bddindex : int
      val mutable v_careset : Bdd.t
      val v_cond : CondDD.DHashCond.t
      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 : typdef 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 : typ Var.Map.t
      method private add_label : Var.t -> typ -> unit
      method add_typ : Var.t -> typdef -> unit
      method add_var : Var.t -> typ -> unit
      method bddincr : int
      method bddindex : int
      method careset : Bdd.t
      method cond : CondDD.DHashCond.t
      method cond_of_idb : int * bool -> CondDD.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 : 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 : typ Var.Map.t -> unit
      method typ_of_var : Var.t -> typ
      method typdef : typdef Var.Map.t
      method typdef_of_typ : Var.t -> typdef
      method var_of_idcond : int -> Var.t
      method varinfo : Bddvar.info Var.Map.t
      method varset : Bdd.t Var.Map.t
      method vartyp : typ Var.Map.t
    end
  class make_db : Manager.t -> db
  val print_cond : Format.formatter -> CondDD.cond -> unit
  val print_typ : Format.formatter -> CondDD.typ -> unit
  val print_typdef : Format.formatter -> CondDD.typdef -> unit
  val print_db : Format.formatter -> #CondDD.db -> unit
  val cond_support : CondDD.cond -> Var.Set.t
  val condition :
    leaf_of_id:(int -> 'a) ->
    cond_of_leaf:('a -> [ `Arith of Arith.Condition.t | `Bool of bool ]) ->
    #CondDD.db -> ('a, 'b) CondDD.ddexpr -> Bdd.t
  val substitute_ddexpr :
    substitute_leaf:((#CondDD.db as 'a) ->
                     'b -> 'c Var.Map.t -> ('b, 'd) CondDD.ddexpr) ->
    guardleafs:('d -> (Bdd.t * 'b) array) ->
    ite:('a ->
         Bdd.t ->
         ('b, 'd) CondDD.ddexpr ->
         ('b, 'd) CondDD.ddexpr -> ('b, 'd) CondDD.ddexpr) ->
    'a ->
    ('b, 'd) CondDD.ddexpr ->
    Bdd.t array option -> 'c Var.Map.t -> ('b, 'd) CondDD.ddexpr
  val compute_careset : #CondDD.db -> unit
end