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.25.0.tar.gz
md5=9ef240b636d7059d48bb54e6b8f0a4c4
sha512=2c73a5baa2e4f8a496f575087597510edae58a4416959108e7a4b063fb9a35ae7461227c679868d82cd324865a563bd2a0df6da1fa3a88d416f76be32ea07809

doc/smtml/Smtml/Eval/index.html

Module Smtml.EvalSource

Operators and Evaluation Functions. This module defines types and functions for representing and evaluating various kinds of operations, including unary, binary, ternary, relational, conversion, and n-ary operations. It also defines exceptions for handling errors during evaluation.

Operation Types

Sourcetype op_type = [
  1. | `Unop of Ty.Unop.t
    (*

    Unary operation.

    *)
  2. | `Binop of Ty.Binop.t
    (*

    Binary operation.

    *)
  3. | `Relop of Ty.Relop.t
    (*

    Relational operation.

    *)
  4. | `Triop of Ty.Triop.t
    (*

    Ternary operation.

    *)
  5. | `Cvtop of Ty.Cvtop.t
    (*

    Conversion operation.

    *)
  6. | `Naryop of Ty.Naryop.t
    (*

    N-ary operation.

    *)
]

A type representing various kinds of operations.

Sourceval pp_op_type : op_type Fmt.t

Exceptions

Sourcetype type_error_info = {
  1. index : int;
    (*

    The position of the erroneous value.

    *)
  2. value : Value.t;
    (*

    The actual value that caused the error.

    *)
  3. ty : Ty.t;
    (*

    The expected type.

    *)
  4. op : op_type;
    (*

    The operation that led to the error.

    *)
  5. msg : string;
}

Context payload for type errors

Sourceval pp_type_error_info : type_error_info Fmt.t
Sourcetype error_kind = [
  1. | `Divide_by_zero
  2. | `Conversion_to_integer
  3. | `Integer_overflow
  4. | `Index_out_of_bounds
  5. | `Invalid_format_conversion
  6. | `Unsupported_operator of op_type * Ty.t
  7. | `Unsupported_theory of Ty.t
  8. | `Type_error of type_error_info
]

Classification of errors that can occur during evaluation.

Sourceval pp_error_kind : error_kind Fmt.t
Sourceexception Eval_error of error_kind

Exception raised when an error occurs during concrete evaluation.

Sourceexception Value of Ty.t

Exception raised when an invalid value is encountered during evaluation.

Evaluation Functions

Sourcemodule Int : sig ... end
Sourcemodule Real : sig ... end
Sourcemodule Bool : sig ... end
Sourcemodule Str : sig ... end
Sourcemodule Lst : sig ... end
Sourcemodule Bitv : sig ... end
Sourceval unop : Ty.t -> Ty.Unop.t -> Value.t -> Value.t

unop ty op v applies a unary operation op on the value v of type ty. Raises Type_error if the value does not match the expected type.

Sourceval binop : Ty.t -> Ty.Binop.t -> Value.t -> Value.t -> Value.t

binop ty op v1 v2 applies a binary operation op on the values v1 and v2 of type ty. Raises DivideByZero if the operation involves division by zero. Raises TypeError if the values do not match the expected type.

Sourceval triop : Ty.t -> Ty.Triop.t -> Value.t -> Value.t -> Value.t -> Value.t

triop ty op v1 v2 v3 applies a ternary operation op on the values v1, v2, and v3 of type ty. Raises TypeError if any value does not match the expected type.

Sourceval relop : Ty.t -> Ty.Relop.t -> Value.t -> Value.t -> bool

relop ty op v1 v2 applies a relational operation op on the values v1 and v2 of type ty. Returns true if the relation holds, otherwise false. Raises TypeError if the values do not match the expected type.

Sourceval cvtop : Ty.t -> Ty.Cvtop.t -> Value.t -> Value.t

cvtop ty op v applies a conversion operation op on the value v of type ty. Raises TypeError if the value does not match the expected type.

Sourceval naryop : Ty.t -> Ty.Naryop.t -> Value.t list -> Value.t

naryop ty op vs applies an n-ary operation op on the list of values vs of type ty. Raises TypeError if any value does not match the expected type.