Module AltErgoLib.Symbols

type builtin =
| LE
| LT
| IsConstr of Hstring.t
type operator =
| Plus
| Minus
| Mult
| Div
| Modulo
| Concat
| Extract
| Get
| Set
| Fixed
| Float
| Reach
| Access of Hstring.t
| Record
| Sqrt_real
| Abs_int
| Abs_real
| Real_of_int
| Int_floor
| Int_ceil
| Sqrt_real_default
| Sqrt_real_excess
| Min_real
| Min_int
| Max_real
| Max_int
| Integer_log2
| Pow_real_int
| Pow_real_real
| Integer_round
| Constr of Hstring.t
| Destruct of Hstring.t * bool
| Tite
type lit =
| L_eq
| L_built of builtin
| L_neg_eq
| L_neg_built of builtin
| L_neg_pred
type form =
| F_Unit of bool
| F_Clause of bool
| F_Iff
| F_Xor
| F_Lemma
| F_Skolem
type name_kind =
| Ac
| Other
type bound_kind =
| VarBnd of Var.t
| ValBnd of Numbers.Q.t
type bound = private {
kind : bound_kind;
sort : Ty.t;
is_open : bool;
is_lower : bool;
}
type t =
| True
| False
| Void
| Name of Hstring.t * name_kind
| Int of Hstring.t
| Real of Hstring.t
| Bitv of string
| Op of operator
| Lit of lit
| Form of form
| Var of Var.t
| In of bound * bound
| MapsTo of Var.t
| 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