Module AltErgoLib.Symbols

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

Empties the labels Hashtable

module Set : Stdlib.Set.S with type elt = t
module Map : Stdlib.Map.S with type key = t