module Ordering: sig .. end
Term Orderings
Type definitions
type FOTerm.t
type
Partial ordering on terms
type t
val compare : t -> term -> term -> Comparison.t
Compare two terms using the given ordering
val precedence : t -> Precedence.t
Current precedence
val add_list : t -> ID.t list -> unit
Update precedence with symbols
val add_seq : t -> ID.t Sequence.t -> unit
Update precedence with signature
val name : t -> string
Name that describes this ordering
val clear_cache : t -> unit
include Interfaces.PRINT
Ordering 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 : Precedence.t -> t
Knuth-Bendix simplification ordering
val rpo6 : Precedence.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 : ID.t list -> t
default ordering on terms (RPO6) using default precedence
val default_of_prec : Precedence.t -> t
val by_name : string -> Precedence.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 -> (Precedence.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.