Module Logtk.Precedence

Precedence (total ordering) on symbols

type symbol_status =
  1. | Multiset
  2. | Lexicographic
  3. | 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
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 -> clauses:Term.t SLiteral.t Iter.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