diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index fccdf9b55..0b71fff1c 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1300,6 +1300,9 @@ namespace opt { } get_memory_statistics(stats); get_rlimit_statistics(m.limit(), stats); + if (m_qmax) { + m_qmax->collect_statistics(stats); + } } void context::collect_param_descrs(param_descrs & r) { @@ -1440,6 +1443,9 @@ namespace opt { m_objectives[0].m_type != O_MINIMIZE) { return false; } + if (!m_arith.is_real(m_objectives[0].m_term)) { + return false; + } for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { if (has_quantifiers(m_hard_constraints[i].get())) { return true; @@ -1456,12 +1462,21 @@ namespace opt { term = m_arith.mk_uminus(term); } inf_eps value; - lbool result = qe::maximize(m_hard_constraints, term, value, m_model, m_params); + m_qmax = alloc(qe::qmax, m, m_params); + lbool result = (*m_qmax)(m_hard_constraints, term, value, m_model); if (result != l_undef && obj.m_type == O_MINIMIZE) { value.neg(); } - if (result != l_undef) { - m_optsmt.setup(*m_opt_solver.get()); + m_optsmt.setup(*m_opt_solver.get()); + if (result == l_undef) { + if (obj.m_type == O_MINIMIZE) { + m_optsmt.update_upper(obj.m_index, value); + } + else { + m_optsmt.update_lower(obj.m_index, value); + } + } + else { m_optsmt.update_lower(obj.m_index, value); m_optsmt.update_upper(obj.m_index, value); } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 3339dc37a..07fe53268 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -28,7 +28,7 @@ Notes: #include "arith_decl_plugin.h" #include "bv_decl_plugin.h" #include "cmd_context.h" - +#include "qsat.h" namespace opt { @@ -145,6 +145,7 @@ namespace opt { ref m_solver; ref m_sat_solver; scoped_ptr m_pareto; + scoped_ptr m_qmax; sref_vector m_box_models; unsigned m_box_index; params_ref m_params; diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index bdfd45133..38d46fefe 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -64,6 +64,7 @@ namespace qe { expr_ref_vector m_div_terms; vector m_div_divisors, m_div_coeffs; expr_ref_vector m_new_lits; + expr_ref_vector m_trail; rational m_delta, m_u; scoped_ptr m_var; unsigned m_num_pos, m_num_neg; @@ -98,7 +99,7 @@ namespace qe { // It uses the current model to choose values for conditionals and it primes mbo with the current // interpretation of sub-expressions that are treated as variables for mbo. // - void linearize(opt::model_based_opt& mbo, model& model, expr* lit, obj_map& tids) { + bool linearize(opt::model_based_opt& mbo, model& model, expr* lit, expr_ref_vector& fmls, obj_map& tids) { obj_map ts; rational c(0), mul(1); expr_ref t(m); @@ -111,33 +112,45 @@ namespace qe { mul.neg(); } SASSERT(!m.is_not(lit)); - if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) { - linearize(mbo, model, mul, e1, c, ts, tids); - linearize(mbo, model, -mul, e2, c, ts, tids); + if ((a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) && a.is_real(e1)) { + linearize(mbo, model, mul, e1, c, fmls, ts, tids); + linearize(mbo, model, -mul, e2, c, fmls, 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)) { - linearize(mbo, model, mul, e1, c, ts, tids); - linearize(mbo, model, -mul, e2, c, ts, tids); + else if ((a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) && a.is_real(e1)) { + linearize(mbo, model, mul, e1, c, fmls, ts, tids); + linearize(mbo, model, -mul, e2, c, fmls, ts, tids); ty = is_not ? opt::t_le: opt::t_lt; } - else if (m.is_eq(lit, e1, e2) && !is_not && is_arith(e1)) { - linearize(mbo, model, mul, e1, c, ts, tids); - linearize(mbo, model, -mul, e2, c, ts, tids); + else if (m.is_eq(lit, e1, e2) && !is_not && a.is_real(e1)) { + linearize(mbo, model, mul, e1, c, fmls, ts, tids); + linearize(mbo, model, -mul, e2, c, fmls, ts, tids); ty = opt::t_eq; } - else if (m.is_distinct(lit) && !is_not && is_arith(to_app(lit)->get_arg(0))) { - UNREACHABLE(); + else if (m.is_eq(lit, e1, e2) && is_not && a.is_real(e1)) { + expr_ref val1(m), val2(m); + rational r1, r2; + VERIFY(model.eval(e1, val1) && a.is_numeral(val1, r1)); + VERIFY(model.eval(e2, val2) && a.is_numeral(val2, r2)); + SASSERT(r1 != r2); + if (r2 < r1) { + std::swap(e1, e2); + } + ty = opt::t_lt; + linearize(mbo, model, mul, e1, c, fmls, ts, tids); + linearize(mbo, model, -mul, e2, c, fmls, ts, tids); + } + else if (m.is_distinct(lit) && !is_not && a.is_real(to_app(lit)->get_arg(0))) { + TRACE("qe", tout << "TBD: handle distinc\n";); + return false; } - else if (m.is_distinct(lit) && is_not && is_arith(to_app(lit)->get_arg(0))) { - UNREACHABLE(); + else if (m.is_distinct(lit) && is_not && a.is_real(to_app(lit)->get_arg(0))) { + TRACE("qe", tout << "TBD: handle negation of distinc\n";); + return false; } - else if (m.is_eq(lit, e1, e2) && is_not && is_arith(e1)) { - UNREACHABLE(); - } else { TRACE("qe", tout << "Skipping " << mk_pp(lit, m) << "\n";); - return; + return false; } #if 0 TBD for integers @@ -149,34 +162,35 @@ namespace qe { vars coeffs; extract_coefficients(mbo, model, ts, tids, coeffs); mbo.add_constraint(coeffs, c, ty); + return true; } // // convert linear arithmetic term into an inequality for mbo. // void linearize(opt::model_based_opt& mbo, model& model, rational const& mul, expr* t, rational& c, - obj_map& ts, obj_map& tids) { + expr_ref_vector& fmls, obj_map& ts, obj_map& tids) { expr* t1, *t2, *t3; rational mul1; expr_ref val(m); if (a.is_mul(t, t1, t2) && is_numeral(model, t1, mul1)) { - linearize(mbo, model, mul* mul1, t2, c, ts, tids); + linearize(mbo, model, mul* mul1, t2, c, fmls, ts, tids); } else if (a.is_mul(t, t1, t2) && is_numeral(model, t2, mul1)) { - linearize(mbo, model, mul* mul1, t1, c, ts, tids); + linearize(mbo, model, mul* mul1, t1, c, fmls, ts, tids); } else if (a.is_add(t)) { app* ap = to_app(t); for (unsigned i = 0; i < ap->get_num_args(); ++i) { - linearize(mbo, model, mul, ap->get_arg(i), c, ts, tids); + linearize(mbo, model, mul, ap->get_arg(i), c, fmls, ts, tids); } } else if (a.is_sub(t, t1, t2)) { - linearize(mbo, model, mul, t1, c, ts, tids); - linearize(mbo, model, -mul, t2, c, ts, tids); + linearize(mbo, model, mul, t1, c, fmls, ts, tids); + linearize(mbo, model, -mul, t2, c, fmls, ts, tids); } else if (a.is_uminus(t, t1)) { - linearize(mbo, model, -mul, t1, c, ts, tids); + linearize(mbo, model, -mul, t1, c, fmls, ts, tids); } else if (a.is_numeral(t, mul1)) { c += mul*mul1; @@ -186,13 +200,13 @@ namespace qe { SASSERT(m.is_true(val) || m.is_false(val)); TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";); if (m.is_true(val)) { - linearize(mbo, model, mul, t2, c, ts, tids); - linearize(mbo, model, t1, tids); + linearize(mbo, model, mul, t2, c, fmls, ts, tids); + fmls.push_back(t1); } else { expr_ref not_t1(mk_not(m, t1), m); - linearize(mbo, model, mul, t3, c, ts, tids); - linearize(mbo, model, not_t1, tids); + fmls.push_back(not_t1); + linearize(mbo, model, mul, t3, c, fmls, ts, tids); } } else { @@ -433,6 +447,7 @@ namespace qe { return a.is_int(e) || a.is_real(e); } + expr_ref add(expr_ref_vector const& ts) { switch (ts.size()) { case 0: @@ -952,7 +967,7 @@ namespace qe { } imp(ast_manager& m): - m(m), a(m), m_rw(m), m_ineq_terms(m), m_div_terms(m), m_new_lits(m) { + m(m), a(m), m_rw(m), m_ineq_terms(m), m_div_terms(m), m_new_lits(m), m_trail(m) { params_ref params; params.set_bool("gcd_rouding", true); m_rw.updt_params(params); @@ -979,11 +994,115 @@ namespace qe { } typedef opt::model_based_opt::var var; + typedef opt::model_based_opt::row row; typedef vector vars; - - opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) { + + void operator()(model& model, app_ref_vector& vars, expr_ref_vector& fmls) { + bool has_real = false; + for (unsigned i = 0; !has_real && i < vars.size(); ++i) { + has_real = a.is_real(vars[i].get()); + } + if (!has_real) { + return; + } + + opt::model_based_opt mbo; + obj_map tids; + m_trail.reset(); + unsigned j = 0; + for (unsigned i = 0; i < fmls.size(); ++i) { + if (!linearize(mbo, model, fmls[i].get(), fmls, tids)) { + if (i != j) { + fmls[j] = fmls[i].get(); + } + ++j; + } + } + fmls.resize(j); + + // fmls holds residue, + // mbo holds linear inequalities that are in scope + // collect variables in residue an in tids. + // filter variables that are absent from residue. + // project those. + // collect result of projection + // return those to fmls. + + expr_mark var_mark, fmls_mark; + for (unsigned i = 0; i < vars.size(); ++i) { + app* v = vars[i].get(); + var_mark.mark(v); + if (a.is_real(v) && !tids.contains(v)) { + tids.insert(v, tids.size()); + } + } + for (unsigned i = 0; i < fmls.size(); ++i) { + fmls_mark.mark(fmls[i].get()); + } + obj_map::iterator it = tids.begin(), end = tids.end(); + ptr_vector index2expr; + for (; it != end; ++it) { + expr* e = it->m_key; + if (!var_mark.is_marked(e)) { + mark_rec(fmls_mark, e); + } + index2expr.setx(it->m_value, e, 0); + } + j = 0; + unsigned_vector real_vars; + for (unsigned i = 0; i < vars.size(); ++i) { + app* v = vars[i].get(); + if (a.is_real(v) && !fmls_mark.is_marked(v)) { + real_vars.push_back(tids.find(v)); + } + else { + if (i != j) { + vars[j] = v; + } + ++j; + } + } + vars.resize(j); + mbo.project(real_vars.size(), real_vars.c_ptr()); + vector rows; + mbo.get_live_rows(rows); + + for (unsigned i = 0; i < rows.size(); ++i) { + expr_ref_vector ts(m); + expr_ref t(m), s(m); + row const& r = rows[i]; + for (j = 0; j < r.m_vars.size(); ++j) { + var const& v = r.m_vars[j]; + t = index2expr[v.m_id]; + if (!v.m_coeff.is_one()) { + t = a.mk_mul(t, a.mk_numeral(v.m_coeff, v.m_coeff.is_int())); + } + ts.push_back(t); + } + if (ts.empty()) { + continue; + } + s = a.mk_numeral(-r.m_coeff, r.m_coeff.is_int()); + if (ts.size() == 1) { + t = ts[0].get(); + } + else { + t = a.mk_add(ts.size(), ts.c_ptr()); + } + switch (r.m_type) { + case opt::t_lt: t = a.mk_lt(t, s); break; + case opt::t_le: t = a.mk_le(t, s); break; + case opt::t_eq: t = a.mk_eq(t, s); break; + } + fmls.push_back(t); + } + } + + opt::inf_eps maximize(expr_ref_vector const& fmls0, model& mdl, app* t, expr_ref& bound) { + m_trail.reset(); SASSERT(a.is_real(t)); + expr_ref_vector fmls(fmls0); opt::model_based_opt mbo; opt::inf_eps value; obj_map ts; @@ -992,13 +1111,14 @@ namespace qe { // extract objective function. vars coeffs; rational c(0), mul(1); - linearize(mbo, mdl, mul, t, c, ts, tids); + linearize(mbo, mdl, mul, t, c, fmls, ts, tids); extract_coefficients(mbo, mdl, ts, tids, coeffs); mbo.set_objective(coeffs, c); // extract linear constraints + for (unsigned i = 0; i < fmls.size(); ++i) { - linearize(mbo, mdl, fmls[i], tids); + linearize(mbo, mdl, fmls[i].get(), fmls, tids); } // find optimal value @@ -1052,6 +1172,7 @@ namespace qe { return; } tids.insert(it->m_key, id); + m_trail.push_back(it->m_key); } coeffs.push_back(var(id, it->m_value)); } @@ -1071,6 +1192,10 @@ namespace qe { return (*m_imp)(model, var, vars, lits); } + void arith_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + (*m_imp)(model, vars, lits); + } + bool arith_project_plugin::solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return m_imp->solve(model, vars, lits); } diff --git a/src/qe/qe_arith.h b/src/qe/qe_arith.h index b89d16d04..f71156b1e 100644 --- a/src/qe/qe_arith.h +++ b/src/qe/qe_arith.h @@ -29,6 +29,8 @@ namespace qe { virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits); virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits); virtual family_id get_family_id(); + virtual void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits); + opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound); }; diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index d7ec22eee..727832d70 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -38,6 +38,17 @@ struct noop_op_proc { }; +void project_plugin::mark_rec(expr_mark& visited, expr* e) { + for_each_expr_proc fe; + for_each_expr(fe, visited, e); +} + +void project_plugin::mark_rec(expr_mark& visited, expr_ref_vector const& es) { + for (unsigned i = 0; i < es.size(); ++i) { + mark_rec(visited, es[i]); + } +} + /** \brief return two terms that are equal in the model. The distinct term t is false in model, so there @@ -185,10 +196,8 @@ class mbp::impl { void filter_variables(model& model, app_ref_vector& vars, expr_ref_vector& lits, expr_ref_vector& unused_lits) { ast_manager& m = vars.get_manager(); expr_mark lit_visited; - for_each_expr_proc fe; - for (unsigned i = 0; i < lits.size(); ++i) { - for_each_expr(fe, lit_visited, lits[i].get()); - } + project_plugin::mark_rec(lit_visited, lits); + unsigned j = 0; for (unsigned i = 0; i < vars.size(); ++i) { app* var = vars[i].get(); @@ -425,13 +434,18 @@ public: app_ref var(m); expr_ref_vector unused_fmls(m); bool progress = true; - TRACE("qe", tout << vars << " " << fmls << "\n";); preprocess_solve(model, vars, fmls); filter_variables(model, vars, fmls, unused_fmls); project_bools(model, vars, fmls); while (progress && !vars.empty() && !fmls.empty()) { app_ref_vector new_vars(m); progress = false; + for (unsigned i = 0; i < m_plugins.size(); ++i) { + project_plugin* p = m_plugins[i]; + if (p) { + (*p)(model, vars, fmls); + } + } while (!vars.empty() && !fmls.empty()) { var = vars.back(); vars.pop_back(); diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h index 7cf086824..6c28555b0 100644 --- a/src/qe/qe_mbp.h +++ b/src/qe/qe_mbp.h @@ -37,13 +37,15 @@ namespace qe { virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) = 0; virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) = 0; virtual family_id get_family_id() = 0; - virtual bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; }; + virtual void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { }; static expr_ref pick_equality(ast_manager& m, model& model, expr* t); static void partition_values(model& model, expr_ref_vector const& vals, expr_ref_vector& lits); static void partition_args(model& model, app_ref_vector const& sels, expr_ref_vector& lits); static void erase(expr_ref_vector& lits, unsigned& i); static void push_back(expr_ref_vector& lits, expr* lit); + static void mark_rec(expr_mark& visited, expr* e); + static void mark_rec(expr_mark& visited, expr_ref_vector const& es); }; class mbp { diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 0ab3c86bb..a9ca9e99d 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -33,6 +33,7 @@ Notes: #include "label_rewriter.h" #include "expr_replacer.h" #include "th_rewriter.h" +#include "model_evaluator.h" namespace qe { @@ -154,12 +155,14 @@ namespace qe { if (level == 0) { return; } + model_evaluator eval(*mdl); + expr_ref val(m); for (unsigned j = 0; j < m_preds[level - 1].size(); ++j) { app* p = m_preds[level - 1][j].get(); TRACE("qe", tout << "process level: " << level - 1 << ": " << mk_pp(p, m) << "\n";); - VERIFY(mdl->eval(p, val)); + eval(p, val); if (m.is_false(val)) { m_asms.push_back(m.mk_not(p)); @@ -179,7 +182,7 @@ namespace qe { (lvl.m_fa == i && (lvl.m_ex == UINT_MAX || lvl.m_ex < level)) || (lvl.m_ex == i && (lvl.m_fa == UINT_MAX || lvl.m_fa < level)); if (use) { - VERIFY(mdl->eval(p, val)); + eval(p, val); if (m.is_false(val)) { asms.push_back(m.mk_not(p)); } @@ -566,6 +569,9 @@ namespace qe { qsat_mode m_mode; app_ref_vector m_avars; // variables to project app_ref_vector m_free_vars; + app* m_objective; + opt::inf_eps* m_value; + bool m_was_sat; /** @@ -1067,7 +1073,10 @@ namespace qe { m_level(0), m_mode(mode), m_avars(m), - m_free_vars(m) + m_free_vars(m), + m_objective(0), + m_value(0), + m_was_sat(false) { reset(); } @@ -1162,6 +1171,9 @@ namespace qe { void collect_statistics(statistics & st) const { st.copy(m_st); + m_fa.k().collect_statistics(st); + m_ex.k().collect_statistics(st); + m_pred_abs.collect_statistics(st); st.update("qsat num rounds", m_stats.m_num_rounds); m_pred_abs.collect_statistics(st); } @@ -1169,7 +1181,7 @@ namespace qe { void reset_statistics() { m_stats.reset(); m_fa.k().reset_statistics(); - m_ex.k().reset_statistics(); + m_ex.k().reset_statistics(); } void cleanup() { @@ -1186,16 +1198,12 @@ namespace qe { return alloc(qsat, m, m_params, m_mode); } - app* m_objective; - opt::inf_eps m_value; - bool m_was_sat; - lbool maximize(expr_ref_vector const& fmls, app* t, model_ref& mdl, opt::inf_eps& value) { expr_ref_vector defs(m); expr_ref fml = mk_and(fmls); hoist(fml); m_objective = t; - m_value = opt::inf_eps(); + m_value = &value; m_was_sat = false; m_pred_abs.abstract_atoms(fml, defs); fml = m_pred_abs.mk_abstract(fml); @@ -1219,17 +1227,20 @@ namespace qe { if (s == "ok") { s = m_fa.k().last_failure_as_string(); } + throw tactic_exception(s.c_str()); } - value = m_value; return l_true; } void maximize(expr_ref_vector const& core, model& mdl) { + SASSERT(m_value); + SASSERT(m_objective); TRACE("qe", tout << "maximize: " << core << "\n";); m_was_sat |= !core.empty(); expr_ref bound(m); - m_value = m_mbp.maximize(core, mdl, m_objective, bound); + *m_value = m_mbp.maximize(core, mdl, m_objective, bound); + IF_VERBOSE(0, verbose_stream() << "(maximize " << *m_value << " bound: " << bound << ")\n";); m_ex.assert_expr(bound); } @@ -1243,6 +1254,30 @@ namespace qe { return qs.maximize(fmls, t, mdl, value); } + + struct qmax::imp { + qsat m_qsat; + imp(ast_manager& m, params_ref const& p): + m_qsat(m, p, qsat_maximize) + {} + }; + + qmax::qmax(ast_manager& m, params_ref const& p) { + m_imp = alloc(imp, m, p); + } + + qmax::~qmax() { + dealloc(m_imp); + } + + lbool qmax::operator()(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl) { + return m_imp->m_qsat.maximize(fmls, t, mdl, value); + } + + void qmax::collect_statistics(statistics& st) const { + m_imp->m_qsat.collect_statistics(st); + }; + }; tactic * mk_qsat_tactic(ast_manager& m, params_ref const& p) { diff --git a/src/qe/qsat.h b/src/qe/qsat.h index 456711c4f..66676da05 100644 --- a/src/qe/qsat.h +++ b/src/qe/qsat.h @@ -114,6 +114,16 @@ namespace qe { void collect_statistics(statistics& st) const; }; + class qmax { + struct imp; + imp* m_imp; + public: + qmax(ast_manager& m, params_ref const& p = params_ref()); + ~qmax(); + lbool operator()(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl); + void collect_statistics(statistics& st) const; + }; + lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p); }