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. | Tite
  2. | Plus
  3. | Minus
  4. | Mult
  5. | Div
  6. | Modulo
  7. | Pow
  8. | Reach
  9. | Access of Hstring.t
  10. | Record
  11. | Constr of Hstring.t
  12. | Destruct of Hstring.t * bool
  13. | Get
  14. | Set
  15. | Concat
  16. | Extract of int * int
  17. | BVnot
  18. | BVand
  19. | BVor
  20. | Int2BV of int
  21. | BV2Nat
  22. | Float
  23. | Integer_round
  24. | Fixed
  25. | Sqrt_real
  26. | Sqrt_real_default
  27. | Sqrt_real_excess
  28. | Abs_int
  29. | Abs_real
  30. | Real_of_int
  31. | Real_is_int
  32. | Int_floor
  33. | Int_ceil
  34. | Integer_log2
  35. | Max_real
  36. | Max_int
  37. | Min_real
  38. | Min_int
  39. | Not_theory_constant
  40. | Is_theory_constant
  41. | Linear_dependency
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 * bool
  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 -> ?defined:bool -> 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 reinit_fresh_sy_cpt : unit -> unit

Resets to 0 the fresh symbol counter

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
val clear_labels : unit -> unit

Empties the labels Hashtable

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