mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Improve intra-doc linking. (#6191)
This commit is contained in:
Bruce Mitchener
GitHub
parent
43f2b848d4
commit
70895b2375
|
|
@ -4822,6 +4822,8 @@ extern "C" {
|
|||
\brief Return the number of argument of an application. If \c t
|
||||
is an constant, then the number of arguments is 0.
|
||||
|
||||
\sa Z3_get_app_arg
|
||||
|
||||
def_API('Z3_get_app_num_args', UINT, (_in(CONTEXT), _in(APP)))
|
||||
*/
|
||||
unsigned Z3_API Z3_get_app_num_args(Z3_context c, Z3_app a);
|
||||
|
|
@ -4831,6 +4833,8 @@ extern "C" {
|
|||
|
||||
\pre i < Z3_get_app_num_args(c, a)
|
||||
|
||||
\sa Z3_get_app_num_args
|
||||
|
||||
def_API('Z3_get_app_arg', AST, (_in(CONTEXT), _in(APP), _in(UINT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_get_app_arg(Z3_context c, Z3_app a, unsigned i);
|
||||
|
|
@ -5425,6 +5429,7 @@ extern "C" {
|
|||
\pre i < Z3_model_get_num_consts(c, m)
|
||||
|
||||
\sa Z3_model_eval
|
||||
\sa Z3_model_get_num_consts
|
||||
|
||||
def_API('Z3_model_get_const_decl', FUNC_DECL, (_in(CONTEXT), _in(MODEL), _in(UINT)))
|
||||
*/
|
||||
|
|
@ -5436,6 +5441,8 @@ extern "C" {
|
|||
A function interpretation is represented as a finite map and an 'else' value.
|
||||
Each entry in the finite map represents the value of a function given a set of arguments.
|
||||
|
||||
\sa Z3_model_get_func_decl
|
||||
|
||||
def_API('Z3_model_get_num_funcs', UINT, (_in(CONTEXT), _in(MODEL)))
|
||||
*/
|
||||
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m);
|
||||
|
|
@ -5561,6 +5568,8 @@ extern "C" {
|
|||
Each entry in the finite map represents the value of a function given a set of arguments.
|
||||
This procedure return the number of element in the finite map of \c f.
|
||||
|
||||
\sa Z3_func_interp_get_entry
|
||||
|
||||
def_API('Z3_func_interp_get_num_entries', UINT, (_in(CONTEXT), _in(FUNC_INTERP)))
|
||||
*/
|
||||
unsigned Z3_API Z3_func_interp_get_num_entries(Z3_context c, Z3_func_interp f);
|
||||
|
|
@ -5649,6 +5658,7 @@ extern "C" {
|
|||
/**
|
||||
\brief Return the number of arguments in a \c Z3_func_entry object.
|
||||
|
||||
\sa Z3_func_entry_get_arg
|
||||
\sa Z3_func_interp_get_entry
|
||||
|
||||
def_API('Z3_func_entry_get_num_args', UINT, (_in(CONTEXT), _in(FUNC_ENTRY)))
|
||||
|
|
@ -5660,6 +5670,7 @@ extern "C" {
|
|||
|
||||
\pre i < Z3_func_entry_get_num_args(c, e)
|
||||
|
||||
\sa Z3_func_entry_get_num_args
|
||||
\sa Z3_func_interp_get_entry
|
||||
|
||||
def_API('Z3_func_entry_get_arg', AST, (_in(CONTEXT), _in(FUNC_ENTRY), _in(UINT)))
|
||||
|
|
@ -5672,6 +5683,9 @@ extern "C" {
|
|||
/**
|
||||
\brief Log interaction to a file.
|
||||
|
||||
\sa Z3_append_log
|
||||
\sa Z3_close_log
|
||||
|
||||
extra_API('Z3_open_log', INT, (_in(STRING),))
|
||||
*/
|
||||
bool Z3_API Z3_open_log(Z3_string filename);
|
||||
|
|
@ -5679,10 +5693,13 @@ extern "C" {
|
|||
/**
|
||||
\brief Append user-defined string to interaction log.
|
||||
|
||||
The interaction log is opened using Z3_open_log.
|
||||
The interaction log is opened using #Z3_open_log.
|
||||
It contains the formulas that are checked using Z3.
|
||||
You can use this command to append comments, for instance.
|
||||
|
||||
\sa Z3_open_log
|
||||
\sa Z3_close_log
|
||||
|
||||
extra_API('Z3_append_log', VOID, (_in(STRING),))
|
||||
*/
|
||||
void Z3_API Z3_append_log(Z3_string string);
|
||||
|
|
@ -5690,6 +5707,9 @@ extern "C" {
|
|||
/**
|
||||
\brief Close interaction log.
|
||||
|
||||
\sa Z3_open_log
|
||||
\sa Z3_append_log
|
||||
|
||||
extra_API('Z3_close_log', VOID, ())
|
||||
*/
|
||||
void Z3_API Z3_close_log(void);
|
||||
|
|
@ -6388,6 +6408,8 @@ extern "C" {
|
|||
/**
|
||||
\brief Return the number of builtin tactics available in Z3.
|
||||
|
||||
\sa Z3_get_tactic_name
|
||||
|
||||
def_API('Z3_get_num_tactics', UINT, (_in(CONTEXT),))
|
||||
*/
|
||||
unsigned Z3_API Z3_get_num_tactics(Z3_context c);
|
||||
|
|
@ -6397,6 +6419,8 @@ extern "C" {
|
|||
|
||||
\pre i < Z3_get_num_tactics(c)
|
||||
|
||||
\sa Z3_get_num_tactics
|
||||
|
||||
def_API('Z3_get_tactic_name', STRING, (_in(CONTEXT), _in(UINT)))
|
||||
*/
|
||||
Z3_string Z3_API Z3_get_tactic_name(Z3_context c, unsigned i);
|
||||
|
|
@ -6404,6 +6428,8 @@ extern "C" {
|
|||
/**
|
||||
\brief Return the number of builtin probes available in Z3.
|
||||
|
||||
\sa Z3_get_probe_name
|
||||
|
||||
def_API('Z3_get_num_probes', UINT, (_in(CONTEXT),))
|
||||
*/
|
||||
unsigned Z3_API Z3_get_num_probes(Z3_context c);
|
||||
|
|
@ -6413,6 +6439,8 @@ extern "C" {
|
|||
|
||||
\pre i < Z3_get_num_probes(c)
|
||||
|
||||
\sa Z3_get_num_probes
|
||||
|
||||
def_API('Z3_get_probe_name', STRING, (_in(CONTEXT), _in(UINT)))
|
||||
*/
|
||||
Z3_string Z3_API Z3_get_probe_name(Z3_context c, unsigned i);
|
||||
|
|
@ -6456,6 +6484,8 @@ extern "C" {
|
|||
/**
|
||||
\brief Apply tactic \c t to the goal \c g.
|
||||
|
||||
\sa Z3_tactic_apply_ex
|
||||
|
||||
def_API('Z3_tactic_apply', APPLY_RESULT, (_in(CONTEXT), _in(TACTIC), _in(GOAL)))
|
||||
*/
|
||||
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g);
|
||||
|
|
@ -6463,6 +6493,8 @@ extern "C" {
|
|||
/**
|
||||
\brief Apply tactic \c t to the goal \c g using the parameter set \c p.
|
||||
|
||||
\sa Z3_tactic_apply
|
||||
|
||||
def_API('Z3_tactic_apply_ex', APPLY_RESULT, (_in(CONTEXT), _in(TACTIC), _in(GOAL), _in(PARAMS)))
|
||||
*/
|
||||
Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p);
|
||||
|
|
@ -6491,6 +6523,8 @@ extern "C" {
|
|||
/**
|
||||
\brief Return the number of subgoals in the \c Z3_apply_result object returned by #Z3_tactic_apply.
|
||||
|
||||
\sa Z3_apply_result_get_subgoal
|
||||
|
||||
def_API('Z3_apply_result_get_num_subgoals', UINT, (_in(CONTEXT), _in(APPLY_RESULT)))
|
||||
*/
|
||||
unsigned Z3_API Z3_apply_result_get_num_subgoals(Z3_context c, Z3_apply_result r);
|
||||
|
|
@ -6500,6 +6534,8 @@ extern "C" {
|
|||
|
||||
\pre i < Z3_apply_result_get_num_subgoals(c, r)
|
||||
|
||||
\sa Z3_apply_result_get_num_subgoals
|
||||
|
||||
def_API('Z3_apply_result_get_subgoal', GOAL, (_in(CONTEXT), _in(APPLY_RESULT), _in(UINT)))
|
||||
*/
|
||||
Z3_goal Z3_API Z3_apply_result_get_subgoal(Z3_context c, Z3_apply_result r, unsigned i);
|
||||
|
|
@ -6542,6 +6578,10 @@ extern "C" {
|
|||
\remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects.
|
||||
Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
|
||||
|
||||
\sa Z3_mk_simple_solver
|
||||
\sa Z3_mk_solver_for_logic
|
||||
\sa Z3_mk_solver_from_tactic
|
||||
|
||||
def_API('Z3_mk_solver', SOLVER, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_solver Z3_API Z3_mk_solver(Z3_context c);
|
||||
|
|
@ -6569,6 +6609,10 @@ extern "C" {
|
|||
\remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects.
|
||||
Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
|
||||
|
||||
\sa Z3_mk_solver
|
||||
\sa Z3_mk_solver_for_logic
|
||||
\sa Z3_mk_solver_from_tactic
|
||||
|
||||
def_API('Z3_mk_simple_solver', SOLVER, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_solver Z3_API Z3_mk_simple_solver(Z3_context c);
|
||||
|
|
@ -6580,6 +6624,10 @@ extern "C" {
|
|||
\remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects.
|
||||
Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
|
||||
|
||||
\sa Z3_mk_solver
|
||||
\sa Z3_mk_simple_solver
|
||||
\sa Z3_mk_solver_from_tactic
|
||||
|
||||
def_API('Z3_mk_solver_for_logic', SOLVER, (_in(CONTEXT), _in(SYMBOL)))
|
||||
*/
|
||||
Z3_solver Z3_API Z3_mk_solver_for_logic(Z3_context c, Z3_symbol logic);
|
||||
|
|
@ -6592,6 +6640,10 @@ extern "C" {
|
|||
\remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects.
|
||||
Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc.
|
||||
|
||||
\sa Z3_mk_solver
|
||||
\sa Z3_mk_simple_solver
|
||||
\sa Z3_mk_solver_for_logic
|
||||
|
||||
def_API('Z3_mk_solver_from_tactic', SOLVER, (_in(CONTEXT), _in(TACTIC)))
|
||||
*/
|
||||
Z3_solver Z3_API Z3_mk_solver_from_tactic(Z3_context c, Z3_tactic t);
|
||||
|
|
|
|||
Loading…
Reference in a new issue