General organisation

The Alt-Ergo codebase is roughly divided into the following categories:

• Utilities, augmenting the standard library with useful types and fonctions, and defining some pervasives structures, such as the global options of Alt-Ergo and a bit of configuration.
• Structures, defining the main structures used throughout Alt-Ergo, defining the structures of parsed terms, typed terms, expressions and statements used as input for Alt-Ergo
• The Frontend, defining the frontend-related functions in Alt-Ergo, including typechecking and transformation from typed terms to expressions.
• The Backend where most of the proof search occurs

Structures

In this category are defined most of the structures used in Alt-Ergo.

First are the Abstract Syntax Trees used in Alt-Ergo. There exists three main different ASTs: the AltErgoLib.Parsed module defines the terms generated by the native parser of Alt-Ergo, the AltErgoLib.Typed module defines typechecked terms, which are an intermediary used by Alt-Ergo before translating them into hashconsed expressions as defined in AltErgoLib.Expr. The AltErgoLib.Ty module defines the structure used to represent types (which are common between typed terms and hashconsed expressions). Finally, the AltErgoLib.Commands module defines a notion of commands that can be sent to the SMT solver.

• AltErgoLib.Parsed
• AltErgoLib.Ty Types
• AltErgoLib.Typed Typed AST
• AltErgoLib.Expr Data structures
• AltErgoLib.Commands

These modules make use of the following modules to abstract over variables and symbols:

• AltErgoLib.Var
• AltErgoLib.Symbols

Lastly, the following modules are used by the reasonners in the backend:

• AltErgoLib.Explanation
• AltErgoLib.Satml_types
• AltErgoLib.Fpa_rounding
• AltErgoLib.Xliteral
• AltErgoLib.Profiling

The Frontend

The frontend provides an easily usable user interface for the Alt-Ergo solver. It is split into three main parts.

The AltErgoLib.Frontend defines a frontend for the core solver, as a functor parametrized by a SAT solver implementation, and returning a solver that can process commands as defined by the AltErgoLib.Commands module.

The AltErgoLib.Input module defines a notion of input method. An input method is used to transform a string input (typically one or more files), into typed terms and statements. These typed terms can then be translated into commands using the AltErgoLib.Cnf module.

Finally, the native input method is defined in the AltErgoLib.Parsed_interface and AltErgoLib.Typechecker modules.

• AltErgoLib.Cnf
• AltErgoLib.Frontend
• AltErgoLib.Input Typed input
• AltErgoLib.Parsed_interface Declaration of types *
• AltErgoLib.Typechecker

The Backend

TODO: Add some more explanations.

• AltErgoLib.Arrays_rel
• AltErgoLib.Theory
• AltErgoLib.Ccx
• AltErgoLib.Relation
• AltErgoLib.Intervals
• AltErgoLib.Inequalities
• AltErgoLib.IntervalCalculus
• AltErgoLib.Records_rel
• AltErgoLib.Ite_rel
• AltErgoLib.Sig_rel
• AltErgoLib.Enum_rel
• AltErgoLib.Bitv_rel
• AltErgoLib.Uf
• AltErgoLib.Use
• AltErgoLib.Matching
• AltErgoLib.Instances
• AltErgoLib.Sat_solver_sig
• AltErgoLib.Fun_sat
• AltErgoLib.Satml
• AltErgoLib.Satml_frontend
• AltErgoLib.Satml_frontend_hybrid
• AltErgoLib.Sat_solver
• AltErgoLib.Matching_types
• AltErgoLib.Shostak
• AltErgoLib.Ac
• AltErgoLib.Arith
• AltErgoLib.Arrays
• AltErgoLib.Bitv
• AltErgoLib.Enum
• AltErgoLib.Ite
• AltErgoLib.Polynome
• AltErgoLib.Records
• AltErgoLib.Sig
• AltErgoLib.Th_util

Utilities

Utilities module specific to Alt-Ergo:

• AltErgoLib.Config
• AltErgoLib.Errors
• AltErgoLib.Steps Module_Name
• AltErgoLib.Options
• AltErgoLib.Version
• AltErgoLib.Printer

Stdlib extensions/replacements/wrappers:

• AltErgoLib.Util
• AltErgoLib.Heap Heaps.
• AltErgoLib.Emap
• AltErgoLib.Hstring
• AltErgoLib.Compat
• AltErgoLib.Gc_debug
• AltErgoLib.Timers
• AltErgoLib.Hconsing Generic Hashconsing.
• AltErgoLib.Vec
• AltErgoLib.Loc Position in input files
• AltErgoLib.My_unix Unix wrapper
• AltErgoLib.My_list Lists utilies This modules defines some helper functions on lists
• AltErgoLib.Numbers

Module index

Unfortunately, odoc doesn't seem to correctly generate the index list the same way that ocamldoc does, :/ While the index of types and values is not generated yet, you can always browse the list of modules.

indexlist