Module Type

Types of terms

A type has to be hash-consed to be used in hash-consed terms.

Types and hash-consing

type kindtype =
  1. | Bool
  2. | Int
  3. | IntRange of Numeral.t option * Numeral.t option
  4. | Enum of Numeral.t * Numeral.t
  5. | Real
  6. | UBV of int
  7. | BV of int
  8. | Array of t * t
  9. | Abstr of string
  10. | Datatype of string * (string * t list) list
  11. | DatatypeRef of string

Type of an expression

and t

Hashconsed type

val node_of_type : t -> kindtype

Return the value kindtype in a hashconsed type

val get_bv_size : t -> int option

Hashtables, maps and sets

val compare_types : t -> t -> int

Comparison function on types

val equal_types : t -> t -> bool

Equality function on types

val hash_type : t -> int

Hashing function on types

module TypeHashtbl : Stdlib.Hashtbl.S with type key = t

Hash table over types

module TypeSet : Stdlib.Set.S with type elt = t

Set over types

module TypeMap : Stdlib.Map.S with type key = t

Map over types

Constructor

val mk_type : kindtype -> t

Hashcons a type

val mk_bool : unit -> t

Return the boolean type

val mk_int : unit -> t

Return the integer type

val mk_int_range : Numeral.t option -> Numeral.t option -> t

Return the integer range type

val mk_real : unit -> t

Return the real decimal type

val mk_ubv : int -> t

Return the unsigned bitvector type

val mk_bv : int -> t

Return the bitvector type

val mk_array : t -> t -> t

Return an array type of index sort and element sort

val mk_abstr : string -> t

Return an abstract type

val mk_enum : string -> string list -> t

Return an enumerated datatype type

val mk_datatype : string -> (string * t list) list -> t

Return a recursive algebraic datatype. Self-referential field types should be represented with mk_datatype_ref name.

val mk_datatype_ref : string -> t

Return a placeholder for a direct self-reference to the named datatype, for use as a field type within that datatype's own constructor list.

val import : t -> t

Import a type from a different instance into this hashcons table

val t_bool : t

The boolean type

val t_int : t

The integer type

val t_real : t

The real decimal type

val t_ubv : int -> t

The unsigned bitvector type

val t_bv : int -> t

The bitvector type

Type checking

val check_type : t -> t -> bool

check_type s t returns true if s is a subtype of t

Predicates

val is_bool : t -> bool

Return true if the type is the Boolean type

val is_int : t -> bool

Return true if the type is the integer type

val is_ubitvector : t -> bool

Return true if the type is an unsigned bitvector (integern) type

val is_ubitvector_len : int -> t -> bool

Return true if the type is an unsigned bitvector (integern) type of the given width

val is_bitvector : t -> bool

Return true if the type is a bitvector (integern) type

val is_bitvector_len : int -> t -> bool

Return true if the type is a bitvector (integern) type of the given width

val bitvectorsize : t -> int

Return true if the type is a bitvector (integern) type

val is_uint8 : t -> bool

Return true if the type is the unsigned integer8 type

val is_uint16 : t -> bool

Return true if the type is the unsigned integer16 type

val is_uint32 : t -> bool

Return true if the type is the unsigned integer32 type

val is_uint64 : t -> bool

Return true if the type is the unsigned integer64 type

val is_int8 : t -> bool

Return true if the type is the integer8 type

val is_int16 : t -> bool

Return true if the type is the integer16 type

val is_int32 : t -> bool

Return true if the type is the integer32 type

val is_int64 : t -> bool

Return true if the type is the integer64 type

val is_int_range : t -> bool

Return true if the type is an integer range type

val is_enum : t -> bool

Return true if the type is an integer range type

val is_real : t -> bool

Return true if the type is the real type

val is_array : t -> bool

Return true if the type is an array type

val is_abstr : t -> bool

Return true if the type is abstract

val is_datatype : t -> bool

Return true if the type is a recursive algebraic datatype (not a self-reference placeholder -- see is_datatype_ref)

val constructors_of_datatype : t -> (string * t list) list

Return the constructors of a datatype, fail if not a datatype

val name_of_datatype : t -> string

Return the name of a datatype, fail if not a datatype

val is_datatype_ref : t -> bool

Return true if the type is a self-reference placeholder (see mk_datatype_ref)

val name_of_datatype_ref : t -> string

Return the name of a self-reference placeholder, fail if not one

Ranges

val bounds_of_int_range : t -> Numeral.t option * Numeral.t option

Return bounds of an integer range type, fail with Invalid_argument "bounds_of_int_range" if the type is not an integer range type.

val bounds_of_enum : t -> Numeral.t * Numeral.t

Return bounds of an enum type, fail with Invalid_argument "bounds_of_enum" if the type is not an integer range type.

val generalize : t -> t

Generalize a type (remove actual intranges)

Arrays

val index_type_of_array : t -> t

Return type of array index

val all_index_types_of_array : t -> t list

Return all array index types of a nested array type

val elem_type_of_array : t -> t

Return type of array elements

val idx_type_of_array : t -> t

Return type of array indices

val last_elem_type_of_array : t -> t

Return all array index types of a nested array type

Enumerated datatypes

val constructors_of_enum : t -> string list

Return constructors of an enumerated datatype

val name_of_enum : t -> string

Return the name of an enumerated datatype encoded as int ranges

val get_constr_of_num : Numeral.t -> string

Return the constructor encoded by the numeral argument

val get_all_abstr_types : unit -> t list

Return abstract types that have been built

val get_num_of_constr : string -> Numeral.t

Return the numeral encoding of a construcor of an enumerated datatype

val enum_of_constr : string -> t

Return the enumerated dataype to which the constructor belongs

Pretty-printing

val pp_print_type_node : Stdlib.Format.formatter -> kindtype -> unit

Pretty-print a type

val pp_print_type : Stdlib.Format.formatter -> t -> unit

Pretty-print a type

val print_type : t -> unit

Pretty-print a type to the standard formatter

val string_of_type : t -> string

Return a string representation of a type

Pretty-printing for debugging - differentiates UBV and BV

val pp_print_type_node_debug : Stdlib.Format.formatter -> kindtype -> unit

Pretty-print a type

val pp_print_type_debug : Stdlib.Format.formatter -> t -> unit

Pretty-print a type

val print_type_debug : t -> unit

Pretty-print a type to the standard formatter

val string_of_type_debug : t -> string

Return a string representation of a type