Module Compute_prec

module Compute_prec: sig .. end

Compute Precedence

type t

val empty : t

val add_constr : int ->
       [ `partial ] Libzipperposition.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 ] Libzipperposition.Precedence.Constr.t) list ->
       t -> t

type 'a parametrized = Libzipperposition.Statement.clause_t Sequence.t -> 'a

Some values are parametrized by the list of statements

val add_constr_rule : int ->
       [ `partial ] Libzipperposition.Precedence.Constr.t parametrized ->
       t -> t

Add a precedence constraint rule

val set_weight_rule : (Libzipperposition.ID.t -> int) parametrized ->
       t -> t

Choose the way weights are computed

val add_status : (Libzipperposition.ID.t * Libzipperposition.Precedence.symbol_status) list ->
       t -> t

Specify explicitely the status of some symbols

val mk_precedence : t ->
       Libzipperposition.Statement.clause_t Sequence.t ->
       Libzipperposition.Precedence.t

Make a precedence