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 term = Term.ttype ordering = tval compare : t -> term -> term -> Comparison.tCompare two terms using the given ordering
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 monotonic : t -> boolIs the ordering fully monotonic? Is it in particular compatible with arguments, i.e., t > s ==> t a > s a
val precedence : t -> Precedence.tCurrent precedence
val add_list : signature:Signature.t -> t -> ID.t list -> unitUpdate precedence with symbols
val name : t -> stringName that describes this ordering
val clear_cache : t -> unitAn 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 lambda_kbo : Precedence.t -> tKnuth-Bendix simplification ordering
val lambda_rpo : Precedence.t -> tEfficient implementation of RPO (recursive path ordering)
Takes a function that is going to be run before the chosen order and the order. If the first argument returns Comparison.Eq, then the order determined by second arg. Otherwise, the result of the first argument is returned.
val lambdafree_kbo : Precedence.t -> tTakes a function that is going to be run before the chosen order and the order. If the first argument returns Comparison.Eq, then the order determined by second arg. Otherwise, the result of the first argument is returned.
Knuth-Bendix simplification ordering - lambdafree version
val lambdafree_rpo : Precedence.t -> tEfficient implementation of RPO (recursive path ordering) - lambdafree version
val epo : Precedence.t -> tEmbedding path order
val none : tAll terms are incomparable (equality still works). Not a simplification ordering.
val subterm : tSubterm ordering. Not a simplification ordering.
val default_of_prec : Precedence.t -> tval by_name : string -> Precedence.t -> tChoose ordering by name among registered ones, or
Invalid_argument if no ordering with the given name are registered.
val register : string -> (Precedence.t -> t) -> unitRegister a new ordering, which can depend on a precedence. The name must not be registered already.
Invalid_argument if the name is already used.
val ty1comb_to_var : Term.t -> Term.t Term.Tbl.t -> Term.t