A term in the abstract syntax tree.

The different types of expressions.

view term extracts the underlying expression from a term.

hash term computes the hash of a term.

equal t1 t2 compares two terms for equality.

compare t1 t2 compares two terms lexicographically.

ty expr determines the type of an expression.

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

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

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

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

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

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

to_string term converts a term to a string representation.

value v constructs a value expression from the given value.

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

loc l constructs an abstract location

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

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

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

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

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

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

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

unop ty op expr applies a unary operation with simplification.

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

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

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

cvtop ty op expr applies a conversion operation with simplification.

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

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

concat expr1 expr2 concatenates two expressions with simplification.

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.

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.

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.

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.

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.

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

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

raw_concat expr1 expr2 concatenates two expressions without simplification.

simplify expr simplifies an expression until a fixpoint is reached.