From c7ff05cc78f90f3b10901e4efb5ba8be85246915 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Jun 2016 15:58:12 -0700 Subject: [PATCH] enable core minimization with qsat in case it turns out to be useful Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt2_pp.cpp | 43 +++++++--- src/opt/maxres.cpp | 14 +--- src/opt/opt_context.cpp | 7 +- src/opt/opt_solver.cpp | 3 +- src/opt/opt_solver.h | 2 +- src/qe/qe_arith.cpp | 25 ++++-- src/qe/qsat.cpp | 109 +++++++++++++----------- src/sat/sat_solver/inc_sat_solver.cpp | 2 +- src/smt/smt_solver.cpp | 3 +- src/solver/check_sat_result.h | 5 ++ src/solver/combined_solver.cpp | 4 +- src/solver/mus.cpp | 114 +++++++++++++++----------- src/solver/mus.h | 9 ++ src/solver/solver.cpp | 10 ++- src/solver/solver.h | 12 ++- src/solver/tactic2solver.cpp | 5 +- 16 files changed, 235 insertions(+), 132 deletions(-) diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 1a7f051a0..2e2d99a38 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -1125,6 +1125,21 @@ void mk_smt2_format(func_decl * f, smt2_pp_environment & env, params_ref const & pr(f, r); } +void mk_smt2_format(unsigned sz, expr * const* es, smt2_pp_environment & env, params_ref const & p, + unsigned num_vars, char const * var_prefix, + format_ref & r, sbuffer & var_names) { + smt2_printer pr(env, p); + ast_manager & m = env.get_manager(); + + format_ref_vector fmts(fm(m)); + for (unsigned i = 0; i < sz; ++i) { + format_ref fr(fm(m)); + pr(es[i], num_vars, var_prefix, fr, var_names); + fmts.push_back(fr); + } + r = mk_seq(m, fmts.c_ptr(), fmts.c_ptr() + fmts.size(), f2f()); +} + std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, params_ref const & p, unsigned indent, unsigned num_vars, char const * var_prefix) { ast_manager & m = env.get_manager(); @@ -1159,6 +1174,18 @@ std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environmen return out; } +std::ostream & ast_smt2_pp(std::ostream & out, unsigned sz, expr * const* es, smt2_pp_environment & env, params_ref const & p, unsigned indent, + unsigned num_vars, char const * var_prefix) { + ast_manager & m = env.get_manager(); + format_ref r(fm(m)); + sbuffer var_names; + mk_smt2_format(sz, es, env, p, num_vars, var_prefix, r, var_names); + if (indent > 0) + r = mk_indent(m, indent, r.get()); + pp(out, r.get(), m, p); + return out; +} + mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent, unsigned num_vars, char const * var_prefix): m_ast(t), m_manager(m), @@ -1209,19 +1236,15 @@ std::ostream& operator<<(std::ostream& out, sort_ref const& e) { } std::ostream& operator<<(std::ostream& out, expr_ref_vector const& e) { - for (unsigned i = 0; i < e.size(); ++i) { - out << mk_ismt2_pp(e[i], e.get_manager()); - if (i + 1 < e.size()) out << "; "; - } - return out; + smt2_pp_environment_dbg env(e.get_manager()); + params_ref p; + return ast_smt2_pp(out, e.size(), e.c_ptr(), env, p, 0, 0, 0); } std::ostream& operator<<(std::ostream& out, app_ref_vector const& e) { - for (unsigned i = 0; i < e.size(); ++i) { - out << mk_ismt2_pp(e[i], e.get_manager()); - if (i + 1 < e.size()) out << "; "; - } - return out; + smt2_pp_environment_dbg env(e.get_manager()); + params_ref p; + return ast_smt2_pp(out, e.size(), (expr*const*)e.c_ptr(), env, p, 0, 0, 0); } std::ostream& operator<<(std::ostream& out, func_decl_ref_vector const& e) { diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 741bab4b5..b52c7d9b9 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -545,7 +545,7 @@ public: } m_mus.reset(); for (unsigned i = 0; i < core.size(); ++i) { - m_mus.add_soft(core[i]); + VERIFY(i == m_mus.add_soft(core[i])); } unsigned_vector mus_idx; lbool is_sat = m_mus.get_mus(mus_idx); @@ -832,12 +832,8 @@ public: tout << m_defs; tout << m_asms; ); - for (unsigned i = 0; i < m_defs.size(); ++i) { - s().assert_expr(m_defs[i].get()); - } - for (unsigned i = 0; i < m_asms.size(); ++i) { - s().assert_expr(m_asms[i].get()); - } + s().assert_expr(m_defs); + s().assert_expr(m_asms); } // else: there is only a single assignment to these soft constraints. } @@ -848,9 +844,7 @@ public: for (unsigned i = 0; i < s().get_num_assertions(); ++i) { smt_solver->assert_expr(s().get_assertion(i)); } - for (unsigned i = 0; i < core.size(); ++i) { - smt_solver->assert_expr(core[i]); - } + smt_solver->assert_expr(core); lbool is_sat = smt_solver->check_sat(0, 0); if (is_sat == l_true) { IF_VERBOSE(0, verbose_stream() << "not a core\n";); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 5082fde37..f90b31476 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -555,10 +555,9 @@ namespace opt { m_params.set_bool("minimize_core_partial", true); // false); m_params.set_bool("minimize_core", true); m_sat_solver = mk_inc_sat_solver(m, m_params); - unsigned sz = get_solver().get_num_assertions(); - for (unsigned i = 0; i < sz; ++i) { - m_sat_solver->assert_expr(get_solver().get_assertion(i)); - } + expr_ref_vector fmls(m); + get_solver().get_assertions(fmls); + m_sat_solver->assert_expr(fmls); m_solver = m_sat_solver.get(); } diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index fccc7fa1c..3c2ac207c 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -316,8 +316,9 @@ namespace opt { return m_context.get_formulas()[idx]; } - void opt_solver::display(std::ostream & out) const { + std::ostream& opt_solver::display(std::ostream & out) const { m_context.display(out); + return out; } smt::theory_var opt_solver::add_objective(app* term) { diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 3c58a4fec..e5ee5afcf 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -104,7 +104,7 @@ namespace opt { virtual void set_progress_callback(progress_callback * callback); virtual unsigned get_num_assertions() const; virtual expr * get_assertion(unsigned idx) const; - virtual void display(std::ostream & out) const; + virtual std::ostream& display(std::ostream & out) const; virtual ast_manager& get_manager() { return m; } void set_logic(symbol const& logic); diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index 38d46fefe..d071765fc 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -1072,18 +1072,33 @@ namespace qe { expr_ref_vector ts(m); expr_ref t(m), s(m); row const& r = rows[i]; + if (r.m_vars.size() == 0) { + continue; + } + if (r.m_vars.size() == 1 && r.m_vars[0].m_coeff.is_neg()) { + var const& v = r.m_vars[0]; + t = index2expr[v.m_id]; + if (!v.m_coeff.is_minus_one()) { + t = a.mk_mul(t, a.mk_numeral(-v.m_coeff, a.is_int(t))); + } + s = a.mk_numeral(r.m_coeff, a.is_int(t)); + switch (r.m_type) { + case opt::t_lt: t = a.mk_gt(t, s); break; + case opt::t_le: t = a.mk_ge(t, s); break; + case opt::t_eq: t = a.mk_eq(t, s); break; + } + fmls.push_back(t); + continue; + } for (j = 0; j < r.m_vars.size(); ++j) { var const& v = r.m_vars[j]; t = index2expr[v.m_id]; if (!v.m_coeff.is_one()) { - t = a.mk_mul(t, a.mk_numeral(v.m_coeff, v.m_coeff.is_int())); + t = a.mk_mul(t, a.mk_numeral(v.m_coeff, a.is_int(t))); } ts.push_back(t); } - if (ts.empty()) { - continue; - } - s = a.mk_numeral(-r.m_coeff, r.m_coeff.is_int()); + s = a.mk_numeral(-r.m_coeff, a.is_int(t)); if (ts.size() == 1) { t = ts[0].get(); } diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 4c6efdcd4..a409b23c2 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -534,34 +534,10 @@ namespace qe { m_solver->assert_expr(e); } - ptr_vector m_core; - void get_core(expr_ref_vector& core) { core.reset(); - 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_solver->display(tout); - tout << "\n"; - ); + m_solver->get_unsat_core(core); + TRACE("qe", m_solver->display(tout << "core: " << core << "\n") << "\n";); } }; @@ -624,11 +600,14 @@ namespace qe { break; case l_false: switch (m_level) { - case 0: return l_false; + case 0: + return l_false; case 1: - if (m_mode == qsat_sat) return l_true; + if (m_mode == qsat_sat) { + return l_true; + } if (m_model.get()) { - project_qe(asms); + if (!project_qe(asms)) return l_undef; } else { pop(1); @@ -636,7 +615,7 @@ namespace qe { break; default: if (m_model.get()) { - project(asms); + if (!project(asms)) return l_undef; } else { pop(1); @@ -755,9 +734,42 @@ namespace qe { } } - void get_core(expr_ref_vector& core, unsigned level) { + bool get_core(expr_ref_vector& core, unsigned level) { get_kernel(level).get_core(core); m_pred_abs.pred2lit(core); + return true; + } + + bool minimize_core(expr_ref_vector& core, unsigned level) { + expr_ref_vector core1(m), core2(m), dels(m); + TRACE("qe", tout << core.size() << "\n";); + mus mus(get_kernel(level).s()); + for (unsigned i = 0; i < core.size(); ++i) { + app* a = to_app(core[i].get()); + max_level lvl = m_pred_abs.compute_level(a); + if (lvl.max() + 2 <= level) { + VERIFY(core1.size() == mus.add_soft(a)); + core1.push_back(a); + } + else { + core2.push_back(a); + mus.add_assumption(a); + } + } + TRACE("qe", tout << core1.size() << " " << core2.size() << "\n";); + if (core1.size() > 8) { + unsigned_vector core_idxs; + if (l_true != mus.get_mus(core_idxs)) { + return false; + } + TRACE("qe", tout << core1.size() << " -> " << core_idxs.size() << "\n";); + for (unsigned i = 0; i < core_idxs.size(); ++i) { + core2.push_back(core1[core_idxs[i]].get()); + } + core.reset(); + core.append(core2); + } + return true; } void check_cancel() { @@ -795,11 +807,13 @@ namespace qe { m_pred_abs.set_expr_level(b, lvl); } - void project_qe(expr_ref_vector& core) { + bool project_qe(expr_ref_vector& core) { SASSERT(m_level == 1); expr_ref fml(m); model& mdl = *m_model.get(); - get_core(core, m_level); + if (!get_core(core, m_level)) { + return false; + } SASSERT(validate_core(core)); get_vars(m_level); m_mbp(force_elim(), m_avars, mdl, core); @@ -814,10 +828,11 @@ namespace qe { m_free_vars.append(m_avars); pop(1); } + return true; } - void project(expr_ref_vector& core) { - get_core(core, m_level); + 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); @@ -860,6 +875,7 @@ namespace qe { fml = m_pred_abs.mk_abstract(fml); get_kernel(m_level).assert_expr(fml); } + return true; } void get_vars(unsigned level) { @@ -990,14 +1006,15 @@ namespace qe { } bool validate_core(expr_ref_vector const& core) { + return true; +#if 0 TRACE("qe", tout << "Validate core\n";); solver& s = get_kernel(m_level).s(); expr_ref_vector fmls(m); fmls.append(core.size(), core.c_ptr()); - for (unsigned i = 0; i < s.get_num_assertions(); ++i) { - fmls.push_back(s.get_assertion(i)); - } + s.get_assertions(fmls); return check_fmls(fmls) || m.canceled(); +#endif } bool check_fmls(expr_ref_vector const& fmls) { @@ -1013,15 +1030,16 @@ namespace qe { } bool validate_model(expr_ref_vector const& asms) { + return true; +#if 0 TRACE("qe", tout << "Validate model\n";); 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)); - } + s.get_assertions(fmls); return validate_model(*m_model, asms.size(), asms.c_ptr()) && validate_model(*m_model, fmls.size(), fmls.c_ptr()); +#endif } bool validate_model(model& mdl, unsigned sz, expr* const* fmls) { @@ -1047,6 +1065,8 @@ namespace qe { // (core[model(vars)/vars] => proj) bool validate_project(model& mdl, expr_ref_vector const& core) { + return true; +#if 0 TRACE("qe", tout << "Validate projection\n";); if (!validate_model(mdl, core.size(), core.c_ptr())) return false; @@ -1090,6 +1110,7 @@ namespace qe { TRACE("qe", tout << "implication check failed, could be due to turning != into >\n";); } return true; +#endif } @@ -1159,7 +1180,6 @@ namespace qe { fml = push_not(fml); } hoist(fml); -// hoist_ite(fml); redundant provided theories understand to deal with ite terms. m_pred_abs.abstract_atoms(fml, defs); fml = m_pred_abs.mk_abstract(fml); m_ex.assert_expr(mk_and(defs)); @@ -1277,8 +1297,6 @@ namespace qe { m_ex.assert_expr(bound); } - - }; lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p) { @@ -1309,8 +1327,7 @@ namespace qe { void qmax::collect_statistics(statistics& st) const { m_imp->m_qsat.collect_statistics(st); - }; - + } }; tactic * mk_qsat_tactic(ast_manager& m, params_ref const& p) { diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 6d8b8c1d9..fb1c98a74 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -477,6 +477,6 @@ void inc_sat_display(std::ostream& out, solver& _s, unsigned sz, expr*const* sof } weights.push_back(_weights[i].get_unsigned()); } - return s.display_weighted(out, sz, soft, weights.c_ptr()); + s.display_weighted(out, sz, soft, weights.c_ptr()); } diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 1778ce076..59c08006b 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -122,8 +122,9 @@ namespace smt { return m_context.get_formulas()[idx]; } - virtual void display(std::ostream & out) const { + virtual std::ostream& display(std::ostream & out) const { m_context.display(out); + return out; } }; diff --git a/src/solver/check_sat_result.h b/src/solver/check_sat_result.h index b981b3119..3da6b72a7 100644 --- a/src/solver/check_sat_result.h +++ b/src/solver/check_sat_result.h @@ -48,6 +48,11 @@ public: lbool status() const { return m_status; } virtual void collect_statistics(statistics & st) const = 0; virtual void get_unsat_core(ptr_vector & r) = 0; + virtual void get_unsat_core(expr_ref_vector & r) { + ptr_vector core; + get_unsat_core(core); + r.append(core.size(), core.c_ptr()); + } virtual void get_model(model_ref & m) = 0; virtual proof * get_proof() = 0; virtual std::string reason_unknown() const = 0; diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 4e645116c..7db056396 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -262,8 +262,8 @@ public: return m_solver2->get_assumption(idx - c1); } - virtual void display(std::ostream & out) const { - m_solver1->display(out); + virtual std::ostream& display(std::ostream & out) const { + return m_solver1->display(out); } virtual void collect_statistics(statistics & st) const { diff --git a/src/solver/mus.cpp b/src/solver/mus.cpp index ebdffca13..4960a3d2a 100644 --- a/src/solver/mus.cpp +++ b/src/solver/mus.cpp @@ -26,40 +26,50 @@ Notes: struct mus::imp { - solver& m_s; + solver& m_solver; ast_manager& m; - expr_ref_vector m_cls2expr; - obj_map m_expr2cls; + expr_ref_vector m_lit2expr; + expr_ref_vector m_assumptions; + obj_map m_expr2lit; model_ref m_model; expr_ref_vector m_soft; vector m_weights; rational m_weight; imp(solver& s): - m_s(s), m(s.get_manager()), m_cls2expr(m), m_soft(m) + m_solver(s), m(s.get_manager()), m_lit2expr(m), m_assumptions(m), m_soft(m) {} void reset() { - m_cls2expr.reset(); - m_expr2cls.reset(); - } + m_lit2expr.reset(); + m_expr2lit.reset(); + m_assumptions.reset(); + } + + bool is_literal(expr* lit) const { + expr* l; + return is_uninterp_const(lit) || (m.is_not(lit, l) && is_uninterp_const(l)); + } - unsigned add_soft(expr* cls) { - SASSERT(is_uninterp_const(cls) || - (m.is_not(cls) && is_uninterp_const(to_app(cls)->get_arg(0)))); - unsigned idx = m_cls2expr.size(); - m_expr2cls.insert(cls, idx); - m_cls2expr.push_back(cls); - TRACE("opt", tout << idx << ": " << mk_pp(cls, m) << "\n"; - display_vec(tout, m_cls2expr);); + unsigned add_soft(expr* lit) { + SASSERT(is_literal(lit)); + unsigned idx = m_lit2expr.size(); + m_expr2lit.insert(lit, idx); + m_lit2expr.push_back(lit); + TRACE("opt", tout << idx << ": " << mk_pp(lit, m) << "\n" << m_lit2expr << "\n";); return idx; } + + void add_assumption(expr* lit) { + SASSERT(is_literal(lit)); + m_assumptions.push_back(lit); + } lbool get_mus(unsigned_vector& mus) { // SASSERT: mus does not have duplicates. m_model.reset(); unsigned_vector core; - for (unsigned i = 0; i < m_cls2expr.size(); ++i) { + for (unsigned i = 0; i < m_lit2expr.size(); ++i) { core.push_back(i); } if (core.size() == 1) { @@ -68,7 +78,7 @@ struct mus::imp { } mus.reset(); - if (core.size() > 64) { + if (false && core.size() > 64) { return qx(mus); } @@ -76,40 +86,40 @@ struct mus::imp { ptr_vector core_exprs; while (!core.empty()) { IF_VERBOSE(12, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";); - unsigned cls_id = core.back(); + unsigned lit_id = core.back(); TRACE("opt", display_vec(tout << "core: ", core); display_vec(tout << "mus: ", mus); ); core.pop_back(); - expr* cls = m_cls2expr[cls_id].get(); - expr_ref not_cls(m); - not_cls = mk_not(m, cls); + expr* lit = m_lit2expr[lit_id].get(); + expr_ref not_lit(m); + not_lit = mk_not(m, lit); lbool is_sat = l_undef; { - scoped_append _sa(*this, assumptions, core); - assumptions.push_back(not_cls); - is_sat = m_s.check_sat(assumptions); + scoped_append _sa1(*this, assumptions, core); + scoped_append _sa2(*this, assumptions, m_assumptions); + assumptions.push_back(not_lit); + is_sat = m_solver.check_sat(assumptions); } switch (is_sat) { case l_undef: return is_sat; case l_true: - assumptions.push_back(cls); - mus.push_back(cls_id); + assumptions.push_back(lit); + mus.push_back(lit_id); update_model(); break; default: core_exprs.reset(); - m_s.get_unsat_core(core_exprs); - if (!core_exprs.contains(not_cls)) { + m_solver.get_unsat_core(core_exprs); + if (!core_exprs.contains(not_lit)) { // core := core_exprs \ mus core.reset(); for (unsigned i = 0; i < core_exprs.size(); ++i) { - cls = core_exprs[i]; - cls_id = m_expr2cls.find(cls); - if (!mus.contains(cls_id)) { - core.push_back(cls_id); + lit = core_exprs[i]; + if (m_expr2lit.find(lit, lit_id) && !mus.contains(lit_id)) { + core.push_back(lit_id); } } TRACE("opt", display_vec(tout << "core exprs:", core_exprs); @@ -125,9 +135,9 @@ struct mus::imp { DEBUG_CODE( assumptions.reset(); for (unsigned i = 0; i < mus.size(); ++i) { - assumptions.push_back(m_cls2expr[mus[i]].get()); + assumptions.push_back(m_lit2expr[mus[i]].get()); } - lbool is_sat = m_s.check_sat(assumptions.size(), assumptions.c_ptr()); + lbool is_sat = m_solver.check_sat(assumptions.size(), assumptions.c_ptr()); SASSERT(is_sat == l_false); ); #endif @@ -142,7 +152,7 @@ struct mus::imp { m_fmls(fmls1), m_size(fmls1.size()) { for (unsigned i = 0; i < fmls2.size(); ++i) { - fmls1.push_back(imp.m_cls2expr[fmls2[i]].get()); + fmls1.push_back(imp.m_lit2expr[fmls2[i]].get()); } } scoped_append(imp& imp, expr_ref_vector& fmls1, uint_set const& fmls2): @@ -150,9 +160,14 @@ struct mus::imp { 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()); + fmls1.push_back(imp.m_lit2expr[*it].get()); } } + scoped_append(imp& imp, expr_ref_vector& fmls1, expr_ref_vector const& fmls2): + m_fmls(fmls1), + m_size(fmls1.size()) { + fmls1.append(fmls2); + } ~scoped_append() { m_fmls.shrink(m_size); } @@ -160,7 +175,7 @@ struct mus::imp { 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()); + assumptions.push_back(m_lit2expr[core[i]].get()); } } @@ -199,7 +214,7 @@ struct mus::imp { if (m_soft.empty()) return; model_ref mdl; expr_ref tmp(m); - m_s.get_model(mdl); + m_solver.get_model(mdl); rational w; for (unsigned i = 0; i < m_soft.size(); ++i) { mdl->eval(m_soft[i].get(), tmp); @@ -221,7 +236,7 @@ struct mus::imp { lbool qx(unsigned_vector& mus) { uint_set core, support; - for (unsigned i = 0; i < m_cls2expr.size(); ++i) { + for (unsigned i = 0; i < m_lit2expr.size(); ++i) { core.insert(i); } lbool is_sat = qx(core, support, false); @@ -245,8 +260,9 @@ struct mus::imp { #endif if (has_support) { expr_ref_vector asms(m); - scoped_append _sa(*this, asms, support); - is_sat = m_s.check_sat(asms); + scoped_append _sa1(*this, asms, support); + scoped_append _sa2(*this, asms, m_assumptions); + is_sat = m_solver.check_sat(asms); switch (is_sat) { case l_false: { uint_set core; @@ -282,10 +298,12 @@ struct mus::imp { void get_core(uint_set& core) { ptr_vector core_exprs; - m_s.get_unsat_core(core_exprs); + unsigned lit_id; + m_solver.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)); + if (m_expr2lit.find(core_exprs[i], lit_id)) { + core.insert(lit_id); + } } } @@ -329,8 +347,12 @@ mus::~mus() { dealloc(m_imp); } -unsigned mus::add_soft(expr* cls) { - return m_imp->add_soft(cls); +unsigned mus::add_soft(expr* lit) { + return m_imp->add_soft(lit); +} + +void mus::add_assumption(expr* lit) { + return m_imp->add_assumption(lit); } lbool mus::get_mus(unsigned_vector& mus) { diff --git a/src/solver/mus.h b/src/solver/mus.h index d66049030..d2411b6ec 100644 --- a/src/solver/mus.h +++ b/src/solver/mus.h @@ -34,6 +34,15 @@ class mus { */ unsigned add_soft(expr* cls); + /** + Additional assumption for solver to be used along with solver context, + but not used in core computation. This facility is useful when querying + for a core over only a subset of soft constraints. It has the same + logical functionality as asserting 'lit' to the solver and pushing a scope + (and popping the scope before the solver is used for other constraints). + */ + void add_assumption(expr* lit); + lbool get_mus(unsigned_vector& mus); void reset(); diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 59118c5ca..3bbe1c3fd 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -28,7 +28,13 @@ expr * solver::get_assertion(unsigned idx) const { return 0; } -void solver::display(std::ostream & out) const { - out << "(solver)"; +std::ostream& solver::display(std::ostream & out) const { + return out << "(solver)"; } +void solver::get_assertions(expr_ref_vector& fmls) const { + unsigned sz = get_num_assertions(); + for (unsigned i = 0; i < sz; ++i) { + fmls.push_back(get_assertion(i)); + } +} diff --git a/src/solver/solver.h b/src/solver/solver.h index 0b2578968..f320bec7c 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -79,6 +79,10 @@ public: for (unsigned i = 0; i < ts.size(); ++i) assert_expr(ts[i]); } + void assert_expr(ptr_vector const& ts) { + for (unsigned i = 0; i < ts.size(); ++i) assert_expr(ts[i]); + } + /** \brief Add a new formula \c t to the assertion stack, and "tag" it with \c a. The propositional variable \c a is used to track the use of \c t in a proof @@ -130,6 +134,11 @@ public: */ virtual expr * get_assertion(unsigned idx) const; + /** + \brief Retrieves assertions as a vector. + */ + void get_assertions(expr_ref_vector& fmls) const; + /** \brief The number of tracked assumptions (see assert_expr(t, a)). */ @@ -142,10 +151,11 @@ public: + /** \brief Display the content of this solver. */ - virtual void display(std::ostream & out) const; + virtual std::ostream& display(std::ostream & out) const; class scoped_push { solver& s; diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 5235be230..56b246c1e 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -73,7 +73,7 @@ public: virtual unsigned get_num_assertions() const; virtual expr * get_assertion(unsigned idx) const; - virtual void display(std::ostream & out) const; + virtual std::ostream& display(std::ostream & out) const; virtual ast_manager& get_manager(); }; @@ -240,7 +240,7 @@ expr * tactic2solver::get_assertion(unsigned idx) const { return m_assertions.get(idx); } -void tactic2solver::display(std::ostream & out) const { +std::ostream& tactic2solver::display(std::ostream & out) const { ast_pp_util visitor(m_assertions.m()); visitor.collect(m_assertions); visitor.display_decls(out); @@ -254,6 +254,7 @@ void tactic2solver::display(std::ostream & out) const { } out << ")"; #endif + return out; } solver * mk_tactic2solver(ast_manager & m,