package alt-ergo-lib

You can search for identifiers within the package.

in-package search v0.2.0

The Alt-Ergo SMT prover library

Install

Dune Dependency

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

Authors

A

Alt-Ergo developers

Maintainers

A

Alt-Ergo developers

Sources

alt-ergo-2.5.1.tbz

sha256=9cf8d69a0e457a939b86aba2a18c6154faba51d387b42a361ece55d329dd601d

sha512=09694d18496ba1938daaa7b4e28e6b3d6811687dd3aaede17917f20511be9d8328394fac021af683d4c0217d4b030da9a60a5b9c14d968f1948735ea7ec52543

doc/alt-ergo-lib/AltErgoLib/Input/index.html

Module `AltErgoLib.Input`

Typed input

This module defines an abstraction layer over the parsing and typechecking of input formulas. The goal is to be able to use different parsing and/or typechecking engines (e.g. the legacy typechecker, psmt2, or dolmen). To do so, an input method actually generates the typed representation of the input.

Input method

exception Method_not_registered of string

Exceptions raised when trying to lookup an input method that has not been registered.

module type S = sig ... end

This modules defines an input method. Input methods are responsible for two things: parsing and typechceking either an input file (possibly with some preludes files), or arbitrary terms. This last functionality is currently only used in the GUI.

val register : string -> (module S) -> unit

Register a new input method.

val find : string -> (module S)

Find an input method by name.

raises Method_not_registered
if the name is not registered.

On This Page

Input method