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 |