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

• product canonizer Product.map
• product solver Product.solve

In particular, there is no branching for this theory, and the inference system is complete as the product solver itself is complete.

val current : unit -> e

val initialize : e -> unit

Intitialize inference system with equality set.

val finalize : unit -> e

Retrieve modified equality set.

val abstract : Term.t -> unit

(g[a]; e; p) ==> (g[x]; e, x = a; p) with

• a a nonvariable term,
• a an i-pure term,
• and x fresh.

val merge : Fact.Equal.t -> unit

(g, a = b; e; p) ==> (g; e'; p') with

• a, b i-pure,
• |= e', p' <=> |= e, a = b, p
• if e' |= x = y then p' |= x = y.

val propagate : Fact.Equal.t -> unit

(g, e; p) ==> (g; e'; p) with

• e |= x = y,
• notp |= x = y,
• |= e, p <=> |= e', p'

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.

val propagate_diseq : Fact.Diseq.t -> unit

(g; e; p) ==> (g; e'; p') with

• p' |= x <> y
• |= e', p' <=> |= e, p.

val branch : unit -> unit

(g; e; p) ==> (g, c1; e; p) | ... | (g, cn; e; p) with

• e, p |= c1 \/ ... \/ cn
• not e, p |= ci

val normalize : unit -> unit

(g; e; p) ==> (g'; e'; p') where source and target configuration are equivalent.