Module Smtml.Ty

Type Module. This module defines types and operations for working with SMT types, including unary, binary, relational, ternary, conversion, and n-ary operations. It also provides utilities for type comparison, pretty-printing, and parsing.

type _ cast =
  1. | C8 : int cast
    (*

    Cast to an 8-bit integer.

    *)
  2. | C32 : int32 cast
    (*

    Cast to a 32-bit integer.

    *)
  3. | C64 : int64 cast
    (*

    Cast to a 64-bit integer.

    *)

The type _ cast represents type casts for integers of different bit widths.

Type Definitions

type t =
  1. | Ty_app
    (*

    Application type.

    *)
  2. | Ty_bitv of int
    (*

    Bitvector type with a specified bit width.

    *)
  3. | Ty_bool
    (*

    Boolean type.

    *)
  4. | Ty_fp of int
    (*

    Floating-point type with a specified bit width.

    *)
  5. | Ty_int
    (*

    Integer type.

    *)
  6. | Ty_list
    (*

    List type.

    *)
  7. | Ty_none
    (*

    None type.

    *)
  8. | Ty_real
    (*

    Real number type.

    *)
  9. | Ty_str
    (*

    String type.

    *)
  10. | Ty_unit
    (*

    Unit type.

    *)
  11. | Ty_regexp
    (*

    Regular expression type.

    *)
  12. | Ty_roundingMode

The type t represents smtml types.

Type Comparison

val hash : t -> int
val compare : t -> t -> int

compare t1 t2 performs a total order comparison of types t1 and t2.

val equal : t -> t -> bool

equal t1 t2 checks if types t1 and t2 are equal.

Pretty Printing

type printer =
  1. | With_type_and_hexa_float
    (*

    Print with type information and hexadecimal format for floats and bitvectors.

    *)
  2. | With_type
    (*

    Print with type information.

    *)
  3. | Without_type
    (*

    Print without type information.

    *)

The type printer represents the different formats for printing values.

val pp : t Fmt.t

pp fmt t pretty-prints the type t using the formatter fmt.

String Conversion

val string_of_type : t -> string

string_of_type t converts the type t to a string representation.

val of_string : string -> (t, [> `Msg of string ]) Smtml_prelude.Result.t

of_string s attempts to parse the string s into a type. Returns Ok t if successful, or an error message otherwise.

Type Size

val size : t -> int

size t returns the size (in bytes) of the type t, if applicable.

val bitsize : t -> int

bitsize t returns the size (in bits) of the type t, if applicable.

Unary Operations

module Unop : sig ... end

Binary Operations

module Binop : sig ... end

Relational Operations

module Relop : sig ... end

Ternary Operations

module Triop : sig ... end

Conversion Operations

module Cvtop : sig ... end

N-ary Operations

module Naryop : sig ... end
module Smtlib : sig ... end