Module LogtkOrdering.Default

module Default: S  with module Prec = LogtkPrecedence.Default and type term = LogtkFOTerm.t

module Prec: LogtkPrecedence.S  with type symbol = LogtkSymbol.t
type term 
type symbol = Prec.symbol 
type t 
Partial ordering on terms
type ordering = t 
val compare : t ->
term -> term -> LogtkComparison.t
Compare two terms using the given ordering
val precedence : t -> Prec.t
Current precedence
val set_precedence : t ->
Prec.t -> t
Change the precedence. The new one must be a superset of the old one.
Raises Invalid_argument if the new precedence is not compatible with the old one
val update_precedence : t ->
(Prec.t -> Prec.t) ->
Update the precedence with a function.
Raises Invalid_argument if the new precedence is not compatible with the previous one (see LogtkOrdering_intf.S.set_precedence).
val add_list : t ->
symbol list -> t
Update precedence with symbols
val add_seq : t ->
symbol Sequence.t -> t
Update precedence with signature
val name : t -> string
Name that describes this ordering
val clear_cache : t -> unit
val pp : Buffer.t -> t -> unit
val fmt : Format.formatter -> t -> unit
val to_string : t -> string

LogtkOrdering implementations

An ordering is a partial ordering on terms. Several implementations are simplification orderings (compatible with substitution, with the subterm property, and monotonic), some other are not.
val kbo : Prec.t -> t
Knuth-Bendix simplification ordering
val rpo6 : Prec.t -> t
Efficient implementation of RPO (recursive path ordering)
val none : t
All terms are incomparable (equality still works). Not a simplification ordering.
val subterm : t
Subterm ordering. Not a simplification ordering.

Global table of Orders

val default_of_list : symbol list -> t
default ordering on terms (RPO6) using default precedence
val default_of_prec : Prec.t -> t
val by_name : string -> Prec.t -> t
Choose ordering by name among registered ones, or
Raises Invalid_argument if no ordering with the given name are registered.
val register : string -> (Prec.t -> t) -> unit
Register a new ordering, which can depend on a precedence. The name must not be registered already.
Raises Invalid_argument if the name is already used.