package alt-ergo
Alt_ergo_common
See also the list of modules.
Main Solving
The solving loop is done in the Alt_ergo_common.Solving_loop module. This module uses the registered input method (parser and typechecker) to compute the input file (see Input Frontend). It relies on initialised options (see Command line parsing).
Command line parsing
The command line parsing is done with cmdliner in the module Alt_ergo_common.Parse_command. This module initialises options of the Alt-Ergo-Lib library.
Input Frontend
The Alt_ergo_common.Input_frontend module register an input method capable of parsing and typechecking the input files
The legacy frontend is used to parse and typecheck file with the native Alt-Ergo syntaxe and also the smtlib2 and psmt2 syntaxe.
Signals and profiling
The Alt_ergo_common.Signals_profiling module initialise handlers for system signals and profiling informations and timers.