package logtk

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

Elements that can be compared

type t

the partial order on elements of type elt

val create : elt list -> t

build an empty partial order for the list of elements

val copy : t -> t

Copy of the partial order

val size : t -> int

Number of elements

val extend : t -> elt list -> t

Add new elements to the ordering, creating a new ordering. They will not be ordered at all w.r.t previous elements.

val is_total : t -> bool

Is the ordering total (i.e. each pair of elements it contains is ordered)?

val is_total_details : t -> [ `total | `unordered of elt * elt | `eq of elt * elt ]

More details than is_total, which returns true iff this function returns `total.

  • since 0.6.1
val enrich : t -> (elt -> elt -> LogtkComparison.t) -> unit

Compare unordered pairs with the given partial order function. If the function returns LogtkComparison.t.Eq on two elements x and y, then the ordering cannot be total anymore.

val complete : t -> (elt -> elt -> int) -> unit

complete po f completes po using the function f elements to compare still unordered pairs. If f x y returns 0 then x and y are still incomparable in po afterwards. If the given comparison function is not total, the ordering may still not be complete. The comparison function f is assumed to be such that transitive_closure f is a partial order.

val compare : t -> elt -> elt -> LogtkComparison.t

compare two elements in the ordering.

val pairs : t -> (elt * elt) list

list of pairs (a > b)

val elements : t -> elt list

Elements of the partial order. If the ordering is total, they will be sorted by decreasing order (maximum first)