sig
  module Add :
    sig
      type leaf = Arith.expr
      type t
      type id_unop
      type id_binop
      type id_combinop
      type mtbdd = Leaf of leaf | Ite of int * t * t
      val leafbackground : leaf
      module Hash :
        sig
          type key = leaf
          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 length : 'a t -> int
        end
      val hasht : int Hash.t
      module Assoc :
        sig
          type key = int
          type +'a t
          val empty : 'a t
          val is_empty : 'a t -> bool
          val add : key -> 'a -> 'a t -> 'a t
          val find : key -> 'a t -> 'a
          val remove : key -> 'a t -> 'a t
          val mem : key -> 'a t -> bool
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val map : ('a -> 'b) -> 'a t -> 'b t
          val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
          val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
        end
      val assoct : leaf Assoc.t ref
      val leaf_of_id : int -> leaf
      val id_of_leaf : leaf -> int
      val remove_leaf : leaf -> unit
      val iter_leaf : (int -> leaf -> unit) -> unit
      external to_idd : t -> Idd.t = "%identity"
      external of_idd : Idd.t -> t = "%identity"
      external manager : t -> Manager.t = "camlidl_cudd_bdd_manager"
      external is_cst : t -> bool = "camlidl_cudd_bdd_is_cst"
      external topvar : t -> int = "camlidl_cudd_bdd_topvar"
      external dthen : t -> t = "camlidl_cudd_rdd_dthen"
      external delse : t -> t = "camlidl_cudd_rdd_delse"
      external cofactors : int -> t -> t * t = "camlidl_cudd_rdd_cofactors"
      external cofactor : t -> Bdd.t -> t = "camlidl_cudd_rdd_cofactor"
      val dval : t -> leaf
      val inspect : t -> mtbdd
      external support : t -> Bdd.t = "camlidl_cudd_bdd_support"
      external supportsize : t -> int = "camlidl_cudd_bdd_supportsize"
      external is_var_in : int -> t -> bool = "camlidl_cudd_bdd_is_var_in"
      external vectorsupport : t array -> Bdd.t
        = "camlidl_cudd_bdd_vectorsupport"
      external vectorsupport2 : Bdd.t array -> t array -> Bdd.t
        = "camlidl_cudd_rdd_vectorsupport2"
      val cst : Manager.t -> leaf -> t
      external ite : Bdd.t -> t -> t -> t = "camlidl_cudd_rdd_ite"
      external compose : int -> Bdd.t -> t -> t = "camlidl_cudd_rdd_compose"
      external vectorcompose : Bdd.t array -> t -> t
        = "camlidl_cudd_rdd_vectorcompose"
      external is_equal : t -> t -> bool = "camlidl_cudd_bdd_is_equal"
      external is_equal_when : t -> t -> Bdd.t -> bool
        = "camlidl_cudd_bdd_is_equal_when"
      val is_eval_cst : t -> Bdd.t -> leaf option
      val is_ite_cst : Bdd.t -> t -> t -> leaf option
      external size : t -> int = "camlidl_cudd_bdd_size"
      external nbpaths : t -> float = "camlidl_cudd_bdd_nbpaths"
      external nbnonzeropaths : t -> float
        = "camlidl_cudd_rdd_nbnonzeropaths"
      external nbminterms : int -> t -> float = "camlidl_cudd_bdd_nbminterms"
      external density : int -> t -> float = "camlidl_cudd_bdd_density"
      external nbleaves : t -> int = "camlidl_cudd_rdd_nbleaves"
      external varmap : t -> t = "camlidl_cudd_rdd_varmap"
      external permute : int array -> t -> t = "camlidl_cudd_rdd_permute"
      external iter_node : (t -> unit) -> t -> unit
        = "camlidl_cudd_iter_node"
      val iter_cube : (Manager.tbool array -> leaf -> unit) -> t -> unit
      external guard_of_node : t -> t -> Bdd.t
        = "camlidl_cudd_rdd_guard_of_node"
      external guard_of_nonbackground : t -> Bdd.t
        = "camlidl_cudd_rdd_guard_of_nonbackground"
      external nodes_below_level : t -> int option -> t array
        = "camlidl_cudd_rdd_nodes_below_level"
      val leaves : t -> leaf array
      val guard_of_leaf : t -> leaf -> Bdd.t
      val guardleafs : t -> (Bdd.t * leaf) array
      external constrain : t -> Bdd.t -> t = "camlidl_cudd_rdd_constrain"
      external tdconstrain : t -> Bdd.t -> t = "camlidl_cudd_rdd_tdconstrain"
      external restrict : t -> Bdd.t -> t = "camlidl_cudd_rdd_restrict"
      external tdrestrict : t -> Bdd.t -> t = "camlidl_cudd_rdd_tdrestrict"
      external to_bdd : t -> Bdd.t = "camlidl_cudd_rdd_to_bdd"
      val alloc_unop : (leaf -> leaf) -> id_unop
      val alloc_binop : (leaf -> leaf -> leaf) -> id_binop
      val alloc_combinop : (leaf -> leaf -> leaf) -> id_combinop
      external apply_unop : id_unop -> t -> t = "camlidl_cudd_idd_apply_unop"
      external apply_binop : id_binop -> t -> t -> t
        = "camlidl_cudd_idd_apply_binop"
      external apply_combinop : id_combinop -> t -> t -> t
        = "camlidl_cudd_idd_apply_combinop"
      external transfer : t -> Manager.t -> t = "camlidl_cudd_rdd_transfer"
      external _print : t -> unit = "camlidl_cudd_print"
      val print__minterm : Format.formatter -> t -> unit
      val print_minterm :
        (int -> string) -> (leaf -> string) -> Format.formatter -> t -> unit
      val print :
        (int -> string) -> (leaf -> string) -> Format.formatter -> t -> unit
    end
  type t = (Arith.expr, ArithDD.Add.t) CondDD.ddexpr
  val of_expr : [> `Arith of ArithDD.t ] -> ArithDD.t
  val to_expr : ArithDD.t -> [> `Arith of ArithDD.t ]
  val to_add : #CondDD.db -> ArithDD.t -> ArithDD.Add.t
  val var : #CondDD.db -> Var.t -> ArithDD.t
  val cst : Mpqf.t -> ArithDD.t
  val add : #CondDD.db -> ArithDD.t -> ArithDD.t -> ArithDD.t
  val mul : #CondDD.db -> ArithDD.t -> ArithDD.t -> ArithDD.t
  val sub : #CondDD.db -> ArithDD.t -> ArithDD.t -> ArithDD.t
  val div : #CondDD.db -> ArithDD.t -> ArithDD.t -> ArithDD.t
  val gmod : #CondDD.db -> ArithDD.t -> ArithDD.t -> ArithDD.t
  val other : #CondDD.db -> Var.t -> ArithDD.t list -> ArithDD.t
  val negate : #CondDD.db -> ArithDD.t -> ArithDD.t
  val ite : #CondDD.db -> Bdd.t -> ArithDD.t -> ArithDD.t -> ArithDD.t
  val condition : #CondDD.db -> Arith.Condition.typ -> ArithDD.t -> Bdd.t
  val supeq : #CondDD.db -> ArithDD.t -> Bdd.t
  val sup : #CondDD.db -> ArithDD.t -> Bdd.t
  val eq : #CondDD.db -> ArithDD.t -> Bdd.t
  val cofactor : ArithDD.t -> Bdd.t -> ArithDD.t
  val tdrestrict : ArithDD.t -> Bdd.t -> ArithDD.t
  val support_cond : #CondDD.db -> ArithDD.t -> Bdd.t
  val support_leaf : #CondDD.db -> ArithDD.t -> Var.Set.t
  val substitute_expr :
    #CondDD.db ->
    Arith.expr -> [> `Arith of ArithDD.t ] Var.Map.t -> ArithDD.t
  val substitute_cond :
    #CondDD.db ->
    Arith.Condition.t -> [> `Arith of ArithDD.t ] Var.Map.t -> Bdd.t
  val print : #CondDD.db -> Format.formatter -> ArithDD.t -> unit
end