package smtml

  1. Overview
  2. Docs
An SMT solver frontend for OCaml

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (25)

Authors

  1. J
    João Pereira <joaomhmpereira@tecnico.ulisboa.pt>
  2. F
    Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>
  3. H
    Hichem Rami Ait El Hara <hra@ocamlpro.com>
  4. R
    redianthus <redopam@pm.me>
  5. A
    Arthur Carcano <arthur.carcano@ocamlpro.com>
  6. P
    Pierre Chambart <pierre.chambart@ocamlpro.com>
  7. J
    José Fragoso Santos <jose.fragoso@tecnico.ulisboa.pt>

Maintainers

  1. F
    Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>

Sources

v0.28.0.tar.gz
md5=dccec4e664735d96f7d5e867f8c0841f
sha512=4e1586451c0e61dcae6bd46bb8fe899430b383c776dbf214cffcd6802449ee522f4658e2990ac1a1ad6f8e89f72a8d83ba0a40a7d33b2faaa9f8ae0c7a1d0c67

doc/smtml/Smtml/Ty/index.html

Module Smtml.TySource

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.

Sourcetype _ 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

Sourcetype 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

Sourceval hash : t -> int
Sourceval compare : t -> t -> int

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

Sourceval equal : t -> t -> bool

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

Pretty Printing

Sourcetype 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.

Sourceval pp : t Fmt.t

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

String Conversion

Sourceval string_of_type : t -> string

string_of_type t converts the type t to a string representation.

Sourceval 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

Sourceval size : t -> int

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

Sourceval bitsize : t -> int

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

Unary Operations

Sourcemodule Unop : sig ... end

Binary Operations

Sourcemodule Binop : sig ... end

Relational Operations

Sourcemodule Relop : sig ... end

Ternary Operations

Sourcemodule Triop : sig ... end

Conversion Operations

Sourcemodule Cvtop : sig ... end

N-ary Operations

Sourcemodule Naryop : sig ... end
Sourcemodule Smtlib : sig ... end