module AC (A : AC_SPEC) : sig .. end
val flatten : ID.t -> FOTerm.t list -> FOTerm.t list
flatten_ac f l flattens the list of terms l by deconstructing all its
elements that have f as head ID.t. For instance, if l=1+2; 3+(4+5)
with f="+", this will return 1;2;3;4;5, perhaps in a different order
val normal_form : FOTerm.t -> FOTerm.t
normal form of the term modulo AC
val equal : FOTerm.t -> FOTerm.t -> bool
Check whether the two terms are AC-equal. Optional arguments specify
which ID.ts are AC or commutative (by default by looking at
attr_ac and attr_commut).
val symbols : FOTerm.t Sequence.t -> ID.Set.t
Set of ID.ts occurring in the terms, that are AC
val seq_symbols : FOTerm.t -> ID.t Sequence.t
Sequence of AC symbols in this term