Alt-ergo-parsers

Since version 2.2.0, a specific package containing the code for the alt-ergo native language parser is installed separately. This package also contains an interface with the library psmt2-frontend and a way to dynamicaly load parsers into Alt-Ergo

Parsers loader

offer an interface to register a parser

Native input parser

The native input language of Alt-Ergo is defined by these two following modules :

SMT-LIB2 input parser

Offer an interface with the library psmt2-frontend and register a parser for smt2 and psmt2 extensions. This interface allows Alt-Ergo to partially support the SMT-LIB2 standard and a polymorphic extension.

Users can add new parsers to Alt-Ergo with the option --add-parser. This parser should have the same interface as AltErgoParsers.Parsers.PARSER_INTERFACE and should be registered using AltErgoParsers.Parsers.register_parser

Why3 parser plugin

See the ABWhy3 plugin.