package alt-ergo-lib

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module ZarithNumbers.ZSource

Integers implementation. Based on Zarith's integers *

Sourcetype 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 add : t -> t -> t
Sourceval sub : t -> t -> t
Sourceval mult : t -> t -> t
Sourceval div : t -> t -> t
Sourceval rem : t -> t -> t
Sourceval div_rem : t -> t -> t * t
Sourceval minus : t -> t
Sourceval abs : t -> t
Sourceval my_gcd : t -> t -> t
Sourceval my_lcm : t -> t -> t
Sourceval max : t -> t -> t
Sourceval from_int : int -> t
Sourceval from_string : string -> t
Sourceval to_string : t -> string
Sourceval to_machine_int : t -> int option

convert to machine integer. returns None in case of overflow

Sourceval to_float : t -> float
Sourceval fdiv : t -> t -> t
Sourceval cdiv : t -> t -> t
Sourceval power : t -> int -> t
Sourceval print : Format.formatter -> t -> unit
Sourceval shift_left : t -> int -> t

Shifts left by (n:int >= 0) bits. This is the same as t * pow(2,n)

Sourceval sqrt_rem : t -> t * t

returns sqrt truncated with the remainder. It assumes that the argument is positive, otherwise, Invalid_argument is raised.

Sourceval testbit : t -> int -> bool

testbit z n returns true iff the nth bit of z is set to 1. n is supposed to be positive

Sourceval numbits : t -> int

return the number of bits set to one in the given integer

OCaml

Innovation. Community. Security.