From 9635a74e52f723873e23329f3ceade0ae523ec50 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Jan 2018 08:23:22 -0800 Subject: [PATCH 1/2] add clausification features Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 11 +++++ src/opt/maxres.cpp | 4 +- src/opt/maxsmt.cpp | 22 ++++++++-- src/opt/opt_cmds.cpp | 4 +- src/sat/ba_solver.cpp | 91 ++++++++++++++++++++++++++++++++++------- src/sat/ba_solver.h | 5 +++ src/sat/sat_solver.h | 1 + 7 files changed, 117 insertions(+), 21 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index e16459fda..cf86ee03d 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1407,6 +1407,17 @@ def is_or(a): """ return is_app_of(a, Z3_OP_OR) +def is_implies(a): + """Return `True` if `a` is a Z3 implication expression. + + >>> p, q = Bools('p q') + >>> is_implies(Implies(p, q)) + True + >>> is_implies(And(p, q)) + False + """ + return is_app_of(a, Z3_OP_IMPLIES) + def is_not(a): """Return `True` if `a` is a Z3 not expression. diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 5fa87b3ba..e1a4a74eb 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -285,13 +285,13 @@ public: m_last_index = 0; bool first = index > 0; SASSERT(index < asms.size() || asms.empty()); - IF_VERBOSE(1, verbose_stream() << "start hill climb " << index << " asms: " << asms.size() << "\n";); + IF_VERBOSE(10, verbose_stream() << "start hill climb " << index << " asms: " << asms.size() << "\n";); while (index < asms.size() && is_sat == l_true) { while (!first && asms.size() > 20*(index - m_last_index) && index < asms.size()) { index = next_index(asms, index); } - IF_VERBOSE(1, verbose_stream() << "hill climb " << index << "\n";); first = false; + IF_VERBOSE(3, verbose_stream() << "hill climb " << index << "\n";); // IF_VERBOSE(3, verbose_stream() << "weight: " << get_weight(asms[0].get()) << " " << get_weight(asms[index-1].get()) << " num soft: " << index << "\n";); m_last_index = index; is_sat = check_sat(index, asms.c_ptr()); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 25616b00f..636bbf9f9 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -353,12 +353,26 @@ namespace opt { m_upper += w; } + struct cmp_first { + bool operator()(std::pair const& x, std::pair const& y) const { + return x.first < y.first; + } + }; + void maxsmt::display_answer(std::ostream& out) const { - for (unsigned i = 0; i < m_soft_constraints.size(); ++i) { - expr* e = m_soft_constraints[i]; + vector> sorted_weights; + unsigned n = m_weights.size(); + for (unsigned i = 0; i < n; ++i) { + sorted_weights.push_back(std::make_pair(i, m_weights[i])); + } + std::sort(sorted_weights.begin(), sorted_weights.end(), cmp_first()); + sorted_weights.reverse(); + for (unsigned i = 0; i < n; ++i) { + unsigned idx = sorted_weights[i].first; + expr* e = m_soft_constraints[idx]; bool is_not = m.is_not(e, e); - out << m_weights[i] << ": " << mk_pp(e, m) - << ((is_not != get_assignment(i))?" |-> true ":" |-> false ") + out << m_weights[idx] << ": " << mk_pp(e, m) + << ((is_not != get_assignment(idx))?" |-> true ":" |-> false ") << "\n"; } diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 89264a9c8..a614b774c 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -166,7 +166,9 @@ public: } virtual void execute(cmd_context & ctx) { - get_opt(ctx, m_opt).display_assignment(ctx.regular_stream()); + if (!ctx.ignore_check()) { + get_opt(ctx, m_opt).display_assignment(ctx.regular_stream()); + } } }; diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index be4498061..963a7723e 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -446,7 +446,7 @@ namespace sat { } /* - \brief slit PB constraint into two because root is reused in arguments. + \brief split PB constraint into two because root is reused in arguments. x <=> a*x + B*y >= k @@ -825,6 +825,9 @@ namespace sat { p.set_k(k); SASSERT(p.well_formed()); + if (clausify(p)) { + return; + } if (p.lit() == null_literal || value(p.lit()) == l_true) { init_watch(p); } @@ -1543,6 +1546,9 @@ namespace sat { s().mk_clause(_lits.size(), _lits.c_ptr(), learned); return 0; } + if (!learned && clausify(lit, lits.size(), lits.c_ptr(), k)) { + return 0; + } void * mem = m_allocator.allocate(card::get_obj_size(lits.size())); card* c = new (mem) card(next_id(), lit, lits, k); c->set_learned(learned); @@ -2370,13 +2376,16 @@ namespace sat { SASSERT(s().at_base_lvl()); switch (c.tag()) { case card_t: - simplify(c.to_card()); + if (!clausify(c.to_card())) + simplify(c.to_card()); break; case pb_t: - simplify(c.to_pb()); + if (!clausify(c.to_pb())) + simplify(c.to_pb()); break; case xor_t: - simplify(c.to_xor()); + if (!clausify(c.to_xor())) + simplify(c.to_xor()); break; default: UNREACHABLE(); @@ -2480,8 +2489,9 @@ namespace sat { } void ba_solver::ba_sort::mk_clause(unsigned n, literal const* lits) { - literal_vector _lits(n, lits); - s.s().mk_clause(n, _lits.c_ptr()); + m_lits.reset(); + m_lits.append(n, lits); + s.s().mk_clause(n, m_lits.c_ptr()); } // ------------------------------- @@ -2623,8 +2633,25 @@ namespace sat { } } + bool ba_solver::clausify(literal lit, unsigned n, literal const* lits, unsigned k) { + bool is_def = lit != null_literal; + if ((!is_def || !s().was_eliminated(lit)) && + !std::any_of(lits, lits + n, [&](literal l) { return s().was_eliminated(l); })) { + literal def_lit = m_sort.ge(is_def, k, n, lits); + if (is_def) { + s().mk_clause(~lit, def_lit); + s().mk_clause( lit, ~def_lit); + } + return true; + } + return false; + } + + bool ba_solver::clausify(xor& x) { + return false; + } + bool ba_solver::clausify(card& c) { -#if 0 if (get_config().m_card_solver) return false; @@ -2632,18 +2659,54 @@ namespace sat { // TBD: conditions for when to clausify are TBD and // handling of conditional cardinality as well. // - if (c.lit() == null_literal) { - if (!c.learned() && !std::any_of(c.begin(), c.end(), [&](literal l) { return s().was_eliminated(l.var()); })) { - IF_VERBOSE(0, verbose_stream() << "clausify " << c << "\n"; - m_sort.ge(false, c.k(), c.size(), c.begin()); - } - remove_constraint(c, "recompiled to clauses"); + if (!c.learned() && clausify(c.lit(), c.size(), c.begin(), c.k())) { + IF_VERBOSE(0, verbose_stream() << "clausify " << c << "\n";); + // compiled + } + remove_constraint(c, "recompiled to clauses"); + return true; + } + + bool ba_solver::clausify(pb& p) { + if (get_config().m_card_solver) + return false; + + bool ok = !p.learned(); + bool is_def = p.lit() != null_literal; + for (wliteral wl : p) { + ok &= !s().was_eliminated(wl.second); + } + ok &= !is_def || !s().was_eliminated(p.lit()); + if (!ok) { + remove_constraint(p, "recompiled to clauses"); + return true; + } + + if (is_cardinality(p, m_lemma)) { + literal lit = m_sort.ge(is_def, p.k(), m_lemma.size(), m_lemma.c_ptr()); + if (is_def) { + s().mk_clause(p.lit(), ~lit); + s().mk_clause(~p.lit(), lit); + } + remove_constraint(p, "recompiled to clauses"); return true; } -#endif return false; } + bool ba_solver::is_cardinality(pb const& p, literal_vector& lits) { + lits.reset(); + p.size(); + for (wliteral wl : p) { + if (lits.size() > 2*p.size() + wl.first) { + return false; + } + for (unsigned i = 0; i < wl.first; ++i) { + lits.push_back(wl.second); + } + } + return true; + } void ba_solver::split_root(constraint& c) { switch (c.tag()) { diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index f447be64c..1116bb166 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -234,6 +234,7 @@ namespace sat { struct ba_sort { ba_solver& s; literal m_true; + literal_vector m_lits; typedef sat::literal literal; typedef sat::literal_vector literal_vector; @@ -343,6 +344,7 @@ namespace sat { void flush_roots(card& c); void recompile(card& c); bool clausify(card& c); + bool clausify(literal lit, unsigned n, literal const* lits, unsigned k); lbool eval(card const& c) const; double get_reward(card const& c, literal_occs_fun& occs) const; @@ -355,6 +357,7 @@ namespace sat { void get_xor_antecedents(literal l, unsigned index, justification js, literal_vector& r); void get_antecedents(literal l, xor const& x, literal_vector & r); void simplify(xor& x); + bool clausify(xor& x); void flush_roots(xor& x); lbool eval(xor const& x) const; @@ -371,6 +374,8 @@ namespace sat { bool is_cardinality(pb const& p); void flush_roots(pb& p); void recompile(pb& p); + bool clausify(pb& p); + bool is_cardinality(pb const& p, literal_vector& lits); lbool eval(pb const& p) const; double get_reward(pb const& p, literal_occs_fun& occs) const; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index bbeb87f83..0ca1bf7a8 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -270,6 +270,7 @@ namespace sat { void set_non_external(bool_var v); bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } void set_eliminated(bool_var v, bool f) { m_eliminated[v] = f; } + bool was_eliminated(literal l) const { return was_eliminated(l.var()); } unsigned scope_lvl() const { return m_scope_lvl; } unsigned search_lvl() const { return m_search_lvl; } bool at_search_lvl() const { return m_scope_lvl == m_search_lvl; } From d79c33fb21eda6a2804d4820d2547526579ee128 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 Jan 2018 16:12:38 -0800 Subject: [PATCH 2/2] fix model bugs Signed-off-by: Nikolaj Bjorner --- src/ast/expr2var.cpp | 8 ++--- src/sat/sat_solver/inc_sat_solver.cpp | 26 ++++++++------- src/sat/tactic/atom2bool_var.cpp | 6 ++++ src/sat/tactic/atom2bool_var.h | 1 + src/sat/tactic/goal2sat.cpp | 46 ++++++++++----------------- src/sat/tactic/goal2sat.h | 2 +- 6 files changed, 43 insertions(+), 46 deletions(-) diff --git a/src/ast/expr2var.cpp b/src/ast/expr2var.cpp index 2f850d645..ffa0b4fba 100644 --- a/src/ast/expr2var.cpp +++ b/src/ast/expr2var.cpp @@ -58,11 +58,9 @@ void expr2var::display(std::ostream & out) const { } void expr2var::mk_inv(expr_ref_vector & var2expr) const { - obj_map::iterator it = m_mapping.begin(); - obj_map::iterator end = m_mapping.end(); - for (; it != end; ++it) { - expr * t = it->m_key; - var x = it->m_value; + for (auto & kv : m_mapping) { + expr * t = kv.m_key; + var x = kv.m_value; if (x >= var2expr.size()) var2expr.resize(x+1, 0); var2expr.set(x, t); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 97818e155..bfa1731b2 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -533,11 +533,11 @@ private: TRACE("sat", g->display_with_dependencies(tout);); // ensure that if goal is already internalized, then import mc from m_solver. - if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m); - m_sat_mc->flush_smc(m_solver); m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, is_incremental(), is_lemma); m_goal2sat.get_interpreted_atoms(atoms); + if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m); + m_sat_mc->flush_smc(m_solver, m_map); if (!atoms.empty()) { std::stringstream strm; strm << "interpreted atoms sent to SAT solver " << atoms; @@ -798,16 +798,20 @@ private: } SASSERT(m_model); - DEBUG_CODE( - for (expr * f : m_fmls) { - expr_ref tmp(m); - if (m_model->eval(f, tmp, true)) { - CTRACE("sat", !m.is_true(tmp), - tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n"; - model_smt2_pp(tout, m, *(m_model.get()), 0);); - SASSERT(m.is_true(tmp)); + IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";); + for (expr * f : m_fmls) { + expr_ref tmp(m); + if (m_model->eval(f, tmp, true)) { + CTRACE("sat", !m.is_true(tmp), + tout << "Evaluation failed: " << mk_pp(f, m) << " to " << tmp << "\n"; + model_smt2_pp(tout, m, *(m_model.get()), 0);); + if (!m.is_true(tmp)) { + IF_VERBOSE(0, verbose_stream() << "failed to verify: " << tmp << "\n";); + IF_VERBOSE(0, verbose_stream() << m_params << "\n";); } - }); + VERIFY(m.is_true(tmp)); + } + } } }; diff --git a/src/sat/tactic/atom2bool_var.cpp b/src/sat/tactic/atom2bool_var.cpp index d8827fe66..e3c9b6767 100644 --- a/src/sat/tactic/atom2bool_var.cpp +++ b/src/sat/tactic/atom2bool_var.cpp @@ -31,6 +31,12 @@ void atom2bool_var::mk_inv(expr_ref_vector & lit2expr) const { } } +void atom2bool_var::mk_var_inv(app_ref_vector & var2expr) const { + for (auto const& kv : m_mapping) { + var2expr.set(kv.m_value, to_app(kv.m_key)); + } +} + sat::bool_var atom2bool_var::to_bool_var(expr * n) const { sat::bool_var v = sat::null_bool_var; m_mapping.find(n, v); diff --git a/src/sat/tactic/atom2bool_var.h b/src/sat/tactic/atom2bool_var.h index d360d3fe0..b7f533537 100644 --- a/src/sat/tactic/atom2bool_var.h +++ b/src/sat/tactic/atom2bool_var.h @@ -31,6 +31,7 @@ public: void insert(expr * n, sat::bool_var v) { expr2var::insert(n, v); } sat::bool_var to_bool_var(expr * n) const; void mk_inv(expr_ref_vector & lit2expr) const; + void mk_var_inv(app_ref_vector & var2expr) const; // return true if the mapping contains uninterpreted atoms. bool interpreted_atoms() const { return expr2var::interpreted_vars(); } }; diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index d810c60b7..97129a861 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -880,8 +880,10 @@ void goal2sat::get_interpreted_atoms(expr_ref_vector& atoms) { sat2goal::mc::mc(ast_manager& m): m(m), m_var2expr(m) {} -void sat2goal::mc::flush_smc(sat::solver& s) { +void sat2goal::mc::flush_smc(sat::solver& s, atom2bool_var const& map) { s.flush(m_smc); + m_var2expr.resize(s.num_vars()); + map.mk_var_inv(m_var2expr); } void sat2goal::mc::flush_gmc() { @@ -941,6 +943,7 @@ void sat2goal::mc::operator()(model_ref & md) { // create a SAT model using md sat::model sat_md; expr_ref val(m); + VERIFY(!m_var2expr.empty()); for (expr * atom : m_var2expr) { if (!atom) { sat_md.push_back(l_undef); @@ -1011,7 +1014,6 @@ expr_ref sat2goal::mc::lit2expr(sat::literal l) { struct sat2goal::imp { typedef mc sat_model_converter; - typedef ref sat_model_converter_ref; ast_manager & m; expr_ref_vector m_lit2expr; @@ -1034,23 +1036,7 @@ struct sat2goal::imp { throw tactic_exception(TACTIC_MAX_MEMORY_MSG); } - void init_lit2expr(sat::solver const & s, atom2bool_var const & map, sat_model_converter_ref & mc) { - unsigned num_vars = s.num_vars(); - m_lit2expr.resize(num_vars * 2); - map.mk_inv(m_lit2expr); - if (mc) { - for (sat::bool_var v = 0; v < num_vars; v++) { - checkpoint(); - sat::literal l(v, false); - if (m_lit2expr.get(l.index()) && !mc->var2expr(v)) { - mc->insert(v, to_app(m_lit2expr.get(l.index())), false); - SASSERT(m_lit2expr.get((~l).index())); - } - } - } - } - - expr * lit2expr(sat_model_converter_ref& mc, sat::literal l) { + expr * lit2expr(ref& mc, sat::literal l) { if (!m_lit2expr.get(l.index())) { SASSERT(m_lit2expr.get((~l).index()) == 0); app* aux = mc ? mc->var2expr(l.var()) : nullptr; @@ -1059,13 +1045,14 @@ struct sat2goal::imp { if (mc) mc->insert(l.var(), aux, true); } - m_lit2expr.set(l.index(), aux); - m_lit2expr.set((~l).index(), m.mk_not(aux)); + sat::literal lit(l.var(), false); + m_lit2expr.set(lit.index(), aux); + m_lit2expr.set((~lit).index(), m.mk_not(aux)); } return m_lit2expr.get(l.index()); } - void assert_pb(sat_model_converter_ref& mc, goal& r, sat::ba_solver::pb const& p) { + void assert_pb(ref& mc, goal& r, sat::ba_solver::pb const& p) { pb_util pb(m); ptr_buffer lits; vector coeffs; @@ -1082,7 +1069,7 @@ struct sat2goal::imp { r.assert_expr(fml); } - void assert_card(sat_model_converter_ref& mc, goal& r, sat::ba_solver::card const& c) { + void assert_card(ref& mc, goal& r, sat::ba_solver::card const& c) { pb_util pb(m); ptr_buffer lits; for (sat::literal l : c) { @@ -1096,7 +1083,7 @@ struct sat2goal::imp { r.assert_expr(fml); } - void assert_xor(sat_model_converter_ref& mc, goal & r, sat::ba_solver::xor const& x) { + void assert_xor(ref& mc, goal & r, sat::ba_solver::xor const& x) { ptr_buffer lits; for (sat::literal l : x) { lits.push_back(lit2expr(mc, l)); @@ -1109,7 +1096,7 @@ struct sat2goal::imp { r.assert_expr(fml); } - void assert_clauses(sat_model_converter_ref& mc, sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) { + void assert_clauses(ref& mc, sat::solver const & s, sat::clause_vector const& clauses, goal & r, bool asserted) { ptr_buffer lits; for (sat::clause* cp : clauses) { checkpoint(); @@ -1136,8 +1123,9 @@ struct sat2goal::imp { if (r.models_enabled() && !mc) { mc = alloc(sat_model_converter, m); } - if (mc) mc->flush_smc(s); - init_lit2expr(s, map, mc); + if (mc) mc->flush_smc(s, map); + m_lit2expr.resize(s.num_vars() * 2); + map.mk_inv(m_lit2expr); // collect units unsigned trail_sz = s.init_trail_size(); for (unsigned i = 0; i < trail_sz; ++i) { @@ -1173,7 +1161,7 @@ struct sat2goal::imp { } } - void add_clause(sat_model_converter_ref& mc, sat::literal_vector const& lits, expr_ref_vector& lemmas) { + void add_clause(ref& mc, sat::literal_vector const& lits, expr_ref_vector& lemmas) { expr_ref_vector lemma(m); for (sat::literal l : lits) { expr* e = lit2expr(mc, l); @@ -1183,7 +1171,7 @@ struct sat2goal::imp { lemmas.push_back(mk_or(lemma)); } - void add_clause(sat_model_converter_ref& mc, sat::clause const& c, expr_ref_vector& lemmas) { + void add_clause(ref& mc, sat::clause const& c, expr_ref_vector& lemmas) { expr_ref_vector lemma(m); for (sat::literal l : c) { expr* e = lit2expr(mc, l); diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index 43ee5a835..463a50ff6 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -88,7 +88,7 @@ public: mc(ast_manager& m); virtual ~mc() {} // flush model converter from SAT solver to this structure. - void flush_smc(sat::solver& s); + void flush_smc(sat::solver& s, atom2bool_var const& map); void operator()(model_ref& md) override; void operator()(expr_ref& fml) override; model_converter* translate(ast_translation& translator) override;