An ID.t is a unique identifier (an integer) with a human-readable name. We use those to give names to variables that are not hashconsed (the hashconsing does not play nice with names).
An identifier is primarily determined by its id (a unique number for this identifier), and contains a string name for readability. Sometimes we display identifiers as "name/id".
Identifiers are generative: you can easily create new ones or copy them.
Identifiers can carry some payload (values, of type exn because it's extensible). It is useful to remember easily some information about the identifier (e.g. special sugar notation, whether it's a skolem, etc.)
val make : string -> tMakes a fresh ID
val makef : ('a, Format.formatter, unit, t) format4 -> 'aval id : t -> intval name : t -> stringval payload : t -> exn listval dummy_of_int : int -> tval payload_find : f:(exn -> 'a option) -> t -> 'a optionval payload_pred : f:(exn -> bool) -> t -> boolval set_payload : ?can_erase:(exn -> bool) -> t -> exn -> unitSet given exception as payload.
if provided, checks whether an existing value is to be replaced instead of adding a new entry
include Interfaces.ORD with type t := tNOTE: default printer does not display the id field
val pp_full : t CCFormat.printerPrints the ID with its internal number
val pp_fullc : t CCFormat.printerPrints the ID with its internal number colored in gray (better for readability). Only use for debugging.
val pp_tstp : t CCFormat.printerval pp_zf : t CCFormat.printerval gensym : unit -> tGenerate a new ID with a new, unique name
module Tbl : CCHashtbl.S with type key = texception Attr_skolem of skolem_kindval as_infix : t -> string optionval is_infix : t -> boolval as_prefix : t -> string optionval is_prefix : t -> boolval as_parameter : t -> int optionval is_parameter : t -> boolval is_skolem : t -> boolis_skolem id returns true iff id is a Skolem symbol
val is_postcnf_skolem : t -> boolis_postcnf_skolem id returns true iff id is a Skolem symbol introduced during proof search
val as_skolem : t -> skolem_kind optionval is_distinct_object : t -> boolwhether the identifier is a distinct object (as defined in TPTP syntax)
val is_comm : t -> boolval is_assoc : t -> boolval is_ac : t -> bool