dolmen 0.7 · OCaml Package

Interfaces for Terms. This module defines Interfaces that implementation of terms must respect in order to be used to instantiated the corresponding language classes.

Signature for Parsing Logic languages

module type Logic = sig ... end

Signature used by the Logic class, which parses languages such as tptp, smtlib, etc... Mainly used to parse first-order terms, it is also used to parse tptp's THF language, which uses higher order terms, so some first-order constructs such as conjunction, equality, etc... also need to be represented by standalone terms.

Signature for Typechecked terms

module type Tff = sig ... end

Signature required by terms for typing first-order polymorphic terms.

module type Thf = sig ... end

module type Dimacs = sig ... end

Minimum required to type dimacs

module type Ae_Base = sig ... end

Minimum required to type ae's tff

module type Ae_Arith_Common = sig ... end

module type Ae_Arith = sig ... end

Minimum required to type ae's arith

module type Ae_Array = sig ... end

module type Ae_Bitv = sig ... end

Minimum required to type ae's bitvectors

module type Tptp_Tff_Core = sig ... end

Minimum required to type tptp's tff

module type Tptp_Thf_Core_Const = sig ... end

module type Tptp_Thf_Core = sig ... end

Minimum required to type tptp's thf

module type Tptp_Tff_Arith_Common = sig ... end

Common signature for tptp arithmetics

module type Tptp_Tff_Arith = sig ... end

Signature required by terms for typing tptp arithmetic.

module type Smtlib_Base = sig ... end

Minimum required to type smtlib's core theory.

module type Smtlib_Arith_Common = sig ... end

Common signature for first-order arithmetic

module type Smtlib_Int = sig ... end

Signature required by terms for typing smtlib int arithmetic.

module type Smtlib_Real = sig ... end

Signature required by terms for typing smtlib real arithmetic.

module type Smtlib_Real_Int = sig ... end

Signature required by terms for typing smtlib real_int arithmetic.

module type Smtlib_Array = sig ... end

module type Smtlib_Bitv = sig ... end

module type Smtlib_Float_Bitv = sig ... end

Bitvector part of the smtlib float requirements

module type Smtlib_Float_Real = sig ... end

Real part of the smtlib float requirements

module type Smtlib_Float_Float = sig ... end

Float part of the smtlib float requirements

module type Smtlib_Float = sig ... end

Floating points are complicated so this documentation is not in anyway sufficient. A detailed description of the theory together with the rationale of several models decisions as well as a formal semantics of the theory can be found in

module type Smtlib_String_RegLan = sig ... end

module type Smtlib_String_String = sig ... end

module type Smtlib_String = sig ... end

module type Zf_Base = sig ... end

module type Zf_Arith = sig ... end

package dolmen

Signature for Parsing Logic languages

Signature for Typechecked terms