Module `Logtk.Compute_prec`

Compute Precedence

type t

val empty : t
val add_constr : int -> [ `partial ] Precedence.Constr.t -> t -> t: Add a precedence constraint with its priority. The lower the priority, the stronger influence the constraint will have.

val add_constrs : (int * [ `partial ] Precedence.Constr.t) list -> t -> t

type 'a parametrized = Statement.clause_t Sequence.t -> 'a: Some values are parametrized by the list of statements

val add_constr_rule : int -> [ `partial ] Precedence.Constr.t parametrized -> t -> t: Add a precedence constraint rule

val set_weight_rule : Precedence.weight_fun parametrized -> t -> t: Choose the way weights are computed

val add_status : (ID.t * Precedence.symbol_status) list -> t -> t: Specify explicitely the status of some symbols

val mk_precedence : t -> Statement.clause_t Sequence.t -> Precedence.t: Make a precedence