Functor LogtkFOTerm.AC

module AC (A : AC_SPEC) : sig .. end
Parameters:
A : AC_SPEC

val flatten : LogtkSymbol.t -> LogtkFOTerm.t list -> LogtkFOTerm.t list
flatten_ac f l flattens the list of terms l by deconstructing all its elements that have f as head symbol. 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 : LogtkFOTerm.t -> LogtkFOTerm.t
normal form of the term modulo AC
val eq : LogtkFOTerm.t -> LogtkFOTerm.t -> bool
Check whether the two terms are AC-equal. Optional arguments specify which symbols are AC or commutative (by default by looking at attr_ac and attr_commut).
val symbols : LogtkFOTerm.t Sequence.t -> LogtkSymbol.Set.t
Set of symbols occurring in the terms, that are AC