module Sl_ptos: sig .. end
Multiset of points-tos.
include Utilsigs.OrderedContainer
val subst : Sl_subst.t -> t -> t
val terms : t -> Sl_term.Set.t
val vars : t -> Sl_term.Set.t
val to_string_list : t -> string list
val to_melt : t -> Latex.t
val subsumed : ?total:bool -> Sl_uf.t -> t -> t -> bool
subsumed eqs ptos ptos' is true iff ptos can be rewritten using the
equalities eqs such that it becomes equal to ptos'.
If the optional argument ~total=true is set to false then
check if rewriting could make the first multiset a sub(multi)set of
the second.
val unify : ?total:bool ->
?update_check:Sl_unify.Unidirectional.update_check ->
t Sl_unify.Unidirectional.unifier
Compute substitution that would make the two multisets equal.
If the optional argument ~total=true is set to false then
compute a substitution that would make the first multiset a sub(multi)set of
the second.
val biunify : ?total:bool ->
?update_check:Sl_unify.Bidirectional.update_check ->
t Sl_unify.Bidirectional.unifier
val norm : Sl_uf.t -> t -> t
Replace all terms with their UF representative. NB this may replace nil
with a variable.