diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 92dd399c5..6e3ce57a1 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -4751,6 +4751,8 @@ extern "C" { The returned AST is simplified using algebraic simplification rules, such as constant propagation (propagating true/false over logical connectives). + \sa Z3_simplify_ex + def_API('Z3_simplify', AST, (_in(CONTEXT), _in(AST))) */ Z3_ast Z3_API Z3_simplify(Z3_context c, Z3_ast a); @@ -4762,6 +4764,10 @@ extern "C" { This procedure is similar to #Z3_simplify, but the behavior of the simplifier can be configured using the given parameter set. + \sa Z3_simplify + \sa Z3_simplify_get_help + \sa Z3_simplify_get_param_descrs + def_API('Z3_simplify_ex', AST, (_in(CONTEXT), _in(AST), _in(PARAMS))) */ Z3_ast Z3_API Z3_simplify_ex(Z3_context c, Z3_ast a, Z3_params p); @@ -4769,6 +4775,9 @@ extern "C" { /** \brief Return a string describing all available parameters. + \sa Z3_simplify_ex + \sa Z3_simplify_get_param_descrs + def_API('Z3_simplify_get_help', STRING, (_in(CONTEXT),)) */ Z3_string Z3_API Z3_simplify_get_help(Z3_context c); @@ -4776,6 +4785,9 @@ extern "C" { /** \brief Return the parameter description set for the simplify procedure. + \sa Z3_simplify_ex + \sa Z3_simplify_get_help + def_API('Z3_simplify_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT),)) */ Z3_param_descrs Z3_API Z3_simplify_get_param_descrs(Z3_context c); @@ -6050,6 +6062,9 @@ extern "C" { /** \brief Return a string describing all solver available parameters. + \sa Z3_solver_get_param_descrs + \sa Z3_solver_set_params + def_API('Z3_solver_get_help', STRING, (_in(CONTEXT), _in(SOLVER))) */ Z3_string Z3_API Z3_solver_get_help(Z3_context c, Z3_solver s); @@ -6057,6 +6072,9 @@ extern "C" { /** \brief Return the parameter description set for the given solver object. + \sa Z3_solver_get_help + \sa Z3_solver_set_params + def_API('Z3_solver_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT), _in(SOLVER))) */ Z3_param_descrs Z3_API Z3_solver_get_param_descrs(Z3_context c, Z3_solver s); @@ -6064,6 +6082,9 @@ extern "C" { /** \brief Set the given solver using the given parameters. + \sa Z3_solver_get_help + \sa Z3_solver_get_param_descrs + def_API('Z3_solver_set_params', VOID, (_in(CONTEXT), _in(SOLVER), _in(PARAMS))) */ void Z3_API Z3_solver_set_params(Z3_context c, Z3_solver s, Z3_params p); @@ -6087,6 +6108,7 @@ extern "C" { The solver contains a stack of assertions. + \sa Z3_solver_get_num_scopes \sa Z3_solver_pop def_API('Z3_solver_push', VOID, (_in(CONTEXT), _in(SOLVER))) @@ -6096,6 +6118,7 @@ extern "C" { /** \brief Backtrack \c n backtracking points. + \sa Z3_solver_get_num_scopes \sa Z3_solver_push \pre n <= Z3_solver_get_num_scopes(c, s) @@ -6107,6 +6130,9 @@ extern "C" { /** \brief Remove all assertions from the solver. + \sa Z3_solver_assert + \sa Z3_solver_assert_and_track + def_API('Z3_solver_reset', VOID, (_in(CONTEXT), _in(SOLVER))) */ void Z3_API Z3_solver_reset(Z3_context c, Z3_solver s); @@ -6127,6 +6153,9 @@ extern "C" { The functions #Z3_solver_check and #Z3_solver_check_assumptions should be used to check whether the logical context is consistent or not. + \sa Z3_solver_assert_and_track + \sa Z3_solver_reset + def_API('Z3_solver_assert', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST))) */ void Z3_API Z3_solver_assert(Z3_context c, Z3_solver s, Z3_ast a); @@ -6143,6 +6172,9 @@ extern "C" { \pre \c a must be a Boolean expression \pre \c p must be a Boolean constant (aka variable). + \sa Z3_solver_assert + \sa Z3_solver_reset + def_API('Z3_solver_assert_and_track', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST), _in(AST))) */ void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p); @@ -6150,6 +6182,9 @@ extern "C" { /** \brief load solver assertions from a file. + \sa Z3_solver_from_string + \sa Z3_solver_to_string + def_API('Z3_solver_from_file', VOID, (_in(CONTEXT), _in(SOLVER), _in(STRING))) */ void Z3_API Z3_solver_from_file(Z3_context c, Z3_solver s, Z3_string file_name); @@ -6157,6 +6192,9 @@ extern "C" { /** \brief load solver assertions from a string. + \sa Z3_solver_from_file + \sa Z3_solver_to_string + def_API('Z3_solver_from_string', VOID, (_in(CONTEXT), _in(SOLVER), _in(STRING))) */ void Z3_API Z3_solver_from_string(Z3_context c, Z3_solver s, Z3_string file_name); @@ -6323,6 +6361,9 @@ extern "C" { /** \brief Convert a solver into a string. + \sa Z3_solver_from_file + \sa Z3_solver_from_string + def_API('Z3_solver_to_string', STRING, (_in(CONTEXT), _in(SOLVER))) */ Z3_string Z3_API Z3_solver_to_string(Z3_context c, Z3_solver s); diff --git a/src/api/z3_fixedpoint.h b/src/api/z3_fixedpoint.h index 246228ae6..393cba224 100644 --- a/src/api/z3_fixedpoint.h +++ b/src/api/z3_fixedpoint.h @@ -253,6 +253,9 @@ extern "C" { /** \brief Set parameters on fixedpoint context. + \sa Z3_fixedpoint_get_help + \sa Z3_fixedpoint_get_param_descrs + def_API('Z3_fixedpoint_set_params', VOID, (_in(CONTEXT), _in(FIXEDPOINT), _in(PARAMS))) */ void Z3_API Z3_fixedpoint_set_params(Z3_context c, Z3_fixedpoint f, Z3_params p); @@ -260,6 +263,9 @@ extern "C" { /** \brief Return a string describing all fixedpoint available parameters. + \sa Z3_fixedpoint_get_param_descrs + \sa Z3_fixedpoint_set_params + def_API('Z3_fixedpoint_get_help', STRING, (_in(CONTEXT), _in(FIXEDPOINT))) */ Z3_string Z3_API Z3_fixedpoint_get_help(Z3_context c, Z3_fixedpoint f); @@ -267,6 +273,9 @@ extern "C" { /** \brief Return the parameter description set for the given fixedpoint object. + \sa Z3_fixedpoint_get_help + \sa Z3_fixedpoint_set_params + def_API('Z3_fixedpoint_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT), _in(FIXEDPOINT))) */ Z3_param_descrs Z3_API Z3_fixedpoint_get_param_descrs(Z3_context c, Z3_fixedpoint f); @@ -278,6 +287,9 @@ extern "C" { \param num_queries - number of additional queries to print. \param queries - additional queries. + \sa Z3_fixedpoint_from_file + \sa Z3_fixedpoint_from_string + def_API('Z3_fixedpoint_to_string', STRING, (_in(CONTEXT), _in(FIXEDPOINT), _in(UINT), _in_array(2, AST))) */ Z3_string Z3_API Z3_fixedpoint_to_string( @@ -295,6 +307,9 @@ extern "C" { \param f - fixedpoint context. \param s - string containing SMT2 specification. + \sa Z3_fixedpoint_from_file + \sa Z3_fixedpoint_to_string + def_API('Z3_fixedpoint_from_string', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(STRING))) */ Z3_ast_vector Z3_API Z3_fixedpoint_from_string(Z3_context c, @@ -310,6 +325,9 @@ extern "C" { \param f - fixedpoint context. \param s - path to file containing SMT2 specification. + \sa Z3_fixedpoint_from_string + \sa Z3_fixedpoint_to_string + def_API('Z3_fixedpoint_from_file', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(STRING))) */ Z3_ast_vector Z3_API Z3_fixedpoint_from_file(Z3_context c, diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index fffaac212..750f286a5 100644 --- a/src/api/z3_optimization.h +++ b/src/api/z3_optimization.h @@ -129,6 +129,11 @@ extern "C" { \param num_assumptions - number of additional assumptions \param assumptions - the additional assumptions + \sa Z3_optimize_get_reason_unknown + \sa Z3_optimize_get_model + \sa Z3_optimize_get_statistics + \sa Z3_optimize_get_unsat_core + def_API('Z3_optimize_check', INT, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT), _in_array(2, AST))) */ Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[]); @@ -169,6 +174,9 @@ extern "C" { \param o - optimization context \param p - parameters + \sa Z3_optimize_get_help + \sa Z3_optimize_get_param_descrs + def_API('Z3_optimize_set_params', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(PARAMS))) */ void Z3_API Z3_optimize_set_params(Z3_context c, Z3_optimize o, Z3_params p); @@ -179,6 +187,9 @@ extern "C" { \param c - context \param o - optimization context + \sa Z3_optimize_get_help + \sa Z3_optimize_set_params + def_API('Z3_optimize_get_param_descrs', PARAM_DESCRS, (_in(CONTEXT), _in(OPTIMIZE))) */ Z3_param_descrs Z3_API Z3_optimize_get_param_descrs(Z3_context c, Z3_optimize o); @@ -190,6 +201,10 @@ extern "C" { \param o - optimization context \param idx - index of optimization objective + \sa Z3_optimize_get_upper + \sa Z3_optimize_get_lower_as_vector + \sa Z3_optimize_get_upper_as_vector + def_API('Z3_optimize_get_lower', AST, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT))) */ Z3_ast Z3_API Z3_optimize_get_lower(Z3_context c, Z3_optimize o, unsigned idx); @@ -201,6 +216,10 @@ extern "C" { \param o - optimization context \param idx - index of optimization objective + \sa Z3_optimize_get_lower + \sa Z3_optimize_get_lower_as_vector + \sa Z3_optimize_get_upper_as_vector + def_API('Z3_optimize_get_upper', AST, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT))) */ Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx); @@ -216,6 +235,10 @@ extern "C" { \param o - optimization context \param idx - index of optimization objective + \sa Z3_optimize_get_lower + \sa Z3_optimize_get_upper + \sa Z3_optimize_get_upper_as_vector + def_API('Z3_optimize_get_lower_as_vector', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT))) */ Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx); @@ -227,6 +250,10 @@ extern "C" { \param o - optimization context \param idx - index of optimization objective + \sa Z3_optimize_get_lower + \sa Z3_optimize_get_upper + \sa Z3_optimize_get_lower_as_vector + def_API('Z3_optimize_get_upper_as_vector', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT))) */ Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx); @@ -237,6 +264,9 @@ extern "C" { \param c - context. \param o - optimization context. + \sa Z3_optimize_from_file + \sa Z3_optimize_from_string + def_API('Z3_optimize_to_string', STRING, (_in(CONTEXT), _in(OPTIMIZE))) */ Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o); @@ -250,6 +280,9 @@ extern "C" { \param o - optimize context. \param s - string containing SMT2 specification. + \sa Z3_optimize_from_file + \sa Z3_optimize_to_string + def_API('Z3_optimize_from_string', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(STRING))) */ void Z3_API Z3_optimize_from_string(Z3_context c, Z3_optimize o, Z3_string s); @@ -263,6 +296,9 @@ extern "C" { \param o - optimize context. \param s - path to file containing SMT2 specification. + \sa Z3_optimize_from_string + \sa Z3_optimize_to_string + def_API('Z3_optimize_from_file', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(STRING))) */ void Z3_API Z3_optimize_from_file(Z3_context c, Z3_optimize o, Z3_string s); @@ -270,6 +306,9 @@ extern "C" { /** \brief Return a string containing a description of parameters accepted by optimize. + \sa Z3_optimize_get_param_descrs + \sa Z3_optimize_set_params + def_API('Z3_optimize_get_help', STRING, (_in(CONTEXT), _in(OPTIMIZE))) */ Z3_string Z3_API Z3_optimize_get_help(Z3_context c, Z3_optimize t);