module Infsys: functor (Sig : SIG) -> sig end
Inference system for a theory with a single AC symbol.
An AC context consists of equalities of the form x = y*z
with x, y, z variables, with * an associative-commutative
function symbol.
The following invariants are maintained.
- Right-hand sides of context equalities
x = a are kept in
canonical form. That is, if the variable equality y = z
has been merged using merge, then the noncanonical y
is not appearing on any right-hand side.
- Also, if
x = a and y = b in a context, then the
variables x and y are different (that is, they are not Term.eq)
- If
u = y * v in a context, then y is always atomic in the
sense that it is an original variable from one of the arguments
of process or name, whereas u, v may be generated
variables.
Forward chaining is used to keep contexts
confluent
x' = y * v, z = x*u, x =v x' ==> z = y * v * u
with =v generated by the current variable partitioning.
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.