From 761c7d9a40373f0e37b9d0786c27a48c2c414a40 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 25 Jan 2015 04:01:18 -0800 Subject: [PATCH] adding annotation to logging to show number of columns and rows, adding dual propagation sketch Signed-off-by: Nikolaj Bjorner --- src/muz/rel/dl_base.h | 1 + src/muz/rel/dl_instruction.cpp | 80 ++++---- src/muz/rel/dl_instruction.h | 13 +- src/muz/rel/rel_context.cpp | 2 +- src/opt/inc_sat_solver.cpp | 7 +- src/opt/maxres.cpp | 330 +++++++++------------------------ src/opt/maxres.h | 4 +- src/opt/maxsmt.cpp | 9 +- src/opt/opt_context.cpp | 3 +- src/opt/opt_params.pyg | 2 +- src/sat/sat_solver.cpp | 2 +- src/shell/datalog_frontend.cpp | 2 +- 12 files changed, 152 insertions(+), 303 deletions(-) diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index fa9bc84ee..2dffa04f6 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -506,6 +506,7 @@ namespace datalog { virtual unsigned get_size_estimate_rows() const { return UINT_MAX; } virtual unsigned get_size_estimate_bytes() const { return UINT_MAX; } virtual bool knows_exact_size() const { return false; } + unsigned num_columns() const { return get_signature().size(); } virtual void display(std::ostream & out) const = 0; }; diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index 7fbe2f5ad..ea25dfc59 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -62,6 +62,10 @@ namespace datalog { return dynamic_cast(*m_context.get_rel_context()); } + rel_context const& execution_context::get_rel_context() const { + return dynamic_cast(*m_context.get_rel_context()); + } + struct compare_size_proc { typedef std::pair pr; bool operator()(pr const& a, pr const& b) const { @@ -164,21 +168,21 @@ namespace datalog { } - void instruction::display_indented(rel_context_base const & _ctx, std::ostream & out, std::string indentation) const { + void instruction::display_indented(execution_context const & _ctx, std::ostream & out, std::string indentation) const { out << indentation; - rel_context const& ctx = dynamic_cast(_ctx); - display_head_impl(ctx, out); + rel_context const& ctx = _ctx.get_rel_context(); + display_head_impl(_ctx, out); if (ctx.output_profile()) { out << " {"; output_profile(out); out << '}'; } out << "\n"; - display_body_impl(ctx, out, indentation); + display_body_impl(_ctx, out, indentation); } void instruction::log_verbose(execution_context& ctx) { - IF_VERBOSE(2, display(ctx.get_rel_context(), verbose_stream());); + IF_VERBOSE(2, display(ctx, verbose_stream());); } class instr_io : public instruction { @@ -217,7 +221,7 @@ namespace datalog { virtual void make_annotations(execution_context & ctx) { ctx.set_register_annotation(m_reg, m_pred->get_name().bare_str()); } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { const char * rel_name = m_pred->get_name().bare_str(); if (m_store) { out << "store " << m_reg << " into " << rel_name; @@ -248,7 +252,7 @@ namespace datalog { virtual void make_annotations(execution_context & ctx) { ctx.set_register_annotation(m_reg, "alloc"); } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << "dealloc " << m_reg; } }; @@ -283,7 +287,7 @@ namespace datalog { ctx.set_register_annotation(m_src, str); } } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << (m_clone ? "clone " : "move ") << m_src << " into " << m_tgt; } }; @@ -340,11 +344,11 @@ namespace datalog { virtual void make_annotations(execution_context & ctx) { m_body->make_annotations(ctx); } - virtual void display_head_impl(rel_context const & ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const & ctx, std::ostream & out) const { out << "while"; print_container(m_controls, out); } - virtual void display_body_impl(rel_context_base const & ctx, std::ostream & out, std::string indentation) const { + virtual void display_body_impl(execution_context const & ctx, std::ostream & out, std::string indentation) const { m_body->display_indented(ctx, out, indentation+" "); } }; @@ -409,7 +413,7 @@ namespace datalog { ctx.get_register_annotation(m_rel1, a1); ctx.set_register_annotation(m_res, "join " + a1 + " " + a2); } - virtual void display_head_impl(rel_context const & ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const & ctx, std::ostream & out) const { out << "join " << m_rel1; print_container(m_cols1, out); out << " and " << m_rel2; @@ -460,9 +464,9 @@ namespace datalog { a << "filter_equal " << m_col << " val: " << ctx.get_rel_context().get_rmanager().to_nice_string(m_value); ctx.set_register_annotation(m_reg, a.str()); } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << "filter_equal " << m_reg << " col: " << m_col << " val: " - << ctx.get_rmanager().to_nice_string(m_value); + << ctx.get_rel_context().get_rmanager().to_nice_string(m_value); } }; @@ -504,7 +508,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << "filter_identical " << m_reg << " "; print_container(m_cols, out); } @@ -552,7 +556,7 @@ namespace datalog { return true; } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << "filter_interpreted " << m_reg << " using " << mk_pp(m_cond, m_cond.get_manager()); } @@ -609,7 +613,7 @@ namespace datalog { return true; } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << "filter_interpreted_and_project " << m_src << " into " << m_res; out << " using " << mk_pp(m_cond, m_cond.get_manager()); out << " deleting columns "; @@ -726,7 +730,7 @@ namespace datalog { } ctx.set_register_annotation(m_delta, str); } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << (m_widen ? "widen " : "union ") << m_src << " into " << m_tgt; if (m_delta!=execution_context::void_register) { out << " with delta " << m_delta; @@ -782,7 +786,7 @@ namespace datalog { return true; } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << (m_projection ? "project " : "rename ") << m_src << " into " << m_tgt; out << (m_projection ? " deleting columns " : " with cycle "); print_container(m_cols, out); @@ -846,10 +850,20 @@ namespace datalog { } return true; } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { - out << "join_project " << m_rel1; + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { + relation_base const* r1 = ctx.reg(m_rel1); + relation_base const* r2 = ctx.reg(m_rel2); + out << "join_project " << m_rel1; + if (r1) { + out << ":" << r1->num_columns(); + out << "-" << r1->get_size_estimate_rows(); + } print_container(m_cols1, out); out << " and " << m_rel2; + if (r2) { + out << ":" << r2->num_columns(); + out << "-" << r2->get_size_estimate_rows(); + } print_container(m_cols2, out); out << " into " << m_res << " removing columns "; print_container(m_removed_cols, out); @@ -908,9 +922,9 @@ namespace datalog { } return true; } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << "select_equal_and_project " << m_src <<" into " << m_result << " col: " << m_col - << " val: " << ctx.get_rmanager().to_nice_string(m_value); + << " val: " << ctx.get_rel_context().get_rmanager().to_nice_string(m_value); } virtual void make_annotations(execution_context & ctx) { std::stringstream s; @@ -965,7 +979,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << "filter_by_negation on " << m_tgt; print_container(m_cols1, out); out << " with " << m_neg_rel; @@ -1004,10 +1018,10 @@ namespace datalog { ctx.set_reg(m_tgt, rel); return true; } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << "mk_unary_singleton into " << m_tgt << " sort:" - << ctx.get_rmanager().to_nice_string(m_sig[0]) << " val:" - << ctx.get_rmanager().to_nice_string(m_sig[0], m_fact[0]); + << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig[0]) << " val:" + << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig[0], m_fact[0]); } virtual void make_annotations(execution_context & ctx) { std::string s; @@ -1035,9 +1049,9 @@ namespace datalog { ctx.set_reg(m_tgt, ctx.get_rel_context().get_rmanager().mk_full_relation(m_sig, m_pred)); return true; } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << "mk_total into " << m_tgt << " sort:" - << ctx.get_rmanager().to_nice_string(m_sig); + << ctx.get_rel_context().get_rmanager().to_nice_string(m_sig); } virtual void make_annotations(execution_context & ctx) { std::string s; @@ -1061,7 +1075,7 @@ namespace datalog { ctx.get_rel_context().get_rmanager().mark_saturated(m_pred); return true; } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << "mark_saturated " << m_pred->get_name().bare_str(); } virtual void make_annotations(execution_context & ctx) { @@ -1085,7 +1099,7 @@ namespace datalog { } return true; } - virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { out << "instr_assert_signature of " << m_tgt << " signature:"; print_container(m_sig, out); } @@ -1166,14 +1180,14 @@ namespace datalog { } } - void instruction_block::display_indented(rel_context_base const& _ctx, std::ostream & out, std::string indentation) const { - rel_context const& ctx = dynamic_cast(_ctx); + void instruction_block::display_indented(execution_context const& _ctx, std::ostream & out, std::string indentation) const { + rel_context const& ctx = _ctx.get_rel_context(); instr_seq_type::const_iterator it = m_data.begin(); instr_seq_type::const_iterator end = m_data.end(); for(; it!=end; ++it) { instruction * i = (*it); if (i->passes_output_thresholds(ctx.get_context()) || i->being_recorded()) { - i->display_indented(ctx, out, indentation); + i->display_indented(_ctx, out, indentation); } } } diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h index 331b153e8..3910f6d0b 100644 --- a/src/muz/rel/dl_instruction.h +++ b/src/muz/rel/dl_instruction.h @@ -73,6 +73,7 @@ namespace datalog { void reset(); rel_context & get_rel_context(); + rel_context const & get_rel_context() const; void set_timelimit(unsigned time_in_ms); void reset_timelimit(); @@ -224,7 +225,7 @@ namespace datalog { The newline character at the end should not be printed. */ - virtual void display_head_impl(rel_context const & ctx, std::ostream & out) const { + virtual void display_head_impl(execution_context const & ctx, std::ostream & out) const { out << ""; } /** @@ -232,7 +233,7 @@ namespace datalog { Each line must be prepended by \c indentation and ended by a newline character. */ - virtual void display_body_impl(rel_context_base const & ctx, std::ostream & out, std::string indentation) const {} + virtual void display_body_impl(execution_context const & ctx, std::ostream & out, std::string indentation) const {} void log_verbose(execution_context& ctx); public: @@ -245,10 +246,10 @@ namespace datalog { virtual void make_annotations(execution_context & ctx) = 0; - void display(rel_context_base const& ctx, std::ostream & out) const { + void display(execution_context const& ctx, std::ostream & out) const { display_indented(ctx, out, ""); } - void display_indented(rel_context_base const & ctx, std::ostream & out, std::string indentation) const; + void display_indented(execution_context const & ctx, std::ostream & out, std::string indentation) const; static instruction * mk_load(ast_manager & m, func_decl * pred, reg_idx tgt); /** @@ -353,10 +354,10 @@ namespace datalog { void make_annotations(execution_context & ctx); - void display(rel_context_base const & ctx, std::ostream & out) const { + void display(execution_context const & ctx, std::ostream & out) const { display_indented(ctx, out, ""); } - void display_indented(rel_context_base const & ctx, std::ostream & out, std::string indentation) const; + void display_indented(execution_context const & ctx, std::ostream & out, std::string indentation) const; unsigned num_instructions() const { return m_data.size(); } }; diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index 5054bc192..37d5a22f3 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -630,7 +630,7 @@ namespace datalog { out << "\n--------------\n"; out << "Instructions\n"; - m_code.display(*this, out); + m_code.display(m_ectx, out); out << "\n--------------\n"; out << "Big relations\n"; diff --git a/src/opt/inc_sat_solver.cpp b/src/opt/inc_sat_solver.cpp index 6dd562f82..65264e0d9 100644 --- a/src/opt/inc_sat_solver.cpp +++ b/src/opt/inc_sat_solver.cpp @@ -56,6 +56,7 @@ class inc_sat_solver : public solver { expr_dependency_ref m_dep_core; expr_ref_vector m_soft; vector m_weights; + bool m_soft_assumptions; typedef obj_map dep2asm_t; @@ -69,7 +70,8 @@ public: m_map(m), m_num_scopes(0), m_dep_core(m), - m_soft(m) { + m_soft(m), + m_soft_assumptions(false) { m_params.set_bool("elim_vars", false); m_solver.updt_params(m_params); params_ref simp2_p = p; @@ -177,6 +179,7 @@ public: m_params = p; m_params.set_bool("elim_vars", false); m_solver.updt_params(m_params); + m_soft_assumptions = m_params.get_bool("soft_assumptions", false); m_optimize_model = m_params.get_bool("optimize_model", false); } virtual void collect_statistics(statistics & st) const { @@ -355,7 +358,7 @@ private: dep2asm_t::iterator it = dep2asm.begin(), end = dep2asm.end(); for (; it != end; ++it) { sat::literal lit = it->m_value; - if (sat::value_at(lit, ll_m) != l_true) { + if (!m_soft_assumptions && sat::value_at(lit, ll_m) != l_true) { IF_VERBOSE(0, verbose_stream() << mk_pp(it->m_key, m) << " does not evaluate to true\n"; verbose_stream() << m_asms << "\n"; m_solver.display_assignment(verbose_stream()); diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 6bc0cfa9b..c9b52f370 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -11,7 +11,6 @@ Abstract: - mus: max-sat algorithm by Nina and Bacchus, AAAI 2014. - mus-mss: based on dual refinement of bounds. - - mss: based on maximal satisfying sets (only). MaxRes is a core-guided approach to maxsat. MusMssMaxRes extends the core-guided approach by @@ -71,11 +70,19 @@ using namespace opt; class maxres : public maxsmt_solver_base { public: enum strategy_t { - s_mus, - s_mus_mss, - s_mss + s_primal, + s_primal_dual }; private: + struct stats { + unsigned m_num_cores; + unsigned m_num_cs; + stats() { reset(); } + void reset() { + memset(this, 0, sizeof(*this)); + } + }; + stats m_stats; expr_ref_vector m_B; expr_ref_vector m_asms; expr_ref_vector m_defs; @@ -167,7 +174,7 @@ public: trace_bounds("maxres"); while (m_lower < m_upper) { TRACE("opt", - display_vec(tout, m_asms.size(), m_asms.c_ptr()); + display_vec(tout, m_asms); s().display(tout); tout << "\n"; display(tout); @@ -194,159 +201,51 @@ public: return l_true; } - - lbool mss_solver() { + lbool primal_dual_solver() { init(); init_local(); - sls(); - set_mus(false); - exprs mcs; + set_soft_assumptions(); lbool is_sat = l_true; - while (m_lower < m_upper && is_sat == l_true) { - trace_bounds("maxres"); - if (m_cancel) { - return l_undef; - } - vector cores; - exprs mss; - model_ref mdl; - expr_ref tmp(m); - mcs.reset(); - s().get_model(mdl); - update_assignment(mdl.get()); - - exprs cs; - get_current_correction_set(mdl.get(), cs); - process_sat(cs); - + trace_bounds("max_res"); + exprs cs; + while (m_lower < m_upper) { #if 0 - is_sat = get_mss(mdl.get(), cores, mss, mcs); - - switch (is_sat) { - case l_undef: - return l_undef; - case l_false: - m_lower = m_upper; - return l_true; - case l_true: - process_sat(mcs); - get_mss_model(); - break; - } + expr_ref_vector asms(m_asms); + sort_assumptions(asms); + is_sat = s().check_sat(asms.size(), asms.c_ptr()); +#else + is_sat = check_sat_hill_climb(m_asms); #endif - if (m_lower < m_upper) { - is_sat = s().check_sat(0, 0); - } - } - m_lower = m_upper; - return l_true; - } - - /** - Plan: - - Get maximal set of disjoint cores. - - Update the lower bound using the cores. - - As a side-effect find a satisfying assignment that has maximal weight. - (during core minimization several queries are bound to be SAT, - those can be used to boot-strap the MCS search). - - Use the best satisfying assignment from the MUS search to find an MCS of least weight. - - Update the upper bound using the MCS. - - Update the soft constraints using first the cores. - - Then update the resulting soft constraints using the evaluation of the MCS/MSS - - Add a cardinality constraint to force new satisfying assignments to improve - the new upper bound. - - In every iteration, the lower bound is improved using the cores. - - In every iteration, the upper bound is improved using the MCS. - - Optionally: add a cardinality constraint to prune the upper bound. - - What are the corner cases: - - suppose that cost of cores adds up to current upper bound. - -> it means that each core is a unit (?) - - TBD: - - Block upper bound using wmax or pb constraint, or in case of - unweighted constraints using incremental tricks. - - Throttle when correction set gets added based on its size. - Suppose correction set is huge. Do we really need it? - - */ - lbool mus_mss_solver() { - init(); - init_local(); - sls(); - vector cores; - m_mus.set_soft(m_soft.size(), m_soft.c_ptr(), m_weights.c_ptr()); - lbool is_sat = l_true; - while (m_lower < m_upper && is_sat == l_true) { - TRACE("opt", - display_vec(tout, m_asms.size(), m_asms.c_ptr()); - s().display(tout); - tout << "\n"; - display(tout); - ); - lbool is_sat = check_sat_hill_climb(m_asms); if (m_cancel) { return l_undef; } switch (is_sat) { case l_true: - found_optimum(); - return l_true; - case l_false: - is_sat = get_cores(cores); + get_current_correction_set(cs); + IF_VERBOSE(2, display_vec(verbose_stream() << "correction set: ", cs);); + if (cs.empty()) { + m_found_feasible_optimum = m_model.get() != 0; + m_lower = m_upper; + } + else { + process_sat(cs); + } break; + case l_false: + is_sat = process_unsat(); + if (is_sat != l_true) return is_sat; + break; + case l_undef: + return l_undef; default: break; } - if (is_sat == l_undef) { - return l_undef; - } - SASSERT((is_sat == l_false) == cores.empty()); - SASSERT((is_sat == l_true) == !cores.empty()); - if (cores.empty()) { - break; - } - - // - // There is a best model, retrieve - // it from the previous core calls. - // - model_ref mdl; - get_mus_model(mdl); - - // - // Extend the current model to a (maximal) - // assignment extracting the ss and cs. - // ss - satisfying subset - // cs - correction set (complement of ss). - // - if (m_maximize_assignment && mdl.get()) { - exprs ss, cs; - is_sat = get_mss(mdl.get(), cores, ss, cs); - if (is_sat != l_true) return is_sat; - get_mss_model(); - } - // - // block the hard constraints corresponding to the cores. - // block the soft constraints corresponding to the cs - // obtained from the current best model. - // - - exprs cs; - get_current_correction_set(mdl.get(), cs); - unsigned max_core = max_core_size(cores); - if (!cs.empty() && cs.size() < max_core) { - process_sat(cs); - } - else { - process_unsat(cores); - } } - - m_lower = m_upper; + trace_bounds("maxres"); return l_true; } + lbool check_sat_hill_climb(expr_ref_vector& asms1) { expr_ref_vector asms(asms1); lbool is_sat = l_true; @@ -399,16 +298,19 @@ public: virtual lbool operator()() { m_defs.reset(); switch(m_st) { - case s_mus: + case s_primal: return mus_solver(); - case s_mus_mss: - return mus_mss_solver(); - case s_mss: - return mss_solver(); + case s_primal_dual: + return primal_dual_solver(); } return l_undef; } + virtual void collect_statistics(statistics& st) const { + st.update("maxres-cores", m_stats.m_num_cores); + st.update("maxres-correction-sets", m_stats.m_num_cs); + } + lbool get_cores(vector& cores) { // assume m_s is unsat. lbool is_sat = l_false; @@ -422,12 +324,14 @@ public: model_ref mdl; get_mus_model(mdl); is_sat = minimize_core(core); + ++m_stats.m_num_cores; if (is_sat != l_true) { break; } if (core.empty()) { cores.reset(); - return l_false; + m_lower = m_upper; + return l_true; } cores.push_back(core); if (core.size() >= m_max_core_size) { @@ -442,22 +346,30 @@ public: TRACE("opt", tout << "num cores: " << cores.size() << "\n"; for (unsigned i = 0; i < cores.size(); ++i) { - display_vec(tout, cores[i].size(), cores[i].c_ptr()); + display_vec(tout, cores[i]); } tout << "num satisfying: " << asms.size() << "\n";); return is_sat; } + void get_current_correction_set(exprs& cs) { + model_ref mdl; + s().get_model(mdl); + update_assignment(mdl.get()); + get_current_correction_set(mdl.get(), cs); + } + void get_current_correction_set(model* mdl, exprs& cs) { + ++m_stats.m_num_cs; cs.reset(); if (!mdl) return; for (unsigned i = 0; i < m_asms.size(); ++i) { - if (!is_true(mdl, m_asms[i].get())) { + if (is_false(mdl, m_asms[i].get())) { cs.push_back(m_asms[i].get()); } } - TRACE("opt", display_vec(tout << "new correction set: ", cs.size(), cs.c_ptr());); + TRACE("opt", display_vec(tout << "new correction set: ", cs);); } struct compare_asm { @@ -492,7 +404,7 @@ public: void process_sat(exprs const& corr_set) { expr_ref fml(m), tmp(m); - TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr());); + TRACE("opt", display_vec(tout << "corr_set: ", corr_set);); remove_core(corr_set); rational w = split_core(corr_set); cs_max_resolve(corr_set, w); @@ -533,7 +445,7 @@ public: remove_core(core); SASSERT(!core.empty()); rational w = split_core(core); - TRACE("opt", display_vec(tout << "minimized core: ", core.size(), core.c_ptr());); + TRACE("opt", display_vec(tout << "minimized core: ", core);); max_resolve(core, w); fml = mk_not(m, mk_and(m, m_B.size(), m_B.c_ptr())); s().assert_expr(fml); @@ -558,22 +470,6 @@ public: return 0 != mdl.get(); } - void get_mss_model() { - model_ref mdl; - m_mss.get_model(mdl); // last model is best way to reduce search space. - update_assignment(mdl.get()); - } - - lbool get_mss(model* mdl, vector const& cores, exprs& literals, exprs& mcs) { - literals.reset(); - mcs.reset(); - literals.append(m_asms.size(), m_asms.c_ptr()); - set_mus(false); - lbool is_sat = m_mss(mdl, cores, literals, mcs); - set_mus(true); - return is_sat; - } - lbool minimize_core(exprs& core) { if (m_c.sat_enabled() || core.empty()) { return l_true; @@ -622,12 +518,19 @@ public: rational w3 = w2 - w; new_assumption(core[i], w3); } - } - + } return w; } - void display_vec(std::ostream& out, unsigned sz, expr* const* args) { + void display_vec(std::ostream& out, exprs const& exprs) { + display_vec(out, exprs.size(), exprs.c_ptr()); + } + + void display_vec(std::ostream& out, expr_ref_vector const& exprs) { + display_vec(out, exprs.size(), exprs.c_ptr()); + } + + void display_vec(std::ostream& out, unsigned sz, expr* const* args) const { for (unsigned i = 0; i < sz; ++i) { out << mk_pp(args[i], m) << " : " << get_weight(args[i]) << " "; } @@ -691,7 +594,7 @@ public: // cs is a correction set (a complement of a (maximal) satisfying assignment). void cs_max_resolve(exprs const& cs, rational const& w) { if (cs.empty()) return; - TRACE("opt", display_vec(tout << "correction set: ", cs.size(), cs.c_ptr());); + TRACE("opt", display_vec(tout << "correction set: ", cs);); expr_ref fml(m), asum(m); app_ref cls(m), d(m), dd(m); m_B.reset(); @@ -733,74 +636,6 @@ public: s().assert_expr(fml); } - lbool try_improve_bound(vector& cores, exprs& mcs) { - cores.reset(); - mcs.reset(); - exprs core; - expr_ref_vector asms(m_asms); - while (true) { - rational upper = m_max_upper; - unsigned sz = 0; - for (unsigned i = 0; m_upper <= rational(2)*upper && i < asms.size(); ++i, ++sz) { - upper -= get_weight(asms[i].get()); - } - lbool is_sat = s().check_sat(sz, asms.c_ptr()); - switch (is_sat) { - case l_true: { - model_ref mdl; - s().get_model(mdl); // last model is best way to reduce search space. - update_assignment(mdl.get()); - exprs mss; - mss.append(asms.size(), asms.c_ptr()); - set_mus(false); - is_sat = m_mss(m_model.get(), cores, mss, mcs); - set_mus(true); - if (is_sat != l_true) { - return is_sat; - } - get_mss_model(); - if (!cores.empty() && mcs.size() > cores.back().size()) { - mcs.reset(); - } - else { - cores.reset(); - } - return l_true; - } - case l_undef: - return l_undef; - case l_false: - core.reset(); - s().get_unsat_core(core); - DEBUG_CODE(verify_core(core);); - is_sat = minimize_core(core); - if (is_sat != l_true) { - break; - } - if (core.empty()) { - cores.reset(); - mcs.reset(); - return l_false; - } - cores.push_back(core); - if (core.size() >= 3) { - return l_true; - } - // - // check arithmetic: cannot improve upper bound - // - if (m_upper <= upper) { - return l_true; - } - - remove_soft(core, asms); - break; - } - } - - return l_undef; - } - void update_assignment(model* mdl) { rational upper(0); expr_ref tmp(m); @@ -842,6 +677,12 @@ public: return m.is_true(tmp); } + bool is_false(model* mdl, expr* e) { + expr_ref tmp(m); + VERIFY(mdl->eval(e, tmp)); + return m.is_false(tmp); + } + bool is_true(expr* e) { return is_true(m_model.get(), e); } @@ -948,16 +789,11 @@ public: opt::maxsmt_solver_base* opt::mk_maxres( context& c, weights_t& ws, expr_ref_vector const& soft) { - return alloc(maxres, c, ws, soft, maxres::s_mus); + return alloc(maxres, c, ws, soft, maxres::s_primal); } -opt::maxsmt_solver_base* opt::mk_mus_mss_maxres( +opt::maxsmt_solver_base* opt::mk_primal_dual_maxres( context& c, weights_t& ws, expr_ref_vector const& soft) { - return alloc(maxres, c, ws, soft, maxres::s_mus_mss); -} - -opt::maxsmt_solver_base* opt::mk_mss_maxres( - context& c, weights_t& ws, expr_ref_vector const& soft) { - return alloc(maxres, c, ws, soft, maxres::s_mss); + return alloc(maxres, c, ws, soft, maxres::s_primal_dual); } diff --git a/src/opt/maxres.h b/src/opt/maxres.h index efe21c214..c942b655e 100644 --- a/src/opt/maxres.h +++ b/src/opt/maxres.h @@ -24,9 +24,7 @@ namespace opt { maxsmt_solver_base* mk_maxres(context& c, weights_t & ws, expr_ref_vector const& soft); - maxsmt_solver_base* mk_mus_mss_maxres(context& c, weights_t & ws, expr_ref_vector const& soft); - - maxsmt_solver_base* mk_mss_maxres(context& c, weights_t & ws, expr_ref_vector const& soft); + maxsmt_solver_base* mk_primal_dual_maxres(context& c, weights_t & ws, expr_ref_vector const& soft); }; diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 48d7e48bd..710f10d48 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -106,7 +106,7 @@ namespace opt { } void maxsmt_solver_base::set_soft_assumptions() { - m_c.set_soft_assumptions() + m_c.set_soft_assumptions(); } app* maxsmt_solver_base::mk_fresh_bool(char const* name) { @@ -174,11 +174,8 @@ namespace opt { else if (maxsat_engine == symbol("maxres")) { m_msolver = mk_maxres(m_c, m_weights, m_soft_constraints); } - else if (maxsat_engine == symbol("mus-mss-maxres")) { - m_msolver = mk_mus_mss_maxres(m_c, m_weights, m_soft_constraints); - } - else if (maxsat_engine == symbol("mss-maxres")) { - m_msolver = mk_mss_maxres(m_c, m_weights, m_soft_constraints); + else if (maxsat_engine == symbol("pd-maxres")) { + m_msolver = mk_primal_dual_maxres(m_c, m_weights, m_soft_constraints); } else if (maxsat_engine == symbol("bcd2")) { m_msolver = mk_bcd2(m_c, m_weights, m_soft_constraints); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 028cb4414..5971cceb7 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -474,8 +474,7 @@ namespace opt { return; } if (m_maxsat_engine != symbol("maxres") && - m_maxsat_engine != symbol("mus-mss-maxres") && - m_maxsat_engine != symbol("mss-maxres") && + m_maxsat_engine != symbol("pd-maxres") && m_maxsat_engine != symbol("bcd2") && m_maxsat_engine != symbol("sls")) { return; diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index f84c6eebf..059ac0bd2 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -3,7 +3,7 @@ def_module_params('opt', export=True, params=(('timeout', UINT, UINT_MAX, 'set timeout'), ('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"), - ('maxsat_engine', SYMBOL, 'wmax', "select engine for maxsat: 'fu_malik', 'core_maxsat', 'wmax', 'pbmax', 'maxres', 'bcd2', 'wpm2', 'sls', 'maxhs'"), + ('maxsat_engine', SYMBOL, 'wmax', "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'), ('print_model', BOOL, False, 'display model for satisfiable constraints'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 1915f363f..6a5148192 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -922,7 +922,7 @@ namespace sat { SASSERT(is_external((lit).var())); m_assumption_set.insert(lit); - if (m_config.soft_assumptions) { + if (m_config.m_soft_assumptions) { if (value(lit) == l_undef) { m_assumptions.push_back(lit); assign(lit, justification()); diff --git a/src/shell/datalog_frontend.cpp b/src/shell/datalog_frontend.cpp index a487a99b4..affe299d8 100644 --- a/src/shell/datalog_frontend.cpp +++ b/src/shell/datalog_frontend.cpp @@ -77,7 +77,7 @@ static void display_statistics( out << "--------------\n"; out << "instructions \n"; - code.display(*ctx.get_rel_context(), out); + code.display(ex_ctx, out); out << "--------------\n"; out << "big relations \n";