Module Z3.Expr

type expr
val ast_of_expr : expr -> AST.ast
val expr_of_ast : AST.ast -> expr
val simplify : expr -> Params.params option -> expr
val get_simplify_help : context -> string
val get_simplify_parameter_descrs : context -> Params.ParamDescrs.param_descrs
val get_func_decl : expr -> FuncDecl.func_decl
val get_num_args : expr -> int
val get_args : expr -> expr list
val update : expr -> expr list -> expr
val substitute : expr -> expr list -> expr list -> expr
val substitute_one : expr -> expr -> expr -> expr
val substitute_vars : expr -> expr list -> expr
val translate : expr -> context -> expr
val to_string : expr -> string
val is_numeral : expr -> bool
val is_well_sorted : expr -> bool
val get_sort : expr -> Sort.sort
val is_const : expr -> bool
val mk_const : context -> Symbol.symbol -> Sort.sort -> expr
val mk_const_s : context -> string -> Sort.sort -> expr
val mk_const_f : context -> FuncDecl.func_decl -> expr
val mk_fresh_const : context -> string -> Sort.sort -> expr
val mk_app : context -> FuncDecl.func_decl -> expr list -> expr
val mk_numeral_string : context -> string -> Sort.sort -> expr
val mk_numeral_int : context -> int -> Sort.sort -> expr
val equal : expr -> expr -> bool
val compare : expr -> expr -> int