mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Mark up Z3_L_TRUE and friends correctly in the docs.
This commit is contained in:
parent
ea0d253308
commit
42d2a46826
|
@ -4416,7 +4416,7 @@ extern "C" {
|
|||
bool Z3_API Z3_is_well_sorted(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Return Z3_L_TRUE if \c a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.
|
||||
\brief Return \c Z3_L_TRUE if \c a is true, \c Z3_L_FALSE if it is false, and \c Z3_L_UNDEF otherwise.
|
||||
|
||||
def_API('Z3_get_bool_value', INT, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
|
@ -6227,7 +6227,7 @@ extern "C" {
|
|||
The function #Z3_solver_get_model retrieves a model if the
|
||||
assertions is satisfiable (i.e., the result is \c
|
||||
Z3_L_TRUE) and model construction is enabled.
|
||||
Note that if the call returns Z3_L_UNDEF, Z3 does not
|
||||
Note that if the call returns \c Z3_L_UNDEF, Z3 does not
|
||||
ensure that calls to #Z3_solver_get_model succeed and any models
|
||||
produced in this case are not guaranteed to satisfy the assertions.
|
||||
|
||||
|
@ -6269,7 +6269,7 @@ extern "C" {
|
|||
the current context implies that they are equal.
|
||||
|
||||
A side-effect of the function is a satisfiability check on the assertions on the solver that is passed in.
|
||||
The function return Z3_L_FALSE if the current assertions are not satisfiable.
|
||||
The function return \c Z3_L_FALSE if the current assertions are not satisfiable.
|
||||
|
||||
def_API('Z3_get_implied_equalities', INT, (_in(CONTEXT), _in(SOLVER), _in(UINT), _in_array(2, AST), _out_array(2, UINT)))
|
||||
*/
|
||||
|
@ -6342,7 +6342,7 @@ extern "C" {
|
|||
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s);
|
||||
|
||||
/**
|
||||
\brief Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for
|
||||
\brief Return a brief justification for an "unknown" result (i.e., \c Z3_L_UNDEF) for
|
||||
the commands #Z3_solver_check and #Z3_solver_check_assumptions
|
||||
|
||||
def_API('Z3_solver_get_reason_unknown', STRING, (_in(CONTEXT), _in(SOLVER)))
|
||||
|
|
|
@ -106,9 +106,9 @@ extern "C" {
|
|||
\endcode
|
||||
|
||||
query returns
|
||||
- Z3_L_FALSE if the query is unsatisfiable.
|
||||
- Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling #Z3_fixedpoint_get_answer.
|
||||
- Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.
|
||||
- \c Z3_L_FALSE if the query is unsatisfiable.
|
||||
- \c Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling #Z3_fixedpoint_get_answer.
|
||||
- \c Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.
|
||||
|
||||
def_API('Z3_fixedpoint_query', INT, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST)))
|
||||
*/
|
||||
|
@ -120,9 +120,9 @@ extern "C" {
|
|||
The queries are encoded as relations (function declarations).
|
||||
|
||||
query returns
|
||||
- Z3_L_FALSE if the query is unsatisfiable.
|
||||
- Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling #Z3_fixedpoint_get_answer.
|
||||
- Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.
|
||||
- \c Z3_L_FALSE if the query is unsatisfiable.
|
||||
- \c Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling #Z3_fixedpoint_get_answer.
|
||||
- \c Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.
|
||||
|
||||
def_API('Z3_fixedpoint_query_relations', INT, (_in(CONTEXT), _in(FIXEDPOINT), _in(UINT), _in_array(2, FUNC_DECL)))
|
||||
*/
|
||||
|
@ -138,8 +138,8 @@ 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 with the PDR engine, the previous call must have been either Z3_L_TRUE or Z3_L_FALSE.
|
||||
When used in Datalog mode the previous call to #Z3_fixedpoint_query must have returned \c Z3_L_TRUE.
|
||||
When used with the PDR engine, the previous call must have been either \c Z3_L_TRUE or \c Z3_L_FALSE.
|
||||
|
||||
def_API('Z3_fixedpoint_get_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT)))
|
||||
*/
|
||||
|
@ -148,7 +148,7 @@ extern "C" {
|
|||
/**
|
||||
\brief Retrieve a string that describes the last status returned by #Z3_fixedpoint_query.
|
||||
|
||||
Use this method when #Z3_fixedpoint_query returns Z3_L_UNDEF.
|
||||
Use this method when #Z3_fixedpoint_query returns \c Z3_L_UNDEF.
|
||||
|
||||
def_API('Z3_fixedpoint_get_reason_unknown', STRING, (_in(CONTEXT), _in(FIXEDPOINT) ))
|
||||
*/
|
||||
|
|
|
@ -142,7 +142,7 @@ extern "C" {
|
|||
/**
|
||||
\brief Retrieve a string that describes the last status returned by #Z3_optimize_check.
|
||||
|
||||
Use this method when #Z3_optimize_check returns Z3_L_UNDEF.
|
||||
Use this method when #Z3_optimize_check returns \c Z3_L_UNDEF.
|
||||
|
||||
def_API('Z3_optimize_get_reason_unknown', STRING, (_in(CONTEXT), _in(OPTIMIZE) ))
|
||||
*/
|
||||
|
|
|
@ -37,9 +37,9 @@ extern "C" {
|
|||
\endcode
|
||||
|
||||
query returns
|
||||
- Z3_L_FALSE if the query is unsatisfiable.
|
||||
- Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling #Z3_fixedpoint_get_answer.
|
||||
- Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.
|
||||
- \c Z3_L_FALSE if the query is unsatisfiable.
|
||||
- \c Z3_L_TRUE if the query is satisfiable. Obtain the answer by calling #Z3_fixedpoint_get_answer.
|
||||
- \c Z3_L_UNDEF if the query was interrupted, timed out or otherwise failed.
|
||||
|
||||
def_API('Z3_fixedpoint_query_from_lvl', INT, (_in(CONTEXT), _in(FIXEDPOINT), _in(AST), _in(UINT)))
|
||||
*/
|
||||
|
@ -48,7 +48,7 @@ extern "C" {
|
|||
/**
|
||||
\brief Retrieve a bottom-up (from query) sequence of ground facts
|
||||
|
||||
The previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE.
|
||||
The previous call to Z3_fixedpoint_query must have returned \c Z3_L_TRUE.
|
||||
|
||||
def_API('Z3_fixedpoint_get_ground_sat_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT)))
|
||||
*/
|
||||
|
|
Loading…
Reference in a new issue