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