diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 5cef19234..ccf03a943 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -54,6 +54,8 @@ struct pb2bv_rewriter::imp { vector m_coeffs; bool m_keep_cardinality_constraints; bool m_keep_pb_constraints; + bool m_pb_num_system; + bool m_pb_totalizer; unsigned m_min_arity; template @@ -114,23 +116,24 @@ struct pb2bv_rewriter::imp { return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m); } -#if 0 - expr_ref result(m); - switch (is_le) { - case l_true: if (mk_le_tot(sz, args, k, result)) return result; else break; - case l_false: if (mk_ge_tot(sz, args, k, result)) return result; else break; - case l_undef: break; + if (m_pb_totalizer) { + expr_ref result(m); + switch (is_le) { + case l_true: if (mk_le_tot(sz, args, k, result)) return result; else break; + case l_false: if (mk_ge_tot(sz, args, k, result)) return result; else break; + case l_undef: break; + } + } + + if (m_pb_num_system) { + expr_ref result(m); + switch (is_le) { + case l_true: if (mk_le(sz, args, k, result)) return result; else break; + case l_false: if (mk_ge(sz, args, k, result)) return result; else break; + case l_undef: if (mk_eq(sz, args, k, result)) return result; else break; + } } -#endif -#if 0 - expr_ref result(m); - switch (is_le) { - case l_true: if (mk_le(sz, args, k, result)) return result; else break; - case l_false: if (mk_ge(sz, args, k, result)) return result; else break; - case l_undef: if (mk_eq(sz, args, k, result)) return result; else break; - } -#endif // fall back to divide and conquer encoding. SASSERT(k.is_pos()); expr_ref zero(m), bound(m); @@ -397,22 +400,30 @@ struct pb2bv_rewriter::imp { for (unsigned j = 0; j + lim - 1 < out.size(); j += n) { expr_ref tmp(m); tmp = out[j + lim - 1]; - if (j + n < out.size()) { - tmp = m.mk_and(tmp, m.mk_not(out[j + n])); + if (j + n - 1 < out.size()) { + tmp = m.mk_and(tmp, m.mk_not(out[j + n - 1])); } ors.push_back(tmp); } return ::mk_or(ors); } + // x0 + 5x1 + 3x2 >= k + // x0 x1 x1 -> s0 s1 s2 + // s2 x1 x2 -> s3 s4 s5 + // k = 7: s5 or (s4 & not s2 & s0) + // k = 6: s4 + // k = 5: s4 or (s3 & not s2 & s1) + // k = 4: s4 or (s3 & not s2 & s0) + // k = 3: s3 + // bool mk_ge(unsigned sz, expr * const* args, rational bound, expr_ref& result) { if (!create_basis()) return false; if (!bound.is_unsigned()) return false; vector coeffs(m_coeffs); result = m.mk_true(); expr_ref_vector carry(m), new_carry(m); - for (unsigned i = 0; i < m_base.size(); ++i) { - rational b_i = m_base[i]; + for (rational b_i : m_base) { unsigned B = b_i.get_unsigned(); unsigned d_i = (bound % b_i).get_unsigned(); bound = div(bound, b_i); @@ -425,16 +436,16 @@ struct pb2bv_rewriter::imp { coeffs[j] = div(coeffs[j], b_i); } TRACE("pb", tout << "Carry: " << carry << "\n"; - for (unsigned j = 0; j < coeffs.size(); ++j) tout << coeffs[j] << " "; + for (auto c : coeffs) tout << c << " "; tout << "\n"; ); ptr_vector out; m_sort.sorting(carry.size(), carry.c_ptr(), out); - + expr_ref gt = mod_ge(out, B, d_i + 1); expr_ref ge = mod_ge(out, B, d_i); result = mk_or(gt, mk_and(ge, result)); - TRACE("pb", tout << result << "\n";); + TRACE("pb", tout << "b: " << b_i << " d: " << d_i << " gt: " << gt << " ge: " << ge << " " << result << "\n";); new_carry.reset(); for (unsigned j = B - 1; j < out.size(); j += B) { @@ -443,7 +454,10 @@ struct pb2bv_rewriter::imp { carry.reset(); carry.append(new_carry); } - TRACE("pb", tout << result << "\n";); + if (!carry.empty()) { + result = m.mk_or(result, carry[0].get()); + } + TRACE("pb", tout << "Carry: " << carry << " result: " << result << "\n";); return true; } @@ -567,6 +581,8 @@ struct pb2bv_rewriter::imp { m_args(m), m_keep_cardinality_constraints(false), m_keep_pb_constraints(false), + m_pb_num_system(false), + m_pb_totalizer(false), m_min_arity(2) {} @@ -761,6 +777,14 @@ struct pb2bv_rewriter::imp { void keep_pb_constraints(bool f) { m_keep_pb_constraints = f; } + + void pb_num_system(bool f) { + m_pb_num_system = f; + } + + void pb_totalizer(bool f) { + m_pb_totalizer = f; + } }; struct card2bv_rewriter_cfg : public default_rewriter_cfg { @@ -774,6 +798,8 @@ struct pb2bv_rewriter::imp { card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {} void keep_cardinality_constraints(bool f) { m_r.keep_cardinality_constraints(f); } void keep_pb_constraints(bool f) { m_r.keep_pb_constraints(f); } + void pb_num_system(bool f) { m_r.pb_num_system(f); } + void pb_totalizer(bool f) { m_r.pb_totalizer(f); } }; class card_pb_rewriter : public rewriter_tpl { @@ -784,27 +810,59 @@ struct pb2bv_rewriter::imp { m_cfg(i, m) {} void keep_cardinality_constraints(bool f) { m_cfg.keep_cardinality_constraints(f); } void keep_pb_constraints(bool f) { m_cfg.keep_pb_constraints(f); } + void pb_num_system(bool f) { m_cfg.pb_num_system(f); } + void pb_totalizer(bool f) { m_cfg.pb_totalizer(f); } }; card_pb_rewriter m_rw; + bool keep_cardinality() const { + params_ref const& p = m_params; + return + p.get_bool("keep_cardinality_constraints", false) || + p.get_bool("sat.cardinality.solver", false) || + p.get_bool("cardinality.solver", false) || keep_pb(); + } + + bool keep_pb() const { + params_ref const& p = m_params; + return + p.get_bool("keep_pb_constraints", false) || + p.get_bool("sat.pb.solver", false) || + p.get_bool("pb.solver", false); + } + + bool pb_num_system() const { + return m_params.get_bool("pb_num_system", false); + } + + bool pb_totalizer() const { + return m_params.get_bool("pb_totalizer", false); + } + imp(ast_manager& m, params_ref const& p): m(m), m_params(p), m_lemmas(m), m_fresh(m), m_num_translated(0), m_rw(*this, m) { - m_rw.keep_cardinality_constraints(p.get_bool("keep_cardinality_constraints", false)); - m_rw.keep_pb_constraints(p.get_bool("keep_pb_constraints", false)); + m_rw.keep_cardinality_constraints(keep_cardinality()); + m_rw.keep_pb_constraints(keep_pb()); + m_rw.pb_num_system(pb_num_system()); + m_rw.pb_totalizer(pb_totalizer()); } void updt_params(params_ref const & p) { m_params.append(p); - m_rw.keep_cardinality_constraints(m_params.get_bool("keep_cardinality_constraints", false)); - m_rw.keep_pb_constraints(m_params.get_bool("keep_pb_constraints", false)); + m_rw.keep_cardinality_constraints(keep_cardinality()); + m_rw.keep_pb_constraints(keep_pb()); + m_rw.pb_num_system(pb_num_system()); + m_rw.pb_totalizer(pb_totalizer()); } void collect_param_descrs(param_descrs& r) const { r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints (don't bit-blast them) and use built-in cardinality solver"); r.insert("keep_pb_constraints", CPK_BOOL, "(default: true) retain pb constraints (don't bit-blast them) and use built-in pb solver"); + r.insert("pb_num_system", CPK_BOOL, "(default: false) use pb number system encoding"); + r.insert("pb_totalizer", CPK_BOOL, "(default: false) use pb totalizer encoding"); } unsigned get_num_steps() const { return m_rw.get_num_steps(); } diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp index b91018217..c328a30cd 100644 --- a/src/sat/card_extension.cpp +++ b/src/sat/card_extension.cpp @@ -250,7 +250,7 @@ namespace sat { p.swap(i, j); } if (slack < bound) { - slack += p[i].first; + slack += p[j].first; ++num_watch; } ++j; @@ -267,7 +267,7 @@ namespace sat { if (slack < bound) { literal lit = p[j].second; SASSERT(value(p[j].second) == l_false); - for (unsigned i = j + 1; j < sz; ++i) { + for (unsigned i = j + 1; i < sz; ++i) { if (lvl(lit) < lvl(p[i].second)) { lit = p[i].second; } @@ -386,16 +386,24 @@ namespace sat { p.swap(num_watch, index); if (slack < bound + m_a_max) { - while (!s().inconsistent() && !m_pb_undef.empty()) { + TRACE("sat", display(tout, p, false); for(auto j : m_pb_undef) tout << j << "\n";); + literal_vector to_assign; + while (!m_pb_undef.empty()) { index1 = m_pb_undef.back(); literal lit = p[index1].second; + TRACE("sat", tout << index1 << " " << lit << "\n";); if (slack >= bound + p[index1].first) { break; } m_pb_undef.pop_back(); + to_assign.push_back(lit); + } + + for (literal lit : to_assign) { + if (s().inconsistent()) break; if (value(lit) == l_undef) { assign(p, lit); - } + } } } @@ -474,7 +482,8 @@ namespace sat { } void card_extension::display(std::ostream& out, pb const& p, bool values) const { - out << p.lit() << "[ watch: " << p.num_watch() << ", slack: " << p.slack() << "]"; + if (p.lit() != null_literal) out << p.lit(); + out << "[watch: " << p.num_watch() << ", slack: " << p.slack() << "]"; if (p.lit() != null_literal && values) { out << "@(" << value(p.lit()); if (value(p.lit()) != l_undef) { @@ -1350,7 +1359,25 @@ namespace sat { if (p.lit() != null_literal) r.push_back(p.lit()); SASSERT(p.lit() == null_literal || value(p.lit()) == l_true); TRACE("sat", display(tout, p, true);); - for (unsigned i = p.num_watch(); i < p.size(); ++i) { + + // unsigned coeff = get_coeff(p, l); + unsigned coeff = 0; + for (unsigned j = 0; j < p.num_watch(); ++j) { + if (p[j].second == l) { + coeff = p[j].first; + break; + } + } + unsigned slack = p.slack() - coeff; + unsigned i = p.num_watch(); + + // skip entries that are not required for unit propagation. + // slack - coeff + w_head < k + unsigned h = 0; + for (; i < p.size() && p[i].first + h + slack < p.k(); ++i) { + h += p[i].first; + } + for (; i < p.size(); ++i) { literal lit = p[i].second; SASSERT(l_false == value(lit)); r.push_back(~lit); @@ -1714,7 +1741,9 @@ namespace sat { std::ostream& card_extension::display_justification(std::ostream& out, ext_justification_idx idx) const { if (is_card_index(idx)) { card& c = index2card(idx); - out << "bound " << c.lit() << ": "; + out << "bound "; + if (c.lit() != null_literal) out << c.lit(); + out << ": "; for (unsigned i = 0; i < c.size(); ++i) { out << c[i] << " "; } @@ -1722,14 +1751,18 @@ namespace sat { } else if (is_xor_index(idx)) { xor& x = index2xor(idx); - out << "xor " << x.lit() << ": "; + out << "xor "; + if (x.lit() != null_literal) out << x.lit(); + out << ": "; for (unsigned i = 0; i < x.size(); ++i) { out << x[i] << " "; } } else if (is_pb_index(idx)) { pb& p = index2pb(idx); - out << "pb " << p.lit() << ": "; + out << "pb "; + if (p.lit() != null_literal) out << p.lit(); + out << ": "; for (unsigned i = 0; i < p.size(); ++i) { out << p[i].first << "*" << p[i].second << " "; } @@ -1773,26 +1806,16 @@ namespace sat { bool card_extension::validate_unit_propagation(pb const& p, literal alit) { if (p.lit() != null_literal && value(p.lit()) != l_true) return false; - unsigned k = p.k(); unsigned sum = 0; - unsigned a_min = 0; TRACE("sat", display(tout << "validate: " << alit << "\n", p, true);); for (unsigned i = 0; i < p.size(); ++i) { literal lit = p[i].second; lbool val = value(lit); - if (val == l_false) { - // no-op - } - else if (lit == alit) { - a_min = p[i].first; - sum += p[i].first; - } - else { + if (val != l_false && lit != alit) { sum += p[i].first; } } - return sum < k + a_min; - return true; + return sum < p.k(); } bool card_extension::validate_lemma() { diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index 10acc0bb6..c8aa82e97 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -20,6 +20,7 @@ Notes: #include "solver_na2as.h" #include "tactic.h" #include "pb2bv_rewriter.h" +#include "th_rewriter.h" #include "filter_model_converter.h" #include "ast_pp.h" #include "model_smt2_pp.h" @@ -29,6 +30,7 @@ class pb2bv_solver : public solver_na2as { params_ref m_params; mutable expr_ref_vector m_assertions; mutable ref m_solver; + mutable th_rewriter m_th_rewriter; mutable pb2bv_rewriter m_rewriter; public: @@ -39,6 +41,7 @@ public: m_params(p), m_assertions(m), m_solver(s), + m_th_rewriter(m, p), m_rewriter(m, p) { } @@ -121,10 +124,11 @@ public: private: void flush_assertions() const { proof_ref proof(m); - expr_ref fml(m); + expr_ref fml1(m), fml(m); expr_ref_vector fmls(m); for (unsigned i = 0; i < m_assertions.size(); ++i) { - m_rewriter(m_assertions[i].get(), fml, proof); + m_th_rewriter(m_assertions[i].get(), fml1, proof); + m_rewriter(fml1, fml, proof); m_solver->assert_expr(fml); } m_rewriter.flush_side_constraints(fmls);