Module Letify

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).

look for the shape: \forall x:integer. (csta <= x /\ x <= cstb) => t1=t2 and return Some(csta,cstb)

< on integer are always normalized to <=


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 occuring literals to split cases.