More see also content in C API docs.

Z3Prover · Aug 13, 2019 · e89bb37 · e89bb37
1 parent 375c0ff
commit e89bb37
Show file tree

Hide file tree

Showing 3 changed files with 89 additions and 5 deletions.
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
@@ -1456,6 +1456,9 @@ extern "C" {
        Z3_global_param_set('pp.decimal', 'true')
        will set the parameter "decimal" in the module "pp" to true.
 
+       \sa Z3_global_param_get
+       \sa Z3_global_param_reset_all
+
        def_API('Z3_global_param_set', VOID, (_in(STRING), _in(STRING)))
     */
     void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value);
@@ -1465,6 +1468,7 @@ extern "C" {
        \brief Restore the value of all global (and module) parameters.
        This command will not affect already created objects (such as tactics and solvers).
 
+       \sa Z3_global_param_get
        \sa Z3_global_param_set
 
        def_API('Z3_global_param_reset_all', VOID, ())
@@ -1476,6 +1480,7 @@ extern "C" {
 
        Returns \c false if the parameter value does not exist.
 
+       \sa Z3_global_param_reset_all
        \sa Z3_global_param_set
 
        \remark This function cannot be invoked simultaneously from different threads without synchronization.
@@ -1997,6 +2002,10 @@ extern "C" {
                         sort reference is 0, then the value in sort_refs should be an index referring to
                         one of the recursive datatypes that is declared.
 
+       \sa Z3_del_constructor
+       \sa Z3_mk_constructor_list
+       \sa Z3_query_constructor
+
        def_API('Z3_mk_constructor', CONSTRUCTOR, (_in(CONTEXT), _in(SYMBOL), _in(SYMBOL), _in(UINT), _in_array(3, SYMBOL), _in_array(3, SORT), _in_array(3, UINT)))
     */
     Z3_constructor Z3_API Z3_mk_constructor(Z3_context c,
@@ -2014,6 +2023,8 @@ extern "C" {
        \param c logical context.
        \param constr constructor.
 
+       \sa Z3_mk_constructor
+
        def_API('Z3_del_constructor', VOID, (_in(CONTEXT), _in(CONSTRUCTOR)))
     */
     void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr);
@@ -2027,6 +2038,10 @@ extern "C" {
        \param num_constructors number of constructors passed in.
        \param constructors array of constructor containers.
 
+       \sa Z3_mk_constructor
+       \sa Z3_mk_constructor_list
+       \sa Z3_mk_datatypes
+
        def_API('Z3_mk_datatype', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _inout_array(2, CONSTRUCTOR)))
     */
     Z3_sort Z3_API Z3_mk_datatype(Z3_context c,
@@ -2041,6 +2056,9 @@ extern "C" {
        \param num_constructors number of constructors in list.
        \param constructors list of constructors.
 
+       \sa Z3_del_constructor_list
+       \sa Z3_mk_constructor
+
        def_API('Z3_mk_constructor_list', CONSTRUCTOR_LIST, (_in(CONTEXT), _in(UINT), _in_array(1, CONSTRUCTOR)))
     */
     Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c,
@@ -2055,6 +2073,8 @@ extern "C" {
        \param c logical context.
        \param clist constructor list container.
 
+       \sa Z3_mk_constructor_list
+
        def_API('Z3_del_constructor_list', VOID, (_in(CONTEXT), _in(CONSTRUCTOR_LIST)))
     */
     void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist);
@@ -2068,6 +2088,10 @@ extern "C" {
        \param sorts array of datatype sorts.
        \param constructor_lists list of constructors, one list per sort.
 
+       \sa Z3_mk_constructor
+       \sa Z3_mk_constructor_list
+       \sa Z3_mk_datatype
+
        def_API('Z3_mk_datatypes', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, SYMBOL), _out_array(1, SORT), _inout_array(1, CONSTRUCTOR_LIST)))
     */
     void Z3_API Z3_mk_datatypes(Z3_context c,
@@ -2086,6 +2110,8 @@ extern "C" {
        \param tester constructor test function declaration, allocated by user.
        \param accessors array of accessor function declarations allocated by user. The array must contain num_fields elements.
 
+       \sa Z3_mk_constructor
+
        def_API('Z3_query_constructor', VOID, (_in(CONTEXT), _in(CONSTRUCTOR), _in(UINT), _out(FUNC_DECL), _out(FUNC_DECL), _out_array(2, FUNC_DECL)))
     */
     void Z3_API Z3_query_constructor(Z3_context c,
@@ -2114,6 +2140,8 @@ extern "C" {
        application.
 
        \sa Z3_mk_app
+       \sa Z3_mk_fresh_func_decl
+       \sa Z3_mk_rec_func_decl
 
        def_API('Z3_mk_func_decl', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT)))
     */
@@ -2126,7 +2154,9 @@ extern "C" {
     /**
        \brief Create a constant or function application.
 
+       \sa Z3_mk_fresh_func_decl
        \sa Z3_mk_func_decl
+       \sa Z3_mk_rec_func_decl
 
        def_API('Z3_mk_app', AST, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT), _in_array(2, AST)))
     */
@@ -2145,8 +2175,9 @@ extern "C" {
        Z3_ast n            = Z3_mk_app(c, d, 0, 0);
        \endcode
 
-       \sa Z3_mk_func_decl
        \sa Z3_mk_app
+       \sa Z3_mk_fresh_const
+       \sa Z3_mk_func_decl
 
        def_API('Z3_mk_const', AST, (_in(CONTEXT), _in(SYMBOL), _in(SORT)))
     */
@@ -2176,8 +2207,10 @@ extern "C" {
 
        \remark If \c prefix is \c NULL, then it is assumed to be the empty string.
 
-       \sa Z3_mk_func_decl
        \sa Z3_mk_app
+       \sa Z3_mk_const
+       \sa Z3_mk_fresh_func_decl
+       \sa Z3_mk_func_decl
 
        def_API('Z3_mk_fresh_const', AST, (_in(CONTEXT), _in(STRING), _in(SORT)))
     */
@@ -2197,8 +2230,9 @@ extern "C" {
        The function #Z3_mk_app can be used to create a constant or function
        application.
 
-       \sa Z3_mk_app
        \sa Z3_add_rec_def
+       \sa Z3_mk_app
+       \sa Z3_mk_func_decl
 
        def_API('Z3_mk_rec_func_decl', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT)))
     */
@@ -5557,21 +5591,27 @@ extern "C" {
     /**
        \brief Return Z3 version number information.
 
+       \sa Z3_get_full_version
+
        def_API('Z3_get_version', VOID, (_out(UINT), _out(UINT), _out(UINT), _out(UINT)))
     */
     void Z3_API Z3_get_version(unsigned * major, unsigned * minor, unsigned * build_number, unsigned * revision_number);
 
     /**
-        \brief Return a string that fully describes the version of Z3 in use.
+       \brief Return a string that fully describes the version of Z3 in use.
+
+       \sa Z3_get_version
 
-        def_API('Z3_get_full_version', STRING, ())
+       def_API('Z3_get_full_version', STRING, ())
     */
     Z3_string Z3_API Z3_get_full_version(void);
 
     /**
        \brief Enable tracing messages tagged as \c tag when Z3 is compiled in debug mode.
        It is a NOOP otherwise
 
+       \sa Z3_disable_trace
+
        def_API('Z3_enable_trace', VOID, (_in(STRING),))
     */
     void Z3_API Z3_enable_trace(Z3_string tag);
@@ -5580,6 +5620,8 @@ extern "C" {
        \brief Disable tracing messages tagged as \c tag when Z3 is compiled in debug mode.
        It is a NOOP otherwise
 
+       \sa Z3_enable_trace
+
        def_API('Z3_disable_trace', VOID, (_in(STRING),))
     */
     void Z3_API Z3_disable_trace(Z3_string tag);

diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h
@@ -218,6 +218,9 @@ extern "C" {
         \param c logical context
         \param s target sort
 
+        \sa Z3_mk_fpa_inf
+        \sa Z3_mk_fpa_zero
+
         def_API('Z3_mk_fpa_nan', AST, (_in(CONTEXT),_in(SORT)))
     */
     Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s);
@@ -231,6 +234,9 @@ extern "C" {
 
         When \c negative is \c true, -oo will be generated instead of +oo.
 
+        \sa Z3_mk_fpa_nan
+        \sa Z3_mk_fpa_zero
+
         def_API('Z3_mk_fpa_inf', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
     */
     Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative);
@@ -244,6 +250,9 @@ extern "C" {
 
         When \c negative is \c true, -zero will be generated instead of +zero.
 
+        \sa Z3_mk_fpa_inf
+        \sa Z3_mk_fpa_nan
+
         def_API('Z3_mk_fpa_zero', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
     */
     Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative);
@@ -262,6 +271,13 @@ extern "C" {
         \param exp exponent
         \param sig significand
 
+        \sa Z3_mk_fpa_numeral_double
+        \sa Z3_mk_fpa_numeral_float
+        \sa Z3_mk_fpa_numeral_int
+        \sa Z3_mk_fpa_numeral_int_uint
+        \sa Z3_mk_fpa_numeral_int64_uint64
+        \sa Z3_mk_numeral
+
         def_API('Z3_mk_fpa_fp', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
     */
     Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig);
@@ -278,6 +294,11 @@ extern "C" {
 
         \c ty must be a FloatingPoint sort
 
+        \sa Z3_mk_fpa_fp
+        \sa Z3_mk_fpa_numeral_double
+        \sa Z3_mk_fpa_numeral_int
+        \sa Z3_mk_fpa_numeral_int_uint
+        \sa Z3_mk_fpa_numeral_int64_uint64
         \sa Z3_mk_numeral
 
         def_API('Z3_mk_fpa_numeral_float', AST, (_in(CONTEXT), _in(FLOAT), _in(SORT)))
@@ -296,6 +317,11 @@ extern "C" {
 
         \c ty must be a FloatingPoint sort
 
+        \sa Z3_mk_fpa_fp
+        \sa Z3_mk_fpa_numeral_float
+        \sa Z3_mk_fpa_numeral_int
+        \sa Z3_mk_fpa_numeral_int_uint
+        \sa Z3_mk_fpa_numeral_int64_uint64
         \sa Z3_mk_numeral
 
         def_API('Z3_mk_fpa_numeral_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT)))
@@ -311,6 +337,11 @@ extern "C" {
 
         \c ty must be a FloatingPoint sort
 
+        \sa Z3_mk_fpa_fp
+        \sa Z3_mk_fpa_numeral_double
+        \sa Z3_mk_fpa_numeral_float
+        \sa Z3_mk_fpa_numeral_int_uint
+        \sa Z3_mk_fpa_numeral_int64_uint64
         \sa Z3_mk_numeral
 
         def_API('Z3_mk_fpa_numeral_int', AST, (_in(CONTEXT), _in(INT), _in(SORT)))
@@ -328,6 +359,11 @@ extern "C" {
 
         \c ty must be a FloatingPoint sort
 
+        \sa Z3_mk_fpa_fp
+        \sa Z3_mk_fpa_numeral_double
+        \sa Z3_mk_fpa_numeral_float
+        \sa Z3_mk_fpa_numeral_int
+        \sa Z3_mk_fpa_numeral_int64_uint64
         \sa Z3_mk_numeral
 
         def_API('Z3_mk_fpa_numeral_int_uint', AST, (_in(CONTEXT), _in(BOOL), _in(INT), _in(UINT), _in(SORT)))
@@ -345,6 +381,11 @@ extern "C" {
 
         \c ty must be a FloatingPoint sort
 
+        \sa Z3_mk_fpa_fp
+        \sa Z3_mk_fpa_numeral_double
+        \sa Z3_mk_fpa_numeral_float
+        \sa Z3_mk_fpa_numeral_int
+        \sa Z3_mk_fpa_numeral_int_uint
         \sa Z3_mk_numeral
 
         def_API('Z3_mk_fpa_numeral_int64_uint64', AST, (_in(CONTEXT), _in(BOOL), _in(INT64), _in(UINT64), _in(SORT)))

diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h
@@ -82,6 +82,7 @@ extern "C" {
        \param id - optional identifier to group soft constraints
 
        \sa Z3_optimize_assert
+       \sa Z3_optimize_assert_and_track
 
        def_API('Z3_optimize_assert_soft', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(STRING), _in(SYMBOL)))
     */