Module Logtk__Term.AC

Parameters

• A : AC_SPEC

Signature

val flatten : Logtk.ID.t -> t list -> 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 : t -> t

normal form of the term modulo AC

val equal : t -> 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 : t Iter.t -> Logtk.ID.Set.t

Set of ID.ts occurring in the terms, that are AC

val seq_symbols : t -> Logtk.ID.t Iter.t

Iter of AC symbols in this term