mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Improve intra-doc linking.

Browse source
This commit is contained in:
Bruce Mitchener 2018-11-21 06:55:47 +07:00
parent 2cc654081c
commit 236f85d82b
3 changed files with 98 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

41
src/api/z3_api.h
View file

@ -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);

18
src/api/z3_fixedpoint.h
View file

@ -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,

39
src/api/z3_optimization.h
View file

@ -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);