package alt-ergo-lib

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

Install

Dune 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/Intervals/index.html

Module AltErgoLib.IntervalsSource

Sourcetype t
Sourceexception NotConsistent of Explanation.t
Sourceexception No_finite_bound
Sourceval undefined : Ty.t -> t
Sourceval is_undefined : t -> bool
Sourceval point : Numbers.Q.t -> Ty.t -> Explanation.t -> t
Sourceval doesnt_contain_0 : t -> Th_util.answer
Sourceval is_positive : t -> Th_util.answer
Sourceval is_strict_smaller : t -> t -> bool
Sourceval new_borne_sup : Explanation.t -> Numbers.Q.t -> is_le:bool -> t -> t
Sourceval new_borne_inf : Explanation.t -> Numbers.Q.t -> is_le:bool -> t -> t
Sourceval is_point : t -> (Numbers.Q.t * Explanation.t) option
Sourceval intersect : t -> t -> t
Sourceval exclude : t -> t -> t
Sourceval mult : t -> t -> t
Sourceval power : int -> t -> t
Sourceval sqrt : t -> t
Sourceval root : int -> t -> t
Sourceval add : t -> t -> t
Sourceval scale : Numbers.Q.t -> t -> t
Sourceval affine_scale : const:Numbers.Q.t -> coef:Numbers.Q.t -> t -> t

Perform an affine transformation on the given bounds. Suposing input bounds (b1, b2), this will return (const + coef * b1, const + coef * b2). This function is useful to avoid the incorrect roundings that can take place when scaling down an integer range.

Sourceval sub : t -> t -> t
Sourceval merge : t -> t -> t
Sourceval abs : t -> t
Sourceval pretty_print : Format.formatter -> t -> unit
Sourceval print : Format.formatter -> t -> unit
Sourceval finite_size : t -> Numbers.Q.t option
Sourceval borne_inf : t -> Numbers.Q.t * Explanation.t * bool

bool is true when bound is large. Raise: No_finite_bound if no finite lower bound

Sourceval borne_sup : t -> Numbers.Q.t * Explanation.t * bool

bool is true when bound is large. Raise: No_finite_bound if no finite upper bound

Sourceval div : t -> t -> t
Sourceval mk_closed : Numbers.Q.t -> Numbers.Q.t -> bool -> bool -> Explanation.t -> Explanation.t -> Ty.t -> t

takes as argument in this order:

  • a lower bound
  • an upper bound
  • a bool that says if the lower bound it is large (true) or strict
  • a bool that says if the upper bound it is large (true) or strict
  • an explanation of the lower bound
  • an explanation of the upper bound
  • a type Ty.t (Tint or Treal
Sourceval bounds_of : t -> (bnd * bnd) list
Sourceval contains : t -> Numbers.Q.t -> bool
Sourceval add_explanation : t -> Explanation.t -> t
Sourceval equal : t -> t -> bool
Sourcetype interval_matching = ((Numbers.Q.t * bool) option * (Numbers.Q.t * bool) option * Ty.t) Var.Map.t

matchs the given lower and upper bounds against the given interval, and update the given accumulator with the constraints. Returns None if the matching problem is inconsistent

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct