A  
attribute [Smtlib_attribute] 
Attributes that may appear in benchmark, logic and theory files.

D  
db_index [Term] 
de Bruijn indices for bound variables

E  
elem [Union_find.S] 
Type of elements in the union find.

elt [Priority_queue] 
Elements in the queue are integers.

elt [Index.PriorityQueue] 
Type of elements.

elt [Index.Set] 
Type of elements.

elt [Bihashtbl.S] 
Elements in the range.

G  
generator [Id.Generator] 
A source of fresh identifiers.

K  
key [Term] 
Hash keys for terms

key [Index.Map] 
Type of indexed objects.

key [Bihashtbl.S] 
Keys in the domain.

key0 [Index.Map2] 
Type of indexed objects, which serve as the first map key.

key1 [Index.Map2] 
Type of the second map key.

L  
lemma [Cc_literal] 
The type of lemmas.

literal [Dl_core.T]  
literal [Cc_literal] 
The type of (dis)equality literals.

N  
num [Dl_core.T] 
The type of numbers.

number [Dl_core.L] 
The type of numbers.

R  
recognizer [Smtlib_parser] 
Generic parser.

S  
solver [Dpll_core] 
Type of DPLLbased SAT solver instances.

solver [Cc_core] 
Type of Congruence closurebased solver for Equality and
Uninterpreted Functions.

status [Smtlib_attribute] 
Expected status of a benchmark.

T  
t [Vec] 
Resizable vector of
'a elements.

t [Variable] 
Variables

t [Union_find.S] 
Type for the unionfind data structure.

t [Util.ComparedType] 
Abstract type of comparable values.

t [Symbol] 
Abstract type of symbols.

t [Priority_queue] 
The type of priority queues.

t [Index.IndexedType] 
The type of map keys.

t [Id.T] 
An abstract type of identifiers.

t [Index.PriorityQueue] 
Type of priority queues of elements.

t [Dl_number.T] 
The type of numbers.

t [Dl_core.L] 
The type of literals.

t [Dl_core.T] 
The type of the solver.

t [Constant] 
Constants

t [Index.Set] 
Type of set of elements.

t [Index.Map2] 
Maps indexed by a key from
key0 and a key from key1 .

t [Index.Map] 
Map from indices
0, ... ,n  1 (where n is the number of keys in
the map) to 'a .

t [Bunch] 
Collection of elements.

t [Bihashtbl.S] 
Partial bijective hash tables from
Bihashtbl.S.key to
Bihashtbl.S.elt .

term [Term] 
Terms

ternary [Ternary] 
Ternary values.

time [Time] 
Time point.

tokenizer [Smtlib_parser] 
Generic tokenizer.
