package alt-ergo-lib

  1. Overview
  2. Docs
The Alt-Ergo SMT prover library

Install 

dune-project
 Dependency

alt-ergo.ocamlpro.com Edit opam file Versions (15)

Authors

  1. A
    Alt-Ergo developers

Maintainers

  1. O
    OCamlPro <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.3.3.tar.gz
sha256=52e9e9cdbedf7afd1b32154dfb71ca7bead44fa2efcab7eb6d9ccc1989129388
md5=3b060044767d16d1de3416944abd2dd5

doc/alt-ergo-lib/AltErgoLib/NumbersInterface/module-type-ZSig/index.html

Module type NumbersInterface.ZSig

Interface of Integers *

type t
val zero : t
val one : t
val m_one : t
val compare : t -> t -> int
val compare_to_0 : t -> int
val equal : t -> t -> bool
val sign : t -> int
val hash : t -> int
val is_zero : t -> bool
val is_one : t -> bool
val is_m_one : t -> bool
val add : t -> t -> t
val sub : t -> t -> t
val mult : t -> t -> t
val div : t -> t -> t
val rem : t -> t -> t
val div_rem : t -> t -> t * t
val minus : t -> t
val abs : t -> t
val my_gcd : t -> t -> t
val my_lcm : t -> t -> t
val max : t -> t -> t
val from_int : int -> t
val from_string : string -> t
val to_string : t -> string
val to_machine_int : t -> int option

convert to machine integer. returns None in case of overflow

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

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

val sqrt_rem : t -> t * t

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

val 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

val numbits : t -> int

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