From 9c099d6b1bf499f5bf548279590fb4d6e9af3a8c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Jun 2016 16:39:03 -0700 Subject: [PATCH] fix mb maximization logic, so far not accessible Signed-off-by: Nikolaj Bjorner --- src/math/simplex/model_based_opt.cpp | 149 ++++++++++++++++++--------- src/math/simplex/model_based_opt.h | 14 ++- src/opt/opt_context.cpp | 8 +- src/opt/opt_params.pyg | 3 +- src/qe/qe_arith.cpp | 63 ++++++++--- src/qe/qe_arith.h | 2 +- src/qe/qe_mbp.cpp | 19 +++- src/qe/qe_mbp.h | 2 +- src/qe/qsat.cpp | 127 ++++++++++++++++++++--- src/qe/qsat.h | 2 + src/smt/smt_context.h | 2 - src/smt/smt_model_checker.cpp | 36 ++++--- 12 files changed, 318 insertions(+), 109 deletions(-) diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index 06ba38b4a..c4e4b110e 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -41,7 +41,6 @@ namespace opt { bool model_based_opt::invariant() { - // variables in each row are sorted. for (unsigned i = 0; i < m_rows.size(); ++i) { if (!invariant(i, m_rows[i])) { return false; @@ -50,19 +49,21 @@ namespace opt { return true; } +#define PASSERT(_e_) if (!(_e_)) { TRACE("opt", display(tout, r);); SASSERT(_e_); } + bool model_based_opt::invariant(unsigned index, row const& r) { - rational val = r.m_coeff; vector const& vars = r.m_vars; for (unsigned i = 0; i < vars.size(); ++i) { - var const& v = vars[i]; - SASSERT(i + 1 == vars.size() || v.m_id < vars[i+1].m_id); - SASSERT(!v.m_coeff.is_zero()); - val += v.m_coeff * m_var2value[v.m_id]; + // variables in each row are sorted and have non-zero coefficients + SASSERT(i + 1 == vars.size() || vars[i].m_id < vars[i+1].m_id); + SASSERT(!vars[i].m_coeff.is_zero()); } - SASSERT(val == r.m_value); - SASSERT(r.m_type != t_eq || val.is_zero()); - SASSERT(index == 0 || r.m_type != t_lt || val.is_neg()); - SASSERT(index == 0 || r.m_type != t_le || !val.is_pos()); + + PASSERT(r.m_value == get_row_value(r)); + PASSERT(r.m_type != t_eq || r.m_value.is_zero()); + // values satisfy constraints + PASSERT(index == 0 || r.m_type != t_lt || r.m_value.is_neg()); + PASSERT(index == 0 || r.m_type != t_le || !r.m_value.is_pos()); return true; } @@ -90,20 +91,25 @@ namespace opt { // inf_eps model_based_opt::maximize() { SASSERT(invariant()); - unsigned_vector other; unsigned_vector bound_trail, bound_vars; + TRACE("opt", display(tout << "tableau\n");); while (!objective().m_vars.empty()) { - TRACE("opt", display(tout << "tableau\n");); var v = objective().m_vars.back(); unsigned x = v.m_id; rational const& coeff = v.m_coeff; unsigned bound_row_index; rational bound_coeff; - other.reset(); - if (find_bound(x, bound_row_index, bound_coeff, other, coeff.is_pos())) { + if (find_bound(x, bound_row_index, bound_coeff, coeff.is_pos())) { SASSERT(!bound_coeff.is_zero()); - for (unsigned i = 0; i < other.size(); ++i) { - resolve(bound_row_index, bound_coeff, other[i], x); + TRACE("opt", display(tout << "update: " << v << " ", objective()); + for (unsigned i = 0; i < m_above.size(); ++i) { + display(tout << "resolve: ", m_rows[m_above[i]]); + }); + for (unsigned i = 0; i < m_above.size(); ++i) { + resolve(bound_row_index, bound_coeff, m_above[i], x); + } + for (unsigned i = 0; i < m_below.size(); ++i) { + resolve(bound_row_index, bound_coeff, m_below[i], x); } // coeff*x + objective <= ub // a2*x + t2 <= 0 @@ -116,6 +122,8 @@ namespace opt { bound_vars.push_back(x); } else { + TRACE("opt", display(tout << "unbound: " << v << " ", objective());); + update_values(bound_vars, bound_trail); return inf_eps::infinity(); } } @@ -136,15 +144,33 @@ namespace opt { } + void model_based_opt::update_value(unsigned x, rational const& val) { + rational old_val = m_var2value[x]; + m_var2value[x] = val; + unsigned_vector const& row_ids = m_var2row_ids[x]; + for (unsigned i = 0; i < row_ids.size(); ++i) { + unsigned row_id = row_ids[i]; + rational coeff = get_coefficient(row_id, x); + if (coeff.is_zero()) { + continue; + } + row & r = m_rows[row_id]; + rational delta = coeff * (val - old_val); + r.m_value += delta; + SASSERT(invariant(row_id, r)); + } + } + + void model_based_opt::update_values(unsigned_vector const& bound_vars, unsigned_vector const& bound_trail) { - rational eps(0); for (unsigned i = bound_trail.size(); i > 0; ) { --i; unsigned x = bound_vars[i]; row& r = m_rows[bound_trail[i]]; rational val = r.m_coeff; - rational x_val; - rational x_coeff; + rational old_x_val = m_var2value[x]; + rational new_x_val; + rational x_coeff, eps(0); vector const& vars = r.m_vars; for (unsigned j = 0; j < vars.size(); ++j) { var const& v = vars[j]; @@ -155,28 +181,21 @@ namespace opt { val += m_var2value[v.m_id]*v.m_coeff; } } - TRACE("opt", display(tout << "v" << x << " val: " << val - << " coeff_x: " << x_coeff << " val_x: " << m_var2value[x] << " ", r); ); SASSERT(!x_coeff.is_zero()); - x_val = -val/x_coeff; - // - // - // ax + t < 0 - // <=> x < -t/a - // <=> x := -t/a - epsilon - // - if (r.m_type == t_lt) { - // Adjust epsilon to be - if (!x_val.is_zero() && (eps.is_zero() || eps >= abs(x_val))) { - eps = abs(x_val)/rational(2); - } - if (!r.m_value.is_zero() && (eps.is_zero() || eps >= abs(r.m_value))) { - eps = abs(r.m_value)/rational(2); - } + new_x_val = -val/x_coeff; + if (r.m_type == t_lt) { + eps = abs(old_x_val - new_x_val)/rational(2); + eps = std::min(rational::one(), eps); SASSERT(!eps.is_zero()); + + // + // ax + t < 0 + // <=> x < -t/a + // <=> x := -t/a - epsilon + // if (x_coeff.is_pos()) { - x_val -= eps; + new_x_val -= eps; } // // -ax + t < 0 @@ -185,27 +204,47 @@ namespace opt { // <=> x > t/a // <=> x := t/a + epsilon // - else if (x_coeff.is_neg()) { - x_val += eps; + else { + new_x_val += eps; } } - m_var2value[x] = x_val; - r.m_value = (x_val * x_coeff) + val; + TRACE("opt", display(tout << "v" << x + << " coeff_x: " << x_coeff + << " old_x_val: " << old_x_val + << " new_x_val: " << new_x_val + << " eps: " << eps << " ", r); ); + m_var2value[x] = new_x_val; - TRACE("opt", display(tout << "v" << x << " val: " << val << " coeff_x: " - << x_coeff << " val_x: " << m_var2value[x] << " ", r); ); + r.m_value = get_row_value(r); SASSERT(invariant(bound_trail[i], r)); } + + // update and check bounds for all other affected rows. + for (unsigned i = bound_trail.size(); i > 0; ) { + --i; + unsigned x = bound_vars[i]; + unsigned_vector const& row_ids = m_var2row_ids[x]; + for (unsigned j = 0; j < row_ids.size(); ++j) { + unsigned row_id = row_ids[j]; + row & r = m_rows[row_id]; + r.m_value = get_row_value(r); + SASSERT(invariant(row_id, r)); + } + } + SASSERT(invariant()); } - bool model_based_opt::find_bound(unsigned x, unsigned& bound_row_index, rational& bound_coeff, unsigned_vector& other, bool is_pos) { + bool model_based_opt::find_bound(unsigned x, unsigned& bound_row_index, rational& bound_coeff, bool is_pos) { bound_row_index = UINT_MAX; rational lub_val; rational const& x_val = m_var2value[x]; unsigned_vector const& row_ids = m_var2row_ids[x]; uint_set visited; + m_above.reset(); + m_below.reset(); for (unsigned i = 0; i < row_ids.size(); ++i) { unsigned row_id = row_ids[i]; + SASSERT(row_id != m_objective_id); if (visited.contains(row_id)) { continue; } @@ -226,24 +265,34 @@ namespace opt { else if ((value == lub_val && r.m_type == opt::t_lt) || (is_pos && value < lub_val) || (!is_pos && value > lub_val)) { - other.push_back(bound_row_index); + m_above.push_back(bound_row_index); lub_val = value; - bound_row_index = row_id; + bound_row_index = row_id; bound_coeff = a; } else { - other.push_back(row_id); + m_above.push_back(row_id); } } else { - r.m_alive = false; + m_below.push_back(row_id); } } } return bound_row_index != UINT_MAX; } - - rational model_based_opt::get_coefficient(unsigned row_id, unsigned var_id) { + + rational model_based_opt::get_row_value(row const& r) const { + vector const& vars = r.m_vars; + rational val = r.m_coeff; + for (unsigned i = 0; i < vars.size(); ++i) { + var const& v = vars[i]; + val += v.m_coeff * m_var2value[v.m_id]; + } + return val; + } + + rational model_based_opt::get_coefficient(unsigned row_id, unsigned var_id) const { row const& r = m_rows[row_id]; if (r.m_vars.empty()) { return rational::zero(); diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h index e4ba288c8..3bbcc7bf2 100644 --- a/src/math/simplex/model_based_opt.h +++ b/src/math/simplex/model_based_opt.h @@ -65,24 +65,29 @@ namespace opt { vector m_var2value; vector m_new_vars; unsigned_vector m_lub, m_glb; + unsigned_vector m_above, m_below; bool invariant(); bool invariant(unsigned index, row const& r); row& objective() { return m_rows[0]; } - bool find_bound(unsigned x, unsigned& bound_index, rational& bound_coeff, unsigned_vector& other, bool is_pos); + bool find_bound(unsigned x, unsigned& bound_index, rational& bound_coeff, bool is_pos); - rational get_coefficient(unsigned row_id, unsigned var_id); + rational get_coefficient(unsigned row_id, unsigned var_id) const; + + rational get_row_value(row const& r) const; void resolve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x); void mul_add(bool same_sign, unsigned row_id1, rational const& c, unsigned row_id2); - void set_row(unsigned row_id, vector const& coeffs, rational const& c, ineq_type rel); - + void set_row(unsigned row_id, vector const& coeffs, rational const& c, ineq_type rel); + void update_values(unsigned_vector const& bound_vars, unsigned_vector const& bound_trail); + void update_value(unsigned x, rational const& val); + void project(unsigned var); void solve_for(unsigned row_id, unsigned x); @@ -132,5 +137,6 @@ namespace opt { std::ostream& operator<<(std::ostream& out, opt::ineq_type ie); +inline std::ostream& operator<<(std::ostream& out, opt::model_based_opt::var const v) { return out << "v" << v.m_id; } #endif diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index f90b31476..788921205 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -225,7 +225,7 @@ namespace opt { normalize(); internalize(); update_solver(); -#if 1 +#if 0 if (is_qsat_opt()) { return run_qsat_opt(); } @@ -367,6 +367,7 @@ namespace opt { lbool context::execute_box() { if (m_box_index < m_objectives.size()) { + SASSERT(m_box_index < m_box_models.size()); m_model = m_box_models[m_box_index]; ++m_box_index; return l_true; @@ -383,7 +384,9 @@ namespace opt { if (obj.m_type == O_MAXSMT) { solver::scoped_push _sp(get_solver()); r = execute(obj, false, false); - if (r == l_true) m_box_models.push_back(m_model.get()); + if (r == l_true) { + m_box_models.push_back(m_model.get()); + } } else { m_box_models.push_back(m_optsmt.get_model(j)); @@ -391,6 +394,7 @@ namespace opt { } } if (r == l_true && m_objectives.size() > 0) { + SASSERT(!m_box_models.empty()); m_model = m_box_models[0]; } return r; diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 37b9ff372..629b3aa53 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -1,8 +1,7 @@ def_module_params('opt', description='optimization parameters', export=True, - params=(('timeout', UINT, UINT_MAX, 'set timeout'), - ('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), + params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'fu_malik', 'core_maxsat', 'wmax', 'pbmax', 'maxres', 'pd-maxres', 'bcd2', 'wpm2', 'sls', 'maxhs'"), ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"), ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'), diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index d071765fc..a4129d5cd 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -105,7 +105,10 @@ 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));); + DEBUG_CODE(expr_ref val(m); + VERIFY(model.eval(lit, val)); + CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";); + SASSERT(m.is_true(val));); bool is_not = m.is_not(lit, lit); if (is_not) { @@ -942,7 +945,7 @@ namespace qe { SASSERT(m_u < m_delta && rational(0) <= m_u); for (unsigned i = 0; i < n; ++i) { add_lit(model, lits, mk_divides(div_divisor(i), - mk_add(mk_num(div_coeff(i) * m_u), div_term(i)))); + mk_add(mk_num(div_coeff(i) * m_u), div_term(i)))); } reset_divs(); // @@ -1070,7 +1073,7 @@ namespace qe { for (unsigned i = 0; i < rows.size(); ++i) { expr_ref_vector ts(m); - expr_ref t(m), s(m); + expr_ref t(m), s(m), val(m); row const& r = rows[i]; if (r.m_vars.size() == 0) { continue; @@ -1088,6 +1091,8 @@ namespace qe { case opt::t_eq: t = a.mk_eq(t, s); break; } fmls.push_back(t); + VERIFY(model.eval(t, val)); + CTRACE("qe", !m.is_true(val), tout << "Evaluated unit " << t << " to " << val << "\n";); continue; } for (j = 0; j < r.m_vars.size(); ++j) { @@ -1111,10 +1116,16 @@ namespace qe { case opt::t_eq: t = a.mk_eq(t, s); break; } fmls.push_back(t); + + + VERIFY(model.eval(t, val)); + CTRACE("qe", !m.is_true(val), tout << "Evaluated " << t << " to " << val << "\n";); + } } - opt::inf_eps maximize(expr_ref_vector const& fmls0, model& mdl, app* t, expr_ref& bound) { + opt::inf_eps maximize(expr_ref_vector const& fmls0, model& mdl, app* t, expr_ref& ge, expr_ref& gt) { + validate_model(mdl, fmls0); m_trail.reset(); SASSERT(a.is_real(t)); expr_ref_vector fmls(fmls0); @@ -1139,11 +1150,6 @@ namespace qe { // find optimal value value = mbo.maximize(); - expr_ref val(a.mk_numeral(value.get_rational(), false), m); - if (!value.is_finite()) { - bound = m.mk_false(); - return value; - } // update model to use new values that satisfy optimality ptr_vector vars; @@ -1160,17 +1166,42 @@ namespace qe { TRACE("qe", tout << "omitting model update for non-uninterpreted constant " << mk_pp(e, m) << "\n";); } } + expr_ref val(a.mk_numeral(value.get_rational(), false), m); + expr_ref tval(m); + VERIFY (mdl.eval(t, tval)); - // update the predicate 'bound' which forces larger values. - if (value.get_infinitesimal().is_neg()) { - bound = a.mk_le(val, t); + // update the predicate 'bound' which forces larger values when 'strict' is true. + // strict: bound := valuue < t + // !strict: bound := value <= t + if (!value.is_finite()) { + ge = a.mk_ge(t, tval); + gt = m.mk_false(); + } + else if (value.get_infinitesimal().is_neg()) { + ge = a.mk_ge(t, tval); + gt = a.mk_ge(t, val); } else { - bound = a.mk_lt(val, t); - } + ge = a.mk_ge(t, val); + gt = a.mk_gt(t, val); + } + validate_model(mdl, fmls0); return value; } + bool validate_model(model& mdl, expr_ref_vector const& fmls) { + bool valid = true; + for (unsigned i = 0; i < fmls.size(); ++i) { + expr_ref val(m); + VERIFY(mdl.eval(fmls[i], val)); + if (!m.is_true(val)) { + valid = false; + TRACE("qe", tout << mk_pp(fmls[i], m) << " := " << val << "\n";); + } + } + return valid; + } + void extract_coefficients(opt::model_based_opt& mbo, model& model, obj_map const& ts, obj_map& tids, vars& coeffs) { coeffs.reset(); obj_map::iterator it = ts.begin(), end = ts.end(); @@ -1219,8 +1250,8 @@ namespace qe { return m_imp->a.get_family_id(); } - opt::inf_eps arith_project_plugin::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) { - return m_imp->maximize(fmls, mdl, t, bound); + opt::inf_eps arith_project_plugin::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) { + return m_imp->maximize(fmls, mdl, t, ge, gt); } bool arith_project(model& model, app* var, expr_ref_vector& lits) { diff --git a/src/qe/qe_arith.h b/src/qe/qe_arith.h index f71156b1e..dce9b1af4 100644 --- a/src/qe/qe_arith.h +++ b/src/qe/qe_arith.h @@ -32,7 +32,7 @@ namespace qe { 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); + opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt); }; bool arith_project(model& model, app* var, expr_ref_vector& lits); diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 2bacb3a4f..219a4b45a 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -285,9 +285,9 @@ class mbp::impl { public: - opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) { + opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) { arith_project_plugin arith(m); - return arith.maximize(fmls, mdl, t, bound); + return arith.maximize(fmls, mdl, t, ge, gt); } void extract_literals(model& model, expr_ref_vector& fmls) { @@ -428,7 +428,16 @@ public: } } + bool validate_model(model& model, expr_ref_vector const& fmls) { + expr_ref val(m); + for (unsigned i = 0; i < fmls.size(); ++i) { + VERIFY(model.eval(fmls[i], val) && m.is_true(val)); + } + return true; + } + void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls) { + SASSERT(validate_model(model, fmls)); expr_ref val(m), tmp(m); app_ref var(m); expr_ref_vector unused_fmls(m); @@ -446,6 +455,7 @@ public: } } while (!vars.empty() && !fmls.empty()) { + std::cout << "mbp: " << var << "\n"; var = vars.back(); vars.pop_back(); project_plugin* p = get_plugin(var); @@ -483,6 +493,7 @@ public: vars.reset(); } fmls.append(unused_fmls); + SASSERT(validate_model(model, fmls)); TRACE("qe", tout << vars << " " << fmls << "\n";); } @@ -508,6 +519,6 @@ void mbp::extract_literals(model& model, expr_ref_vector& lits) { m_impl->extract_literals(model, lits); } -opt::inf_eps mbp::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) { - return m_impl->maximize(fmls, mdl, t, bound); +opt::inf_eps mbp::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) { + return m_impl->maximize(fmls, mdl, t, ge, gt); } diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h index 6c28555b0..b195d3a35 100644 --- a/src/qe/qe_mbp.h +++ b/src/qe/qe_mbp.h @@ -79,7 +79,7 @@ namespace qe { \brief Maximize objective t under current model for constraints in fmls. */ - opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound); + opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt); }; } diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index a409b23c2..74b6769ae 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -507,6 +507,26 @@ namespace qe { } } + bool pred_abs::validate_defs(model& model) const { + bool valid = true; + obj_map::iterator it = m_pred2lit.begin(), end = m_pred2lit.end(); + for (; it != end; ++it) { + expr_ref val_a(m), val_b(m); + expr* a = it->m_key; + expr* b = it->m_value; + VERIFY(model.eval(a, val_a)); + VERIFY(model.eval(b, val_b)); + if (val_a != val_b) { + TRACE("qe", + tout << mk_pp(a, m) << " := " << val_a << "\n"; + tout << mk_pp(b, m) << " := " << val_b << "\n"; + tout << m_elevel.find(a) << "\n";); + valid = false; + } + } + return valid; + } + class kernel { ast_manager& m; params_ref m_params; @@ -575,6 +595,9 @@ namespace qe { app* m_objective; opt::inf_eps* m_value; bool m_was_sat; + model_ref m_model_save; + expr_ref m_gt; + opt::inf_eps m_value_save; /** @@ -588,15 +611,23 @@ namespace qe { check_cancel(); expr_ref_vector asms(m_asms); m_pred_abs.get_assumptions(m_model.get(), asms); + if (m_model.get()) { + validate_assumptions(*m_model.get(), asms); + } TRACE("qe", tout << asms << "\n";); solver& s = get_kernel(m_level).s(); lbool res = s.check_sat(asms); switch (res) { case l_true: s.get_model(m_model); + SASSERT(validate_defs("check_sat")); + SASSERT(validate_assumptions(*m_model.get(), asms)); SASSERT(validate_model(asms)); TRACE("qe", s.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); ); push(); + if (m_level == 1 && m_mode == qsat_maximize) { + maximize_model(); + } break; case l_false: switch (m_level) { @@ -607,6 +638,7 @@ namespace qe { return l_true; } if (m_model.get()) { + SASSERT(validate_assumptions(*m_model.get(), asms)); if (!project_qe(asms)) return l_undef; } else { @@ -734,7 +766,28 @@ namespace qe { } } + bool validate_defs(char const* msg) { + if (m_model.get() && !m_pred_abs.validate_defs(*m_model.get())) { + TRACE("qe", + tout << msg << "\n"; + display(tout); + if (m_level > 0) { + get_kernel(m_level-1).s().display(tout); + } + expr_ref_vector asms(m); + m_pred_abs.get_assumptions(m_model.get(), asms); + tout << asms << "\n"; + m_pred_abs.pred2lit(asms); + tout << asms << "\n";); + return false; + } + else { + return true; + } + } + bool get_core(expr_ref_vector& core, unsigned level) { + SASSERT(validate_defs("get_core")); get_kernel(level).get_core(core); m_pred_abs.pred2lit(core); return true; @@ -814,33 +867,33 @@ namespace qe { if (!get_core(core, m_level)) { return false; } - SASSERT(validate_core(core)); + SASSERT(validate_core(mdl, core)); get_vars(m_level); + SASSERT(validate_assumptions(mdl, core)); m_mbp(force_elim(), m_avars, mdl, core); + SASSERT(validate_defs("project_qe")); if (m_mode == qsat_maximize) { - maximize(core, mdl); - pop(1); + maximize_core(core, mdl); } else { fml = negate_core(core); add_assumption(fml); m_answer.push_back(fml); m_free_vars.append(m_avars); - pop(1); } + pop(1); return true; } bool project(expr_ref_vector& core) { if (!get_core(core, m_level)) return false; TRACE("qe", display(tout); display(tout << "core\n", core);); - SASSERT(validate_core(core)); SASSERT(m_level >= 2); expr_ref fml(m); expr_ref_vector defs(m), core_save(m); max_level level; model& mdl = *m_model.get(); - + SASSERT(validate_core(mdl, core)); get_vars(m_level-1); SASSERT(validate_project(mdl, core)); m_mbp(force_elim(), m_avars, mdl, core); @@ -875,6 +928,7 @@ namespace qe { fml = m_pred_abs.mk_abstract(fml); get_kernel(m_level).assert_expr(fml); } + SASSERT(!m_model.get()); return true; } @@ -1005,7 +1059,19 @@ namespace qe { } } - bool validate_core(expr_ref_vector const& core) { + bool validate_assumptions(model& mdl, expr_ref_vector const& core) { + for (unsigned i = 0; i < core.size(); ++i) { + expr_ref val(m); + VERIFY(mdl.eval(core[i], val)); + if (!m.is_true(val)) { + TRACE("qe", tout << "component of core is not true: " << mk_pp(core[i], m) << "\n";); + return false; + } + } + return true; + } + + bool validate_core(model& mdl, expr_ref_vector const& core) { return true; #if 0 TRACE("qe", tout << "Validate core\n";); @@ -1130,7 +1196,8 @@ namespace qe { m_free_vars(m), m_objective(0), m_value(0), - m_was_sat(false) + m_was_sat(false), + m_gt(m) { reset(); } @@ -1258,6 +1325,7 @@ namespace qe { m_objective = t; m_value = &value; m_was_sat = false; + m_model_save.reset(); m_pred_abs.abstract_atoms(fml, defs); fml = m_pred_abs.mk_abstract(fml); m_ex.assert_expr(mk_and(defs)); @@ -1271,6 +1339,7 @@ namespace qe { if (!m_was_sat) { return l_false; } + mdl = m_model_save; break; case l_true: UNREACHABLE(); @@ -1286,15 +1355,49 @@ namespace qe { return l_true; } - void maximize(expr_ref_vector const& core, model& mdl) { + void maximize_core(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); - IF_VERBOSE(0, verbose_stream() << "(maximize " << *m_value << " bound: " << bound << ")\n";); - m_ex.assert_expr(bound); + *m_value = m_value_save; + IF_VERBOSE(3, verbose_stream() << "(maximize " << *m_value << ")\n";); + m_ex.assert_expr(m_gt); + m_fa.assert_expr(m_gt); + } + + void maximize_model() { + SASSERT(m_level == 1 && m_mode == qsat_maximize); + SASSERT(m_objective); + expr_ref ge(m); + expr_ref_vector asms(m), defs(m); + m_pred_abs.get_assumptions(m_model.get(), asms); + m_pred_abs.pred2lit(asms); + + SASSERT(validate_defs("maximize_model1")); + + m_value_save = m_mbp.maximize(asms, *m_model.get(), m_objective, ge, m_gt); + + SASSERT(validate_defs("maximize_model2")); + + // bound := val <= m_objective + + IF_VERBOSE(3, verbose_stream() << "(qsat-maximize-bound: " << m_value_save << ")\n";); + + max_level level; + m_pred_abs.abstract_atoms(ge, level, defs); + m_ex.assert_expr(mk_and(defs)); + m_fa.assert_expr(mk_and(defs)); + + ge = m_pred_abs.mk_abstract(ge); + + SASSERT(is_uninterp_const(ge)); + // update model with evaluation for bound. + if (is_uninterp_const(ge)) { + m_model->register_decl(to_app(ge)->get_decl(), m.mk_true()); + } + SASSERT(validate_defs("maximize_model3")); } }; diff --git a/src/qe/qsat.h b/src/qe/qsat.h index 66676da05..b6d21db1e 100644 --- a/src/qe/qsat.h +++ b/src/qe/qsat.h @@ -112,6 +112,8 @@ namespace qe { void display(std::ostream& out) const; void display(std::ostream& out, expr_ref_vector const& asms) const; void collect_statistics(statistics& st) const; + + bool validate_defs(model& model) const; }; class qmax { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 8b2453e31..3c260abbe 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1406,10 +1406,8 @@ namespace smt { void internalize_instance(expr * body, proof * pr, unsigned generation) { internalize_assertion(body, pr, generation); -#ifndef SMTCOMP if (relevancy()) m_case_split_queue->internalize_instance_eh(body, generation); -#endif } bool already_internalized() const { return m_e_internalized_stack.size() > 2 || m_b_internalized_stack.size() > 1; } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 0d9c361f8..df271095f 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -138,8 +138,10 @@ namespace smt { } bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) { - if (cex == 0) - return false; // no model available. + if (cex == 0) { + TRACE("model_checker", tout << "no model is available\n";); + return false; + } unsigned num_decls = q->get_num_decls(); // Remark: sks were created for the flat version of q. SASSERT(sks.size() >= num_decls); @@ -153,8 +155,10 @@ namespace smt { sk_value = cex->get_const_interp(sk_d); if (sk_value == 0) { sk_value = cex->get_some_value(sk_d->get_range()); - if (sk_value == 0) + if (sk_value == 0) { + TRACE("model_checker", tout << "Could not get value for " << sk_d->get_name() << "\n";); return false; // get_some_value failed... giving up + } } if (use_inv) { unsigned sk_term_gen; @@ -166,6 +170,7 @@ namespace smt { sk_value = sk_term; } else { + TRACE("model_checker", tout << "no inverse value for " << sk_value << "\n";); return false; } } @@ -175,8 +180,10 @@ namespace smt { sk_value = sk_term; } } - if (contains_model_value(sk_value)) + if (contains_model_value(sk_value)) { + TRACE("model_checker", tout << "value is private to model: " << sk_value << "\n";); return false; + } bindings.set(num_decls - i - 1, sk_value); } @@ -286,18 +293,15 @@ namespace smt { break; model_ref cex; m_aux_context->get_model(cex); - if (add_instance(q, cex.get(), sks, true)) { - num_new_instances++; - if (num_new_instances < m_max_cexs) { - if (!add_blocking_clause(cex.get(), sks)) - break; // add_blocking_clause failed... stop the search for new counter-examples... - } - } - else { + if (!add_instance(q, cex.get(), sks, true)) { break; } - if (num_new_instances >= m_max_cexs) - break; + num_new_instances++; + if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) { + TRACE("model_checker", tout << "Add blocking clause failed\n";); + // add_blocking_clause failed... stop the search for new counter-examples... + break; + } } if (num_new_instances == 0) { @@ -368,8 +372,10 @@ namespace smt { if (it == end) return true; - if (m_iteration_idx >= m_params.m_mbqi_max_iterations) + if (m_iteration_idx >= m_params.m_mbqi_max_iterations) { + IF_VERBOSE(10, verbose_stream() << "(smt.mbqi \"max instantiations reached \")" << m_iteration_idx << "\n";); return false; + } m_curr_model = md; m_value2expr.reset();