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