package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

Term LogtkOrderings

LogtkType definitions

module type S = LogtkOrdering_intf.S

Functor

module Make (P : LogtkPrecedence.S with type symbol = LogtkSymbol.t) : S with module Prec = P and type term = LogtkFOTerm.t
module Default : S with module Prec = LogtkPrecedence.Default and type term = LogtkFOTerm.t
include module type of Default with module Prec = Default.Prec
module Prec = Default.Prec
type term = LogtkFOTerm.t
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) -> t

Update the precedence with a function.

  • raises Invalid_argument

    if the new precedence is not compatible with the previous one (see 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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct