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 DPLL-based SAT solver instances.
|
| solver [Cc_core] |
Type of Congruence closure-based 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 union-find 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.
|