package logtk

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

LogtkPrecedence (total ordering) on symbols

type symbol_status = LogtkPrecedence_intf.symbol_status =
  1. | Multiset
  2. | Lexicographic

LogtkSignature

module type S = LogtkPrecedence_intf.S

Functor

module type SYMBOL = sig ... end
module Make (Sym : SYMBOL) : S with type symbol = Sym.t
module Default : S with type symbol = LogtkSymbol.t
include module type of Default with type t = Default.t
type symbol = LogtkSymbol.t
type t = Default.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?

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) -> weight_fun
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 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
OCaml

Innovation. Community. Security.