Z3
Loading...
Searching...
No Matches
z3
cast_ast< expr >
Public Member Functions
cast_ast< expr > Class Reference
#include <
z3++.h
>
Public Member Functions
expr
operator()
(
context
&c, Z3_ast a)
Detailed Description
Definition at line
2255
of file
z3++.h
.
Member Function Documentation
◆
operator()()
expr
operator()
(
context
&
c
,
Z3_ast
a
)
inline
Definition at line
2257
of file
z3++.h
.
2257
{
2258
assert(
Z3_get_ast_kind
(c, a) ==
Z3_NUMERAL_AST
||
2259
Z3_get_ast_kind
(c, a) ==
Z3_APP_AST
||
2260
Z3_get_ast_kind
(c, a) ==
Z3_QUANTIFIER_AST
||
2261
Z3_get_ast_kind
(c, a) ==
Z3_VAR_AST
);
2262
return
expr(c, a);
2263
}
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.
Z3_APP_AST
@ Z3_APP_AST
Definition:
z3_api.h:141
Z3_VAR_AST
@ Z3_VAR_AST
Definition:
z3_api.h:142
Z3_NUMERAL_AST
@ Z3_NUMERAL_AST
Definition:
z3_api.h:140
Z3_QUANTIFIER_AST
@ Z3_QUANTIFIER_AST
Definition:
z3_api.h:143
Generated on Sun Jan 8 2023 00:00:00 for Z3 by
1.9.5