From 4415df3fcf7dcf7108f03a27035b8f4e6a0b8b10 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Jun 2014 19:10:20 +0530 Subject: [PATCH] various fixes Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 1 + src/muz/rel/dl_product_relation.cpp | 6 +- src/opt/opt_cmds.cpp | 2 +- src/opt/opt_context.cpp | 67 ++++++++-------------- src/opt/opt_context.h | 3 +- src/opt/weighted_maxsat.cpp | 87 +++++++++++++++++++---------- 6 files changed, 89 insertions(+), 77 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 4373ee33a..a76933912 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1372,6 +1372,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions while (r == l_true && get_opt()->is_pareto()) { was_pareto = true; get_opt()->display_assignment(regular_stream()); + regular_stream() << "\n"; r = get_opt()->optimize(); } } diff --git a/src/muz/rel/dl_product_relation.cpp b/src/muz/rel/dl_product_relation.cpp index 48cd666e6..b66e4d47d 100644 --- a/src/muz/rel/dl_product_relation.cpp +++ b/src/muz/rel/dl_product_relation.cpp @@ -184,8 +184,10 @@ namespace datalog { } relation_base * product_relation_plugin::mk_full(func_decl* p, const relation_signature & s, family_id kind) { - if (kind == null_family_id) { - return alloc(product_relation, *this, s); + if (kind == null_family_id || !m_spec_store.contains_signature(s)) { + product_relation* result = alloc(product_relation, *this, s); + result->m_default_empty = false; + return result; } rel_spec spec; m_spec_store.get_relation_spec(s, kind, spec); diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 42d749cb6..537f4bf22 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -269,6 +269,7 @@ public: if (r == l_true && opt.is_pareto()) { while (r == l_true) { display_result(ctx); + ctx.regular_stream() << "\n"; r = opt.optimize(); } if (p.get_bool("print_statistics", false)) { @@ -314,7 +315,6 @@ public: if (mdl) { ctx.regular_stream() << "(model " << std::endl; model_smt2_pp(ctx.regular_stream(), ctx, *(mdl.get()), 2); - // m->display(ctx.regular_stream()); ctx.regular_stream() << ")" << std::endl; } } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 1ad9909ad..b8eeb0d09 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -42,6 +42,7 @@ namespace opt { void context::scoped_state::push() { m_hard_lim.push_back(m_hard.size()); m_objectives_lim.push_back(m_objectives.size()); + m_objectives_term_trail_lim.push_back(m_objectives_term_trail.size()); } void context::scoped_state::pop() { @@ -372,48 +373,10 @@ namespace opt { void context::yield() { m_pareto->get_model(m_model); - update_lower(true); - for (unsigned i = 0; i < m_objectives.size(); ++i) { - objective const& obj = m_objectives[i]; - switch(obj.m_type) { - case O_MINIMIZE: - case O_MAXIMIZE: - m_optsmt.update_upper(obj.m_index, m_optsmt.get_lower(obj.m_index), true); - break; - case O_MAXSMT: { - rational r = m_maxsmts.find(obj.m_id)->get_lower(); - m_maxsmts.find(obj.m_id)->update_upper(r, true); - break; - } - } - } + update_bound(true, true); + update_bound(true, false); } - -#if 0 - // use PB - expr_ref mk_pb_cmp(objective const& obj, model_ref& mdl, bool is_ge) { - rational r, sum(0); - expr_ref val(m), result(m); - unsigned sz = obj.m_terms.size(); - pb_util pb(m); - - for (unsigned i = 0; i < sz; ++i) { - expr* t = obj.m_terms[i]; - VERIFY(mdl->eval(t, val)); - if (m.is_true(val)) { - sum += r; - } - } - if (is_ge) { - result = pb.mk_ge(obj.m_terms.size(), obj.m_weights.c_ptr(), obj.m_terms.c_ptr(), r); - } - else { - result = pb.mk_le(obj.m_terms.size(), obj.m_weights.c_ptr(), obj.m_terms.c_ptr(), r); - } - } -#endif - lbool context::execute_pareto() { if (!m_pareto) { m_pareto = alloc(gia_pareto, m, *this, m_solver.get(), m_params); @@ -761,7 +724,7 @@ namespace opt { } } - void context::update_lower(bool override) { + void context::update_bound(bool override, bool is_lower) { expr_ref val(m); for (unsigned i = 0; i < m_objectives.size(); ++i) { objective const& obj = m_objectives[i]; @@ -770,18 +733,27 @@ namespace opt { case O_MINIMIZE: if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) { r += obj.m_offset; - m_optsmt.update_lower(obj.m_index, inf_eps(-r), override); + if (is_lower) { + m_optsmt.update_lower(obj.m_index, inf_eps(-r), override); + } + else { + m_optsmt.update_upper(obj.m_index, inf_eps(-r), override); + } } break; case O_MAXIMIZE: if (m_model->eval(obj.m_term, val) && is_numeral(val, r)) { r += obj.m_offset; - m_optsmt.update_lower(obj.m_index, inf_eps(r), override); + if (is_lower) { + m_optsmt.update_lower(obj.m_index, inf_eps(r), override); + } + else { + m_optsmt.update_upper(obj.m_index, inf_eps(r), override); + } } break; case O_MAXSMT: { bool ok = true; - r = obj.m_offset; for (unsigned j = 0; ok && j < obj.m_terms.size(); ++j) { if (m_model->eval(obj.m_terms[j], val)) { if (!m.is_true(val)) { @@ -793,7 +765,12 @@ namespace opt { } } if (ok) { - m_maxsmts.find(obj.m_id)->update_upper(r, override); + if (is_lower) { + m_maxsmts.find(obj.m_id)->update_upper(r, override); + } + else { + m_maxsmts.find(obj.m_id)->update_lower(r, override); + } } break; } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 18d6d3745..1f7eb55af 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -192,7 +192,8 @@ namespace opt { void from_fmls(expr_ref_vector const& fmls); void simplify_fmls(expr_ref_vector& fmls); - void update_lower(bool override); + void update_lower(bool override) { update_bound(override, true); } + void update_bound(bool override, bool is_lower); inf_eps get_lower_as_num(unsigned idx); inf_eps get_upper_as_num(unsigned idx); diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index c1b22f075..6c4bbc1b4 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -39,6 +39,8 @@ Notes: #include "scoped_timer.h" #include "optsmt.h" +#define USE_SIMPLEX 0 + namespace opt { class scoped_stopwatch { @@ -644,7 +646,7 @@ namespace opt { virtual void set_cancel(bool f) { maxsmt_solver_base::set_cancel(f); - // maxs->set_cancel(f); + maxs->set_cancel(f); m_optsmt.set_cancel(f); } @@ -655,7 +657,7 @@ namespace opt { virtual void collect_statistics(statistics& st) const { maxsmt_solver_base::collect_statistics(st); - // maxs->s().collect_statistics(st); + maxs->s().collect_statistics(st); st.update("hsmax-num-iterations", m_stats.m_num_iterations); st.update("hsmax-num-core-reductions-n", m_stats.m_num_core_reductions_failure); st.update("hsmax-num-core-reductions-y", m_stats.m_num_core_reductions_success); @@ -738,21 +740,26 @@ namespace opt { m_aux_active.push_back(false); m_core_activity.push_back(0); m_aux2index.insert(m_aux.back(), i); +#if USE_SIMPLEX m_aux2index.insert(m_iaux.back(), i); fml = m.mk_and(a.mk_le(a.mk_numeral(rational::zero(), true), iaux), a.mk_le(iaux, a.mk_numeral(rational::one(), true))); rational const& w = m_weights[i]; sum.push_back(a.mk_mul(a.mk_numeral(w, w.is_int()), iaux)); m_solver.assert_expr(fml); +#endif if (tt) { m_asms.push_back(m_aux.back()); ensure_active(i); } } +#if USE_SIMPLEX obj = a.mk_add(sum.size(), sum.c_ptr()); m_objective = m_optsmt.add(obj); m_optsmt.setup(m_solver); - // maxs->init_soft(m_weights, m_aux); +#else + maxs->init_soft(m_weights, m_aux); +#endif TRACE("opt", print_seed(tout);); } @@ -878,9 +885,9 @@ namespace opt { // // produce the non-optimal hitting set by using the 10% heuristic. // of most active cores constraints. + // m_asms contains the current core. // void find_non_optimal_hitting_set(ptr_vector& hs) { - // m_asms contains the current core. std::sort(m_asms.begin(), m_asms.end(), lt_activity(*this)); for (unsigned i = m_asms.size(); i > 9*m_asms.size()/10;) { --i; @@ -899,7 +906,7 @@ namespace opt { lbool next_seed() { scoped_stopwatch _sw(m_stats.m_aux_sat_time); TRACE("opt", tout << "\n";); -#if 1 +#if USE_SIMPLEX m_solver.display(std::cout); lbool is_sat = m_optsmt.lex(m_objective); if (is_sat == l_true) { @@ -919,7 +926,27 @@ namespace opt { } #else - lbool is_sat = maxs->s().check_sat(0,0); + + // min c_i*(not x_i) for x_i are soft clauses. + // max c_i*x_i for x_i are soft clauses + + lbool is_sat = l_true; + if (m_lower.is_pos()) { + expr_ref fml(m); + solver::scoped_push _scope(maxs->s()); + fml = pb.mk_le(num_soft(), m_weights.c_ptr(), m_naux.c_ptr(), m_lower); + maxs->add_hard(fml); + //fml = pb.mk_ge(num_soft(), m_weights.c_ptr(), m_naux.c_ptr(), m_lower); + //maxs->add_hard(fml); + std::cout << fml << "\n"; + is_sat = maxs->s().check_sat(0,0); + if (is_sat == l_true) { + maxs->set_model(); + extract_seed(); + return l_true; + } + } + is_sat = maxs->s().check_sat(0,0); if (is_sat == l_true) { maxs->set_model(); } @@ -927,24 +954,27 @@ namespace opt { return is_sat; } is_sat = (*maxs)(); - + if (is_sat == l_true) { - model_ref mdl; - maxs->get_model(mdl); - for (unsigned i = 0; i < num_soft(); ++i) { - if (is_active(i)) { - m_seed[i] = is_true(mdl, m_aux[i].get()); - } - else { - m_seed[i] = false; - } - } - TRACE("opt", print_seed(tout);); + extract_seed(); } #endif return is_sat; } + void extract_seed() { + model_ref mdl; + maxs->get_model(mdl); + m_lower.reset(); + for (unsigned i = 0; i < num_soft(); ++i) { + m_seed[i] = is_active(i) && is_true(mdl, m_aux[i].get()); + if (!m_seed[i]) { + m_lower += m_weights[i]; + } + } + TRACE("opt", print_seed(tout);); + } + // // check assignment returned by maxs with the original // hard constraints. @@ -1018,15 +1048,16 @@ namespace opt { } } } - //rational old_upper = m_upper; - m_upper.reset(); + rational upper(0); for (unsigned i = 0; i < num_soft(); ++i) { if (!m_seed[i]) { - m_upper += m_weights[i]; + upper += m_weights[i]; } - } - //SASSERT(old_upper > m_upper); - TRACE("opt", tout << "new upper: " << m_upper << "\n";); + } + if (upper < m_upper) { + m_upper = upper; + TRACE("opt", tout << "new upper: " << m_upper << "\n";); + } return true; } @@ -1109,7 +1140,7 @@ namespace opt { } expr_ref_vector fmls(m); expr_ref fml(m); -#if 1 +#if USE_SIMPLEX for (unsigned i = 0; i < num_soft(); ++i) { if (!indices.contains(i)) { fmls.push_back(m_iaux[i].get()); @@ -1126,9 +1157,9 @@ namespace opt { } fml = m.mk_or(fmls.size(), fmls.c_ptr()); maxs->add_hard(fml); + set_upper(); #endif TRACE("opt", tout << fml << "\n";); - // set_upper(); } // constrain the upper bound. @@ -1143,7 +1174,7 @@ namespace opt { void block_up() { expr_ref_vector fmls(m); expr_ref fml(m); -#if 1 +#if USE_SIMPLEX for (unsigned i = 0; i < m_asms.size(); ++i) { unsigned index = m_aux2index.find(m_asms[i]); m_core_activity[index]++; @@ -1655,7 +1686,7 @@ namespace opt { else if (m_engine == symbol("hsmax")) { ref s0 = alloc(opt_solver, m, m_params, symbol()); s0->check_sat(0,0); - maxsmt_solver_base* s2 = alloc(pbmax, s0.get(), m); // , s0->get_context(); + maxsmt_solver_base* s2 = alloc(pbmax, s0.get(), m); // , s0->get_context()); s2->set_converter(s0->mc_ref().get()); m_maxsmt = alloc(hsmax, s.get(), m, s2); }