sig
  type typ = [ `Int | `Real ]
  class type ['a] db =
    object constraint 'a = [> Arith.typ ] method typ_of_var : Var.t -> 'a end
  module Lin :
    sig
      type term = Mpqf.t * Var.t
      type expr = { cst : Mpqf.t; lterm : Arith.Lin.term list; }
      val normalize : Arith.Lin.expr -> Arith.Lin.expr
      val compare_lterm : Arith.Lin.term list -> Arith.Lin.term list -> int
      val compare : Arith.Lin.expr -> Arith.Lin.expr -> int
      val var : Var.t -> Arith.Lin.expr
      val cst : Mpqf.t -> Arith.Lin.expr
      val add : Arith.Lin.expr -> Arith.Lin.expr -> Arith.Lin.expr
      val sub : Arith.Lin.expr -> Arith.Lin.expr -> Arith.Lin.expr
      val scale : Mpqf.t -> Arith.Lin.expr -> Arith.Lin.expr
      val negate : Arith.Lin.expr -> Arith.Lin.expr
      val support : Arith.Lin.expr -> Var.Set.t
      val rename : Arith.Lin.expr -> Var.t Var.Map.t -> Arith.Lin.expr
      val normalize_as_constraint : Arith.Lin.expr -> Arith.Lin.expr
      val print : Format.formatter -> Arith.Lin.expr -> unit
    end
  module Poly :
    sig
      type varexp = Var.t * int
      type monomial = Arith.Poly.varexp list
      type term = Mpqf.t * Arith.Poly.monomial
      type expr = Arith.Poly.term list
      val compare_varexp : Arith.Poly.varexp -> Arith.Poly.varexp -> int
      val compare_monomial :
        Arith.Poly.monomial -> Arith.Poly.monomial -> int
      val normalize_monomial : Arith.Poly.monomial -> Arith.Poly.monomial
      val normalize : Arith.Poly.expr -> Arith.Poly.expr
      val normalize_full : Arith.Poly.expr -> Arith.Poly.expr
      val compare : Arith.Poly.expr -> Arith.Poly.expr -> int
      val cst : Mpqf.t -> Arith.Poly.expr
      val var : Var.t -> Arith.Poly.expr
      val add : Arith.Poly.expr -> Arith.Poly.expr -> Arith.Poly.expr
      val sub : Arith.Poly.expr -> Arith.Poly.expr -> Arith.Poly.expr
      val scale :
        Mpqf.t * Arith.Poly.monomial -> Arith.Poly.expr -> Arith.Poly.expr
      val mul : Arith.Poly.expr -> Arith.Poly.expr -> Arith.Poly.expr
      val div : Arith.Poly.expr -> Arith.Poly.expr -> Arith.Poly.expr
      val negate : Arith.Poly.expr -> Arith.Poly.expr
      val support : Arith.Poly.expr -> Var.Set.t
      val rename : Arith.Poly.expr -> Var.t Var.Map.t -> Arith.Poly.expr
      val normalize_as_constraint : Arith.Poly.expr -> Arith.Poly.expr
      val print : Format.formatter -> Arith.Poly.expr -> unit
    end
  module Tree :
    sig
      type binop = Add | Sub | Mul | Div | Mod
      type expr =
          Cst of Mpqf.t
        | Ref of Var.t
        | Binop of Arith.Tree.binop * Arith.Tree.expr * Arith.Tree.expr
        | Other of Var.t * Arith.Tree.expr list
      val support : Arith.Tree.expr -> Var.Set.t
      val rename : Arith.Tree.expr -> Var.t Var.Map.t -> Arith.Tree.expr
      val print : Format.formatter -> Arith.Tree.expr -> unit
    end
  val lin_of_poly : Arith.Poly.expr -> Arith.Lin.expr
  val lin_of_tree : Arith.Tree.expr -> Arith.Lin.expr
  val poly_of_tree : Arith.Tree.expr -> Arith.Poly.expr
  val tree_of_lin : Arith.Lin.expr -> Arith.Tree.expr
  val tree_of_poly : Arith.Poly.expr -> Arith.Tree.expr
  type expr =
      Lin of Arith.Lin.expr
    | Poly of Arith.Poly.expr
    | Tree of Arith.Tree.expr
  val var : [> Arith.typ ] #Arith.db -> Var.t -> Arith.expr
  val cst : Mpqf.t -> Arith.expr
  val add : Arith.expr -> Arith.expr -> Arith.expr
  val sub : Arith.expr -> Arith.expr -> Arith.expr
  val mul : Arith.expr -> Arith.expr -> Arith.expr
  val div : Arith.expr -> Arith.expr -> Arith.expr
  val gmod : Arith.expr -> Arith.expr -> Arith.expr
  val other : Var.t -> Arith.expr list -> Arith.expr
  val negate : Arith.expr -> Arith.expr
  val support : Arith.expr -> Var.Set.t
  val rename : Arith.expr -> Var.t Var.Map.t -> Arith.expr
  val normalize : Arith.expr -> Arith.expr
  val equal : Arith.expr -> Arith.expr -> bool
  val hash : Arith.expr -> int
  val compare : Arith.expr -> Arith.expr -> int
  val normalize_as_constraint : Arith.expr -> Arith.expr
  val is_dependent_on_integer_only :
    [> Arith.typ ] #Arith.db -> Arith.expr -> bool
  val typ_of_expr :
    [> Arith.typ ] #Arith.db -> Arith.expr -> [ `Int | `Real ]
  val print : Format.formatter -> Arith.expr -> unit
  val print_typ : Format.formatter -> [> Arith.typ ] -> unit
  module Condition :
    sig
      type typ = EQ | SUPEQ | SUP | NEQ
      type t = Arith.Condition.typ * Arith.expr
      val make :
        < typ_of_var : Var.t -> [> `Int | `Real ]; .. > ->
        Arith.Condition.typ ->
        Arith.expr -> [ `Arith of Arith.Condition.t | `Bool of bool ]
      val negate :
        < typ_of_var : Var.t -> [> `Int | `Real ]; .. > ->
        Arith.Condition.t -> Arith.Condition.t
      val support : Arith.Condition.t -> Var.Set.t
      val print : Format.formatter -> Arith.Condition.t -> unit
      val compare : Arith.Condition.t -> Arith.Condition.t -> int
    end
end