Module Z3.Expr

module Expr: sig .. end

General Expressions (terms)

type expr =

`\|`	`Expr of AST.ast`

val ast_of_expr : expr -> AST.ast

val expr_of_ast : AST.ast -> expr

val simplify : expr -> Params.params option -> expr

Returns a simplified version of the expression. Expr.get_simplify_help

val get_simplify_help : context -> string

A string describing all available parameters to Expr.Simplify.

val get_simplify_parameter_descrs : context -> Params.ParamDescrs.param_descrs

Retrieves parameter descriptions for simplifier.

val get_func_decl : expr -> FuncDecl.func_decl

The function declaration of the function that is applied in this expression.

val get_num_args : expr -> int

The number of arguments of the expression.

val get_args : expr -> expr list

The arguments of the expression.

val update : expr -> expr list -> expr

Update the arguments of the expression using an array of expressions. The number of new arguments should coincide with the current number of arguments.

val substitute : expr -> expr list -> expr list -> expr

Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs.

The result is the new expression. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].

val substitute_one : expr -> expr -> expr -> expr

Substitute every occurrence of from in the expression with to. Expr.substitute

val substitute_vars : expr -> expr list -> expr

Substitute the free variables in the expression with the expressions in the expr array

For every i smaller than num_exprs, the variable with de-Bruijn index i is replaced with term to[i].

val translate : expr -> context -> expr

Translates (copies) the term to another context.
Returns A copy of the term which is associated with the other context

val to_string : expr -> string

Returns a string representation of the expression.

val is_numeral : expr -> bool

Indicates whether the term is a numeral

val is_well_sorted : expr -> bool

Indicates whether the term is well-sorted.
Returns True if the term is well-sorted, false otherwise.

val get_sort : expr -> Sort.sort

The Sort of the term.

val is_const : expr -> bool

Indicates whether the term represents a constant.

val mk_const : context -> Symbol.symbol -> Sort.sort -> expr

Creates a new constant.

val mk_const_s : context -> string -> Sort.sort -> expr

Creates a new constant.

val mk_const_f : context -> FuncDecl.func_decl -> expr

Creates a constant from the func_decl.

val mk_fresh_const : context -> string -> Sort.sort -> expr

Creates a fresh constant with a name prefixed with a string.

val mk_app : context -> FuncDecl.func_decl -> expr list -> expr

Create a new function application.

val mk_numeral_string : context -> string -> Sort.sort -> expr

Create a numeral of a given sort.
Returns A Term with the given value and sort

val mk_numeral_int : context -> int -> Sort.sort -> expr

Create a numeral of a given sort. This function can be use to create numerals that fit in a machine integer. It is slightly faster than MakeNumeral since it is not necessary to parse a string.
Returns A Term with the given value and sort

val equal : expr -> expr -> bool

Comparison operator.
Returns True if the two expr's are equal; false otherwise.

val compare : expr -> expr -> int

Object Comparison.
Returns Negative if the first expr should be sorted before the second, positive if after, else zero.