module Make: functor (Sh : T) -> sig end
Constructing an inference system from a Shostak theory
Th.
For a description of the correctness statement of these inference
rules, see module
Infsys.
As an invariant, equality sets for representing contexts
of Shostak theories are ordered equalities of the
form x = a with x a variable and a a nonvariable,
Sh.th-pure term. In addition, these equality sets are in
- solved form, that is, there are no
x = a, y = b
with x a variable in b.
- canonical, that is, if
x = y has been propagated
using the propagate rule, then the noncanonical x does
not appear in the equality set. Also, right-hand sides are
always kept in canonical form w.r.t to the given theory canonizer map.
In case of
convex Shostak theories,
disjunction always fails,
and there is no branching.
In case of incomplete Shostak theories, solve might raise
Exc.Incomplete on an equality a = b. Now, a, b are
named apart and the corresponding variable equality is merged.
Notice, that incomplete solvers might lead to an incompleteness in
the inference procedure.
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.