mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
remove min/max, use qmax; disable cancellation during model evaluation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d2622da747
commit
1aa3fdab8a
|
@ -173,6 +173,7 @@ void rewriter_core::elim_reflex_prs(unsigned spos) {
|
|||
rewriter_core::rewriter_core(ast_manager & m, bool proof_gen):
|
||||
m_manager(m),
|
||||
m_proof_gen(proof_gen),
|
||||
m_cancel_check(true),
|
||||
m_result_stack(m),
|
||||
m_result_pr_stack(m),
|
||||
m_num_qvars(0) {
|
||||
|
|
|
@ -48,6 +48,7 @@ protected:
|
|||
};
|
||||
ast_manager & m_manager;
|
||||
bool m_proof_gen;
|
||||
bool m_cancel_check;
|
||||
typedef act_cache cache;
|
||||
ptr_vector<cache> m_cache_stack;
|
||||
cache * m_cache; // current cache.
|
||||
|
@ -114,6 +115,7 @@ public:
|
|||
ast_manager & m() const { return m_manager; }
|
||||
void reset();
|
||||
void cleanup();
|
||||
void set_cancel_check(bool f) { m_cancel_check = f; }
|
||||
#ifdef _TRACE
|
||||
void display_stack(std::ostream & out, unsigned pp_depth);
|
||||
#endif
|
||||
|
|
|
@ -595,7 +595,7 @@ void rewriter_tpl<Config>::set_inv_bindings(unsigned num_bindings, expr * const
|
|||
template<typename Config>
|
||||
template<bool ProofGen>
|
||||
void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & result_pr) {
|
||||
if (m().canceled()) {
|
||||
if (m_cancel_check && m().canceled()) {
|
||||
throw rewriter_exception(m().limit().get_cancel_msg());
|
||||
}
|
||||
SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
|
||||
|
@ -629,7 +629,7 @@ template<bool ProofGen>
|
|||
void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr) {
|
||||
SASSERT(!frame_stack().empty());
|
||||
while (!frame_stack().empty()) {
|
||||
if (m().canceled()) {
|
||||
if (m_cancel_check && m().canceled()) {
|
||||
throw rewriter_exception(m().limit().get_cancel_msg());
|
||||
}
|
||||
SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
|
||||
|
|
|
@ -365,6 +365,7 @@ struct model_evaluator::imp : public rewriter_tpl<evaluator_cfg> {
|
|||
false, // no proofs for evaluator
|
||||
m_cfg),
|
||||
m_cfg(md.get_manager(), md, p) {
|
||||
set_cancel_check(false);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
@ -137,81 +137,12 @@ public:
|
|||
}
|
||||
};
|
||||
|
||||
class alternate_min_max_cmd : public cmd {
|
||||
app_ref_vector* m_vars;
|
||||
svector<bool> m_is_max;
|
||||
unsigned m_position;
|
||||
|
||||
app_ref_vector& vars(cmd_context& ctx) {
|
||||
if (!m_vars) {
|
||||
m_vars = alloc(app_ref_vector, ctx.m());
|
||||
}
|
||||
return *m_vars;
|
||||
}
|
||||
public:
|
||||
alternate_min_max_cmd():
|
||||
cmd("min-max"),
|
||||
m_vars(0),
|
||||
m_position(0)
|
||||
{}
|
||||
|
||||
virtual void reset(cmd_context & ctx) {
|
||||
dealloc(m_vars);
|
||||
m_vars = 0;
|
||||
m_is_max.reset();
|
||||
m_position = 0;
|
||||
}
|
||||
virtual char const * get_usage() const { return "(min | max | var)+ <term>"; }
|
||||
virtual char const * get_descr(cmd_context & ctx) const { return "check sat modulo alternating min-max objectives";}
|
||||
virtual unsigned get_arity() const { return 2; }
|
||||
virtual void prepare(cmd_context & ctx) {}
|
||||
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
|
||||
switch (m_position) {
|
||||
case 0: return CPK_SYMBOL_LIST;
|
||||
case 1: return CPK_EXPR;
|
||||
default: return CPK_SYMBOL;
|
||||
}
|
||||
}
|
||||
|
||||
virtual void set_next_arg(cmd_context & ctx, unsigned num, symbol const * slist) {
|
||||
bool is_max = false;
|
||||
for (unsigned i = 0; i < num; ++i) {
|
||||
if (slist[i] == symbol("max")) {
|
||||
is_max = true;
|
||||
}
|
||||
else if (slist[i] == symbol("min")) {
|
||||
is_max = false;
|
||||
}
|
||||
else {
|
||||
m_is_max.push_back(is_max);
|
||||
vars(ctx).push_back(ctx.m().mk_const(ctx.find_func_decl(slist[i])));
|
||||
}
|
||||
}
|
||||
++m_position;
|
||||
}
|
||||
|
||||
virtual void set_next_arg(cmd_context & ctx, expr * t) {
|
||||
if (!is_app(t)) {
|
||||
throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable");
|
||||
}
|
||||
++m_position;
|
||||
get_opt(ctx).min_max(to_app(t), vars(ctx), m_is_max);
|
||||
reset(ctx);
|
||||
}
|
||||
|
||||
virtual void failure_cleanup(cmd_context & ctx) {
|
||||
reset(ctx);
|
||||
}
|
||||
|
||||
virtual void execute(cmd_context & ctx) { }
|
||||
};
|
||||
|
||||
|
||||
void install_opt_cmds(cmd_context & ctx) {
|
||||
ctx.insert(alloc(assert_soft_cmd));
|
||||
ctx.insert(alloc(min_maximize_cmd, true));
|
||||
ctx.insert(alloc(min_maximize_cmd, false));
|
||||
ctx.insert(alloc(alternate_min_max_cmd));
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -212,18 +212,6 @@ namespace opt {
|
|||
m_hard_constraints.append(s.m_hard);
|
||||
}
|
||||
|
||||
lbool context::min_max(app* t, app_ref_vector const& vars, svector<bool> const& is_max) {
|
||||
clear_state();
|
||||
init_solver();
|
||||
import_scoped_state();
|
||||
normalize();
|
||||
internalize();
|
||||
qe::max_min_opt max_min(m, m_params);
|
||||
max_min.add(m_hard_constraints);
|
||||
return max_min.check(is_max, vars, t);
|
||||
}
|
||||
|
||||
|
||||
lbool context::optimize() {
|
||||
if (m_pareto) {
|
||||
return execute_pareto();
|
||||
|
@ -236,12 +224,12 @@ namespace opt {
|
|||
import_scoped_state();
|
||||
normalize();
|
||||
internalize();
|
||||
update_solver();
|
||||
#if 0
|
||||
if (is_qsat_opt()) {
|
||||
return run_qsat_opt();
|
||||
}
|
||||
#endif
|
||||
update_solver();
|
||||
solver& s = get_solver();
|
||||
s.assert_expr(m_hard_constraints);
|
||||
display_benchmark();
|
||||
|
@ -1473,6 +1461,7 @@ namespace opt {
|
|||
value.neg();
|
||||
}
|
||||
if (result != l_undef) {
|
||||
m_optsmt.setup(*m_opt_solver.get());
|
||||
m_optsmt.update_lower(obj.m_index, value);
|
||||
m_optsmt.update_upper(obj.m_index, value);
|
||||
}
|
||||
|
|
|
@ -172,7 +172,6 @@ namespace opt {
|
|||
virtual ~context();
|
||||
unsigned add_soft_constraint(expr* f, rational const& w, symbol const& id);
|
||||
unsigned add_objective(app* t, bool is_max);
|
||||
lbool min_max(app* t, app_ref_vector const& vars, svector<bool> const& is_max);
|
||||
void add_hard_constraint(expr* f);
|
||||
|
||||
|
||||
|
|
|
@ -344,6 +344,10 @@ namespace opt {
|
|||
}
|
||||
|
||||
expr_ref opt_solver::mk_ge(unsigned var, inf_eps const& val) {
|
||||
if (!val.is_finite())
|
||||
{
|
||||
return expr_ref(val.is_pos() ? m.mk_false() : m.mk_true(), m);
|
||||
}
|
||||
smt::theory_opt& opt = get_optimizer();
|
||||
smt::theory_var v = m_objective_vars[var];
|
||||
|
||||
|
|
|
@ -24,9 +24,9 @@ Revision History:
|
|||
#include "ast_util.h"
|
||||
#include "arith_decl_plugin.h"
|
||||
#include "ast_pp.h"
|
||||
#include "model_v2_pp.h"
|
||||
#include "th_rewriter.h"
|
||||
#include "expr_functors.h"
|
||||
#include "model_v2_pp.h"
|
||||
#include "expr_safe_replace.h"
|
||||
#include "model_based_opt.h"
|
||||
|
||||
|
@ -103,19 +103,19 @@ namespace qe {
|
|||
expr_ref t(m);
|
||||
opt::ineq_type ty = opt::t_le;
|
||||
expr* e1, *e2;
|
||||
DEBUG_CODE(expr_ref val(m); VERIFY(model.eval(lit, val) && m.is_true(val)););
|
||||
|
||||
bool is_not = m.is_not(lit, lit);
|
||||
if (is_not) {
|
||||
mul.neg();
|
||||
}
|
||||
SASSERT(!m.is_not(lit));
|
||||
if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) {
|
||||
if (is_not) mul.neg();
|
||||
linearize(mbo, model, mul, e1, c, ts, tids);
|
||||
linearize(mbo, model, -mul, e2, c, ts, tids);
|
||||
ty = is_not ? opt::t_lt : opt::t_le;
|
||||
}
|
||||
else if (a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) {
|
||||
if (is_not) mul.neg();
|
||||
linearize(mbo, model, mul, e1, c, ts, tids);
|
||||
linearize(mbo, model, -mul, e2, c, ts, tids);
|
||||
ty = is_not ? opt::t_le: opt::t_lt;
|
||||
|
|
138
src/qe/qsat.cpp
138
src/qe/qsat.cpp
|
@ -618,7 +618,7 @@ namespace qe {
|
|||
}
|
||||
|
||||
kernel& get_kernel(unsigned j) {
|
||||
if (m_kernel_ex || is_exists(j)) {
|
||||
if (is_exists(j)) {
|
||||
return m_ex;
|
||||
}
|
||||
else {
|
||||
|
@ -735,11 +735,7 @@ namespace qe {
|
|||
void display(std::ostream& out) const {
|
||||
out << "level: " << m_level << "\n";
|
||||
for (unsigned i = 0; i < m_vars.size(); ++i) {
|
||||
for (unsigned j = 0; j < m_vars[i].size(); ++j) {
|
||||
expr* v = m_vars[i][j];
|
||||
out << mk_pp(v, m) << " ";
|
||||
}
|
||||
out << "\n";
|
||||
out << m_vars[i] << "\n";
|
||||
}
|
||||
m_pred_abs.display(out);
|
||||
}
|
||||
|
@ -1070,8 +1066,7 @@ namespace qe {
|
|||
m_level(0),
|
||||
m_mode(mode),
|
||||
m_avars(m),
|
||||
m_free_vars(m),
|
||||
m_kernel_ex(false)
|
||||
m_free_vars(m)
|
||||
{
|
||||
reset();
|
||||
}
|
||||
|
@ -1238,90 +1233,6 @@ namespace qe {
|
|||
}
|
||||
|
||||
|
||||
bool m_kernel_ex;
|
||||
|
||||
lbool max_min(expr_ref_vector const& fmls, svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
|
||||
m_kernel_ex = true;
|
||||
// Assume this is the only call to check.
|
||||
expr_ref_vector defs(m);
|
||||
app_ref_vector free_vars(m), vars1(m);
|
||||
expr_ref fml = mk_and(fmls);
|
||||
m_pred_abs.get_free_vars(fml, free_vars);
|
||||
m_pred_abs.abstract_atoms(fml, defs);
|
||||
fml = m_pred_abs.mk_abstract(fml);
|
||||
get_kernel(0).k().assert_expr(mk_and(defs));
|
||||
get_kernel(0).k().assert_expr(fml);
|
||||
obj_hashtable<app> var_set;
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
var_set.insert(vars[i]);
|
||||
}
|
||||
for (unsigned i = 0; i < free_vars.size(); ++i) {
|
||||
app* v = free_vars[i].get();
|
||||
if (!var_set.contains(v)) {
|
||||
vars1.push_back(v);
|
||||
}
|
||||
}
|
||||
//
|
||||
// Insert all variables in alternating list of max/min objectives.
|
||||
// By convention, the outer-most level is max.
|
||||
//
|
||||
bool is_m = true;
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
if (is_m != is_max[i]) {
|
||||
m_vars.push_back(vars1);
|
||||
vars1.reset();
|
||||
is_m = is_max[i];
|
||||
}
|
||||
vars1.push_back(vars[i]);
|
||||
}
|
||||
m_vars.push_back(vars1);
|
||||
|
||||
return max_min();
|
||||
}
|
||||
|
||||
lbool max_min() {
|
||||
while (true) {
|
||||
++m_stats.m_num_rounds;
|
||||
check_cancel();
|
||||
expr_ref_vector asms(m_asms);
|
||||
m_pred_abs.get_assumptions(m_model.get(), asms);
|
||||
//
|
||||
// TBD: add bound to asms.
|
||||
//
|
||||
smt::kernel& k = get_kernel(m_level).k();
|
||||
lbool res = k.check(asms);
|
||||
switch (res) {
|
||||
case l_true:
|
||||
k.get_model(m_model);
|
||||
SASSERT(validate_model(asms));
|
||||
TRACE("qe", k.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
|
||||
//
|
||||
// TBD: compute new bound on objective.
|
||||
//
|
||||
push();
|
||||
break;
|
||||
case l_false:
|
||||
switch (m_level) {
|
||||
case 0: return l_false;
|
||||
case 1:
|
||||
// TBD
|
||||
break;
|
||||
default:
|
||||
if (m_model.get()) {
|
||||
project(asms);
|
||||
}
|
||||
else {
|
||||
pop(1);
|
||||
}
|
||||
break;
|
||||
}
|
||||
break;
|
||||
case l_undef:
|
||||
return res;
|
||||
}
|
||||
}
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
@ -1331,49 +1242,6 @@ namespace qe {
|
|||
return qs.maximize(fmls, t, mdl, value);
|
||||
}
|
||||
|
||||
|
||||
struct max_min_opt::imp {
|
||||
|
||||
expr_ref_vector m_fmls;
|
||||
qsat m_qsat;
|
||||
|
||||
imp(ast_manager& m, params_ref const& p):
|
||||
m_fmls(m),
|
||||
m_qsat(m, p, qsat_maximize)
|
||||
{}
|
||||
|
||||
void add(expr* e) {
|
||||
m_fmls.push_back(e);
|
||||
}
|
||||
|
||||
lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
|
||||
return m_qsat.max_min(m_fmls, is_max, vars, t);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
max_min_opt::max_min_opt(ast_manager& m, params_ref const& p) {
|
||||
m_imp = alloc(imp, m, p);
|
||||
}
|
||||
|
||||
max_min_opt::~max_min_opt() {
|
||||
dealloc(m_imp);
|
||||
}
|
||||
|
||||
void max_min_opt::add(expr* e) {
|
||||
m_imp->add(e);
|
||||
}
|
||||
|
||||
void max_min_opt::add(expr_ref_vector const& fmls) {
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
add(fmls[i]);
|
||||
}
|
||||
}
|
||||
|
||||
lbool max_min_opt::check(svector<bool> const& is_max, app_ref_vector const& vars, app* t) {
|
||||
return m_imp->check(is_max, vars, t);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
tactic * mk_qsat_tactic(ast_manager& m, params_ref const& p) {
|
||||
|
|
|
@ -114,17 +114,6 @@ namespace qe {
|
|||
void collect_statistics(statistics& st) const;
|
||||
};
|
||||
|
||||
class max_min_opt {
|
||||
struct imp;
|
||||
imp* m_imp;
|
||||
public:
|
||||
max_min_opt(ast_manager& m, params_ref const& p = params_ref());
|
||||
~max_min_opt();
|
||||
void add(expr* e);
|
||||
void add(expr_ref_vector const& fmls);
|
||||
lbool check(svector<bool> const& is_max, app_ref_vector const& vars, app* t);
|
||||
};
|
||||
|
||||
lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p);
|
||||
|
||||
}
|
||||
|
|
|
@ -300,6 +300,7 @@ public:
|
|||
bool get_sum(expr* x, rational const& mul, expr_ref_vector& conds, expr_ref_vector& args, vector<rational>& coeffs, rational& coeff) {
|
||||
expr *y, *z, *u;
|
||||
rational r, q;
|
||||
if (!is_app(x)) return false;
|
||||
app* f = to_app(x);
|
||||
bool ok = true;
|
||||
if (a.is_add(x)) {
|
||||
|
|
Loading…
Reference in a new issue