module Precedence: sig .. end
Precedence (total ordering) on symbols
type
| |
Multiset |
| |
Lexicographic |
module Constr: sig .. end
Constraints
type
Total Ordering on a finite number of symbols, plus a few more
data (weight for KBO, status for RPC)
type 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 -> int
Weight of a symbol (for KBO). Strictly positive int.
val add_list : t -> ID.t list -> unit
Update the precedence with the given symbols
val add_seq : t -> ID.t Sequence.t -> unit
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
type ID.t -> int
val weight_modarity : arity:(ID.t -> int) -> weight_fun
val weight_constant : 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 ->
[ `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 Sequence.t -> t
default precedence on the given sequence of symbols
val constr : t -> [ `total ] Constr.t
Obtain the constraint