module Infsys: sig end
Inference system for the bitvector theory
Th.bv
as defined in module
Bitvector. This inference system
is a variation of the inference system
Shostak.Make
for Shostak theories.
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.