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

• coproduct canonizer Coproduct.map
• coproduct solver Coproduct.solve

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.