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