sig
  val mk_num : Mpa.Q.t -> Term.t
  val mk_zero : unit -> Term.t
  val mk_one : unit -> Term.t
  val mk_two : unit -> Term.t
  val mk_add : Term.t -> Term.t -> Term.t
  val mk_addl : Term.t list -> Term.t
  val mk_incr : Term.t -> Term.t
  val mk_decr : Term.t -> Term.t
  val mk_sub : Term.t -> Term.t -> Term.t
  val mk_neg : Term.t -> Term.t
  val mk_addq : Mpa.Q.t -> Term.t -> Term.t
  val mk_multq : Mpa.Q.t -> Term.t -> Term.t
  val is_pure : Term.t -> bool
  val is_interp : Term.t -> bool
  val is_num : Term.t -> bool
  val is_q : Mpa.Q.t -> Term.t -> bool
  val is_zero : Term.t -> bool
  val is_one : Term.t -> bool
  val is_nonneg_num : Term.t -> bool
  val is_pos_num : Term.t -> bool
  val is_nonpos_num : Term.t -> bool
  val is_diophantine : Term.t -> bool
  val is_nonneg : Term.t -> Three.t
  val is_pos : Term.t -> Three.t
  val d_interp : Term.t -> Sym.arith * Term.t list
  val constant_of : Term.t -> Mpa.Q.t
  val nonconstant_of : Term.t -> Term.t
  val nonconstant_monomials_of : Term.t -> Term.t list
  val d_num : Term.t -> Mpa.Q.t
  val d_add : Term.t -> Term.t list
  val coefficient_of : Term.t -> Term.t -> Mpa.Q.t
  val lcm_of_denominators : Term.t -> Mpa.Z.t
  val iter : (Term.t -> unit) -> Term.t -> unit
  val fold : (Term.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
  val for_all : (Term.t -> bool) -> Term.t -> bool
  val map : (Term.t -> Term.t) -> Term.t -> Term.t
  val apply : Term.Equal.t -> Term.t -> Term.t
  module Monomials :
    sig
      type pred = Mpa.Q.t -> Term.t -> bool
      val is_true : Arith.Monomials.pred
      val is_pos : Arith.Monomials.pred
      val is_neg : Arith.Monomials.pred
      val is_var : Term.t -> Arith.Monomials.pred
      val mapq : (Mpa.Q.t -> Mpa.Q.t) -> Term.t -> Term.t
      val fold :
        Arith.Monomials.pred ->
        (Mpa.Q.t -> Term.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
      val exists : Arith.Monomials.pred -> Term.t -> bool
      val for_all : Arith.Monomials.pred -> Term.t -> bool
      val variable_choose : Arith.Monomials.pred -> Term.t -> Term.t
      val coefficient_choose : Arith.Monomials.pred -> Term.t -> Mpa.Q.t
      module Pos :
        sig
          val is_empty : Term.t -> bool
          val exists : Arith.Monomials.pred -> Term.t -> bool
          val for_all : Arith.Monomials.pred -> Term.t -> bool
          val fold : (Mpa.Q.t -> Term.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
          val iter : (Mpa.Q.t -> Term.t -> unit) -> Term.t -> unit
          val mem : Term.t -> Term.t -> bool
          val variable_choose :
            (Mpa.Q.t -> Term.t -> bool) -> Term.t -> Term.t
          val variable_least_of : Term.t -> Term.t
          val coefficient_of : Term.t -> Term.t -> Mpa.Q.t
        end
      module Neg :
        sig
          val is_empty : Term.t -> bool
          val exists : Arith.Monomials.pred -> Term.t -> bool
          val for_all : Arith.Monomials.pred -> Term.t -> bool
          val fold : (Mpa.Q.t -> Term.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
          val iter : (Mpa.Q.t -> Term.t -> unit) -> Term.t -> unit
          val mem : Term.t -> Term.t -> bool
          val variable_choose :
            (Mpa.Q.t -> Term.t -> bool) -> Term.t -> Term.t
          val variable_least_of : Term.t -> Term.t
          val coefficient_of : Term.t -> Term.t -> Mpa.Q.t
        end
    end
  val sigma : Sym.arith -> Term.t list -> Term.t
  val qsolve : Term.t * Term.t -> Term.t * Term.t
  val zsolve : Term.t * Term.t -> (Term.t * Term.t) list
  val integer_solve : bool Pervasives.ref
  val solve : Term.t * Term.t -> (Term.t * Term.t) list
  val isolate : Term.t -> Term.Equal.t -> Term.Equal.t
  val dom : (Term.t -> Dom.t) -> Sym.arith -> Term.t list -> Dom.t
  val dom_of : Term.t -> Dom.t
  val is_int : Term.t -> bool
end