Merge branch 'master' of https://github.com/z3prover/z3

src/api/z3_api.h

@@ -1751,6 +1751,7 @@ extern "C" {
        NB. Not all integers can be passed to this function.
        The legal range of unsigned integers is 0 to 2^30-1.
 
+       \sa Z3_get_symbol_int
        \sa Z3_mk_string_symbol
 
        def_API('Z3_mk_int_symbol', SYMBOL, (_in(CONTEXT), _in(INT)))
@@ -1762,6 +1763,7 @@ extern "C" {
 
        Symbols are used to name several term and type constructors.
 
+       \sa Z3_get_symbol_string
        \sa Z3_mk_int_symbol
 
        def_API('Z3_mk_string_symbol', SYMBOL, (_in(CONTEXT), _in(STRING)))
@@ -5950,9 +5952,9 @@ extern "C" {
        on how it is used and how its parameters are set.
 
        If the solver is used in a non incremental way (i.e. no calls to
-       `Z3_solver_push()` or `Z3_solver_pop()`, and no calls to
+       #Z3_solver_push() or #Z3_solver_pop(), and no calls to
-       `Z3_solver_assert()` or `Z3_solver_assert_and_track()` after checking
+       #Z3_solver_assert() or #Z3_solver_assert_and_track() after checking
-       satisfiability without an intervening `Z3_solver_reset()`) then solver1
+       satisfiability without an intervening #Z3_solver_reset()) then solver1
        will be used. This solver will apply Z3's "default" tactic.
 
        The "default" tactic will attempt to probe the logic used by the
@@ -5986,13 +5988,13 @@ extern "C" {
 
        This is equivalent to applying the "smt" tactic.
 
-       Unlike `Z3_mk_solver()` this solver
+       Unlike #Z3_mk_solver() this solver
          - Does not attempt to apply any logic specific tactics.
          - Does not change its behaviour based on whether it used
            incrementally/non-incrementally.
 
        Note that these differences can result in very different performance
-       compared to `Z3_mk_solver()`.
+       compared to #Z3_mk_solver().
 
        The function #Z3_solver_get_model retrieves a model if the
        assertions is satisfiable (i.e., the result is \c
@@ -6195,6 +6197,8 @@ extern "C" {
        generation was enabled when the context was created, and the
        assertions are unsatisfiable (i.e., the result is \c Z3_L_FALSE).
 
+       \sa Z3_solver_check_assumptions
+
        def_API('Z3_solver_check', INT, (_in(CONTEXT), _in(SOLVER)))
     */
     Z3_lbool Z3_API Z3_solver_check(Z3_context c, Z3_solver s);

src/api/z3_fixedpoint.h

@@ -138,7 +138,7 @@ extern "C" {
        Each conjunct encodes values of the bound variables of the query that are satisfied.
        In PDR mode, the returned answer is a single conjunction.
 
-       When used in Datalog mode the previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE.
+       When used in Datalog mode the previous call to #Z3_fixedpoint_query must have returned Z3_L_TRUE.
        When used with the PDR engine, the previous call must have been either Z3_L_TRUE or Z3_L_FALSE.
 
        def_API('Z3_fixedpoint_get_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT)))

src/api/z3_fpa.h

@@ -229,7 +229,7 @@ extern "C" {
         \param s target sort
         \param negative indicates whether the result should be negative
 
-        When \c negative is true, -oo will be generated instead of +oo.
+        When \c negative is \c true, -oo will be generated instead of +oo.
 
         def_API('Z3_mk_fpa_inf', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
     */
@@ -242,7 +242,7 @@ extern "C" {
         \param s target sort
         \param negative indicates whether the result should be negative
 
-        When \c negative is true, -zero will be generated instead of +zero.
+        When \c negative is \c true, -zero will be generated instead of +zero.
 
         def_API('Z3_mk_fpa_zero', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
     */

src/api/z3_optimization.h

@@ -55,6 +55,8 @@ extern "C" {
     /**
        \brief Assert hard constraint to the optimization context.
 
+       \sa Z3_optimize_assert_soft
+
        def_API('Z3_optimize_assert', VOID, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
     */
     void Z3_API Z3_optimize_assert(Z3_context c, Z3_optimize o, Z3_ast a);
@@ -67,6 +69,8 @@ extern "C" {
        \param weight - a positive weight, penalty for violating soft constraint
        \param id - optional identifier to group soft constraints
 
+       \sa Z3_optimize_assert
+
        def_API('Z3_optimize_assert_soft', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(STRING), _in(SYMBOL)))
     */
     unsigned Z3_API Z3_optimize_assert_soft(Z3_context c, Z3_optimize o, Z3_ast a, Z3_string weight, Z3_symbol id);
@@ -76,6 +80,9 @@ extern "C" {
        \param c - context
        \param o - optimization context
        \param t - arithmetical term
+
+       \sa Z3_optimize_minimize
+
        def_API('Z3_optimize_maximize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
     */
     unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t);
@@ -86,6 +93,8 @@ extern "C" {
        \param o - optimization context
        \param t - arithmetical term
 
+       \sa Z3_optimize_maximize
+
        def_API('Z3_optimize_minimize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST)))
     */
     unsigned Z3_API Z3_optimize_minimize(Z3_context c, Z3_optimize o, Z3_ast t);