Functor Infsys.TraceArith


module TraceArith: functor (I : ARITH) -> functor (L : sig  end) -> sig  end
Tracing rule applications.
Parameters:
I : Infsys.ARITH
L : sig end


type e
val current : unit -> e
Parameters:
? : unit
val initialize : e -> unit
Parameters:
? : e
val finalize : unit -> e
Parameters:
? : unit
val abstract : Term.t -> unit
Parameters:
? : Term.t
val merge : Fact.Equal.t -> unit
Parameters:
? : Fact.Equal.t
val propagate : Fact.Equal.t -> unit
Parameters:
? : Fact.Equal.t
val dismerge : Fact.Diseq.t -> unit
Parameters:
? : Fact.Diseq.t
val propagate_diseq : Fact.Diseq.t -> unit
Parameters:
? : Fact.Diseq.t
val branch : unit -> unit
Parameters:
? : unit
val normalize : unit -> unit
Above is identical to Infsys.EQ.
Parameters:
? : unit
val nonneg : Fact.Nonneg.t -> unit
(g, a >= 0; e; p) ==> (g; e'; p') with
Parameters:
? : Fact.Nonneg.t
val pos : Fact.Pos.t -> unit
(g, a > 0; e; p) ==> (g; e'; p') with
Parameters:
? : Fact.Pos.t