mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

Add note about minimized unsat cores to C API docs.

Browse source
This commit is contained in:
Bruce Mitchener 2019-08-15 12:23:42 +07:00 • committed by Nikolaj Bjorner
parent 9949f16525
commit d64dc939b2
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/api/z3_api.h
View file

@ -6559,6 +6559,11 @@ extern "C" {
\brief Retrieve the unsat core for the last #Z3_solver_check_assumptions \brief Retrieve the unsat core for the last #Z3_solver_check_assumptions
The unsat core is a subset of the assumptions \c a. The unsat core is a subset of the assumptions \c a.
By default, the unsat core will not be minimized. Generation of a minimized
unsat core can be enabled via the `"sat.core.minimize"` and `"smt.core.minimize"`
settings for SAT and SMT cores respectively. Generation of minimized unsat cores
will be more expensive.
def_API('Z3_solver_get_unsat_core', AST_VECTOR, (_in(CONTEXT), _in(SOLVER))) def_API('Z3_solver_get_unsat_core', AST_VECTOR, (_in(CONTEXT), _in(SOLVER)))
*/ */
Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s); Z3_ast_vector Z3_API Z3_solver_get_unsat_core(Z3_context c, Z3_solver s);