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; LGPL-2.1-only License Edit opam file Versions (15)

Authors

  1. A
    Alt-Ergo developers

Maintainers

  1. A
    Alt-Ergo developers

Sources

alt-ergo-2.4.3.tar.gz
md5=ba99f4c71bf6de3d2475272af2ee7df2
sha512=90c01175ec5e4c1818b1d370e300f30d6b433d34d3bae5d85394911a9bf145f1a66c41e997627d074206a8c57909c44c22dc86ed2df746f9ba1f1d7f21d7d60c

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

Module AltErgoLib.Symbols

type builtin =
  1. | LE
  2. | LT
  3. | IsConstr of Hstring.t
type 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
type lit =
  1. | L_eq
  2. | L_built of builtin
  3. | L_neg_eq
  4. | L_neg_built of builtin
  5. | L_neg_pred
type form =
  1. | F_Unit of bool
  2. | F_Clause of bool
  3. | F_Iff
  4. | F_Xor
  5. | F_Lemma
  6. | F_Skolem
type name_kind =
  1. | Ac
  2. | Other
type bound_kind =
  1. | VarBnd of Var.t
  2. | ValBnd of Numbers.Q.t
type bound = private {
  1. kind : bound_kind;
  2. sort : Ty.t;
  3. is_open : bool;
  4. is_lower : bool;
}
type 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
val name : ?kind:name_kind -> string -> t
val var : Var.t -> t
val underscore : t
val int : string -> t
val real : string -> t
val constr : string -> t
val destruct : guarded:bool -> string -> t
val mk_bound : bound_kind -> Ty.t -> is_open:bool -> is_lower:bool -> bound
val mk_in : bound -> bound -> t
val mk_maps_to : Var.t -> t
val is_ac : t -> bool
val equal : t -> t -> bool
val compare : t -> t -> int
val compare_bounds : bound -> bound -> int
val hash : t -> int
val to_string : t -> string
val print : Format.formatter -> t -> unit
val to_string_clean : t -> string
val print_clean : Format.formatter -> t -> unit
val fresh : ?is_var:bool -> string -> t
val is_get : t -> bool
val is_set : t -> bool
val fake_eq : t
val fake_neq : t
val fake_lt : t
val fake_le : t
val add_label : Hstring.t -> t -> unit
val label : t -> Hstring.t
val print_bound : Format.formatter -> bound -> unit
val string_of_bound : bound -> string
module Set : Set.S with type elt = t
module Map : sig ... end