From 9635a74e52f723873e23329f3ceade0ae523ec50 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Jan 2018 08:23:22 -0800 Subject: [PATCH] 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; }