Index of modules


A
AltErgo [Trace]
A certificate generator for the SMT solver Alt-Ergo
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]
Hash-tables indexed by hash-consed strings
HMap [Hstring]
Maps indexed by hash-consed strings
HSA [Forward]
HSet [Hstring]
Sets of hash-consed strings
Hashcons
Hash tables for hash consing
Heap
Hstring
Hash-consed 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
Pre-image 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 Alt-Ergo 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.