module Infsys: sig end
A
congruence closure state represents the conjunction of
a set of equalities
x = f(x1,...,xn) with
x,
xi term variables and
f
an uninterpreted function symbol. This set of equalities is
- injective in that
x = a and y = a implies x = y, and
- functional in that
x = a and x = b implies a = b.
type e
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, - not
p |= 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.