Module Smtml.Eval

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

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

val pp_op_type : op_type Fmt.t

Exceptions

type 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

val pp_type_error_info : type_error_info Fmt.t
type 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.

val pp_error_kind : error_kind Fmt.t
exception Eval_error of error_kind

Exception raised when an error occurs during concrete evaluation.

exception Value of Ty.t

Exception raised when an invalid value is encountered during evaluation.

Evaluation Functions

module Int : sig ... end
module Real : sig ... end
module Bool : sig ... end
module Str : sig ... end
module Lst : sig ... end
module Bitv : sig ... end
val 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.

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

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

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

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

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