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 <alt-ergo@ocamlpro.com>

Maintainers

A

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

Sources

alt-ergo-2.6.1.tbz

sha256=df56045a3af79fbcfbd1deeaf09012d5bc390b4c2223e1d9c25c11c301d9eeba

sha512=ff83e5ce7598bc30509be8ca2c14d791856b0269f852903f81216ae1cbc27737d90b6313176fa24768944433b875811ee19b51fc821948634ea678dbcca4befb

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