diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 71f92eeba..45832b5b6 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -124,10 +124,16 @@ extern "C" { } - Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o) { + Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[]) { Z3_TRY; - LOG_Z3_optimize_check(c, o); + LOG_Z3_optimize_check(c, o, num_assumptions, assumptions); RESET_ERROR_CODE(); + for (unsigned i = 0; i < num_assumptions; i++) { + if (!is_expr(to_ast(assumptions[i]))) { + SET_ERROR_CODE(Z3_INVALID_ARG, "assumption is not an expression"); + return Z3_L_UNDEF; + } + } lbool r = l_undef; cancel_eh eh(mk_c(c)->m().limit()); unsigned timeout = to_optimize_ptr(o)->get_params().get_uint("timeout", mk_c(c)->get_timeout()); @@ -137,7 +143,9 @@ extern "C" { scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); try { - r = to_optimize_ptr(o)->optimize(); + expr_ref_vector asms(mk_c(c)->m()); + asms.append(num_assumptions, to_exprs(assumptions)); + r = to_optimize_ptr(o)->optimize(asms); } catch (z3_exception& ex) { if (!mk_c(c)->m().canceled()) { @@ -157,6 +165,22 @@ extern "C" { Z3_CATCH_RETURN(Z3_L_UNDEF); } + Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o) { + Z3_TRY; + LOG_Z3_optimize_get_unsat_core(c, o); + RESET_ERROR_CODE(); + expr_ref_vector core(mk_c(c)->m()); + to_optimize_ptr(o)->get_unsat_core(core); + Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); + mk_c(c)->save_object(v); + for (expr* e : core) { + v->m_ast_vector.push_back(e); + } + RETURN_Z3(of_ast_vector(v)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_string Z3_API Z3_optimize_get_reason_unknown(Z3_context c, Z3_optimize o) { Z3_TRY; LOG_Z3_optimize_to_string(c, o); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index a283571d0..92993da0d 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2455,8 +2455,19 @@ namespace z3 { void pop() { Z3_optimize_pop(ctx(), m_opt); } - check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt); check_error(); return to_check_result(r); } + check_result check() { Z3_lbool r = Z3_optimize_check(ctx(), m_opt, 0, 0); check_error(); return to_check_result(r); } + check_result check(expr_vector const& asms) { + array _asms(n); + for (unsigned i = 0; i < n; i++) { + check_context(*this, asms[i]); + _asms[i] = asms[i]; + } + Z3_lbool r = Z3_optimize_check(ctx(), m_opt, n, _asms.ptr()); + check_error(); + return to_check_result(r); + } model get_model() const { Z3_model m = Z3_optimize_get_model(ctx(), m_opt); check_error(); return model(ctx(), m); } + expr_vector unsat_core() const { Z3_ast_vector r = Z3_optimize_get_unsat_core(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); } void set(params const & p) { Z3_optimize_set_params(ctx(), m_opt, p); check_error(); } expr lower(handle const& h) { Z3_ast r = Z3_optimize_get_lower(ctx(), m_opt, h.h()); diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index 29e5e869a..ce3cc55f7 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -183,9 +183,9 @@ namespace Microsoft.Z3 /// don't use strict inequalities) meets the objectives. /// /// - public Status Check() + public Status Check(params Expr[] assumptions) { - Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject); + Z3_lbool r = (Z3_lbool)Native.Z3_optimize_check(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions)); switch (r) { case Z3_lbool.Z3_L_TRUE: @@ -236,6 +236,25 @@ namespace Microsoft.Z3 } } + /// + /// The unsat core of the last Check. + /// + /// + /// The unsat core is a subset of assumptions + /// The result is empty if Check was not invoked before, + /// if its results was not UNSATISFIABLE, or if core production is disabled. + /// + public BoolExpr[] UnsatCore + { + get + { + Contract.Ensures(Contract.Result() != null); + + ASTVector core = new ASTVector(Context, Native.Z3_optimize_get_unsat_core(Context.nCtx, NativeObject)); + return core.ToBoolExprArray(); + } + } + /// /// Declare an arithmetical maximization objective. /// Return a handle to the objective. The handle is used as diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index c5f8f9449..a91e2a573 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -161,9 +161,23 @@ public class Optimize extends Z3Object { * Produce a model that (when the objectives are bounded and * don't use strict inequalities) meets the objectives. **/ - public Status Check() + public Status Check(Expr... assumptions) { - Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject())); + Z3_lbool r; + if (assumptions == null) { + r = Z3_lbool.fromInt( + Native.optimizeCheck( + getContext().nCtx(), + getNativeObject(), 0, null); + } + else { + r = Z3_lbool.fromInt( + Native.optimizeCheck( + getContext().nCtx(), + getNativeObject(), + assumptions.length, + AST.arrayToNative(assumptions))); + } switch (r) { case Z3_L_TRUE: return Status.SATISFIABLE; @@ -209,6 +223,21 @@ public class Optimize extends Z3Object { } } + /** + * The unsat core of the last {@code Check}. + * Remarks: The unsat core + * is a subset of {@code Assumptions} The result is empty if + * {@code Check} was not invoked before, if its results was not + * {@code UNSATISFIABLE}, or if core production is disabled. + * + * @throws Z3Exception + **/ + public BoolExpr[] getUnsatCore() + { + ASTVector core = new ASTVector(getContext(), Native.optimizeGetUnsatCore(getContext().nCtx(), getNativeObject())); + return core.ToBoolExprArray(); + } + /** * Declare an arithmetical maximization objective. * Return a handle to the objective. The handle is used as diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 231587729..2ad07aee4 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1947,7 +1947,7 @@ struct let minimize (x:optimize) (e:Expr.expr) = mk_handle x (Z3native.optimize_minimize (gc x) x e) let check (x:optimize) = - let r = lbool_of_int (Z3native.optimize_check (gc x) x) in + let r = lbool_of_int (Z3native.optimize_check (gc x) x) 0 [] in match r with | L_TRUE -> Solver.SATISFIABLE | L_FALSE -> Solver.UNSATISFIABLE diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index cefe8bbbb..703105356 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -7311,10 +7311,15 @@ class Optimize(Z3PPObject): """restore to previously created backtracking point""" Z3_optimize_pop(self.ctx.ref(), self.optimize) - def check(self): + def check(self, *assumptions): """Check satisfiability while optimizing objective functions.""" - return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize)) - + assumptions = _get_args(assumptions) + num = len(assumptions) + _assumptions = (Ast * num)() + for i in range(num): + _assumptions[i] = assumptions[i].as_ast() + return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize, num, _assumptions)) + def reason_unknown(self): """Return a string that describes why the last `check()` returned `unknown`.""" return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize) @@ -7326,6 +7331,9 @@ class Optimize(Z3PPObject): except Z3Exception: raise Z3Exception("model is not available") + def unsat_core(self): + return AstVector(Z3_optimize_get_unsat_core(self.ctx.ref(), self.optimize), self.ctx) + def lower(self, obj): if not isinstance(obj, OptimizeObjective): raise Z3Exception("Expecting objective handle returned by maximize/minimize") diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index f49e1b9ce..8f9e2470c 100644 --- a/src/api/z3_optimization.h +++ b/src/api/z3_optimization.h @@ -117,10 +117,12 @@ extern "C" { \brief Check consistency and produce optimal values. \param c - context \param o - optimization context + \param num_assumptions - number of additional assumptions + \param assumptions - the additional assumptions - def_API('Z3_optimize_check', INT, (_in(CONTEXT), _in(OPTIMIZE))) + def_API('Z3_optimize_check', INT, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT), _in_array(2, AST))) */ - Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o); + Z3_lbool Z3_API Z3_optimize_check(Z3_context c, Z3_optimize o, unsigned num_assumptions, Z3_ast const assumptions[]); /** @@ -143,6 +145,14 @@ extern "C" { */ Z3_model Z3_API Z3_optimize_get_model(Z3_context c, Z3_optimize o); + /** + \brief Retrieve the unsat core for the last #Z3_optimize_chec + The unsat core is a subset of the assumptions \c a. + + def_API('Z3_optimize_get_unsat_core', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE))) + */ + Z3_ast_vector Z3_API Z3_optimize_get_unsat_core(Z3_context c, Z3_optimize o); + /** \brief Set parameters on optimization context. diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index be3acc261..89fb4f3cc 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1488,13 +1488,13 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions scoped_ctrl_c ctrlc(eh); scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(m().limit(), rlimit); + expr_ref_vector asms(m()); + asms.append(num_assumptions, assumptions); if (!m_processing_pareto) { - ptr_vector cnstr(m_assertions); - cnstr.append(num_assumptions, assumptions); - get_opt()->set_hard_constraints(cnstr); + get_opt()->set_hard_constraints(m_assertions); } try { - r = get_opt()->optimize(); + r = get_opt()->optimize(asms); if (r == l_true && get_opt()->is_pareto()) { m_processing_pareto = true; } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index a0093191d..87d80babe 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -148,7 +148,7 @@ public: virtual bool empty() = 0; virtual void push() = 0; virtual void pop(unsigned n) = 0; - virtual lbool optimize() = 0; + virtual lbool optimize(expr_ref_vector const& asms) = 0; virtual void set_hard_constraints(ptr_vector & hard) = 0; virtual void display_assignment(std::ostream& out) = 0; virtual bool is_pareto() = 0; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 87da85af5..8941f5a6d 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -130,6 +130,7 @@ namespace opt { m_fm(alloc(generic_model_converter, m, "opt")), m_model_fixed(), m_objective_refs(m), + m_core(m), m_enable_sat(false), m_is_clausal(false), m_pp_neat(false), @@ -173,10 +174,9 @@ namespace opt { } void context::get_unsat_core(expr_ref_vector & r) { - throw default_exception("Unsat cores are not supported with optimization"); + r.append(m_core); } - void context::set_hard_constraints(ptr_vector& fmls) { if (m_scoped_state.set(fmls)) { clear_state(); @@ -253,7 +253,7 @@ namespace opt { m_hard_constraints.append(s.m_hard); } - lbool context::optimize() { + lbool context::optimize(expr_ref_vector const& asms) { if (m_pareto) { return execute_pareto(); } @@ -263,7 +263,10 @@ namespace opt { clear_state(); init_solver(); import_scoped_state(); - normalize(); + normalize(asms); + if (m_hard_constraints.size() == 1 && m.is_false(m_hard_constraints.get(0))) { + return l_false; + } internalize(); update_solver(); if (contains_quantifiers()) { @@ -281,7 +284,7 @@ namespace opt { symbol pri = optp.priority(); IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n"); - lbool is_sat = s.check_sat(0,nullptr); + lbool is_sat = s.check_sat(asms.size(),asms.c_ptr()); TRACE("opt", s.display(tout << "initial search result: " << is_sat << "\n");); if (is_sat != l_false) { s.get_model(m_model); @@ -290,6 +293,9 @@ namespace opt { } if (is_sat != l_true) { TRACE("opt", tout << m_hard_constraints << "\n";); + if (!asms.empty()) { + s.get_unsat_core(m_core); + } return is_sat; } IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n"); @@ -751,22 +757,25 @@ namespace opt { return m_arith.is_numeral(e, n) || m_bv.is_numeral(e, n, sz); } - void context::normalize() { + void context::normalize(expr_ref_vector const& asms) { expr_ref_vector fmls(m); to_fmls(fmls); - simplify_fmls(fmls); + simplify_fmls(fmls, asms); from_fmls(fmls); } - void context::simplify_fmls(expr_ref_vector& fmls) { + void context::simplify_fmls(expr_ref_vector& fmls, expr_ref_vector const& asms) { if (m_is_clausal) { return; } - goal_ref g(alloc(goal, m, true, false)); + goal_ref g(alloc(goal, m, true, !asms.empty())); for (expr* fml : fmls) { g->assert_expr(fml); } + for (expr * a : asms) { + g->assert_expr(a, a); + } tactic_ref tac0 = and_then(mk_simplify_tactic(m, m_params), mk_propagate_values_tactic(m), @@ -788,6 +797,7 @@ namespace opt { set_simplify(tac0.get()); } goal_ref_buffer result; + TRACE("opt", g->display(tout);); (*m_simplify)(g, result); SASSERT(result.size() == 1); goal* r = result[0]; @@ -797,6 +807,12 @@ namespace opt { for (unsigned i = 0; i < r->size(); ++i) { fmls.push_back(r->form(i)); } + if (r->inconsistent()) { + ptr_vector core_elems; + expr_dependency_ref core(r->dep(0), m); + m.linearize(core, core_elems); + m_core.append(core_elems.size(), core_elems.c_ptr()); + } } bool context::is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index) { @@ -1395,6 +1411,7 @@ namespace opt { m_box_index = UINT_MAX; m_model.reset(); m_model_fixed.reset(); + m_core.reset(); } void context::set_pareto(pareto_base* p) { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 1172e68b6..f57e937ba 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -164,6 +164,7 @@ namespace opt { obj_map m_objective_fns; obj_map m_objective_orig; func_decl_ref_vector m_objective_refs; + expr_ref_vector m_core; tactic_ref m_simplify; bool m_enable_sat; bool m_enable_sls; @@ -187,7 +188,7 @@ namespace opt { void pop(unsigned n) override; bool empty() override { return m_scoped_state.m_objectives.empty(); } void set_hard_constraints(ptr_vector & hard) override; - lbool optimize() override; + lbool optimize(expr_ref_vector const& asms) override; void set_model(model_ref& _m) override { m_model = _m; } void get_model_core(model_ref& _m) override; void get_box_model(model_ref& _m, unsigned index) override; @@ -254,7 +255,7 @@ namespace opt { void reset_maxsmts(); void import_scoped_state(); - void normalize(); + void normalize(expr_ref_vector const& asms); void internalize(); bool is_maximize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index); bool is_minimize(expr* fml, app_ref& term, expr_ref& orig_term, unsigned& index); @@ -270,7 +271,7 @@ namespace opt { expr* mk_objective_fn(unsigned index, objective_t ty, unsigned sz, expr*const* args); void to_fmls(expr_ref_vector& fmls); void from_fmls(expr_ref_vector const& fmls); - void simplify_fmls(expr_ref_vector& fmls); + void simplify_fmls(expr_ref_vector& fmls, expr_ref_vector const& asms); void mk_atomic(expr_ref_vector& terms); void update_lower() { update_bound(true); } diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp index 0a2a8f4a1..afa7b79c5 100644 --- a/src/shell/opt_frontend.cpp +++ b/src/shell/opt_frontend.cpp @@ -108,7 +108,8 @@ static unsigned parse_opt(std::istream& in, opt_format f) { unsigned rlimit = std::stoi(gparams::get_value("rlimit")); scoped_timer timer(timeout, &eh); scoped_rlimit _rlimit(m.limit(), rlimit); - lbool r = opt.optimize(); + expr_ref_vector asms(m); + lbool r = opt.optimize(asms); switch (r) { case l_true: std::cout << "sat\n"; break; case l_false: std::cout << "unsat\n"; break;