Module AltErgoLib.Symbols

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 : 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 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 : Format.formatter -> bound -> unit
val string_of_bound : bound -> string
val clear_labels : unit -> unit

Empties the labels Hashtable

module Set : Set.S with type elt = t
module Map : sig ... end