Module type LogtkPrecedence_intf.S

module type S = sig .. end

type symbol 
type t 
Total LogtkOrdering on a finite number of symbols, plus a few more data (weight for KBO, status for RPC)
type precedence = t 
val eq : t -> t -> bool
Check whether the two precedences are equal (same snapshot)
val snapshot : t -> symbol list
Current list of symbols, in decreasing order
val compare : t ->
symbol -> symbol -> int
Compare two symbols using the precedence
val mem : t -> symbol -> bool
Is the symbol part of the precedence?
val status : t ->
symbol -> LogtkPrecedence_intf.symbol_status
Status of the symbol
val weight : t -> symbol -> int
Weight of a symbol (for KBO). Strictly positive int.
val add_list : t ->
symbol list -> t
Update the precedence with the given symbols
val add_seq : t ->
symbol Sequence.t -> t
val declare_status : t ->
symbol ->
LogtkPrecedence_intf.symbol_status -> t
Change the status of the given precedence
module Seq: sig .. end
val pp_snapshot : Buffer.t -> symbol list -> unit
val pp_debug : Buffer.t -> t -> unit
val pp : Buffer.t -> t -> unit
val fmt : Format.formatter -> t -> unit
val to_string : t -> string

Builtin constraints

module Constr: sig .. end
type weight_fun = symbol -> int 
val weight_modarity : arity:(symbol -> int) ->
val weight_constant : weight_fun
val set_weight : t ->
weight_fun -> t
Change the weight function of the precedence
Since 0.5.3

Creation of a precedence from constraints

val create : ?weight:weight_fun ->
Constr.t list ->
symbol 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 create_sort : ?weight:weight_fun ->
(int * Constr.t) list ->
symbol list -> t
Sort the list of constraints by increasing priority, then call LogtkPrecedence_intf.S.create to build a precedence. The constraint with the smallest priority will be considered first.
Since 0.6.1
val default : symbol list -> t
default precedence. Default status for symbols is Lexicographic.
val default_seq : symbol Sequence.t -> t
default precedence on the given sequence of symbols
val constr_list : t -> Constr.t list
Obtain the list of constraints
Since 0.6.1
val with_constr_list : t ->
Constr.t list -> t
Update the precedence by replacing its list of constraints. Caution, this can be dangerous (change the precedence totally, for instance)
Since 0.6.1