package alt-ergo-lib

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

Install 

dune-project
 Dependency

alt-ergo.ocamlpro.com Readme Changelog LicenseRef-OCamlpro-Non-Commercial; Apache-2.0 License Edit opam file Versions (16)

Authors

  1. A
    Alt-Ergo developers <alt-ergo@ocamlpro.com>

Maintainers

  1. A
    Alt-Ergo developers <alt-ergo@ocamlpro.com>

Sources

alt-ergo-2.6.3.tbz
sha256=4ac2b5d8ae6c54a11a0cc349ec76a153aa95727bf57ef9cb3309a706a7fb1bfa
sha512=68b952ec7940c9f5d8ec9750420a6fd9ccaf6ca149ce96f5c32bbd8ff3b07481940b8c2938815b8540df1369e06da02f1edcbaeda809e8386be186011b7dd962

doc/alt-ergo-lib/AltErgoLib/Inequalities/index.html

Module AltErgoLib.Inequalities

type 'a t = {
  1. ple0 : 'a;
  2. is_le : bool;
  3. dep : (Numbers.Q.t * 'a * bool) Util.MI.t;
  4. expl : Explanation.t;
  5. age : Numbers.Z.t;
}
module type S = sig ... end
module FM (P : Polynome.T with type r = Shostak.Combine.r) : S with type p = P.t
module type Container_SIG = sig ... end
val get_current : unit -> (module Container_SIG)

returns the current activated 'inequalities reasoner'. The default value is the Fourier-Motzkin module. When the selected reasoner is an external plugin, the first call of this function will attemp to dynamically load it *

val set_current : (module Container_SIG) -> unit

sets a new 'inequalities reasoner'. This function is intended to be used by dynamically loaded plugins *