module Weight : sig ... endmodule Constr : sig ... endTotal Ordering on a finite number of symbols, plus a few more data (weight for KBO, status for RPC)
type precedence = tval status : t -> ID.t -> symbol_statusStatus of the symbol
Nth argument coefficient of a symbol (for KBO with argument coefficients).
val add_list : signature:Signature.t -> t -> ID.t list -> unitUpdate the precedence with the given symbols
val declare_status : t -> ID.t -> symbol_status -> unitChange the status of the given precedence
Error if the symbol is not in the the precedence already
module Seq : sig ... endval pp_snapshot : ID.t list CCFormat.printerval pp_debugf : t CCFormat.printertype arg_coeff_fun = ID.t -> int listval weight_modarity : signature:Signature.t -> weight_funval weight_constant : weight_funval weight_invfreq : ID.t Iter.t -> weight_funval weight_freq : ID.t Iter.t -> weight_funval weight_invfreqrank : ID.t Iter.t -> weight_funval weight_freqrank : ID.t Iter.t -> weight_funval 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_funval set_weight : t -> weight_fun -> unitChange the weight function of the precedence
val create :
?weight:weight_fun ->
?arg_coeff:arg_coeff_fun ->
?db_w:int ->
?lmb_w:int ->
[ `total ] Constr.t ->
ID.t list ->
tmake 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.
default precedence. Default status for symbols is Lexicographic.