package smtml

  1. Overview
  2. Docs
package smtml
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Smtml.ExprSource

Abstract Syntax Tree (AST) for Expressions. This module defines the representation of terms and expressions in the AST, along with constructors, accessors, simplification utilities, and pretty-printing functions. It also includes submodules for handling Boolean expressions, sets, bitvectors, and floating-point arithmetic.

Expression Types

A term in the abstract syntax tree.

Sourceand expr = private
  1. | Val of Value.t
    (*

    A constant value.

    *)
  2. | Ptr of {
    1. base : int32;
      (*

      Base address.

      *)
    2. offset : t;
      (*

      Offset from base.

      *)
    }
  3. | Symbol of Symbol.t
    (*

    A symbolic variable.

    *)
  4. | List of t list
    (*

    A list of expressions.

    *)
  5. | App of Symbol.t * t list
    (*

    Function application.

    *)
  6. | Unop of Ty.t * Ty.Unop.t * t
    (*

    Unary operation.

    *)
  7. | Binop of Ty.t * Ty.Binop.t * t * t
    (*

    Binary operation.

    *)
  8. | Triop of Ty.t * Ty.Triop.t * t * t * t
    (*

    Ternary operation.

    *)
  9. | Relop of Ty.t * Ty.Relop.t * t * t
    (*

    Relational operation.

    *)
  10. | Cvtop of Ty.t * Ty.Cvtop.t * t
    (*

    Conversion operation.

    *)
  11. | Naryop of Ty.t * Ty.Naryop.t * t list
    (*

    N-ary operation.

    *)
  12. | Extract of t * int * int
    (*

    Extract a bit range from an expression.

    *)
  13. | Concat of t * t
    (*

    Concatenate two expressions.

    *)
  14. | Binder of Binder.t * t list * t
    (*

    A binding expression.

    *)

The different types of expressions.

Constructors and Accessors

Sourceval view : t -> expr

view term extracts the underlying expression from a term.

Sourceval hash : t -> int

hash term computes the hash of a term.

Sourceval equal : t -> t -> bool

equal t1 t2 compares two terms for equality.

Sourceval compare : t -> t -> int

compare t1 t2 compares two terms lexicographically.

Type and Symbol Handling

Sourceval ty : t -> Ty.t

ty expr determines the type of an expression.

Sourceval is_symbolic : t -> bool

is_symbolic expr checks if an expression is symbolic (i.e., contains symbolic variables).

Sourceval get_symbols : t list -> Symbol.t list

get_symbols exprs extracts all symbolic variables from a list of expressions.

Sourceval negate_relop : t -> (t, string) Smtml_prelude.Result.t

negate_relop expr negates a relational operation, if applicable. Returns an error if the expression is not a relational operation.

Pretty Printing

Sourceval pp : t Fmt.t

pp fmt term prints a term in a human-readable format using the formatter fmt.

Sourceval pp_smt : t list Fmt.t

pp_smt fmt terms prints a list of terms in SMT-LIB format using the formatter fmt.

Sourceval pp_list : t list Fmt.t

pp_list fmt terms prints a list of expressions in a human-readable format using the formatter fmt.

Sourceval to_string : t -> string

to_string term converts a term to a string representation.

Expression Constructors

Sourceval value : Value.t -> t

value v constructs a value expression from the given value.

Sourceval ptr : int32 -> t -> t

ptr base offset constructs a pointer expression with the given base address and offset.

Sourceval list : t list -> t

list l constructs a list expression with the given list of expressions

Sourceval symbol : Symbol.t -> t

symbol sym constructs a symbolic variable expression from the given symbol.

Sourceval app : Symbol.t -> t list -> t

app sym args constructs a function application expression with the given symbol and arguments.

Sourceval binder : Binder.t -> t list -> t -> t

binder ty bindings body constructs a ty bidning expression with the given bindings and body.

Sourceval let_in : t list -> t -> t

let_in bindings body constructs a let-binding expression with the given bindings and body.

Sourceval forall : t list -> t -> t

forall bindings body constructs a universal quantification expression with the given bindings and body.

Sourceval exists : t list -> t -> t

exists bindings body constructs an existential quantification expression with the given bindings and body.

Smart Constructors for Operations

These constructors apply simplifications during construction.

Sourceval unop : Ty.t -> Ty.Unop.t -> t -> t

unop ty op expr applies a unary operation with simplification.

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

binop ty op expr1 expr2 applies a binary operation with simplification.

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

triop ty op expr1 expr2 expr3 applies a ternary operation with simplification.

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

relop ty op expr1 expr2 applies a relational operation with simplification.

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

cvtop ty op expr applies a conversion operation with simplification.

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

