package dolmen

Integers (in base 10 notation), e.g. "123456789"

Rational (using quotient notation with '/'), e.g. "123/456"

Real (using decimal floating point notation with exponent), e.g. "123.456e789"

Bitvector in binary notation, e.g. "0b011010111010"

Bitvector in hexadecimal notation, e.g. "0x9a23e5f"

Bitvector litteral.

String litterals.

Namespace for variables. Not all variables are necessarily in this namespace, but ids in this namespace must be variables.

Namepsace for sorts and types (only used in smtlib)

Most used namespace, used for terms in general (and types outside smtlib).

Namespace for attributes (also called annotations).

Namespace used for naming declarations/definitions/statements...

Namespace used to track specific values throughout some files.

The identifier is a value, encoded in a string. Examples include arithmetic constants (e.g. "123456", "123/456", "123.456e789"), bitvectors (i.e. binary notation), etc...