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
993
of file
z3++.h
.
Member Function Documentation
expr
operator()
(
context
&
c
,
Z3_ast
a
)
inline
Definition at line
995
of file
z3++.h
.
995
{
996
assert(
Z3_get_ast_kind
(c, a) == Z3_NUMERAL_AST ||
997
Z3_get_ast_kind
(c, a) == Z3_APP_AST ||
998
Z3_get_ast_kind
(c, a) == Z3_QUANTIFIER_AST ||
999
Z3_get_ast_kind
(c, a) == Z3_VAR_AST);
1000
return
expr(c, a);
1001
}
Z3_get_ast_kind
Z3_ast_kind Z3_API Z3_get_ast_kind(Z3_context c, Z3_ast a)
Return the kind of the given AST.
Generated on Tue Jul 19 2016 21:27:07 for Z3 by
1.8.11