mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

reordered Z3_get_quantifier_num_bound in z3_api

Browse source
This commit is contained in:
Josh Berdine 2012-10-06 15:24:05 +01:00
parent af29bc7dc5
commit c0c98f7d09
1 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
lib/z3_api.h
View file

@ -3725,6 +3725,13 @@ END_MLAPI_EXCLUDE
*/ */
Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(__in Z3_context c, __in Z3_ast a, unsigned i); Z3_ast Z3_API Z3_get_quantifier_no_pattern_ast(__in Z3_context c, __in Z3_ast a, unsigned i);
/**
\brief Return number of bound variables of quantifier.
\pre Z3_get_ast_kind(a) == Z3_QUANTIFIER_AST
*/
unsigned Z3_API Z3_get_quantifier_num_bound(__in Z3_context c, __in Z3_ast a);
/** /**
\brief Return symbol of the i'th bound variable. \brief Return symbol of the i'th bound variable.
@ -3746,13 +3753,6 @@ END_MLAPI_EXCLUDE
*/ */
Z3_ast Z3_API Z3_get_quantifier_body(__in Z3_context c, __in Z3_ast a); Z3_ast Z3_API Z3_get_quantifier_body(__in Z3_context c, __in Z3_ast a);
/**
\brief Return number of bound variables of quantifier.
\pre Z3_get_ast_kind(a) == Z3_QUANTIFIER_AST
*/
unsigned Z3_API Z3_get_quantifier_num_bound(__in Z3_context c, __in Z3_ast a);
/** /**
\mlonly {3 {L Simplification}} \endmlonly \mlonly {3 {L Simplification}} \endmlonly