From 9f5a117443122bfac118a73475f67bbb45adc4a4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 10 Jun 2016 16:24:14 -0700 Subject: [PATCH] move mus to solver Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/opt/CMakeLists.txt | 1 - contrib/cmake/src/solver/CMakeLists.txt | 1 + src/opt/maxres.cpp | 2 +- src/opt/mus.h | 55 -------- src/opt/opt_context.cpp | 2 +- src/qe/qsat.cpp | 103 +++++++++------ src/solver/check_sat_result.h | 1 + src/{opt => solver}/mus.cpp | 160 +++++++++++++++++++++--- src/solver/mus.h | 54 ++++++++ src/solver/solver.h | 4 + 10 files changed, 273 insertions(+), 110 deletions(-) delete mode 100644 src/opt/mus.h rename src/{opt => solver}/mus.cpp (55%) create mode 100644 src/solver/mus.h diff --git a/contrib/cmake/src/opt/CMakeLists.txt b/contrib/cmake/src/opt/CMakeLists.txt index c50f8be52..e4166e3d4 100644 --- a/contrib/cmake/src/opt/CMakeLists.txt +++ b/contrib/cmake/src/opt/CMakeLists.txt @@ -8,7 +8,6 @@ z3_add_component(opt maxsls.cpp maxsmt.cpp mss.cpp - mus.cpp opt_cmds.cpp opt_context.cpp opt_pareto.cpp diff --git a/contrib/cmake/src/solver/CMakeLists.txt b/contrib/cmake/src/solver/CMakeLists.txt index 5e76c91ce..8142ca872 100644 --- a/contrib/cmake/src/solver/CMakeLists.txt +++ b/contrib/cmake/src/solver/CMakeLists.txt @@ -2,6 +2,7 @@ z3_add_component(solver SOURCES check_sat_result.cpp combined_solver.cpp + mus.cpp solver.cpp solver_na2as.cpp tactic2solver.cpp diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 7c1fad80e..741bab4b5 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -119,7 +119,7 @@ public: maxsmt_solver_base(c, ws, soft), m_index(index), m_B(m), m_asms(m), m_defs(m), - m_mus(c.get_solver(), m), + m_mus(c.get_solver()), m_mss(c.get_solver(), m), m_trail(m), m_st(st), diff --git a/src/opt/mus.h b/src/opt/mus.h deleted file mode 100644 index 8ca7ab91d..000000000 --- a/src/opt/mus.h +++ /dev/null @@ -1,55 +0,0 @@ -/*++ -Copyright (c) 2014 Microsoft Corporation - -Module Name: - - mus.h - -Abstract: - - Basic MUS extraction - -Author: - - Nikolaj Bjorner (nbjorner) 2014-20-7 - -Notes: - ---*/ -#ifndef MUS_H_ -#define MUS_H_ - -namespace opt { - class mus { - struct imp; - imp * m_imp; - public: - mus(solver& s, ast_manager& m); - ~mus(); - /** - Add soft constraint. - - Assume that the solver context enforces that - cls is equivalent to a disjunction of args. - Assume also that cls is a literal. - */ - unsigned add_soft(expr* cls); - - lbool get_mus(unsigned_vector& mus); - - void reset(); - - /** - Instrument MUS extraction to also provide the minimal - penalty model, if any is found. - The minimal penalty model has the least weight for the - supplied soft constraints. - */ - void set_soft(unsigned sz, expr* const* soft, rational const* weights); - rational get_best_model(model_ref& mdl); - - }; - -}; - -#endif diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 0b71fff1c..5082fde37 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -225,7 +225,7 @@ namespace opt { normalize(); internalize(); update_solver(); -#if 0 +#if 1 if (is_qsat_opt()) { return run_qsat_opt(); } diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index a9ca9e99d..4c6efdcd4 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -34,7 +34,9 @@ Notes: #include "expr_replacer.h" #include "th_rewriter.h" #include "model_evaluator.h" - +#include "smt_solver.h" +#include "solver.h" +#include "mus.h" namespace qe { @@ -506,33 +508,58 @@ namespace qe { } class kernel { - smt_params m_smtp; - smt::kernel m_kernel; + ast_manager& m; + params_ref m_params; + ref m_solver; public: kernel(ast_manager& m): - m_kernel(m, m_smtp) + m(m), + m_solver(mk_smt_solver(m, m_params, symbol::null)) { - m_smtp.m_model = true; - m_smtp.m_relevancy_lvl = 0; - m_smtp.m_case_split_strategy = CS_ACTIVITY_WITH_CACHE; + m_params.set_bool("model", true); + m_params.set_uint("relevancy_lvl", 0); + m_params.set_uint("case_split_strategy", CS_ACTIVITY_WITH_CACHE); + m_solver->updt_params(m_params); } - smt::kernel& k() { return m_kernel; } - smt::kernel const& k() const { return m_kernel; } + solver& s() { return *m_solver; } + solver const& s() const { return *m_solver; } + + void reset() { + m_solver = mk_smt_solver(m, m_params, symbol::null); + } void assert_expr(expr* e) { - m_kernel.assert_expr(e); + m_solver->assert_expr(e); } + ptr_vector m_core; + void get_core(expr_ref_vector& core) { - unsigned sz = m_kernel.get_unsat_core_size(); core.reset(); - for (unsigned i = 0; i < sz; ++i) { - core.push_back(m_kernel.get_unsat_core_expr(i)); + m_core.reset(); + m_solver->get_unsat_core(m_core); + core.append(m_core.size(), m_core.c_ptr()); + +#if 0 + + mus mus(*m_solver); + for (unsigned i = 0; i < m_core.size(); ++i) { + VERIFY(i == mus.add_soft(m_core[i])); } + unsigned_vector mus2; + core.reset(); + if (mus.get_mus(mus2) != l_undef) { + for (unsigned i = 0; i < mus2.size(); ++i) { + core.push_back(m_core[mus2[i]]); + } + } + std::cout << m_core.size() << " => " << core.size() << "\n"; +#endif + TRACE("qe", tout << "core: " << core << "\n"; - m_kernel.display(tout); + m_solver->display(tout); tout << "\n"; ); } @@ -586,13 +613,13 @@ namespace qe { expr_ref_vector asms(m_asms); m_pred_abs.get_assumptions(m_model.get(), asms); TRACE("qe", tout << asms << "\n";); - smt::kernel& k = get_kernel(m_level).k(); - lbool res = k.check(asms); + solver& s = get_kernel(m_level).s(); + lbool res = s.check_sat(asms); switch (res) { case l_true: - k.get_model(m_model); + s.get_model(m_model); SASSERT(validate_model(asms)); - TRACE("qe", k.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); ); + TRACE("qe", s.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); ); push(); break; case l_false: @@ -655,8 +682,8 @@ namespace qe { void reset() { m_st.reset(); - m_fa.k().collect_statistics(m_st); - m_ex.k().collect_statistics(m_st); + m_fa.s().collect_statistics(m_st); + m_ex.s().collect_statistics(m_st); m_pred_abs.collect_statistics(m_st); m_level = 0; m_answer.reset(); @@ -664,8 +691,8 @@ namespace qe { m_pred_abs.reset(); m_vars.reset(); m_model = 0; - m_fa.k().reset(); - m_ex.k().reset(); + m_fa.reset(); + m_ex.reset(); m_free_vars.reset(); } @@ -964,10 +991,12 @@ namespace qe { bool validate_core(expr_ref_vector const& core) { TRACE("qe", tout << "Validate core\n";); - smt::kernel& k = get_kernel(m_level).k(); + solver& s = get_kernel(m_level).s(); expr_ref_vector fmls(m); fmls.append(core.size(), core.c_ptr()); - fmls.append(k.size(), k.get_formulas()); + for (unsigned i = 0; i < s.get_num_assertions(); ++i) { + fmls.push_back(s.get_assertion(i)); + } return check_fmls(fmls) || m.canceled(); } @@ -985,10 +1014,14 @@ namespace qe { bool validate_model(expr_ref_vector const& asms) { TRACE("qe", tout << "Validate model\n";); - smt::kernel& k = get_kernel(m_level).k(); + solver& s = get_kernel(m_level).s(); + expr_ref_vector fmls(m); + for (unsigned i = 0; i < s.get_num_assertions(); ++i) { + fmls.push_back(s.get_assertion(i)); + } return validate_model(*m_model, asms.size(), asms.c_ptr()) && - validate_model(*m_model, k.size(), k.get_formulas()); + validate_model(*m_model, fmls.size(), fmls.c_ptr()); } bool validate_model(model& mdl, unsigned sz, expr* const* fmls) { @@ -1161,9 +1194,9 @@ namespace qe { break; case l_undef: result.push_back(in.get()); - std::string s = m_ex.k().last_failure_as_string(); - if (s == "ok") { - s = m_fa.k().last_failure_as_string(); + std::string s = m_ex.s().reason_unknown(); + if (s == "ok" || s == "unknown") { + s = m_fa.s().reason_unknown(); } throw tactic_exception(s.c_str()); } @@ -1171,8 +1204,8 @@ 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_fa.s().collect_statistics(st); + m_ex.s().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); @@ -1180,8 +1213,8 @@ namespace qe { void reset_statistics() { m_stats.reset(); - m_fa.k().reset_statistics(); - m_ex.k().reset_statistics(); + m_fa.reset(); + m_ex.reset(); } void cleanup() { @@ -1223,9 +1256,9 @@ namespace qe { UNREACHABLE(); break; case l_undef: - std::string s = m_ex.k().last_failure_as_string(); + std::string s = m_ex.s().reason_unknown(); if (s == "ok") { - s = m_fa.k().last_failure_as_string(); + s = m_fa.s().reason_unknown(); } throw tactic_exception(s.c_str()); diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h index e6586d492..b981b3119 100644 --- a/src/solver/check_sat_result.h +++ b/src/solver/check_sat_result.h @@ -54,6 +54,7 @@ public: virtual void set_reason_unknown(char const* msg) = 0; virtual void get_labels(svector & r) = 0; virtual ast_manager& get_manager() = 0; + }; /** diff --git a/src/opt/mus.cpp b/src/solver/mus.cpp similarity index 55% rename from src/opt/mus.cpp rename to src/solver/mus.cpp index aa8446256..ebdffca13 100644 --- a/src/opt/mus.cpp +++ b/src/solver/mus.cpp @@ -19,14 +19,11 @@ Notes: --*/ #include "solver.h" -#include "smt_literal.h" #include "mus.h" #include "ast_pp.h" #include "ast_util.h" +#include "uint_set.h" -using namespace opt; - -// struct mus::imp { solver& m_s; @@ -38,15 +35,14 @@ struct mus::imp { vector m_weights; rational m_weight; - imp(solver& s, ast_manager& m): - m_s(s), m(m), m_cls2expr(m), m_soft(m) + imp(solver& s): + m_s(s), m(s.get_manager()), m_cls2expr(m), m_soft(m) {} void reset() { m_cls2expr.reset(); m_expr2cls.reset(); - } - + } unsigned add_soft(expr* cls) { SASSERT(is_uninterp_const(cls) || @@ -55,7 +51,7 @@ struct mus::imp { m_expr2cls.insert(cls, idx); m_cls2expr.push_back(cls); TRACE("opt", tout << idx << ": " << mk_pp(cls, m) << "\n"; - display_vec(tout, m_cls2expr);); + display_vec(tout, m_cls2expr);); return idx; } @@ -70,11 +66,16 @@ struct mus::imp { mus.push_back(core.back()); return l_true; } + mus.reset(); + if (core.size() > 64) { + return qx(mus); + } + expr_ref_vector assumptions(m); ptr_vector core_exprs; while (!core.empty()) { - IF_VERBOSE(2, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";); + IF_VERBOSE(12, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";); unsigned cls_id = core.back(); TRACE("opt", display_vec(tout << "core: ", core); @@ -84,11 +85,12 @@ struct mus::imp { expr* cls = m_cls2expr[cls_id].get(); expr_ref not_cls(m); not_cls = mk_not(m, cls); - unsigned sz = assumptions.size(); - assumptions.push_back(not_cls); - add_core(core, assumptions); - lbool is_sat = m_s.check_sat(assumptions.size(), assumptions.c_ptr()); - assumptions.resize(sz); + lbool is_sat = l_undef; + { + scoped_append _sa(*this, assumptions, core); + assumptions.push_back(not_cls); + is_sat = m_s.check_sat(assumptions); + } switch (is_sat) { case l_undef: return is_sat; @@ -132,6 +134,30 @@ struct mus::imp { return l_true; } + class scoped_append { + expr_ref_vector& m_fmls; + unsigned m_size; + public: + scoped_append(imp& imp, expr_ref_vector& fmls1, unsigned_vector const& fmls2): + m_fmls(fmls1), + m_size(fmls1.size()) { + for (unsigned i = 0; i < fmls2.size(); ++i) { + fmls1.push_back(imp.m_cls2expr[fmls2[i]].get()); + } + } + scoped_append(imp& imp, expr_ref_vector& fmls1, uint_set const& fmls2): + m_fmls(fmls1), + m_size(fmls1.size()) { + uint_set::iterator it = fmls2.begin(), end = fmls2.end(); + for (; it != end; ++it) { + fmls1.push_back(imp.m_cls2expr[*it].get()); + } + } + ~scoped_append() { + m_fmls.shrink(m_size); + } + }; + void add_core(unsigned_vector const& core, expr_ref_vector& assumptions) { for (unsigned i = 0; i < core.size(); ++i) { assumptions.push_back(m_cls2expr[core[i]].get()); @@ -193,10 +219,110 @@ struct mus::imp { } + lbool qx(unsigned_vector& mus) { + uint_set core, support; + for (unsigned i = 0; i < m_cls2expr.size(); ++i) { + core.insert(i); + } + lbool is_sat = qx(core, support, false); + if (is_sat == l_true) { + uint_set::iterator it = core.begin(), end = core.end(); + mus.reset(); + for (; it != end; ++it) { + mus.push_back(*it); + } + } + return is_sat; + } + + lbool qx(uint_set& assignment, uint_set& support, bool has_support) { + lbool is_sat = l_true; +#if 0 + if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) { + IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";); + return l_true; + } +#endif + if (has_support) { + expr_ref_vector asms(m); + scoped_append _sa(*this, asms, support); + is_sat = m_s.check_sat(asms); + switch (is_sat) { + case l_false: { + uint_set core; + get_core(core); + support &= core; + assignment.reset(); + return l_true; + } + case l_undef: + return l_undef; + case l_true: + update_model(); + break; + default: + break; + } + } + if (assignment.num_elems() == 1) { + return l_true; + } + uint_set assign2; + split(assignment, assign2); + support |= assignment; + is_sat = qx(assign2, support, !assignment.empty()); + unsplit(support, assignment); + if (is_sat != l_true) return is_sat; + support |= assign2; + is_sat = qx(assignment, support, !assign2.empty()); + assignment |= assign2; + unsplit(support, assign2); + return is_sat; + } + + void get_core(uint_set& core) { + ptr_vector core_exprs; + m_s.get_unsat_core(core_exprs); + for (unsigned i = 0; i < core_exprs.size(); ++i) { + expr* cls = core_exprs[i]; + core.insert(m_expr2cls.find(cls)); + } + } + + void unsplit(uint_set& A, uint_set& B) { + uint_set A1, B1; + uint_set::iterator it = A.begin(), end = A.end(); + for (; it != end; ++it) { + if (B.contains(*it)) { + B1.insert(*it); + } + else { + A1.insert(*it); + } + } + A = A1; + B = B1; + } + + void split(uint_set& lits1, uint_set& lits2) { + unsigned half = lits1.num_elems()/2; + uint_set lits3; + uint_set::iterator it = lits1.begin(), end = lits1.end(); + for (unsigned i = 0; it != end; ++it, ++i) { + if (i < half) { + lits3.insert(*it); + } + else { + lits2.insert(*it); + } + } + lits1 = lits3; + } + }; -mus::mus(solver& s, ast_manager& m) { - m_imp = alloc(imp, s, m); +mus::mus(solver& s) { + m_imp = alloc(imp, s); } mus::~mus() { diff --git a/src/solver/mus.h b/src/solver/mus.h new file mode 100644 index 000000000..d66049030 --- /dev/null +++ b/src/solver/mus.h @@ -0,0 +1,54 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + mus.h + +Abstract: + + Basic MUS extraction + +Author: + + Nikolaj Bjorner (nbjorner) 2014-20-7 + +Notes: + +--*/ +#ifndef MUS_H_ +#define MUS_H_ + +class mus { + struct imp; + imp * m_imp; + public: + mus(solver& s); + ~mus(); + /** + Add soft constraint. + + Assume that the solver context enforces that + cls is equivalent to a disjunction of args. + Assume also that cls is a literal. + */ + unsigned add_soft(expr* cls); + + lbool get_mus(unsigned_vector& mus); + + void reset(); + + /** + Instrument MUS extraction to also provide the minimal + penalty model, if any is found. + The minimal penalty model has the least weight for the + supplied soft constraints. + */ + void set_soft(unsigned sz, expr* const* soft, rational const* weights); + + rational get_best_model(model_ref& mdl); + +}; + + +#endif diff --git a/src/solver/solver.h b/src/solver/solver.h index 5a1514795..0b2578968 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -108,6 +108,10 @@ public: */ virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0; + lbool check_sat(expr_ref_vector const& asms) { return check_sat(asms.size(), asms.c_ptr()); } + + lbool check_sat(app_ref_vector const& asms) { return check_sat(asms.size(), (expr* const*)asms.c_ptr()); } + /** \brief Set a progress callback procedure that is invoked by this solver during check_sat.