Z3
All
Data Structures
Namespaces
Files
Functions
Variables
Typedefs
Enumerations
Enumerator
Friends
Macros
Modules
Pages
z3
cast_ast< expr >
Public Member Functions
cast_ast< expr > Class Template Reference
C++ API
Public Member Functions
expr
operator()
(
context
&c, Z3_ast a)
Detailed Description
template<>
class z3::cast_ast< expr >
Definition at line
1756
of file
z3++.h
.
Member Function Documentation
expr
operator()
(
context
&
c
,
Z3_ast
a
)
inline
Definition at line
1758
of file
z3++.h
.
1758
{
1759
assert(
Z3_get_ast_kind
(c, a) ==
Z3_NUMERAL_AST
||
1760
Z3_get_ast_kind
(c, a) ==
Z3_APP_AST
||
1761
Z3_get_ast_kind
(c, a) ==
Z3_QUANTIFIER_AST
||
1762
Z3_get_ast_kind
(c, a) ==
Z3_VAR_AST
);
1763
return
expr(c, a);
1764
}
Z3_QUANTIFIER_AST
Definition:
z3_api.h:181
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
Definition:
z3_api.h:179
Z3_VAR_AST
Definition:
z3_api.h:180
Z3_NUMERAL_AST
Definition:
z3_api.h:178
Generated on Sat Oct 5 2019 15:21:13 for Z3 by
1.8.8