Module P.Infsys


module Infsys: sig  end
Inference system for the theory Th.p of products as described in module Product. This inference system is obtained as an instantiation of the generic Shostak inference system Shostak.Infsys with a specification of the convex product theory by means of the In particular, there is no branching for this theory, and the inference system is complete as the product solver itself is complete.


type e
val current : unit -> e
Parameters:
? : unit
val initialize : e -> unit
Intitialize inference system with equality set.
Parameters:
? : e
val finalize : unit -> e
Retrieve modified equality set.
Parameters:
? : unit
val abstract : Term.t -> unit
(g[a]; e; p) ==> (g[x]; e, x = a; p) with
Parameters:
? : Term.t
val merge : Fact.Equal.t -> unit
(g, a = b; e; p) ==> (g; e'; p') with
Parameters:
? : Fact.Equal.t
val propagate : Fact.Equal.t -> unit
(g, e; p) ==> (g; e'; p) with
Parameters:
? : Fact.Equal.t
val dismerge : Fact.Diseq.t -> unit
(g, a <> a; e; p) ==> (g; e'; p') with a, b i-pure, |= e', p' <=> |= e, p, a <> b.
Parameters:
? : Fact.Diseq.t
val propagate_diseq : Fact.Diseq.t -> unit
(g; e; p) ==> (g; e'; p') with
Parameters:
? : Fact.Diseq.t
val branch : unit -> unit
(g; e; p) ==> (g, c1; e; p) | ... | (g, cn; e; p) with
Parameters:
? : unit
val normalize : unit -> unit
(g; e; p) ==> (g'; e'; p') where source and target configuration are equivalent.
Parameters:
? : unit