naryop ty op exprs applies an N-ary operation with simplification.

Sourceval extract : t -> high:int -> low:int -> t

extract expr ~high ~low extracts a bit range with simplification.

Sourceval concat : t -> t -> t

concat expr1 expr2 concatenates two expressions with simplification.

Raw Constructors for Operations

Sourceval raw_unop : Ty.t -> Ty.Unop.t -> t -> t

raw_unop ty op expr applies a unary operation, creating a node without immediate simplification.

This function constructs the representation of a unary operation with the specified type ty, operator op, and operand expr. Unlike a "smart constructor" like unop, it does not evaluate the expression if possible, but rather creates the AST node representing the unevaluated operation.

For example:

  raw_unop Ty_int Neg (value (Int 1))

returns the AST node:

  Unop (Ty_int, Neg, Val (Int 1))

rather than the simplified value:

  Val (Int (-1))

which would typically be the result of the smart constructor unop.

Sourceval raw_binop : Ty.t -> Ty.Binop.t -> t -> t -> t

raw_binop ty op expr1 expr2 applies a binary operation, creating a node without immediate simplification.

This function constructs the representation of a binary operation with the specified type ty, operator op, and operands expr1, expr2. Unlike a "smart constructor" like binop, it does not evaluate the expression if possible, but rather creates the AST node representing the unevaluated operation.

For example:

  raw_binop Ty_int Add (value (Int 1)) (value (Int 2))

returns the AST node:

  Binop (Ty_int, Add, Val (Int 1), Val (Int 2))

rather than the simplified value:

  Val (Int 3)

which would typically be the result of the smart constructor binop.

Sourceval raw_triop : Ty.t -> Ty.Triop.t -> t -> t -> t -> t

raw_triop ty op expr1 expr2 expr3 applies a ternary operation, creating a node without immediate simplification.

This function constructs the representation of a ternary operation with the specified type ty, operator op, and operands expr1, expr2, expr3. Unlike a "smart constructor" like triop, it does not evaluate the expression if possible, but rather creates the AST node representing the unevaluated operation.

For example (using a if-then-else operator):

  raw_triop Ty_bool Ite (value True) (value (Int 1)) (value (Int 2))

returns the AST node:

  Triop (Ty_bool, Ite, Val True, Val (Int 1), Val (Int 2))

rather than the simplified value:

  Val (Int 1)

which would typically be the result of the smart constructor triop.

Sourceval raw_relop : Ty.t -> Ty.Relop.t -> t -> t -> t

raw_relop ty op expr1 expr2 applies a relational operation, creating a node without immediate simplification.

This function constructs the representation of a relational operation with the specified operand type ty, operator op, and operands expr1, expr2. Unlike a "smart constructor" like relop, it does not evaluate the expression if possible, but rather creates the AST node representing the unevaluated operation (which will have a boolean type).

For example:

  raw_relop Ty_bool Eq (value (Int 1)) (value (Int 2))

returns the AST node:

  Relop (Ty_bool, Eq, Val (Int 1), Val (Int 2))

rather than the simplified value:

  Val False

which would typically be the result of the smart constructor relop.

Sourceval raw_cvtop : Ty.t -> Ty.Cvtop.t -> t -> t

raw_cvtop ty op expr applies a conversion operation, creating a node without immediate simplification.

This function constructs the representation of a conversion operation with the specified target type ty, operator op, and operand expr. Unlike a "smart constructor" like cvtop, it does not evaluate the conversion if possible, but rather creates the AST node representing the unevaluated operation.

For example:

  raw_cvtop Ty_real Reinterpret_int (value (Int 5))

returns the AST node:

  Cvtop (Ty_real, Reinterpret_int, Val (Int 5))

rather than the simplified value:

  Val (Real 5.0)

which would typically be the result of the smart constructor cvtop.

Sourceval raw_naryop : Ty.t -> Ty.Naryop.t -> t list -> t

raw_naryop ty op exprs applies an N-ary operation without simplification.

Sourceval raw_extract : t -> high:int -> low:int -> t

raw_extract expr ~high ~low extracts a bit range without simplification.

Sourceval raw_concat : t -> t -> t

raw_concat expr1 expr2 concatenates two expressions without simplification.

Expression Simplification

Sourceval simplify : t -> t

simplify expr simplifies an expression until a fixpoint is reached.

Hash-Consing Module

Sourcemodule Hc : sig ... end

Boolean Expressions

Sourcemodule Bool : sig ... end

Set Module

Sourcemodule Set : sig ... end

Bitvectors

Sourcemodule Bitv : sig ... end

Floating-Points

Sourcemodule Fpa : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct