package smtml

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

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.

and expr =
  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

val make : expr -> t

make expr creates a new term from the given expression.

val view : t -> expr

view term extracts the underlying expression from a term.

val hash : t -> int

hash term computes the hash of a term.

val equal : t -> t -> bool

equal t1 t2 compares two terms for equality.

val compare : t -> t -> int

compare t1 t2 compares two terms lexicographically.

Type and Symbol Handling

val ty : t -> Ty.t

ty expr determines the type of an expression.

val is_symbolic : t -> bool

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

val get_symbols : t list -> Symbol.t list

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

val 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

val pp : t Fmt.t

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

val pp_smt : t list Fmt.t

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

val pp_list : t list Fmt.t

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

val to_string : t -> string

to_string term converts a term to a string representation.

Expression Constructors

val value : Value.t -> t

value v constructs a value expression from the given value.

val ptr : int32 -> t -> t

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

val symbol : Symbol.t -> t

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

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

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

val let_in : t list -> t -> t

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

val forall : t list -> t -> t

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

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

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

unop ty op expr applies a unary operation with simplification.

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

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

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

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

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

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

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

cvtop ty op expr applies a conversion operation with simplification.

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

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

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

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

val extract2 : t -> int -> t

extract2 expr pos extracts a bit range with simplification.

val concat : t -> t -> t

concat expr1 expr2 concatenates two expressions with simplification.

val concat3 : msb:t -> lsb:t -> int -> t

concat3 ~msb ~lsb size concatenates two expressions with simplification, specifying the size of the result.

Dumb Constructors for Operations

These constructors do not apply simplifications.

val unop' : Ty.t -> Ty.Unop.t -> t -> t

unop' ty op expr applies a unary operation without simplification.

val binop' : Ty.t -> Ty.Binop.t -> t -> t -> t

binop' ty op expr1 expr2 applies a binary operation without simplification.

val triop' : Ty.t -> Ty.Triop.t -> t -> t -> t -> t

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

val relop' : Ty.t -> Ty.Relop.t -> t -> t -> t

relop' ty op expr1 expr2 applies a relational operation without simplification.

val cvtop' : Ty.t -> Ty.Cvtop.t -> t -> t

cvtop' ty op expr applies a conversion operation without simplification.

val naryop' : Ty.t -> Ty.Naryop.t -> t list -> t

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

val extract' : t -> high:int -> low:int -> t

extract' expr ~high ~low extracts a bit range without simplification.

val concat' : t -> t -> t

concat' expr1 expr2 concatenates two expressions without simplification.

Expression Simplification

val simplify : t -> t

simplify expr simplifies an expression until a fixpoint is reached.

Hash-Consing Module

module Hc : sig ... end

Boolean Expressions

module Bool : sig ... end

Set Module

module Set : sig ... end

Bitvectors

module Bitv : sig ... end

Floating-Points

module 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