A  
AltErgo [Trace] 
A certificate generator for the SMT solver AltErgo

Approx 
Approximations and candidates generation

Arith  
ArrayAtom [Types] 
Interface for the conjunctions of atoms seen as arrays of atoms.

Ast 
Abstract syntax tree and transition systems

Atom [Types] 
Interface for the atoms of the language

B  
BFS [Bwd]  
BFSA [Bwd]  
BFSH [Bwd]  
Bitv  
Brab 
Backward reachability with Approximations and Backtracking

Bwd 
Backward reachability with approximation

C  
CX [Combine]  
Cc 
the choice, the size, choice_sign, the explication set,
the explication for this choice.

Combine  
Cores [Fake_functory]  
Cube 
Cubes and simplifications

Cubetrie 
Trie structure for cubes sets

D  
DFS [Bwd]  
DFSA [Bwd]  
DFSH [Bwd]  
Debug [Enumsolver_types]  
Debug [Solver_types]  
Dot 
Generation of graphical search graphs with dot/graphviz

E  
Enumerative 
Enumerative forward search

Enumsolver  
Enumsolver_types  
Exception  
Explanation  
F  
Fake_functory 
Dummy replacement for Functory library

Fixpoint 
Fixpoint tests with optimizations

FixpointCertif [Fixpoint]  
FixpointList [Fixpoint] 
Fixpoint tests on list structures

FixpointTrie [Fixpoint] 
Fixpoint tests on trie structures

FixpointTrieNaive [Fixpoint]  
Fm  
Formula [Smt]  
Forward 
Symbolic forward exploration

H  
H [Hstring] 
Hashtables indexed by hashconsed strings

HMap [Hstring] 
Maps indexed by hashconsed strings

HSA [Forward]  
HSet [Hstring] 
Sets of hashconsed strings

Hashcons 
Hash tables for hash consing

Heap  
Hstring 
Hashconsed strings

I  
Iheap  
Instantiation 
Exhaustive Instantiation features

Intervals  
L  
L [Bitv]  
LT [Literal]  
Literal  
M  
M [Bitv]  
MA [Forward]  
MConst [Types]  
Main 
Entry point of Cubicle

Make [Use]  
Make [Uf]  
Make [Sum]  
Make [Enumsolver]  
Make [Solver]  
Make [Smt] 
Functor to create several instances of the solver

Make [Polynome]  
Make [Literal]  
Make [Fm]  
Make [Cc]  
Make [Arith]  
Make [Timer] 
Functor to create a new timer.

Make [Heap]  
Make [Hashcons]  
Make [Bwd] 
Functor for creating a strategy given a priority queue

Make [Approx] 
Functor for creating an approximation procedure from an oracle

Make_consed [Hashcons]  
Map [Term]  
Map [Symbols]  
Map [Literal.S]  
N  
Node 
Node of the search graph

O  
Options 
Options given on the command line

Oracle 
Interface for oracles

P  
Polynome  
Pre 
Preimage computation

Pretty 
Pretty printing functions

Prover 
Interface with the SMT solver

R  
R [Uf.S]  
Rel [Sig.X]  
Rel [Sig.COMBINATOR]  
Rel [Sig.THEORY]  
S  
S [Use]  
SA [Use]  
SAtom [Types] 
Interface for the conjunctions of atoms seen as sets of atoms.

SMT [Prover] 
Instance of the SMT solver

ST [Use]  
Safety 
Safety checks

Selected [Trace] 
The certificate generator selected by the command line options.

Selected [Bwd] 
Strategy selected by the options of the command line

Selected [Approx] 
The approximation module constructed with the oracle selected by the
command line options

SelectedOracle [Approx] 
The oracle selected by the command line options

Set [Term]  
Set [Symbols]  
Set [Literal.S]  
Set [Variable] 
set of variables

Set [Types.Term] 
set of terms

Sig 
case_split env returns a list of equalities

Smt 
The AltErgo zero SMT library

Solver  
Solver_types  
Stats 
Statistics

Sum  
Symbol [Smt] 
Function symbols

Symbols  
T  
T [Use]  
Term  
Term [Smt]  
Term [Types] 
Module interface for terms

TimeCheckCand [Util]  
TimeEasyFix [Util]  
TimeFix [Util]  
TimeFormula [Util]  
TimeForward [Util]  
TimeHardFix [Util]  
TimePre [Util]  
TimeRP [Util]  
TimeSimpl [Util]  
TimeSort [Util]  
Timer 
Imperative timers for profiling

TimerApply [Util]  
TimerCC [Cc.S]  
TimerSubset [Util]  
Trace 
Certificate traces for external verifiers

Ty  
Type [Smt] 
Typing

Type [Arith]  
Types 
Terms, atoms and conjunctions

Typing 
Typing of parameterized systems

U  
Uf  
Use  
Util 
Utilitaries

V  
Variable 
Variables of the parameterized domain

Variant [Smt] 
Variants

Vec  
Version  
W  
Why3 [Trace] 
A certificate generator for the deductive platform Why3.
