module Letify: sig
.. end
bind sigma defs xs
select definitions in defs
targeting variables xs
. The result is a new substitution that
potentially augment sigma
with definitions for xs
(and others).
val vmem : Lang.F.Vars.elt -> Lang.F.term -> bool
val occurs : Lang.F.Vars.t -> Lang.F.term -> bool
module Sigma: sig
.. end
module Defs: sig
.. end
module XS: FCSet.Make
(
Lang.F.Var
)
val elements : Lang.F.Vars.t -> XS.t
val iter : (XS.elt -> unit) -> Lang.F.Vars.t -> unit
: Lang.F.Tset.t Lang.F.Vmap.t ->
Sigma.t Pervasives.ref -> Lang.F.Vars.t -> XS.elt -> unit
val bind : Sigma.t ->
Lang.F.Tset.t Lang.F.Vmap.t -> Lang.F.Vars.t -> Sigma.t
bind sigma defs xs
select definitions in defs
targeting variables xs
. The result is a new substitution that
potentially augment sigma
with definitions for xs
(and others).
val get_class : Sigma.t -> Lang.F.Vars.t -> Lang.F.var -> Lang.F.Vars.elt list
val add_eq : Lang.F.pred list -> Lang.F.var -> Lang.F.var list -> Lang.F.pred list
val add_equals : Lang.F.var list -> Lang.F.pred list -> Lang.F.pred list
val add_definitions : Sigma.t ->
'a Lang.F.Vmap.t -> Lang.F.Vars.t -> Lang.F.pred list -> Lang.F.pred list
add_definitions sigma defs xs ps
keep all
definitions of variables xs
from sigma
that comes from defs
.
They are added to ps
.
module Split: sig
.. end
Pruning strategy ; selects most occuring literals to split cases.