Module type LogtkPartialOrder_intf.S

module type S = sig .. end

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 ->
[ `eq of elt * elt
| `total
| `unordered 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.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)