module Unidirectional: sig .. end
include Sl_unify.S
val existential_split_check : state_check
val modulo_entl : update_check
val existential_intro : update_check
val is_substitution : update_check
val trm_check : update_check
When used as state update check in a call to Sl_heap.unify for unifying
heaps h and h', ensures that the generated substitution, when applied
to h, produces a formula which is subsumed by h'
val avoid_replacing_trms : ?inverse:bool -> Sl_term.Set.t -> update_check
A state update check which prevents replacements of variables within the
given set of terms. When the optional flag inverse=false is set to true
the check prevents replacements from substituting any of the variables
within the given set
val avoid_replacing_tags : ?inverse:bool -> Tags.t -> update_check
val tag_check : update_check
val existentials_only : update_check
val unify_tag_constraints : ?total:bool ->
?inverse:bool -> ?update_check:update_check -> Ord_constraints.t unifier
Ord_constraints.unify lifted to the SL unifier type
val remove_dup_substs : state list -> state list
remove_dup_substs states will remove any states in states where the
universal parts (i.e. the mappings from universals to universals) of both
the tag and term substitutions are duplicates of a previous state.