Module `Logtk.Ordering`

Term Orderings

Type definitions

type term = Term.t
type t: Partial ordering on terms

type ordering = t

val compare : t -> term -> term -> Comparison.t: Compare two terms using the given ordering

val might_flip : t -> term -> term -> bool: Returns false for two terms t and s if for any ground substitution θ the ordering of tθ vs sθ cannot change when appending arguments. This function is allowed to overapproximate, i.e. we get no information if it returns true.

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 Iter.t -> unit: Update precedence with signature

val name : t -> string: Name that describes this ordering

val clear_cache : t -> unit
val normalize : (Lambda.term -> Lambda.term) Pervasives.ref

include Interfaces.PRINT with type t := t

type t

val pp : t CCFormat.printer
val to_string : t -> string

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.

val map : (term -> term) -> t -> t

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 names : unit -> string list

val default_name : string

val register : string -> (Precedence.t -> t) -> unit

raises Invalid_argument: if the name is already used.