package smtml

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

Install 

dune-project
 Dependency

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

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.17.0.tar.gz
md5=181cc72de896d7a23787a7c44c9cc8d1
sha512=25b6c2f650d99cc71fbc5c27060a6064808c9736804332417d25194c8ca4e053fb057bbf9ef872c52a6f5ed9d6cb6758abda8e71974bc2b2ae79f5681f7dbe47

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

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