package alt-ergo-lib

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

Install 

dune-project
 Dependency

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

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.2.tbz
sha256=39e2c9128a7d1e89f332e31a2716f359f3b9e1a925fe81f11fa4a749b5d24d82
sha512=ca953fe5a4964287de7e328ec4e3724a9baaa908c22862b075da5870bbf3707c7f78bd9fe0af98ee6c6382b5de0a4ddfcc93e09dc8b5b8e7d6ab6b1196a0656d

doc/index.html

The Alt-ergo library

Since version 2.2.0, the alt-ergo library is built and installed.

You can access the list of modules.

General organisation

The Alt-Ergo codebase is roughly divided into the following categories:

  • Utilities, augmenting the standard library with useful types and fonctions, and defining some pervasives structures, such as the global options of Alt-Ergo and a bit of configuration.
  • Structures, defining the main structures used throughout Alt-Ergo, defining the structures of parsed terms, typed terms, expressions and statements used as input for Alt-Ergo
  • The Frontend, defining the frontend-related functions in Alt-Ergo, including typechecking and transformation from typed terms to expressions.
  • The Backend where most of the proof search occurs

Structures

In this category are defined most of the structures used in Alt-Ergo.

First are the Abstract Syntax Trees used in Alt-Ergo. There exists three main different ASTs: the AltErgoLib.Parsed module defines the terms generated by the native parser of Alt-Ergo, the AltErgoLib.Typed module defines typechecked terms, which are an intermediary used by Alt-Ergo before translating them into hashconsed expressions as defined in AltErgoLib.Expr. The AltErgoLib.Ty module defines the structure used to represent types (which are common between typed terms and hashconsed expressions). Finally, the AltErgoLib.Commands module defines a notion of commands that can be sent to the SMT solver.

These modules make use of the following modules to abstract over variables and symbols:

Lastly, the following modules are used by the reasonners in the backend:

The Frontend

The frontend provides an easily usable user interface for the Alt-Ergo solver. It is split into three main parts.

The AltErgoLib.Frontend defines a frontend for the core solver, as a functor parametrized by a SAT solver implementation, and returning a solver that can process commands as defined by the AltErgoLib.Commands module.

The AltErgoLib.Input module defines a notion of input method. An input method is used to transform a string input (typically one or more files), into typed terms and statements. These typed terms can then be translated into commands using the AltErgoLib.Cnf module.

Finally, the native input method is defined in the AltErgoLib.Parsed_interface and AltErgoLib.Typechecker modules.

The Backend

TODO: Add some more explanations.

Utilities

Utilities module specific to Alt-Ergo:

Stdlib extensions/replacements/wrappers:

Module index

Unfortunately, odoc doesn't seem to correctly generate the index list the same way that ocamldoc does, :/ While the index of types and values is not generated yet, you can always browse the list of modules.

indexlist