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_real_int
  29. | Pow_real_real
  30. | Integer_round
  31. | Constr of Hstring.t
  32. | Destruct of Hstring.t * bool
  33. | 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