Module AltErgoLib.Symbols

type builtin =
  1. | LE
  2. | LT
  3. | IsConstr of Uid.term_cst
  4. | BVULE
type operator =
  1. | Tite
  2. | Plus
  3. | Minus
  4. | Mult
  5. | Div
  6. | Modulo
  7. | Pow
  8. | Access of Uid.term_cst
  9. | Record
  10. | Constr of Uid.term_cst
  11. | Destruct of Uid.term_cst
  12. | Get
  13. | Set
  14. | Concat
  15. | Extract of int * int
  16. | Sign_extend of int
  17. | Repeat of int
  18. | BVnot
  19. | BVand
  20. | BVor
  21. | BVxor
  22. | BVadd
  23. | BVsub
  24. | BVmul
  25. | BVudiv
  26. | BVurem
  27. | BVshl
  28. | BVlshr
  29. | Int2BV of int
  30. | BV2Nat
  31. | Float
  32. | Integer_round
  33. | Sqrt_real
  34. | Sqrt_real_default
  35. | Sqrt_real_excess
  36. | Abs_int
  37. | Abs_real
  38. | Real_of_int
  39. | Real_is_int
  40. | Int_floor
  41. | Int_ceil
  42. | Integer_log2
  43. | Max_real
  44. | Max_int
  45. | Min_real
  46. | Min_int
  47. | Not_theory_constant
  48. | Is_theory_constant
  49. | 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 name_space =
  1. | User
    (*

    This symbol was defined by the user, and appears as is somewhere in a source file.

    As an exception, if the name we got from the user starts with either "." or "@" (which are prefixes reserved for solver use in the SMT-LIB standard), the name will be printed with an extra ".". So if the user writes ".x" or "@x", it will be printed as "..x" and ".@x" instead.

    Normally, this shouldn't occur, but we do this to ensure no confusion even if invalid names ever sneak through.

    *)
  2. | Internal
    (*

    This symbol is an internal implementation detail of the solver, such as a proxy formula or the abstracted counterpart of AC symbols.

    Internal names are printed with a ".!" prefix.

    *)
  3. | Fresh
    (*

    This symbol is a "fresh" internal name. Fresh internal names play a similar role as internal names, but they always represent a constant that was introduced during solving as part of some kind of purification or abstraction procedure.

    In order to correctly implement AC(X) in the presence of distributive symbols, symbols generated for AC(X) abstraction use a special namespace, Fresh_ac below.

    To ensure uniqueness, fresh names must always be generated using Id.Namespace.Internal.fresh ().

    In particular, fresh names are only used to denote constants, not arbitrary functions.

    *)
  4. | Fresh_ac
    (*

    This symbol has been introduced as part of the AC(X) abstraction process. This is notably used by some parts of AC(X) that check if terms contains fresh symbols (see contains_a_fresh_alien in the Arith module for an example).

    These correspond to the K sort in the AC(X) paper. They use a different name space from other fresh symbols because we need to be able to know whether a fresh symbol comes from the AC(X) abstraction procedure in order to prevent loops.

    To ensure uniqueness, AC abstraction names must always be generated using Id.Namespace.Internal.fresh ().

    *)
  5. | Skolem
    (*

    This symbol has been introduced as part of skolemization, and represents the (dependent) variable of an existential quantifier. Skolem names can have arbitrary arity to depend on previous skolem names in binding order (so if you have `(exists (x y) e)` then there will be a skolem variable `sko_x` and a skolem function `(sko_y sko_x)`).

    *)
  6. | Abstract
    (*

    This symbol has been introduced as part of model generation, and represents an abstract value.

    To ensure uniqueness, abstract names must always be generated using Id.Namespace.Abstract.fresh ().

    *)

The name_space type discriminates the different types of names. The same string in different name spaces is considered as different names.

Note that the names stored in the Name constructor below are mangled during creation of the symbol: a special prefix is added depending on the name space.

type bound_kind =
  1. | Unbounded
  2. | VarBnd of Var.t
  3. | 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. | Name of {
    1. hs : Id.t;
      (*

      Note: hs is prefixed according to ns.

      *)
    2. kind : name_kind;
    3. defined : bool;
    4. ns : name_space;
    }
  4. | Int of Z.t
  5. | Real of Q.t
  6. | Bitv of int * Z.t
  7. | Op of operator
  8. | Lit of lit
  9. | Form of form
  10. | Var of Var.t
  11. | In of bound * bound
  12. | MapsTo of Var.t
  13. | Let
val name : ?kind:name_kind -> ?defined:bool -> ?ns:name_space -> string -> t

Create a new symbol with the given name.

By default, names are created in the User name space.

Note that names are pre-mangled: the hs field of the resulting name may not be exactly the name that was passed to this function (however, calling `name` with the same string but two different name spaces is guaranteed to return two Names with distinct hs fields).

val var : Var.t -> t
val int : string -> t
val bitv : string -> t
val real : string -> t
val constr : Uid.term_cst -> t
val destruct : Uid.term_cst -> 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 is_internal : t -> bool

Check if the symbol is internal name that should never be printed on the regular output.

val equal : t -> t -> bool
val compare : t -> t -> int
val compare_bounds : bound -> bound -> int
val compare_operators : operator -> operator -> int
val hash : t -> int
val to_string : t -> string
val print : t Fmt.t
val to_string_clean : t -> string
val print_clean : t Fmt.t
val pp_name : (name_space * string) Fmt.t
val pp_ae_operator : operator Fmt.t
val pp_smtlib_operator : operator Fmt.t
val fresh_skolem_var : string -> Var.t
val fresh_skolem_name : string -> t

Resets to 0 the fresh symbol counter

val is_get : t -> bool
val is_set : t -> bool
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 : Stdlib.Map.S with type key = t