From b6b6035cfb9bb06878f496b03ab5a19d9548a0a4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Feb 2017 16:50:39 -0800 Subject: [PATCH] tuning and fixing drat checker Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb2bv_rewriter.cpp | 35 ++++---- src/ast/rewriter/pb2bv_rewriter.h | 1 + src/sat/sat_drat.cpp | 120 ++++++++++++++++---------- src/sat/sat_drat.h | 9 +- src/sat/sat_params.pyg | 1 - src/sat/sat_solver.cpp | 34 +++++++- src/sat/sat_solver.h | 1 + src/sat/sat_solver/inc_sat_solver.cpp | 2 - src/tactic/portfolio/pb2bv_solver.cpp | 4 +- 9 files changed, 140 insertions(+), 67 deletions(-) diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index 1dd4ea6fa..9bc54ae74 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -49,7 +49,7 @@ struct pb2bv_rewriter::imp { expr_ref_vector m_args; rational m_k; vector m_coeffs; - bool m_enable_card; + bool m_keep_cardinality_constraints; template expr_ref mk_le_ge(expr_ref_vector& fmls, expr* a, expr* b, expr* bound) { @@ -240,7 +240,7 @@ struct pb2bv_rewriter::imp { bv(m), m_trail(m), m_args(m), - m_enable_card(false) + m_keep_cardinality_constraints(true) {} bool mk_app(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { @@ -354,27 +354,27 @@ struct pb2bv_rewriter::imp { bool mk_pb(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { SASSERT(f->get_family_id() == pb.get_family_id()); if (is_or(f)) { - if (m_enable_card) return false; + if (m_keep_cardinality_constraints) return false; result = m.mk_or(sz, args); } else if (pb.is_at_most_k(f) && pb.get_k(f).is_unsigned()) { - if (m_enable_card) return false; + if (m_keep_cardinality_constraints) return false; result = m_sort.le(full, pb.get_k(f).get_unsigned(), sz, args); } else if (pb.is_at_least_k(f) && pb.get_k(f).is_unsigned()) { - if (m_enable_card) return false; + if (m_keep_cardinality_constraints) return false; result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args); } else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { - if (m_enable_card) return false; + if (m_keep_cardinality_constraints) return false; result = m_sort.eq(full, pb.get_k(f).get_unsigned(), sz, args); } else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { - if (m_enable_card) return false; + if (m_keep_cardinality_constraints) return false; result = m_sort.le(full, pb.get_k(f).get_unsigned(), sz, args); } else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { - if (m_enable_card) return false; + if (m_keep_cardinality_constraints) return false; result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args); } else { @@ -406,9 +406,8 @@ struct pb2bv_rewriter::imp { m_imp.m_lemmas.push_back(mk_or(m, n, lits)); } - void enable_card(bool f) { - m_enable_card = f; - m_enable_card = true; + void keep_cardinality_constraints(bool f) { + m_keep_cardinality_constraints = f; } }; @@ -421,7 +420,7 @@ struct pb2bv_rewriter::imp { return m_r.mk_app_core(f, num, args, result); } card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {} - void enable_card(bool f) { m_r.enable_card(f); } + void keep_cardinality_constraints(bool f) { m_r.keep_cardinality_constraints(f); } }; class card_pb_rewriter : public rewriter_tpl { @@ -430,7 +429,7 @@ struct pb2bv_rewriter::imp { card_pb_rewriter(imp& i, ast_manager & m): rewriter_tpl(m, false, m_cfg), m_cfg(i, m) {} - void enable_card(bool f) { m_cfg.enable_card(f); } + void keep_cardinality_constraints(bool f) { m_cfg.keep_cardinality_constraints(f); } }; card_pb_rewriter m_rw; @@ -440,13 +439,17 @@ struct pb2bv_rewriter::imp { m_fresh(m), m_num_translated(0), m_rw(*this, m) { - m_rw.enable_card(p.get_bool("cardinality_solver", false)); + m_rw.keep_cardinality_constraints(p.get_bool("keep_cardinality_constraints", true)); } void updt_params(params_ref const & p) { m_params.append(p); - m_rw.enable_card(m_params.get_bool("cardinality_solver", false)); + m_rw.keep_cardinality_constraints(m_params.get_bool("keep_cardinality_constraints", true)); } + 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"); + } + unsigned get_num_steps() const { return m_rw.get_num_steps(); } void cleanup() { m_rw.cleanup(); } void operator()(expr * e, expr_ref & result, proof_ref & result_proof) { @@ -483,6 +486,8 @@ struct pb2bv_rewriter::imp { pb2bv_rewriter::pb2bv_rewriter(ast_manager & m, params_ref const& p) { m_imp = alloc(imp, m, p); } pb2bv_rewriter::~pb2bv_rewriter() { dealloc(m_imp); } void pb2bv_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); } +void pb2bv_rewriter::collect_param_descrs(param_descrs& r) const { m_imp->collect_param_descrs(r); } + ast_manager & pb2bv_rewriter::m() const { return m_imp->m; } unsigned pb2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); } void pb2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); } diff --git a/src/ast/rewriter/pb2bv_rewriter.h b/src/ast/rewriter/pb2bv_rewriter.h index 47d8361cb..c5a86221d 100644 --- a/src/ast/rewriter/pb2bv_rewriter.h +++ b/src/ast/rewriter/pb2bv_rewriter.h @@ -31,6 +31,7 @@ public: ~pb2bv_rewriter(); void updt_params(params_ref const & p); + void collect_param_descrs(param_descrs& r) const; ast_manager & m() const; unsigned get_num_steps() const; void cleanup(); diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 6d0c2979b..7f6368972 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -38,10 +38,7 @@ namespace sat { dealloc(m_out); for (unsigned i = 0; i < m_proof.size(); ++i) { clause* c = m_proof[i]; - if (m_status[i] == status::deleted || m_status[i] == status::external) { - s.m_cls_allocator.del_clause(c); - } - else if (c && c->size() == 2) { + if (c && (c->size() == 2 || m_status[i] == status::deleted || m_status[i] == status::external)) { s.m_cls_allocator.del_clause(c); } } @@ -116,8 +113,10 @@ namespace sat { clause* c = s.m_cls_allocator.mk_clause(2, lits, st == status::learned); m_proof.push_back(c); m_status.push_back(st); - m_watches[(~l1).index()].push_back(c); - m_watches[(~l2).index()].push_back(c); + unsigned idx = m_watched_clauses.size(); + m_watched_clauses.push_back(watched_clause(c, l1, l2)); + m_watches[(~l1).index()].push_back(idx); + m_watches[(~l2).index()].push_back(idx); if (value(l1) == l_false && value(l2) == l_false) { m_inconsistent = true; @@ -146,34 +145,43 @@ namespace sat { del_watch(c, c[1]); return; } - literal l1 = null_literal, l2 = null_literal; + unsigned num_watch = 0; + literal l1, l2; for (unsigned i = 0; i < n; ++i) { if (value(c[i]) != l_false) { - if (l1 == null_literal) { - l1 = c[i]; + if (num_watch == 0) { + l1 = c[i]; + ++num_watch; } else { l2 = c[i]; + ++num_watch; break; } } } - if (l2 == null_literal && l1 != null_literal) { - assign_propagate(l1); + switch (num_watch) { + case 0: + m_inconsistent = true; + break; + case 1: + assign_propagate(l1); + break; + default: { + SASSERT(num_watch == 2); + unsigned idx = m_watched_clauses.size(); + m_watched_clauses.push_back(watched_clause(&c, l1, l2)); + m_watches[(~l1).index()].push_back(idx); + m_watches[(~l2).index()].push_back(idx); + break; } - else if (l1 == null_literal) { - m_inconsistent = true; - } - else { - m_watches[(~l1).index()].push_back(&c); - m_watches[(~l2).index()].push_back(&c); } } void drat::del_watch(clause& c, literal l) { watch& w = m_watches[(~l).index()]; for (unsigned i = 0; i < w.size(); ++i) { - if (w[i] == &c) { + if (m_watched_clauses[w[i]].m_clause == &c) { w[i] = w.back(); w.pop_back(); break; @@ -196,6 +204,9 @@ namespace sat { for (unsigned i = 0; !m_inconsistent && i < n; ++i) { assign_propagate(~c[i]); } + if (!m_inconsistent) { + TRACE("sat", display(tout);); + } for (unsigned i = num_units; i < m_units.size(); ++i) { m_assignment[m_units[i].var()] = l_undef; } @@ -233,36 +244,53 @@ namespace sat { else { std::cout << "Verification failed\n"; display(std::cout); + TRACE("sat", display(tout); s.display(tout);); + UNREACHABLE(); exit(0); } } void drat::display(std::ostream& out) const { out << "units: " << m_units << "\n"; -#if 0 +#if 1 for (unsigned i = 0; i < m_assignment.size(); ++i) { - lbool v = value(literal(i, false)); - if (v != l_undef) std::cout << i << ": " << v << "\n"; + lbool v = value(literal(i, false)); + if (v != l_undef) out << i << ": " << v << "\n"; } #endif for (unsigned i = 0; i < m_proof.size(); ++i) { clause* c = m_proof[i]; if (m_status[i] != status::deleted && c) { + unsigned num_true = 0; + unsigned num_undef = 0; + for (unsigned j = 0; j < c->size(); ++j) { + switch (value((*c)[j])) { + case l_true: num_true++; break; + case l_undef: num_undef++; break; + default: break; + } + } + if (num_true == 0 && num_undef == 0) { + out << "False "; + } + if (num_true == 0 && num_undef == 1) { + out << "Unit "; + } out << i << ": " << *c << "\n"; } } -#if 0 +#if 1 for (unsigned i = 0; i < m_assignment.size(); ++i) { watch const& w1 = m_watches[2*i]; watch const& w2 = m_watches[2*i + 1]; if (!w1.empty()) { out << i << " |-> "; - for (unsigned i = 0; i < w1.size(); ++i) out << w1[i] << " "; + for (unsigned i = 0; i < w1.size(); ++i) out << *(m_watched_clauses[w1[i]].m_clause) << " "; out << "\n"; } if (!w2.empty()) { out << "-" << i << " |-> "; - for (unsigned i = 0; i < w2.size(); ++i) out << w2[i] << " "; + for (unsigned i = 0; i < w2.size(); ++i) out << *(m_watched_clauses[w2[i]].m_clause) << " "; out << "\n"; } } @@ -302,41 +330,45 @@ namespace sat { watch::iterator it2 = it; watch::iterator end = clauses.end(); for (; it != end; ++it) { - clause& c = *(*it); - if (c[0] == ~l) { - std::swap(c[0], c[1]); + unsigned idx = *it; + watched_clause& wc = m_watched_clauses[idx]; + clause& c = *wc.m_clause; + + TRACE("sat", tout << "Propagate " << l << " " << c << " watch: " << wc.m_l1 << " " << wc.m_l2 << "\n";); + if (wc.m_l1 == ~l) { + std::swap(wc.m_l1, wc.m_l2); } - if (c[1] != ~l) { + if (wc.m_l2 != ~l) { + std::cout << wc.m_l1 << " " << wc.m_l2 << " ~l: " << ~l << "\n"; + std::cout << *wc.m_clause << "\n"; + } + SASSERT(wc.m_l2 == ~l); + if (value(wc.m_l1) == l_true) { *it2 = *it; it2++; - continue; - } - SASSERT(c[1] == ~l); - if (value(c[0]) == l_true) { - it2++; } else { - literal * l_it = c.begin() + 2; - literal * l_end = c.end(); bool done = false; - for (; l_it != l_end && !done; ++l_it) { - if (value(*l_it) != l_false) { - c[1] = *l_it; - *l_it = ~l; - m_watches[(~c[1]).index()].push_back(&c); + for (unsigned i = 0; !done && i < c.size(); ++i) { + literal lit = c[i]; + if (lit != wc.m_l1 && lit != wc.m_l2 && value(lit) != l_false) { + wc.m_l2 = lit; + m_watches[(~lit).index()].push_back(idx); done = true; - } + } } - if (done) + if (done) { + it2++; continue; - else if (value(c[0]) == l_false) { + } + else if (value(wc.m_l1) == l_false) { m_inconsistent = true; goto end_process_watch; } else { *it2 = *it; it2++; - assign(c[0]); + assign(wc.m_l1); } } } diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h index 7236d8065..8edaa5001 100644 --- a/src/sat/sat_drat.h +++ b/src/sat/sat_drat.h @@ -36,7 +36,14 @@ namespace sat { }; private: enum status { asserted, learned, deleted, external }; - typedef ptr_vector watch; + struct watched_clause { + clause* m_clause; + literal m_l1, m_l2; + watched_clause(clause* c, literal l1, literal l2): + m_clause(c), m_l1(l1), m_l2(l2) {} + }; + svector m_watched_clauses; + typedef svector watch; solver& s; std::ostream* m_out; ptr_vector m_proof; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 69b2bcea1..98e7fabf1 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -23,7 +23,6 @@ def_module_params('sat', ('core.minimize', BOOL, False, 'minimize computed core'), ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), ('parallel_threads', UINT, 1, 'number of parallel threads to use'), - ('cardinality_solver', BOOL, False, 'enable cardinality based solver'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'), ('drat', BOOL, False, 'produce DRAT proofs'), ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 221140590..73829c6b8 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -718,8 +718,8 @@ namespace sat { assign_core(c[0], justification(cls_off)); #ifdef UPDATE_GLUE if (update && c.is_learned() && c.glue() > 2) { - unsigned glue = num_diff_levels(c.size(), c.begin()); - if (glue+1 < c.glue()) { + unsigned glue; + if (num_diff_levels_below(c.size(), c.begin(), c.glue()-1, glue)) { c.set_glue(glue); } } @@ -2142,6 +2142,26 @@ namespace sat { return r; } + bool solver::num_diff_levels_below(unsigned num, literal const* lits, unsigned max_glue, unsigned& glue) { + m_diff_levels.reserve(scope_lvl() + 1, false); + glue = 0; + unsigned i = 0; + for (; i < num && glue < max_glue; i++) { + SASSERT(value(lits[i]) != l_undef); + unsigned lit_lvl = lvl(lits[i]); + if (m_diff_levels[lit_lvl] == false) { + m_diff_levels[lit_lvl] = true; + glue++; + } + } + num = i; + // reset m_diff_levels. + for (i = 0; i < num; i++) + m_diff_levels[lvl(lits[i])] = false; + return glue < max_glue; + } + + /** \brief Process an antecedent for lemma minimization. */ @@ -2278,11 +2298,14 @@ namespace sat { unsigned sz = m_lemma.size(); unsigned i = 1; // the first literal is the FUIP unsigned j = 1; + //bool drop = false; + //unsigned bound = sz/5+10; for (; i < sz; i++) { literal l = m_lemma[i]; if (implied_by_marked(l)) { TRACE("sat", tout << "drop: " << l << "\n";); m_unmark.push_back(l.var()); + //drop = true; } else { if (j != i) { @@ -2290,6 +2313,13 @@ namespace sat { } j++; } +#if 0 + if (!drop && i >= bound) { + // std::cout << "drop\n"; + j = sz; + break; + } +#endif } reset_unmark(0); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index d5affd2d4..0e8f17298 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -394,6 +394,7 @@ namespace sat { void updt_phase_counters(); svector m_diff_levels; unsigned num_diff_levels(unsigned num, literal const * lits); + bool num_diff_levels_below(unsigned num, literal const* lits, unsigned max_glue, unsigned& glue); // lemma minimization typedef approx_set_tpl level_approx_set; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index eec734dc7..9e8a31c5d 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -84,7 +84,6 @@ public: m_unknown("no reason given") { m_params.set_bool("elim_vars", false); sat_params p1(m_params); - m_params.set_bool("cardinality_solver", p1.cardinality_solver()); m_solver.updt_params(m_params); init_preprocess(); } @@ -219,7 +218,6 @@ public: virtual void updt_params(params_ref const & p) { m_params.append(p); sat_params p1(p); - m_params.set_bool("cardinality_solver", p1.cardinality_solver()); m_params.set_bool("elim_vars", false); std::cout << m_params << "\n"; m_solver.updt_params(m_params); diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index bfd533e8a..106cba954 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -70,8 +70,8 @@ public: return m_solver->check_sat(num_assumptions, assumptions); } - virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); } - virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } + virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); m_rewriter.updt_params(p); } + virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); m_rewriter.collect_param_descrs(r); } virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } virtual void collect_statistics(statistics & st) const {