package alt-ergo-lib

  1. Overview
  2. Docs
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

  1. A
    Alt-Ergo developers

Maintainers

  1. A
    Alt-Ergo developers

Sources

2.4.1.tar.gz
md5=35d6c6f3fa43bcd10fe7f524b1eb59ca
sha512=c3eee41d3c588ca89c2a1eebe9f10914ef647743b58fb562b682172cf6b6bdeb0920ebbba8a850820c0cb53bad0260f11b82fe71f00830ea9b33f5bb5d4fd048

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

Module AltErgoLib.SymbolsSource

Sourcetype builtin =
  1. | LE
  2. | LT
  3. | IsConstr of Hstring.t
Sourcetype operator =
  1. | Plus
  2. | Minus
  3. | Mult
  4. | Div
  5. | Modulo
  6. | Concat
  7. | Extract
  8. | Get
  9. | Set
  10. | Fixed
  11. | Float
  12. | Reach
  13. | Access of Hstring.t
  14. | Record
  15. | Sqrt_real
  16. | Abs_int
  17. | Abs_real
  18. | Real_of_int
  19. | Int_floor
  20. | Int_ceil
  21. | Sqrt_real_default
  22. | Sqrt_real_excess
  23. | Min_real
  24. | Min_int
  25. | Max_real
  26. | Max_int
  27. | Integer_log2
  28. | Pow
  29. | Integer_round
  30. | Constr of Hstring.t
  31. | Destruct of Hstring.t * bool
  32. | Tite
Sourcetype lit =
  1. | L_eq
  2. | L_built of builtin
  3. | L_neg_eq
  4. | L_neg_built of builtin
  5. | L_neg_pred
Sourcetype form =
  1. | F_Unit of bool
  2. | F_Clause of bool
  3. | F_Iff
  4. | F_Xor
  5. | F_Lemma
  6. | F_Skolem
Sourcetype name_kind =
  1. | Ac
  2. | Other
Sourcetype bound_kind =
  1. | VarBnd of Var.t
  2. | ValBnd of Numbers.Q.t
Sourcetype bound = private {
  1. kind : bound_kind;
  2. sort : Ty.t;
  3. is_open : bool;
  4. is_lower : bool;
}
Sourcetype t =
  1. | True
  2. | False
  3. | Void
  4. | Name of Hstring.t * name_kind
  5. | Int of Hstring.t
  6. | Real of Hstring.t
  7. | Bitv of string
  8. | Op of operator
  9. | Lit of lit
  10. | Form of form
  11. | Var of Var.t
  12. | In of bound * bound
  13. | MapsTo of Var.t
  14. | Let
Sourceval name : ?kind:name_kind -> string -> t
Sourceval var : Var.t -> t
Sourceval underscore : t
Sourceval int : string -> t
Sourceval real : string -> t
Sourceval constr : string -> t
Sourceval destruct : guarded:bool -> string -> t
Sourceval mk_bound : bound_kind -> Ty.t -> is_open:bool -> is_lower:bool -> bound
Sourceval mk_in : bound -> bound -> t
Sourceval mk_maps_to : Var.t -> t
Sourceval is_ac : t -> bool
Sourceval equal : t -> t -> bool
Sourceval compare : t -> t -> int
Sourceval compare_bounds : bound -> bound -> int
Sourceval hash : t -> int
Sourceval to_string : t -> string
Sourceval print : Format.formatter -> t -> unit
Sourceval to_string_clean : t -> string
Sourceval print_clean : Format.formatter -> t -> unit
Sourceval fresh : ?is_var:bool -> string -> t
Sourceval is_get : t -> bool
Sourceval is_set : t -> bool
Sourceval fake_eq : t
Sourceval fake_neq : t
Sourceval fake_lt : t
Sourceval fake_le : t
Sourceval add_label : Hstring.t -> t -> unit
Sourceval label : t -> Hstring.t
Sourceval print_bound : Format.formatter -> bound -> unit
Sourceval string_of_bound : bound -> string
Sourcemodule Set : Set.S with type elt = t
Sourcemodule Map : sig ... end
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