package alt-ergo-parsers

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

• AltErgoParsers.Parsers

offer an interface to register a parser

Native input parser

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

• AltErgoParsers.Native_parser
• AltErgoParsers.Native_lexer

SMT-LIB2 input parser

• AltErgoParsers.Psmt2_to_alt_ergo

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.

Dynamicly link parser

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.