A | |
AltErgo [Trace] | A certificate generator for the SMT solver Alt-Ergo |
Alt_ergo | The Alt-Ergo zero SMT library |
Approx | |
Arith | |
ArrayAtom [Types] | Interface for the conjunctions of atoms seen as arrays of atoms. |
Ast | |
Atom [Types] | Interface for the atoms of the language |
B | |
BFS [Bwd] | |
BFSA [Bwd] | |
BFSH [Bwd] | |
Brab | Backward reachability with Approximations and Backtracking |
Bwd | |
C | |
CX [Combine] | |
Cc | |
Combine | |
Cores [Fake_functory] | |
Cube | |
Cubetrie | |
D | |
DFS [Bwd] | |
DFSA [Bwd] | |
DFSH [Bwd] | |
Debug [Enumsolver_types] | |
Debug [Solver_types] | |
Dot | |
E | |
Enumerative | |
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_sig.S] | |
Forward | |
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 | |
LT [Literal] | |
Literal | |
M | |
MA [Forward] | |
MConst [Types] | |
Main | |
Make [Timer] | Functor to create a new timer. |
Make [Heap] | |
Make [Hashcons] | |
Make [Use] | |
Make [Uf] | |
Make [Sum] | |
Make [Enumsolver] | |
Make [Solver] | |
Make [Smt_sig.S] | Functor to create several instances of the solver |
Make [Polynome] | |
Make [Literal] | |
Make [Fm] | |
Make [Cc] | |
Make [Arith] | |
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] | |
Muparser_globals | State being currently constructed |
Murphi | Oracle for BRAB that calls the explicit state model checker Murphi. |
N | |
Node | |
O | |
Options | Options given on the command line |
Oracle | |
P | |
Polynome | |
Pre | |
Pretty | |
Prover | |
Ptree | |
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 | |
Smt | A module corresponding to the SMT solver selected by the command line options |
Smt_sig | A signature for itegrating SMT solvers in Cubicle |
Solver | |
Solver_types | |
Stats | Statistics |
Sum | |
Symbol [Smt_sig.S] | Function symbols |
Symbols | |
T | |
T [Use] | |
Term | |
Term [Smt_sig.S] | |
Term [Types] | Module interface for terms |
TimeCertificate [Util] | |
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 | |
Ty | |
Type [Smt_sig.S] | Typing |
Type [Arith] | |
Types | Terms, atoms and conjunctions |
Typing | |
U | |
Uf | |
Use | |
Util | Utilitaries |
V | |
VMap [Types] | |
Var [Types] | |
Variable | |
Variant [Smt_sig.S] | Variants |
Vec | |
Version | |
W | |
Why3 [Trace] | A certificate generator for the deductive platform Why3. |
Z | |
Z3wrapper | A solver using the Z3 OCaml API |