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