Module `Logtk.Precedence`Source

Precedence (total ordering) on symbols

Sourcetype symbol_status =

| Multiset
| Lexicographic
| LengthLexicographic

Sourcemodule Weight : sig ... end

Sourcemodule Constr : sig ... end

Sourcetype t

Total Ordering on a finite number of symbols, plus a few more data (weight for KBO, status for RPC)

Sourcetype precedence = t

Sourceval equal : t -> t -> bool

Check whether the two precedences are equal (same snapshot)

Sourceval snapshot : t -> ID.t list

Current list of symbols, in increasing order

Sourceval compare : t -> ID.t -> ID.t -> int

Compare two symbols using the precedence

Sourceval mem : t -> ID.t -> bool

Is the ID.t part of the precedence?

Sourceval status : t -> ID.t -> symbol_status

Status of the symbol

Sourceval weight : t -> ID.t -> Weight.t

Weight of a symbol (for KBO).

Sourceval arg_coeff : t -> ID.t -> int -> int

Nth argument coefficient of a symbol (for KBO with argument coefficients).

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

Update the precedence with the given symbols

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

Sourceval declare_status : t -> ID.t -> symbol_status -> unit

Change the status of the given precedence

raises Error
if the symbol is not in the the precedence already

Sourcemodule Seq : sig ... end

Sourceval pp_snapshot : ID.t list CCFormat.printer

Sourceval pp_debugf : t CCFormat.printer

include Interfaces.PRINT with type t := t

Sourceval pp : t CCFormat.printer

Sourceval to_string : t -> string

Sourcetype weight_fun = ID.t -> Weight.t

Sourcetype arg_coeff_fun = ID.t -> int list

Sourceval weight_modarity : arity:(ID.t -> int) -> weight_fun

Sourceval weight_constant : weight_fun

Sourceval set_weight : t -> weight_fun -> unit

Change the weight function of the precedence

since 0.5.3

Creation of a precedence from constraints

Source

val create : 
  ?weight:weight_fun ->
  ?arg_coeff:arg_coeff_fun ->
  [ `total ] Constr.t ->
  ID.t list ->
  t

make a precedence from the given constraints. Constraints near the head of the list are more important than constraints close to the tail. Only the very first constraint is assured to be totally satisfied if constraints do not agree with one another.

Sourceval default : ID.t list -> t

default precedence. Default status for symbols is Lexicographic.

Sourceval default_seq : ID.t Iter.t -> t

default precedence on the given sequence of symbols

Sourceval constr : t -> [ `total ] Constr.t

Obtain the constraint

package logtk

Module Logtk.PrecedenceSource

Precedence (total ordering) on symbols

Creation of a precedence from constraints

Module `Logtk.Precedence`Source