Module Cop.Infsys


module Infsys: sig  end
Inference system for the theory Th.cop of coproducts as defined in module Coproduct.

This inference system maintains a set of directed equalities x = a with x a variable, a a Th.cop-pure term, and none of the right-hand side variables occurs in any of the left-hand sides.

This inference system is obtained as an instantiation of the generic Shostak inference system Shostak.Infsys with a specification of the coproduct theory by means of the




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