package alt-ergo

Alt_ergo_common

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.