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 LicenseRef-OCamlPro-Non-Commercial-Purpose-License-Version-1 License Edit opam file Versions (15)

Authors

A

Alt-Ergo developers

Maintainers

A

Alt-Ergo developers

Sources

2.4.1.tar.gz

md5=35d6c6f3fa43bcd10fe7f524b1eb59ca

sha512=c3eee41d3c588ca89c2a1eebe9f10914ef647743b58fb562b682172cf6b6bdeb0920ebbba8a850820c0cb53bad0260f11b82fe71f00830ea9b33f5bb5d4fd048

doc/alt-ergo-lib/AltErgoLib/Numbers/Q/index.html

Module `Numbers.Q`Source

Rationals implementation. *

include NumbersInterface.QSig with module Z = Z

Sourcemodule Z = Z

Sourcetype t

Sourceexception Not_a_float

Sourceval num : t -> Z.t

Sourceval den : t -> Z.t

Sourceval zero : t

Sourceval one : t

Sourceval m_one : t

Sourceval compare : t -> t -> int

Sourceval compare_to_0 : t -> int

Sourceval equal : t -> t -> bool

Sourceval sign : t -> int

Sourceval hash : t -> int

Sourceval is_zero : t -> bool

Sourceval is_one : t -> bool

Sourceval is_m_one : t -> bool

Sourceval is_int : t -> bool

Sourceval add : t -> t -> t

Sourceval sub : t -> t -> t

Sourceval mult : t -> t -> t

Sourceval div : t -> t -> t

Sourceval minus : t -> t

Sourceval abs : t -> t

Sourceval min : t -> t -> t

Sourceval max : t -> t -> t

Sourceval inv : t -> t

Sourceval modulo : t -> t -> t

Sourceval from_float : float -> t

Sourceval from_int : int -> t

Sourceval from_z : Z.t -> t

Sourceval from_zz : Z.t -> Z.t -> t

Sourceval from_string : string -> t

Sourceval to_float : t -> float

Sourceval to_z : t -> Z.t

Sourceval to_string : t -> string

Sourceval print : Format.formatter -> t -> unit

Sourceval power : t -> int -> t

Sourceval floor : t -> t

Sourceval ceiling : t -> t

Sourceval truncate : t -> Z.t

converts the argument to an integer by truncation. *

Sourceval mult_2exp : t -> int -> t

multiplies the first argument by 2^(the second argument)

Sourceval div_2exp : t -> int -> t

divides the first argument by 2^(the second argument)

Sourceval root_default : t -> int -> t option

Sourceval root_excess : t -> int -> t option

Sourceval sqrt_default : t -> t option

Sourceval sqrt_excess : t -> t option