Module Z3.Symbol

module Symbol: sig .. end

Symbols are used to name several term and type constructors

type symbol

val kind : symbol -> Z3enums.symbol_kind

The kind of the symbol (int or string)

val is_int_symbol : symbol -> bool

Indicates whether the symbol is of Int kind

val is_string_symbol : symbol -> bool

Indicates whether the symbol is of string kind.

val get_int : symbol -> int

The int value of the symbol.

val get_string : symbol -> string

The string value of the symbol.

val to_string : symbol -> string

A string representation of the symbol.

val mk_int : context -> int -> symbol

Creates a new symbol using an integer. Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1.

val mk_string : context -> string -> symbol

Creates a new symbol using a string.

val mk_ints : context -> int list -> symbol list

Create a list of symbols.

val mk_strings : context -> string list -> symbol list

Create a list of symbols.