mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-17 11:26:17 +00:00
Code Activity

Fix doxygen warnings in C API docs. (#6202)

Browse source
This commit is contained in:
Bruce Mitchener 2022-07-29 16:49:24 +07:00 • committed by GitHub
parent 78237578f3
commit 75339c6db7
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/z3_api.h
View file

@ -3387,6 +3387,7 @@ extern "C" {
*/ */
Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty); Z3_ast Z3_API Z3_mk_numeral(Z3_context c, Z3_string numeral, Z3_sort ty);
#if 0
/** /**
\brief Create an integer numeral from a vector of unsigned numerals. \brief Create an integer numeral from a vector of unsigned numerals.
@ -3394,12 +3395,12 @@ extern "C" {
\param sign - true if positive, false if negative \param sign - true if positive, false if negative
\param n - length of array of numerals \param n - length of array of numerals
\param nums - array of numerals \param nums - array of numerals
\param srt - sort of numeral (int, real, bit-vector). \param s - sort of numeral (int, real, bit-vector).
future_('Z3_mk_mpz_numeral', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in_array(2, UINT), _in(SORT))) future_('Z3_mk_mpz_numeral', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in_array(2, UINT), _in(SORT)))
*/ */
//Z3_ast Z3_mk_mpz_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], Z3_sort s); Z3_ast Z3_mk_mpz_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], Z3_sort s);
/** /**
\brief Create a rational numeral from a vector of unsigned numerals. \brief Create a rational numeral from a vector of unsigned numerals.
@ -3416,7 +3417,8 @@ extern "C" {
future_('Z3_mk_mpq_numeral', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in_array(2, UINT), _in(UINT), _in_array(4, UINT))) future_('Z3_mk_mpq_numeral', AST, (_in(CONTEXT), _in(BOOL), _in(UINT), _in_array(2, UINT), _in(UINT), _in_array(4, UINT)))
*/ */
// Z3_ast Z3_mk_mpq_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], unsigned d, unsigned const dens[]); Z3_ast Z3_mk_mpq_numeral(Z3_context c, bool sign, unsigned n, unsigned const nums[], unsigned d, unsigned const dens[]);
#endif
/** /**
\brief Create a real from a fraction. \brief Create a real from a fraction.
@ -6982,7 +6984,7 @@ extern "C" {
/** /**
Create uninterpreted function declaration for the user propagator. Create uninterpreted function declaration for the user propagator.
When expressions using the function are created by the solver invoke a callback When expressions using the function are created by the solver invoke a callback
to \ref \Z3_solver_propagate_created with arguments to \ref Z3_solver_propagate_created with arguments
1. context and callback solve 1. context and callback solve
2. declared_expr: expression using function that was used as the top-level symbol 2. declared_expr: expression using function that was used as the top-level symbol
3. declared_id: a unique identifier (unique within the current scope) to track the expression. 3. declared_id: a unique identifier (unique within the current scope) to track the expression.