Module `Logtk.Precedence`

Precedence (total ordering) on symbols

type symbol_status = | Multiset | Lexicographic | LengthLexicographic

module Weight : sig ... end

module Constr : sig ... end

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

type precedence = t

val equal : t -> t -> bool: Check whether the two precedences are equal (same snapshot)

val snapshot : t -> ID.t list: Current list of symbols, in increasing order

val compare : t -> ID.t -> ID.t -> int: Compare two symbols using the precedence

val mem : t -> ID.t -> bool: Is the ID.t part of the precedence?

val status : t -> ID.t -> symbol_status: Status of the symbol

val weight : t -> ID.t -> Weight.t: Weight of a symbol (for KBO).

val sel_prec_weight : t -> ID.t -> int
val db_weight : t -> Weight.t
val lam_weight : t -> Weight.t
val arg_coeff : t -> ID.t -> int -> int: Nth argument coefficient of a symbol (for KBO with argument coefficients).

val add_list : signature:Signature.t -> t -> ID.t list -> unit: Update the precedence with the given symbols

val 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

module Seq : sig ... end

val pp_snapshot : ID.t list CCFormat.printer
val pp_debugf : t CCFormat.printer

include Interfaces.PRINT with type t := t

type t

val pp : t CCFormat.printer
val to_string : t -> string

type weight_fun = ID.t -> Weight.t
type arg_coeff_fun = ID.t -> int list

val weight_modarity : signature:Signature.t -> weight_fun

val weight_constant : weight_fun

val weight_invfreq : ID.t Iter.t -> weight_fun

val weight_freq : ID.t Iter.t -> weight_fun

val weight_invfreqrank : ID.t Iter.t -> weight_fun

val weight_freqrank : ID.t Iter.t -> weight_fun

val weight_fun_of_string : signature:Signature.t -> lits:Term.t SLiteral.t Iter.t -> lm_w:int -> db_w:int -> string -> (ID.t * int) Iter.t -> weight_fun

val set_weight : t -> weight_fun -> unit

Change the weight function of the precedence

since: 0.5.3

Creation of a precedence from constraints

val create : ?⁠weight:weight_fun -> ?⁠arg_coeff:arg_coeff_fun -> ?⁠db_w:int -> ?⁠lmb_w:int -> [ `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.

val default : ID.t list -> t: default precedence. Default status for symbols is Lexicographic.

val default_seq : ID.t Iter.t -> t: default precedence on the given sequence of symbols

val constr : t -> [ `total ] Constr.t: Obtain the constraint