Module Logtk.OrderingSource

Term Orderings

Term orderings are well-founded orderings on terms, that (usually) have some nice properties for Superposition, such as being total on ground terms, stable by substitution, and stable by context (monotonic).

We provide several classic orderings, such as RPO and KBO.

Type definitions

Sourcetype term = Term.t
Sourcetype t

Partial ordering on terms

Sourcetype ordering = t
Sourceval compare : t -> term -> term -> Comparison.t

Compare two terms using the given ordering

Sourceval 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.

Sourceval monotonic : t -> bool

Is the ordering fully monotonic? Is it in particular compatible with arguments, i.e., t > s ==> t a > s a

Sourceval precedence : t -> Precedence.t

Current precedence

Sourceval add_list : t -> ID.t list -> unit

Update precedence with symbols

Sourceval add_seq : t -> ID.t Iter.t -> unit

Update precedence with signature

Sourceval name : t -> string

Name that describes this ordering

Sourceval clear_cache : t -> unit
include Interfaces.PRINT with type t := t
Sourceval 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.

Sourceval kbo : Precedence.t -> t

Knuth-Bendix simplification ordering (Blanchette's lambda-free higher-order version)

Sourceval lfhokbo_arg_coeff : Precedence.t -> t

Blanchette's lambda-free higher-order KPO with argument coefficients

Sourceval rpo6 : Precedence.t -> t

Efficient implementation of RPO (recursive path ordering) (Blanchette's lambda-free higher-order version)

Sourceval none : t

All terms are incomparable (equality still works). Not a simplification ordering.

Sourceval subterm : t

Subterm ordering. Not a simplification ordering.

Global table of Orders

Sourceval default_of_list : ID.t list -> t

default ordering on terms (RPO6) using default precedence

Sourceval default_of_prec : Precedence.t -> t
Sourceval by_name : string -> Precedence.t -> t

Choose ordering by name among registered ones, or

Sourceval names : unit -> string list
Sourceval default_name : string
Sourceval register : string -> (Precedence.t -> t) -> unit

Register a new ordering, which can depend on a precedence. The name must not be registered already.