mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

update documentation on models associated with solver objects

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-22 01:16:16 -07:00
parent b243ac945f
commit dca3ce6b24
1 changed files with 12 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/api/z3_api.h
View file

@ -6620,6 +6620,13 @@ END_MLAPI_EXCLUDE
/** /**
\brief Create a new (incremental) solver. \brief Create a new (incremental) solver.
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.
The function #Z3_solver_get_model can also be used even
if the result is \c Z3_L_UNDEF, but the returned model
is not guaranteed to satisfy quantified assertions.
def_API('Z3_mk_simple_solver', SOLVER, (_in(CONTEXT),)) def_API('Z3_mk_simple_solver', SOLVER, (_in(CONTEXT),))
*/ */
Z3_solver Z3_API Z3_mk_simple_solver(__in Z3_context c); Z3_solver Z3_API Z3_mk_simple_solver(__in Z3_context c);
@ -6757,8 +6764,11 @@ END_MLAPI_EXCLUDE
\brief Check whether the assertions in a given solver are consistent or not. \brief Check whether the assertions in a given solver are consistent or not.
The function #Z3_solver_get_model retrieves a model if the The function #Z3_solver_get_model retrieves a model if the
assertions are not unsatisfiable (i.e., the result is not \c assertions is satisfiable (i.e., the result is \c
Z3_L_FALSE) and model construction is enabled. Z3_L_TRUE) and model construction is enabled.
Note that if the call returns 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.
The function #Z3_solver_get_proof retrieves a proof if proof The function #Z3_solver_get_proof retrieves a proof if proof
generation was enabled when the context was created, and the generation was enabled when the context was created, and the