package alt-ergo-parsers

  1. Overview
  2. Docs
The Alt-Ergo SMT prover parser library

Install 

dune-project
 Dependency

alt-ergo.ocamlpro.com Readme Changelog LicenseRef-OCamlpro-Non-Commercial; Apache-2.0 License Edit opam file Versions (16)

Authors

  1. A
    Alt-Ergo developers <alt-ergo@ocamlpro.com>

Maintainers

  1. A
    Alt-Ergo developers <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.6.3.tbz
sha256=4ac2b5d8ae6c54a11a0cc349ec76a153aa95727bf57ef9cb3309a706a7fb1bfa
sha512=68b952ec7940c9f5d8ec9750420a6fd9ccaf6ca149ce96f5c32bbd8ff3b07481940b8c2938815b8540df1369e06da02f1edcbaeda809e8386be186011b7dd962

doc/index.html

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.