Module Logtk__ID

Unique Identifiers

type t = private {
id : int;
name : string;
mutable payload : exn list;

Use exn as an open type for user-defined payload

}
val make : string -> t

Makes a fresh ID

val makef : ('a, Stdlib.Format.formatter, unit, t) Stdlib.format4 -> 'a
val copy : t -> t

Copy with a new ID

val id : t -> int
val name : t -> string
val payload : t -> exn list
val dummy_of_int : int -> t
val payload_find : f:(exn -> 'a option) -> t -> 'a option
val payload_pred : f:(exn -> bool) -> t -> bool
val set_payload : ?⁠can_erase:(exn -> bool) -> t -> exn -> unit

Set given exception as payload.

parameter can_erase

if provided, checks whether an existing value is to be replaced instead of adding a new entry

include Logtk.Interfaces.HASH with type t := t
include Logtk.Interfaces.EQ
type t
val equal : t -> t -> bool
val hash : t -> int
include Logtk.Interfaces.ORD with type t := t
type t
val compare : t -> t -> int
include Logtk.Interfaces.PRINT with type t := t
type t
val pp : t CCFormat.printer
val to_string : t -> string
val pp_full : t CCFormat.printer

Prints the ID with its internal number

val pp_fullc : t CCFormat.printer

Prints the ID with its internal number colored in gray (better for readability). Only use for debugging.

val pp_tstp : t CCFormat.printer
val pp_zf : t CCFormat.printer
val gensym : unit -> t

Generate a new ID with a new, unique name

module Map : CCMap.S with type Map.key = t
module Set : CCSet.S with type Set.elt = t
module Tbl : CCHashtbl.S with type Tbl.key = t
exception Attr_infix of string

Infix name for pretty-printing

exception Attr_prefix of string

Prefix name for pretty-printing

exception Attr_parameter of int

Parameter, used for HO unif

type skolem_kind =
| K_normal
| K_after_cnf
| K_ind
exception Attr_skolem of skolem_kind
exception Attr_distinct
exception Attr_comm
exception Attr_assoc
val as_infix : t -> string option
val is_infix : t -> bool
val as_prefix : t -> string option
val is_prefix : t -> bool
val as_parameter : t -> int option
val is_parameter : t -> bool
val is_skolem : t -> bool

is_skolem id returns true iff id is a Skolem symbol

val is_postcnf_skolem : t -> bool

is_postcnf_skolem id returns true iff id is a Skolem symbol introduced during proof search

val as_skolem : t -> skolem_kind option
val is_distinct_object : t -> bool

whether the identifier is a distinct object (as defined in TPTP syntax)

val is_comm : t -> bool
val is_assoc : t -> bool
val is_ac : t -> bool