mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 03:45:51 +00:00
docs: Fix a number of identifier formatting issues.
This commit is contained in:
Bruce Mitchener
Nikolaj Bjorner
parent
077f518241
commit
f90439fdc5
1 changed files with 22 additions and 22 deletions
|
|
@ -4568,7 +4568,7 @@ extern "C" {
|
|||
Z3_sort Z3_API Z3_get_sort(Z3_context c, Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Return true if the given expression \c t is well sorted.
|
||||
\brief Return \c true if the given expression \c t is well sorted.
|
||||
|
||||
def_API('Z3_is_well_sorted', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
|
|
@ -4599,7 +4599,7 @@ extern "C" {
|
|||
bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Return true if the given AST is a real algebraic number.
|
||||
\brief Return \c true if the given AST is a real algebraic number.
|
||||
|
||||
def_API('Z3_is_algebraic_number', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
|
|
@ -5286,14 +5286,14 @@ extern "C" {
|
|||
void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value);
|
||||
|
||||
/**
|
||||
\brief Increment the reference counter of the given Z3_func_entry object.
|
||||
\brief Increment the reference counter of the given \c Z3_func_entry object.
|
||||
|
||||
def_API('Z3_func_entry_inc_ref', VOID, (_in(CONTEXT), _in(FUNC_ENTRY)))
|
||||
*/
|
||||
void Z3_API Z3_func_entry_inc_ref(Z3_context c, Z3_func_entry e);
|
||||
|
||||
/**
|
||||
\brief Decrement the reference counter of the given Z3_func_entry object.
|
||||
\brief Decrement the reference counter of the given \c Z3_func_entry object.
|
||||
|
||||
def_API('Z3_func_entry_dec_ref', VOID, (_in(CONTEXT), _in(FUNC_ENTRY)))
|
||||
*/
|
||||
|
|
@ -5302,7 +5302,7 @@ extern "C" {
|
|||
/**
|
||||
\brief Return the value of this point.
|
||||
|
||||
A Z3_func_entry object represents an element in the finite map used to encode
|
||||
A \c Z3_func_entry object represents an element in the finite map used to encode
|
||||
a function interpretation.
|
||||
|
||||
\sa Z3_func_interp_get_entry
|
||||
|
|
@ -5312,7 +5312,7 @@ extern "C" {
|
|||
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e);
|
||||
|
||||
/**
|
||||
\brief Return the number of arguments in a Z3_func_entry object.
|
||||
\brief Return the number of arguments in a \c Z3_func_entry object.
|
||||
|
||||
\sa Z3_func_interp_get_entry
|
||||
|
||||
|
|
@ -5321,7 +5321,7 @@ extern "C" {
|
|||
unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e);
|
||||
|
||||
/**
|
||||
\brief Return an argument of a Z3_func_entry object.
|
||||
\brief Return an argument of a \c Z3_func_entry object.
|
||||
|
||||
\pre i < Z3_func_entry_get_num_args(c, e)
|
||||
|
||||
|
|
@ -5377,11 +5377,11 @@ extern "C" {
|
|||
|
||||
The default mode for pretty printing AST nodes is to produce
|
||||
SMT-LIB style output where common subexpressions are printed
|
||||
at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL.
|
||||
at each occurrence. The mode is called \c Z3_PRINT_SMTLIB_FULL.
|
||||
To print shared common subexpressions only once,
|
||||
use the Z3_PRINT_LOW_LEVEL mode.
|
||||
use the \c Z3_PRINT_LOW_LEVEL mode.
|
||||
To print in way that conforms to SMT-LIB standards and uses let
|
||||
expressions to share common sub-expressions use Z3_PRINT_SMTLIB2_COMPLIANT.
|
||||
expressions to share common sub-expressions use \c Z3_PRINT_SMTLIB2_COMPLIANT.
|
||||
|
||||
\sa Z3_ast_to_string
|
||||
\sa Z3_pattern_to_string
|
||||
|
|
@ -5525,7 +5525,7 @@ extern "C" {
|
|||
/**
|
||||
\brief Register a Z3 error handler.
|
||||
|
||||
A call to a Z3 function may return a non Z3_OK error code, when
|
||||
A call to a Z3 function may return a non \c Z3_OK error code, when
|
||||
it is not used correctly. An error handler can be registered
|
||||
and will be called in this case. To disable the use of the
|
||||
error handler, simply register with \c h=NULL.
|
||||
|
|
@ -5616,14 +5616,14 @@ extern "C" {
|
|||
of formulas, that can be solved and/or transformed using
|
||||
tactics and solvers.
|
||||
|
||||
If models == true, then model generation is enabled for the new goal.
|
||||
If \c models is \c true, then model generation is enabled for the new goal.
|
||||
|
||||
If unsat_cores == true, then unsat core generation is enabled for the new goal.
|
||||
If \c unsat_cores is \c true, then unsat core generation is enabled for the new goal.
|
||||
|
||||
If proofs == true, then proof generation is enabled for the new goal. Remark, the
|
||||
Z3 context c must have been created with proof generation support.
|
||||
If \c proofs is \c true, then proof generation is enabled for the new goal. Remark, the
|
||||
Z3 context \c c must have been created with proof generation support.
|
||||
|
||||
\remark Reference counting must be used to manage goals, even when the Z3_context was
|
||||
\remark Reference counting must be used to manage goals, even when the \c Z3_context was
|
||||
created using #Z3_mk_context instead of #Z3_mk_context_rc.
|
||||
|
||||
def_API('Z3_mk_goal', GOAL, (_in(CONTEXT), _in(BOOL), _in(BOOL), _in(BOOL)))
|
||||
|
|
@ -5668,7 +5668,7 @@ extern "C" {
|
|||
void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Return true if the given goal contains the formula \c false.
|
||||
\brief Return \c true if the given goal contains the formula \c false.
|
||||
|
||||
def_API('Z3_goal_inconsistent', BOOL, (_in(CONTEXT), _in(GOAL)))
|
||||
*/
|
||||
|
|
@ -5712,14 +5712,14 @@ extern "C" {
|
|||
unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g);
|
||||
|
||||
/**
|
||||
\brief Return true if the goal is empty, and it is precise or the product of a under approximation.
|
||||
\brief Return \c true if the goal is empty, and it is precise or the product of a under approximation.
|
||||
|
||||
def_API('Z3_goal_is_decided_sat', BOOL, (_in(CONTEXT), _in(GOAL)))
|
||||
*/
|
||||
bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g);
|
||||
|
||||
/**
|
||||
\brief Return true if the goal contains false, and it is precise or the product of an over approximation.
|
||||
\brief Return \c true if the goal contains false, and it is precise or the product of an over approximation.
|
||||
|
||||
def_API('Z3_goal_is_decided_unsat', BOOL, (_in(CONTEXT), _in(GOAL)))
|
||||
*/
|
||||
|
|
@ -5817,7 +5817,7 @@ extern "C" {
|
|||
|
||||
/**
|
||||
\brief Return a tactic that applies \c t1 to a given goal and \c t2
|
||||
to every subgoal produced by t1.
|
||||
to every subgoal produced by \c t1.
|
||||
|
||||
def_API('Z3_tactic_and_then', TACTIC, (_in(CONTEXT), _in(TACTIC), _in(TACTIC)))
|
||||
*/
|
||||
|
|
@ -5840,7 +5840,7 @@ extern "C" {
|
|||
|
||||
/**
|
||||
\brief Return a tactic that applies \c t1 to a given goal and then \c t2
|
||||
to every subgoal produced by t1. The subgoals are processed in parallel.
|
||||
to every subgoal produced by \c t1. The subgoals are processed in parallel.
|
||||
|
||||
def_API('Z3_tactic_par_and_then', TACTIC, (_in(CONTEXT), _in(TACTIC), _in(TACTIC)))
|
||||
*/
|
||||
|
|
@ -6017,7 +6017,7 @@ extern "C" {
|
|||
unsigned Z3_API Z3_get_num_probes(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Return the name of the i probe.
|
||||
\brief Return the name of the \c i probe.
|
||||
|
||||
\pre i < Z3_get_num_probes(c)
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue