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

• AltErgoParsers.Parsers_loader

Allow user to 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 ABWhy3

Utilities

• AltErgoParsers.MyZip A wrapper of the Zip module of CamlZip: we use Zip except when we want to generate the.js file for try-Alt-Ergo *