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 (17)

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.4.tbz
sha256=c35b5b49ec2816a24c9325b083eefe237839ebaceb83331aeef041bed720b137
sha512=ed1486c0a86eb4cc66fc7b77f0d25f64949d7d134a456a78f6cdd19aa455b0808ba430cb6621fa89e89e09f5b48b1ad07fe4d5e29d0088d7804e09b4a2f712ac

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.