mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
commit
b540868cd7
|
@ -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<reslimit> 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);
|
||||
|
|
|
@ -2455,8 +2455,20 @@ 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) {
|
||||
unsigned n = asms.size();
|
||||
array<Z3_ast> _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_opt); 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());
|
||||
|
|
|
@ -183,9 +183,9 @@ namespace Microsoft.Z3
|
|||
/// don't use strict inequalities) meets the objectives.
|
||||
/// </summary>
|
||||
///
|
||||
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
|
|||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// The unsat core of the last <c>Check</c>.
|
||||
/// </summary>
|
||||
/// <remarks>
|
||||
/// The unsat core is a subset of <c>assumptions</c>
|
||||
/// The result is empty if <c>Check</c> was not invoked before,
|
||||
/// if its results was not <c>UNSATISFIABLE</c>, or if core production is disabled.
|
||||
/// </remarks>
|
||||
public BoolExpr[] UnsatCore
|
||||
{
|
||||
get
|
||||
{
|
||||
Contract.Ensures(Contract.Result<Expr[]>() != null);
|
||||
|
||||
ASTVector core = new ASTVector(Context, Native.Z3_optimize_get_unsat_core(Context.nCtx, NativeObject));
|
||||
return core.ToBoolExprArray();
|
||||
}
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
/// Declare an arithmetical maximization objective.
|
||||
/// Return a handle to the objective. The handle is used as
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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")
|
||||
|
|
|
@ -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.
|
||||
|
||||
|
|
|
@ -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<expr> 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;
|
||||
}
|
||||
|
|
|
@ -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<expr> & hard) = 0;
|
||||
virtual void display_assignment(std::ostream& out) = 0;
|
||||
virtual bool is_pareto() = 0;
|
||||
|
|
|
@ -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<expr>& 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");
|
||||
|
@ -749,22 +755,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),
|
||||
|
@ -786,6 +795,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];
|
||||
|
@ -795,6 +805,12 @@ namespace opt {
|
|||
for (unsigned i = 0; i < r->size(); ++i) {
|
||||
fmls.push_back(r->form(i));
|
||||
}
|
||||
if (r->inconsistent()) {
|
||||
ptr_vector<expr> 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) {
|
||||
|
@ -1393,6 +1409,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) {
|
||||
|
|
|
@ -164,6 +164,7 @@ namespace opt {
|
|||
obj_map<func_decl, unsigned> m_objective_fns;
|
||||
obj_map<func_decl, expr*> 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<expr> & 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); }
|
||||
|
|
|
@ -78,6 +78,8 @@ namespace sat {
|
|||
del_clauses(m_clauses);
|
||||
TRACE("sat", tout << "Delete learned\n";);
|
||||
del_clauses(m_learned);
|
||||
dealloc(m_cuber);
|
||||
m_cuber = nullptr;
|
||||
}
|
||||
|
||||
void solver::del_clauses(clause_vector& clauses) {
|
||||
|
|
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue