package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type
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_real_int
  29. | Pow_real_real
  30. | Integer_round
  31. | Constr of Hstring.t
  32. | Destruct of Hstring.t * bool
  33. | 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 : Stdlib.Format.formatter -> t -> unit
val to_string_clean : t -> string
val print_clean : Stdlib.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 : Stdlib.Format.formatter -> bound -> unit
val string_of_bound : bound -> string
module Set : Stdlib.Set.S with type elt = t
module 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