Module LogtkPrecedence_intf.S.Constr

module Constr: sig .. end

type t = LogtkPrecedence_intf.S.symbol ->
LogtkPrecedence_intf.S.symbol -> LogtkComparison.t
A partial order on symbols, used to make the precedence more precise
val cluster : LogtkPrecedence_intf.S.symbol list list -> t
ordering constraint by clustering symbols by decreasing order. all symbols in the first clusters are bigger than those in the second, etc.
val of_list : LogtkPrecedence_intf.S.symbol list -> t
symbols in the given list are in decreasing order
val of_precedence : LogtkPrecedence_intf.S.precedence -> t
Copy of another precedence on the common symbols
val arity : (LogtkPrecedence_intf.S.symbol -> int) -> t
decreasing arity constraint (big arity => high in precedence)
val invfreq : LogtkPrecedence_intf.S.symbol Sequence.t -> t
symbols with high frequency are smaller
val max : LogtkPrecedence_intf.S.symbol list -> t
maximal symbols, in decreasing order
val min : LogtkPrecedence_intf.S.symbol list -> t
minimal symbols, in decreasing order
val alpha : t
alphabetic ordering on symbols