From 49279d70470d9acd5ab018a0058570835486b097 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Jun 2018 21:17:35 -0700 Subject: [PATCH] debugging mbi Signed-off-by: Nikolaj Bjorner --- src/ast/for_each_expr.h | 14 ++++ src/math/simplex/model_based_opt.cpp | 36 ++++++++-- src/math/simplex/model_based_opt.h | 2 + src/qe/qe_arith.cpp | 13 ++-- src/qe/qe_mbi.cpp | 102 ++++++++++++++------------- src/qe/qe_mbi.h | 4 ++ 6 files changed, 112 insertions(+), 59 deletions(-) diff --git a/src/ast/for_each_expr.h b/src/ast/for_each_expr.h index 50a4089dc..6e203ccee 100644 --- a/src/ast/for_each_expr.h +++ b/src/ast/for_each_expr.h @@ -128,6 +128,20 @@ void for_each_expr(ForEachProc & proc, expr * n) { for_each_expr_core(proc, visited, n); } +template +void for_each_expr(ForEachProc & proc, unsigned n, expr * const* es) { + expr_mark visited; + for (unsigned i = 0; i < n; ++i) + for_each_expr_core(proc, visited, es[i]); +} + +template +void for_each_expr(ForEachProc & proc, expr_ref_vector const& es) { + expr_mark visited; + for (expr* e : es) + for_each_expr_core(proc, visited, e); +} + template void quick_for_each_expr(ForEachProc & proc, expr_fast_mark1 & visited, expr * n) { for_each_expr_core(proc, visited, n); diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index 56d51648d..93e55bedd 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/src/math/simplex/model_based_opt.cpp @@ -523,18 +523,26 @@ namespace opt { rational slack = (abs_src_c - rational::one()) * (abs_dst_c - rational::one()); rational dst_val = dst.m_value - x_val*dst_c; rational src_val = src.m_value - x_val*src_c; - bool use_case1 = - (src_c * dst_val + dst_c * src_val + slack).is_nonpos() - || abs_src_c.is_one() - || abs_dst_c.is_one(); + rational distance = src_c * dst_val + dst_c * src_val + slack; + bool use_case1 = distance.is_nonpos() || abs_src_c.is_one() || abs_dst_c.is_one(); + + if (distance.is_nonpos() && !abs_src_c.is_one() && !abs_dst_c.is_one()) { + unsigned r = copy_row(row_src); + mul_add(false, r, rational::one(), row_dst); + del_var(r, x); + add(r, slack); + TRACE("qe", tout << m_rows[r];); + SASSERT(!m_rows[r].m_value.is_pos()); + } if (use_case1) { + TRACE("opt", tout << "slack: " << slack << " " << src_c << " " << dst_val << " " << dst_c << " " << src_val << "\n";); // dst <- abs_src_c*dst + abs_dst_c*src - slack mul(row_dst, abs_src_c); sub(row_dst, slack); - mul_add(false, row_dst, abs_dst_c, row_src); + mul_add(false, row_dst, abs_dst_c, row_src); return; - } + } // // create finite disjunction for |b|. @@ -555,6 +563,7 @@ namespace opt { // exists z in [0 .. |b|-2] . |b| | (z + s) && a*n_sign(b)(s + z) + |b|t <= 0 // + TRACE("qe", tout << "finite disjunction " << distance << " " << src_c << " " << dst_c << "\n";); vector coeffs; if (abs_dst_c <= abs_src_c) { rational z = mod(dst_val, abs_dst_c); @@ -611,6 +620,21 @@ namespace opt { r.m_value -= c; } + void model_based_opt::del_var(unsigned dst, unsigned x) { + row& r = m_rows[dst]; + unsigned j = 0; + for (var & v : r.m_vars) { + if (v.m_id == x) { + r.m_value -= eval(x)*r.m_coeff; + } + else { + r.m_vars[j++] = v; + } + } + r.m_vars.shrink(j); + } + + void model_based_opt::normalize(unsigned row_id) { row& r = m_rows[row_id]; if (r.m_vars.empty()) return; diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h index a1137d2fa..e52d0cfe0 100644 --- a/src/math/simplex/model_based_opt.h +++ b/src/math/simplex/model_based_opt.h @@ -120,6 +120,8 @@ namespace opt { void sub(unsigned dst, rational const& c); + void del_var(unsigned dst, unsigned x); + void set_row(unsigned row_id, vector const& coeffs, rational const& c, rational const& m, ineq_type rel); void add_constraint(vector const& coeffs, rational const& c, rational const& m, ineq_type r); diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index e9653bf14..7e619ccd5 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -417,7 +417,7 @@ namespace qe { ts.push_back(t); } t = mk_add(ts); - s = a.mk_numeral(-r.m_coeff, a.is_int(t)); + s = a.mk_numeral(-r.m_coeff, r.m_coeff.is_int() && a.is_int(t)); 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; @@ -445,7 +445,8 @@ namespace qe { for (var const& v : d.m_vars) { ts.push_back(var2expr(index2expr, v)); } - ts.push_back(a.mk_numeral(d.m_coeff, is_int)); + if (!d.m_coeff.is_zero()) + ts.push_back(a.mk_numeral(d.m_coeff, is_int)); t = mk_add(ts); if (!d.m_div.is_one() && is_int) { t = a.mk_idiv(t, a.mk_numeral(d.m_div, is_int)); @@ -461,10 +462,12 @@ namespace qe { } expr_ref mk_add(expr_ref_vector const& ts) { - if (ts.size() == 1) { + switch (ts.size()) { + case 0: + return expr_ref(a.mk_int(0), m); + case 1: return expr_ref(ts.get(0), m); - } - else { + default: return expr_ref(a.mk_add(ts.size(), ts.c_ptr()), m); } } diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 6f2c346f0..070c5279c 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -259,12 +259,11 @@ namespace qe { app_ref_vector& m_vars; arith_util arith; obj_hashtable m_exclude; - is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& shared): + is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& shared): m(vars.m()), m_vars(vars), arith(m) { for (func_decl* f : shared) m_exclude.insert(f); } void operator()(app* a) { - TRACE("qe", tout << expr_ref(a, m) << " " << arith.is_int_real(a) << " " << a->get_family_id() << "\n";); if (arith.is_int_real(a) && a->get_family_id() != arith.get_family_id() && !m_exclude.contains(a->get_decl())) { m_vars.push_back(a); } @@ -291,17 +290,7 @@ namespace qe { } } - mbi_result euf_arith_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl) { - lbool r = m_solver->check_sat(lits); - - switch (r) { - case l_false: - lits.reset(); - m_solver->get_unsat_core(lits); - // optionally minimize core using superposition. - return mbi_unsat; - case l_true: { - m_solver->get_model(mdl); + bool euf_arith_mbi_plugin::get_literals(model_ref& mdl, expr_ref_vector& lits) { model_evaluator mev(*mdl.get()); lits.reset(); for (expr* e : m_atoms) { @@ -313,49 +302,65 @@ namespace qe { } } TRACE("qe", tout << "atoms from model: " << lits << "\n";); - r = m_dual_solver->check_sat(lits); - expr_ref_vector core(m); - term_graph tg(m); - switch (r) { - case l_false: { + lbool r = m_dual_solver->check_sat(lits); + if (l_false == r) { // use the dual solver to find a 'small' implicant - m_dual_solver->get_unsat_core(core); - TRACE("qe", tout << "core: " << core << "\n";); lits.reset(); - lits.append(core); + m_dual_solver->get_unsat_core(lits); + return true; + } + else { + return false; + } + } + + app_ref_vector euf_arith_mbi_plugin::get_arith_vars(expr_ref_vector const& lits) { arith_util a(m); - // populate set of arithmetic variables to be projected. app_ref_vector avars(m); - is_arith_var_proc _proc(avars, m_shared); - for (expr* l : lits) quick_for_each_expr(_proc, l); - TRACE("qe", tout << "vars: " << avars << " lits: " << lits << "\n";); + is_arith_var_proc _proc(avars, m_shared); + for_each_expr(_proc, lits); + return avars; + } - // 1. project arithmetic variables using mdl that satisfies core. - // ground any remaining arithmetic variables using model. - arith_project_plugin ap(m); - ap.set_check_purified(false); + mbi_result euf_arith_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl) { + lbool r = m_solver->check_sat(lits); - auto defs = ap.project(*mdl.get(), avars, lits); - // 2. Add the projected definitions to the remaining (euf) literals - for (auto const& def : defs) { - lits.push_back(m.mk_eq(def.var, def.term)); - } - TRACE("qe", tout << "# arith defs" << defs.size() << " avars: " << avars << " " << lits << "\n";); - - // 3. Project the remaining literals with respect to EUF. - tg.set_vars(m_shared, false); - tg.add_lits(lits); - lits.reset(); - lits.append(tg.project(*mdl)); - TRACE("qe", tout << "project: " << lits << "\n";); - return mbi_sat; - } - case l_undef: - return mbi_undef; - case l_true: - UNREACHABLE(); + switch (r) { + case l_false: + lits.reset(); + m_solver->get_unsat_core(lits); + TRACE("qe", tout << "unsat core: " << lits << "\n";); + // optionally minimize core using superposition. + return mbi_unsat; + case l_true: { + m_solver->get_model(mdl); + if (!get_literals(mdl, lits)) { return mbi_undef; } + app_ref_vector avars = get_arith_vars(lits); + + TRACE("qe", tout << "vars: " << avars << " lits: " << lits << "\n";); + + // 1. project arithmetic variables using mdl that satisfies core. + // ground any remaining arithmetic variables using model. + arith_project_plugin ap(m); + ap.set_check_purified(false); + + auto defs = ap.project(*mdl.get(), avars, lits); + // 2. Add the projected definitions to the remaining (euf) literals + for (auto const& def : defs) { + lits.push_back(m.mk_eq(def.var, def.term)); + } + TRACE("qe", tout << "# arith defs" << defs.size() << " avars: " << avars << " " << lits << "\n";); + + // 3. Project the remaining literals with respect to EUF. + term_graph tg(m); + tg.set_vars(m_shared, false); + tg.add_lits(lits); + lits.reset(); + //lits.append(tg.project(*mdl)); + lits.append(tg.project()); + TRACE("qe", tout << "project: " << lits << "\n";); return mbi_sat; } default: @@ -448,6 +453,7 @@ namespace qe { case l_undef: return l_undef; } + break; case l_false: itp = mk_and(itps); return l_false; diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h index 5e43a6412..22a0864ba 100644 --- a/src/qe/qe_mbi.h +++ b/src/qe/qe_mbi.h @@ -109,6 +109,10 @@ namespace qe { solver_ref m_dual_solver; struct is_atom_proc; struct is_arith_var_proc; + + app_ref_vector get_arith_vars(expr_ref_vector const& lits); + bool get_literals(model_ref& mdl, expr_ref_vector& lits); + public: euf_arith_mbi_plugin(solver* s, solver* sNot); ~euf_arith_mbi_plugin() override {}