Module Z3.Expr

module Expr: sig .. end
General Expressions (terms)

type expr 
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 used 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.