Public Member Functions | |
expr | operator() (context &c, Z3_ast a) |
Definition at line 986 of file z3++.h.
{ assert(Z3_get_ast_kind(c, a) == Z3_NUMERAL_AST || Z3_get_ast_kind(c, a) == Z3_APP_AST || Z3_get_ast_kind(c, a) == Z3_QUANTIFIER_AST || Z3_get_ast_kind(c, a) == Z3_VAR_AST); return expr(c, a); }