Wp.Letify
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.