package dolmen

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

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

BTRW15 Martin Brain, Cesare Tinelli, Philipp Ruemmer, and Thomas Wahl. An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic Technical Report, 2015. (http://smt-lib.org/papers/BTRW15.pdf)

type t

The type of terms

type ty

The type of types.

val ty : t -> ty

Type of a term.

module Real : Smtlib_Float_Real with type t := t

Sub-module used for namespacing the real part of the theory requirements

module Bitv : Smtlib_Float_Bitv with type t := t

Sub-module used for namespacing the bitvector part of the theory requirements

module Float : Smtlib_Float_Float with type t := t

Sub-module used for namespacing the floating number part of the theory requirements