sig
  type e
  val current : unit -> Infsys.ARITH.e
  val initialize : Infsys.ARITH.e -> unit
  val finalize : unit -> Infsys.ARITH.e
  val abstract : Term.t -> unit
  val merge : Fact.Equal.t -> unit
  val propagate : Fact.Equal.t -> unit
  val dismerge : Fact.Diseq.t -> unit
  val propagate_diseq : Fact.Diseq.t -> unit
  val branch : unit -> unit
  val normalize : unit -> unit
  val nonneg : Fact.Nonneg.t -> unit
  val pos : Fact.Pos.t -> unit
end