Module Logtk.PrecedenceSource

Precedence (total ordering) on symbols

Sourcetype symbol_status =
  1. | Multiset
  2. | Lexicographic
  3. | 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 sel_prec_weight : t -> ID.t -> int
Sourceval db_weight : t -> Weight.t
Sourceval lam_weight : t -> Weight.t
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 to_string : t -> string
Sourcetype weight_fun = ID.t -> Weight.t
Sourcetype arg_coeff_fun = ID.t -> int list
Sourceval weight_modarity : signature:Signature.t -> weight_fun
Sourceval weight_constant : weight_fun
Sourceval weight_invfreq : ID.t Iter.t -> weight_fun
Sourceval weight_freq : ID.t Iter.t -> weight_fun
Sourceval weight_invfreqrank : ID.t Iter.t -> weight_fun
Sourceval weight_freqrank : ID.t Iter.t -> weight_fun
Sourceval weight_fun_of_string : signature:Signature.t -> string -> (ID.t * int) Iter.t -> 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

Sourceval 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.

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