module Letify:sig
..end
module Ground:sig
..end
module Sigma:sig
..end
module Defs:sig
..end
val bind : Sigma.t -> Defs.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 add_definitions : Sigma.t ->
Defs.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 occurring literals to split cases.