module type ARITH = sig end
Abstract interface of an inference system for arithmetic theories
as an extension of the
Infsys.EQ signature.
type e
val current : unit -> e
val initialize : e -> unit
val finalize : unit -> 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
(g, a >= 0; e; p) ==>
(g; e'; p')
with
a pure|= e', p' <=> |= e, a >= 0, p- if
e' |= x = y then p' |= x = y.
val pos : Fact.Pos.t -> unit
(g, a > 0; e; p) ==>
(g; e'; p')
with
a pure|= e', p' <=> |= e, a > 0, p- if
e' |= x = y then p' |= x = y.