Module Dolmen_intf.Term

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 Response terms

module type Response = Logic

Simply an alias to the Logic signature.

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_Bvconv = 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