Z3
z3
cast_ast< expr >
Public Member Functions
cast_ast< expr > Class Template Reference
Public Member Functions
expr
operator()
(
context
&c, Z3_ast a)
Detailed Description
template<>
class z3::cast_ast< expr >
Definition at line
1352
of file
z3++.h
.
Member Function Documentation
§
operator()()
expr
operator()
(
context
&
c
,
Z3_ast
a
)
inline
Definition at line
1354
of file
z3++.h
.
1354
{
1355
assert(Z3_get_ast_kind(c, a) ==
Z3_NUMERAL_AST
||
1356
Z3_get_ast_kind(c, a) ==
Z3_APP_AST
||
1357
Z3_get_ast_kind(c, a) ==
Z3_QUANTIFIER_AST
||
1358
Z3_get_ast_kind(c, a) ==
Z3_VAR_AST
);
1359
return
expr(c, a);
1360
}
Z3_QUANTIFIER_AST
Definition:
z3_api.h:188
Z3_APP_AST
Definition:
z3_api.h:186
Z3_VAR_AST
Definition:
z3_api.h:187
Z3_NUMERAL_AST
Definition:
z3_api.h:185
Generated on Sat Nov 12 2016 22:01:19 for Z3 by
1.8.12