From 8b4f3ac6f0244c463aa3881c3d78134e433adab8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 10 Feb 2017 18:04:54 -0500 Subject: [PATCH] fix drat checker Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/sat/CMakeLists.txt | 2 +- src/sat/card_extension.cpp | 91 ++++++----------- src/sat/card_extension.h | 6 +- src/sat/sat_asymm_branch.cpp | 6 +- src/sat/sat_cleaner.cpp | 4 +- src/sat/sat_config.cpp | 6 +- src/sat/sat_config.h | 2 +- src/sat/sat_drat.cpp | 113 ++++++++++++++-------- src/sat/sat_drat.h | 2 + src/sat/sat_elim_eqs.cpp | 31 +++--- src/sat/{sat_par.cpp => sat_parallel.cpp} | 34 +++---- src/sat/{sat_par.h => sat_parallel.h} | 8 +- src/sat/sat_params.pyg | 2 +- src/sat/sat_simplifier.cpp | 23 ++++- src/sat/sat_solver.cpp | 29 +++--- src/sat/sat_solver.h | 8 +- 16 files changed, 201 insertions(+), 166 deletions(-) rename src/sat/{sat_par.cpp => sat_parallel.cpp} (86%) rename src/sat/{sat_par.h => sat_parallel.h} (96%) diff --git a/contrib/cmake/src/sat/CMakeLists.txt b/contrib/cmake/src/sat/CMakeLists.txt index 6ffbb8c71..00c988f5c 100644 --- a/contrib/cmake/src/sat/CMakeLists.txt +++ b/contrib/cmake/src/sat/CMakeLists.txt @@ -14,7 +14,7 @@ z3_add_component(sat sat_integrity_checker.cpp sat_model_converter.cpp sat_mus.cpp - sat_par.cpp + sat_parallel.cpp sat_probing.cpp sat_scc.cpp sat_simplifier.cpp diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp index 17dcd7f5f..0e03708c9 100644 --- a/src/sat/card_extension.cpp +++ b/src/sat/card_extension.cpp @@ -266,12 +266,6 @@ namespace sat { m_active_vars.reset(); } - void card_extension::reset_marked_literals() { - for (unsigned i = 0; i < m_marked_literals.size(); ++i) { - s().unmark_lit(m_marked_literals[i]); - } - m_marked_literals.reset(); - } bool card_extension::resolve_conflict() { if (0 == m_num_propagations_since_pop) @@ -280,7 +274,7 @@ namespace sat { m_num_marks = 0; m_bound = 0; m_lemma.reset(); - m_lemma.push_back(null_literal); + // m_lemma.push_back(null_literal); literal consequent = s().m_not_l; justification js = s().m_conflict; m_conflict_lvl = s().get_max_lvl(consequent, js); @@ -292,8 +286,6 @@ namespace sat { unsigned idx = lits.size()-1; int offset = 1; - unsigned num_card = 0; - unsigned num_steps = 0; DEBUG_CODE(active2pb(m_A);); unsigned init_marks = m_num_marks; @@ -305,11 +297,13 @@ namespace sat { } // TBD: need proper check for overflow. if (offset > (1 << 12)) { + IF_VERBOSE(2, verbose_stream() << "offset: " << offset << "\n"; + active2pb(m_A); + display(verbose_stream(), m_A); + ); goto bail_out; } - ++num_steps; - // TRACE("sat", display(tout, m_A);); TRACE("sat", tout << "process consequent: " << consequent << ":\n"; s().display_justification(tout, js) << "\n";); SASSERT(offset > 0); @@ -320,9 +314,7 @@ namespace sat { switch(js.get_kind()) { case justification::NONE: SASSERT (consequent != null_literal); - m_lemma.push_back(~consequent); m_bound += offset; - inc_coeff(consequent, offset); break; case justification::BINARY: m_bound += offset; @@ -358,14 +350,10 @@ namespace sat { break; } case justification::EXT_JUSTIFICATION: { - ++num_card; unsigned index = js.get_ext_justification_idx(); card& c = *m_constraints[index]; m_bound += offset * c.k(); - if (!process_card(c, offset)) { - TRACE("sat", tout << "failed to process card\n";); - goto bail_out; - } + process_card(c, offset); break; } default: @@ -394,7 +382,7 @@ namespace sat { v = consequent.var(); if (s().is_marked(v)) break; if (idx == 0) { - std::cout << num_steps << " " << init_marks << "\n"; + IF_VERBOSE(2, verbose_stream() << "did not find marked literal\n";); goto bail_out; } SASSERT(idx > 0); @@ -421,65 +409,45 @@ namespace sat { SASSERT(validate_lemma()); normalize_active_coeffs(); - reset_marked_literals(); - if (consequent == null_literal) { - return false; - } int slack = -m_bound; for (unsigned i = 0; i < m_active_vars.size(); ++i) { bool_var v = m_active_vars[i]; slack += get_abs_coeff(v); } - - consequent = null_literal; ++idx; - - unsigned num_atoms = m_lemma.size(); while (0 <= slack) { literal lit = lits[idx]; bool_var v = lit.var(); if (m_active_var_set.contains(v)) { int coeff = get_coeff(v); - bool append = false; if (coeff < 0 && !lit.sign()) { slack += coeff; - append = true; + m_lemma.push_back(~lit); } else if (coeff > 0 && lit.sign()) { slack -= coeff; - append = true; - } - if (append) { - if (consequent == null_literal) { - consequent = ~lit; - } - else { - m_lemma.push_back(~lit); - } + m_lemma.push_back(~lit); } } + if (idx == 0 && slack >= 0) { + IF_VERBOSE(2, verbose_stream() << "(sat.card non-asserting)\n";); + goto bail_out; + } SASSERT(idx > 0 || slack < 0); --idx; } - for (unsigned i = 1; i < std::min(m_lemma.size(), num_atoms + 1); ++i) { - if (lvl(m_lemma[i]) == m_conflict_lvl) { - TRACE("sat", tout << "Bail out on no progress " << lit << "\n";); - IF_VERBOSE(3, verbose_stream() << "(sat.card bail resolve)\n";); - return false; - } + if (m_lemma.size() >= 2 && lvl(m_lemma[1]) == m_conflict_lvl) { + // TRACE("sat", tout << "Bail out on no progress " << lit << "\n";); + IF_VERBOSE(2, verbose_stream() << "(sat.card bail non-asserting resolvent)\n";); + goto bail_out; } SASSERT(slack < 0); - if (consequent == null_literal) { - if (!m_lemma.empty()) return false; - } - else { - m_lemma[0] = consequent; - SASSERT(validate_conflict(m_lemma, m_A)); - } + SASSERT(validate_conflict(m_lemma, m_A)); + TRACE("sat", tout << m_lemma << "\n";); if (s().m_config.m_drat) { @@ -498,8 +466,6 @@ namespace sat { return true; bail_out: - reset_marked_literals(); - std::cout << "bail num marks: " << m_num_marks << " idx: " << idx << "\n"; while (m_num_marks > 0 && idx >= 0) { bool_var v = lits[idx].var(); if (s().is_marked(v)) { @@ -511,22 +477,18 @@ namespace sat { return false; } - bool card_extension::process_card(card& c, int offset) { + void card_extension::process_card(card& c, int offset) { literal lit = c.lit(); SASSERT(c.k() <= c.size()); SASSERT(value(lit) == l_true); + SASSERT(0 < offset); for (unsigned i = c.k(); i < c.size(); ++i) { process_antecedent(c[i], offset); } for (unsigned i = 0; i < c.k(); ++i) { inc_coeff(c[i], offset); } - if (lvl(lit) > 0 && !s().is_marked_lit(lit)) { - m_lemma.push_back(~lit); - s().mark_lit(lit); - m_marked_literals.push_back(lit); - } - return (lvl(lit) <= m_conflict_lvl); + process_antecedent(~lit, c.k() * offset); } void card_extension::process_antecedent(literal l, int offset) { @@ -900,6 +862,7 @@ namespace sat { for (unsigned i = 0; i < c.size(); ++i) { p.push(c[i], offset); } + p.push(~c.lit(), offset*c.k()); break; } default: @@ -977,7 +940,10 @@ namespace sat { bool card_extension::validate_conflict(literal_vector const& lits, ineq& p) { for (unsigned i = 0; i < lits.size(); ++i) { - if (value(lits[i]) != l_false) return false; + if (value(lits[i]) != l_false) { + TRACE("sat", tout << "literal " << lits[i] << " is not false\n";); + return false; + } } unsigned value = 0; for (unsigned i = 0; i < p.m_lits.size(); ++i) { @@ -986,6 +952,9 @@ namespace sat { value += coeff; } } + CTRACE("sat", value >= p.m_k, tout << "slack: " << value << " bound " << p.m_k << "\n"; + display(tout, p); + tout << lits << "\n";); return value < p.m_k; } diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h index 654665c22..3b65afb6b 100644 --- a/src/sat/card_extension.h +++ b/src/sat/card_extension.h @@ -98,8 +98,7 @@ namespace sat { int m_bound; tracked_uint_set m_active_var_set; literal_vector m_lemma; - literal_vector m_literals; - literal_vector m_marked_literals; +// literal_vector m_literals; unsigned m_num_propagations_since_pop; solver& s() const { return *m_solver; } @@ -125,10 +124,9 @@ namespace sat { int get_coeff(bool_var v) const; int get_abs_coeff(bool_var v) const; - literal_vector& get_literals() { m_literals.reset(); return m_literals; } literal get_asserting_literal(literal conseq); void process_antecedent(literal l, int offset); - bool process_card(card& c, int offset); + void process_card(card& c, int offset); void cut(); // validation utilities diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp index 8a761ea3a..efadc5266 100644 --- a/src/sat/sat_asymm_branch.cpp +++ b/src/sat/sat_asymm_branch.cpp @@ -169,7 +169,9 @@ namespace sat { literal l = c[i]; switch (s.value(l)) { case l_undef: - c[j] = l; + if (i != j) { + std::swap(c[i], c[j]); + } j++; break; case l_false: @@ -201,6 +203,8 @@ namespace sat { default: c.shrink(new_sz); s.attach_clause(c); + if (s.m_config.m_drat) s.m_drat.add(c, true); + // if (s.m_config.m_drat) s.m_drat.del(c0); // TBD SASSERT(s.m_qhead == s.m_trail.size()); return true; } diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp index 10751c622..94da1dd4f 100644 --- a/src/sat/sat_cleaner.cpp +++ b/src/sat/sat_cleaner.cpp @@ -99,7 +99,9 @@ namespace sat { m_elim_literals++; break; case l_undef: - c[j] = c[i]; + if (i != j) { + std::swap(c[j], c[i]); + } j++; break; } diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index 77a93c1e9..cd756d79b 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -35,7 +35,7 @@ namespace sat { m_glue("glue"), m_glue_psm("glue_psm"), m_psm_glue("psm_glue") { - m_num_parallel = 1; + m_num_threads = 1; updt_params(p); } @@ -78,7 +78,7 @@ namespace sat { m_burst_search = p.burst_search(); m_max_conflicts = p.max_conflicts(); - m_num_parallel = p.parallel_threads(); + m_num_threads = p.threads(); // These parameters are not exposed m_simplify_mult1 = _p.get_uint("simplify_mult1", 300); @@ -113,7 +113,7 @@ namespace sat { m_minimize_lemmas = p.minimize_lemmas(); m_core_minimize = p.core_minimize(); m_core_minimize_partial = p.core_minimize_partial(); - m_drat = p.drat(); + m_drat = p.drat() && p.threads() == 1; m_drat_check = p.drat_check(); m_drat_file = p.drat_file(); m_dyn_sub_res = p.dyn_sub_res(); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 03616b6d8..6f29f485e 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -57,7 +57,7 @@ namespace sat { unsigned m_random_seed; unsigned m_burst_search; unsigned m_max_conflicts; - unsigned m_num_parallel; + unsigned m_num_threads; unsigned m_simplify_mult1; double m_simplify_mult2; diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 7f6368972..ba4173eed 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -79,7 +79,6 @@ namespace sat { out << st << " "; literal last = null_literal; for (unsigned i = 0; i < n; ++i) { - declare(c[i]); if (c[i] != last) { out << c[i] << " "; last = c[i]; @@ -89,7 +88,7 @@ namespace sat { } void drat::append(literal l, status st) { - trace(std::cout, 1, &l, st); + IF_VERBOSE(10, trace(verbose_stream(), 1, &l, st);); if (st == status::learned) { verify(1, &l); } @@ -101,7 +100,7 @@ namespace sat { void drat::append(literal l1, literal l2, status st) { literal lits[2] = { l1, l2 }; - trace(std::cout, 2, lits, st); + IF_VERBOSE(10, trace(verbose_stream(), 2, lits, st);); if (st == status::deleted) { // noop // don't record binary as deleted. @@ -132,7 +131,7 @@ namespace sat { void drat::append(clause& c, status st) { unsigned n = c.size(); - trace(std::cout, n, c.begin(), st); + IF_VERBOSE(10, trace(verbose_stream(), n, c.begin(), st);); if (st == status::learned) { verify(n, c.begin()); @@ -205,8 +204,12 @@ namespace sat { assign_propagate(~c[i]); } if (!m_inconsistent) { - TRACE("sat", display(tout);); + DEBUG_CODE(validate_propagation();); } + for (unsigned i = 0; i < m_units.size(); ++i) { + SASSERT(m_assignment[m_units[i].var()] != l_undef); + } + for (unsigned i = num_units; i < m_units.size(); ++i) { m_assignment[m_units[i].var()] = l_undef; } @@ -218,9 +221,37 @@ namespace sat { bool drat::is_drat(unsigned n, literal const* c) { if (m_inconsistent || n == 0) return true; - literal l = c[0]; - literal_vector lits(n - 1, c + 1); - for (unsigned i = 0; m_proof.size(); ++i) { + for (unsigned i = 0; i < n; ++i) { + if (is_drat(n, c, i)) return true; + } + return false; + } + + void drat::validate_propagation() const { + for (unsigned i = 0; i < m_proof.size(); ++i) { + status st = m_status[i]; + if (m_proof[i] && st != status::deleted) { + clause& c = *m_proof[i]; + unsigned num_undef = 0, num_true = 0; + for (unsigned j = 0; j < c.size(); ++j) { + switch (value(c[j])) { + case l_false: break; + case l_true: num_true++; break; + case l_undef: num_undef++; break; + } + } + CTRACE("sat", num_true == 0 && num_undef == 1, display(tout);); + SASSERT(num_true != 0 || num_undef != 1); + } + } + } + + bool drat::is_drat(unsigned n, literal const* c, unsigned pos) { + SASSERT(pos < n); + literal l = c[pos]; + literal_vector lits(n, c); + SASSERT(lits.size() == n); + for (unsigned i = 0; i < m_proof.size(); ++i) { status st = m_status[i]; if (m_proof[i] && (st == status::asserted || st == status::external)) { clause& c = *m_proof[i]; @@ -230,21 +261,22 @@ namespace sat { lits.append(j, c.begin()); lits.append(c.size() - j - 1, c.begin() + j + 1); if (!is_drup(lits.size(), lits.c_ptr())) return false; - lits.resize(n - 1); + lits.resize(n); } } } return true; + } void drat::verify(unsigned n, literal const* c) { - if (is_drup(n, c) || is_drat(n, c)) { - std::cout << "Verified\n"; - } - else { + if (!is_drup(n, c) && !is_drat(n, c)) { std::cout << "Verification failed\n"; display(std::cout); - TRACE("sat", display(tout); s.display(tout);); + TRACE("sat", + tout << literal_vector(n, c) << "\n"; + display(tout); + s.display(tout);); UNREACHABLE(); exit(0); } @@ -252,12 +284,10 @@ namespace sat { void drat::display(std::ostream& out) const { out << "units: " << m_units << "\n"; -#if 1 for (unsigned i = 0; i < m_assignment.size(); ++i) { 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) { @@ -276,10 +306,9 @@ namespace sat { if (num_true == 0 && num_undef == 1) { out << "Unit "; } - out << i << ": " << *c << "\n"; + out << m_status[i] << " " << i << ": " << *c << "\n"; } } -#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]; @@ -294,25 +323,27 @@ namespace sat { out << "\n"; } } -#endif } lbool drat::value(literal l) const { - lbool v = m_assignment[l.var()]; - return v == l_undef || !l.sign() ? v : ~v; + lbool val = m_assignment.get(l.var(), l_undef); + return val == l_undef || !l.sign() ? val : ~val; } void drat::assign(literal l) { lbool new_value = l.sign() ? l_false : l_true; lbool old_value = value(l); - if (new_value != old_value) { - if (old_value == l_undef) { - m_assignment[l.var()] = new_value; - m_units.push_back(l); - } - else { - m_inconsistent = true; - } +// TRACE("sat", tout << "assign " << l << " := " << new_value << " from " << old_value << "\n";); + switch (old_value) { + case l_false: + m_inconsistent = true; + break; + case l_true: + break; + case l_undef: + m_assignment.setx(l.var(), new_value, l_undef); + m_units.push_back(l); + break; } } @@ -334,14 +365,11 @@ namespace sat { 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";); + //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 (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; @@ -358,7 +386,6 @@ namespace sat { } } if (done) { - it2++; continue; } else if (value(wc.m_l1) == l_false) { @@ -385,22 +412,26 @@ namespace sat { void drat::add() { if (m_out) (*m_out) << "0\n"; if (s.m_config.m_drat_check) { - if (m_inconsistent) std::cout << "Verified\n"; - else std::cout << "Failed to verify\n"; + SASSERT(m_inconsistent); } } void drat::add(literal l, bool learned) { + declare(l); status st = get_status(learned); if (m_out) dump(1, &l, st); if (s.m_config.m_drat_check) append(l, st); } void drat::add(literal l1, literal l2, bool learned) { + declare(l1); + declare(l2); literal ls[2] = {l1, l2}; status st = get_status(learned); if (m_out) dump(2, ls, st); if (s.m_config.m_drat_check) append(l1, l2, st); } void drat::add(clause& c, bool learned) { + TRACE("sat", tout << "add: " << c << "\n";); + for (unsigned i = 0; i < c.size(); ++i) declare(c[i]); status st = get_status(learned); if (m_out) dump(c.size(), c.begin(), st); if (s.m_config.m_drat_check) append(c, get_status(learned)); @@ -429,9 +460,11 @@ namespace sat { append(l1, l2, status::deleted); } void drat::del(clause& c) { + TRACE("sat", tout << "del: " << c << "\n";); if (m_out) dump(c.size(), c.begin(), status::deleted); - if (s.m_config.m_drat_check) - append(c, status::deleted); - else s.m_cls_allocator.del_clause(&c); + if (s.m_config.m_drat_check) { + clause* c1 = s.m_cls_allocator.mk_clause(c.size(), c.begin(), c.is_learned()); + append(*c1, status::deleted); + } } } diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h index 8edaa5001..e9663628b 100644 --- a/src/sat/sat_drat.h +++ b/src/sat/sat_drat.h @@ -68,9 +68,11 @@ namespace sat { void verify(unsigned n, literal const* c); bool is_drup(unsigned n, literal const* c); bool is_drat(unsigned n, literal const* c); + bool is_drat(unsigned n, literal const* c, unsigned pos); lbool value(literal l) const; void trace(std::ostream& out, unsigned n, literal const* c, status st); void display(std::ostream& out) const; + void validate_propagation() const; public: drat(solver& s); diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp index 6a7ca6280..8cde147cc 100644 --- a/src/sat/sat_elim_eqs.cpp +++ b/src/sat/sat_elim_eqs.cpp @@ -117,7 +117,9 @@ namespace sat { break; // clause was satisfied if (val == l_false) continue; // skip - c[j] = l; + if (i != j) { + std::swap(c[i], c[j]); + } j++; } if (i < sz) { @@ -136,16 +138,7 @@ namespace sat { return; } TRACE("elim_eqs", tout << "after removing duplicates: " << c << " j: " << j << "\n";); - if (j < sz) - c.shrink(j); - else - c.update_approx(); - SASSERT(c.size() == j); - DEBUG_CODE({ - for (unsigned i = 0; i < c.size(); i++) { - SASSERT(c[i] == norm(roots, c[i])); - } - }); + SASSERT(j >= 1); switch (j) { case 1: @@ -160,8 +153,22 @@ namespace sat { SASSERT(*it == &c); *it2 = *it; it2++; - if (!c.frozen()) + if (j < sz) { + if (m_solver.m_config.m_drat) m_solver.m_drat.del(c); + c.shrink(j); + if (m_solver.m_config.m_drat) m_solver.m_drat.add(c, true); + } + else + c.update_approx(); + + DEBUG_CODE({ + for (unsigned i = 0; i < sz; i++) { + SASSERT(c[i] == norm(roots, c[i])); + } }); + + if (!c.frozen()) { m_solver.attach_clause(c); + } break; } } diff --git a/src/sat/sat_par.cpp b/src/sat/sat_parallel.cpp similarity index 86% rename from src/sat/sat_par.cpp rename to src/sat/sat_parallel.cpp index 8d2c20d56..da0714907 100644 --- a/src/sat/sat_par.cpp +++ b/src/sat/sat_parallel.cpp @@ -3,9 +3,9 @@ Copyright (c) 2017 Microsoft Corporation Module Name: - sat_par.cpp + sat_parallel.cpp -Abstract: + Abstract: Utilities for parallel SAT solving. @@ -16,14 +16,14 @@ Author: Revision History: --*/ -#include "sat_par.h" +#include "sat_parallel.h" #include "sat_clause.h" #include "sat_solver.h" namespace sat { - void par::vector_pool::next(unsigned& index) { + void parallel::vector_pool::next(unsigned& index) { SASSERT(index < m_size); unsigned n = index + 2 + get_length(index); if (n >= m_size) { @@ -34,7 +34,7 @@ namespace sat { } } - void par::vector_pool::reserve(unsigned num_threads, unsigned sz) { + void parallel::vector_pool::reserve(unsigned num_threads, unsigned sz) { m_vectors.reset(); m_vectors.resize(sz, 0); m_heads.reset(); @@ -43,7 +43,7 @@ namespace sat { m_size = sz; } - void par::vector_pool::begin_add_vector(unsigned owner, unsigned n) { + void parallel::vector_pool::begin_add_vector(unsigned owner, unsigned n) { unsigned capacity = n + 2; m_vectors.reserve(m_size + capacity, 0); IF_VERBOSE(3, verbose_stream() << owner << ": begin-add " << n << " tail: " << m_tail << " size: " << m_size << "\n";); @@ -71,11 +71,11 @@ namespace sat { m_vectors[m_tail++] = n; } - void par::vector_pool::add_vector_elem(unsigned e) { + void parallel::vector_pool::add_vector_elem(unsigned e) { m_vectors[m_tail++] = e; } - bool par::vector_pool::get_vector(unsigned owner, unsigned& n, unsigned const*& ptr) { + bool parallel::vector_pool::get_vector(unsigned owner, unsigned& n, unsigned const*& ptr) { unsigned head = m_heads[owner]; unsigned iterations = 0; while (head != m_tail) { @@ -97,15 +97,15 @@ namespace sat { return false; } - par::par(solver& s): m_scoped_rlimit(s.rlimit()) {} + parallel::parallel(solver& s): m_scoped_rlimit(s.rlimit()) {} - par::~par() { + parallel::~parallel() { for (unsigned i = 0; i < m_solvers.size(); ++i) { dealloc(m_solvers[i]); } } - void par::init_solvers(solver& s, unsigned num_extra_solvers) { + void parallel::init_solvers(solver& s, unsigned num_extra_solvers) { unsigned num_threads = num_extra_solvers + 1; m_solvers.resize(num_extra_solvers, 0); symbol saved_phase = s.m_params.get_sym("phase", symbol("caching")); @@ -127,7 +127,7 @@ namespace sat { } - void par::exchange(solver& s, literal_vector const& in, unsigned& limit, literal_vector& out) { + void parallel::exchange(solver& s, literal_vector const& in, unsigned& limit, literal_vector& out) { if (s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); #pragma omp critical (par_solver) @@ -147,7 +147,7 @@ namespace sat { } } - void par::share_clause(solver& s, literal l1, literal l2) { + void parallel::share_clause(solver& s, literal l1, literal l2) { if (s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); #pragma omp critical (par_solver) @@ -159,7 +159,7 @@ namespace sat { } } - void par::share_clause(solver& s, clause const& c) { + void parallel::share_clause(solver& s, clause const& c) { if (!enable_add(c) || s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); unsigned n = c.size(); @@ -174,7 +174,7 @@ namespace sat { } } - void par::get_clauses(solver& s) { + void parallel::get_clauses(solver& s) { if (s.m_par_syncing_clauses) return; flet _disable_sync_clause(s.m_par_syncing_clauses, true); #pragma omp critical (par_solver) @@ -183,7 +183,7 @@ namespace sat { } } - void par::_get_clauses(solver& s) { + void parallel::_get_clauses(solver& s) { unsigned n; unsigned const* ptr; unsigned owner = s.m_par_id; @@ -198,7 +198,7 @@ namespace sat { } } - bool par::enable_add(clause const& c) const { + bool parallel::enable_add(clause const& c) const { // plingeling, glucose heuristic: return (c.size() <= 40 && c.glue() <= 8) || c.glue() <= 2; } diff --git a/src/sat/sat_par.h b/src/sat/sat_parallel.h similarity index 96% rename from src/sat/sat_par.h rename to src/sat/sat_parallel.h index dd2e93f95..9d060aaaf 100644 --- a/src/sat/sat_par.h +++ b/src/sat/sat_parallel.h @@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation Module Name: - sat_par.h + sat_parallel.h Abstract: @@ -26,7 +26,7 @@ Revision History: namespace sat { - class par { + class parallel { // shared pool of learned clauses. class vector_pool { @@ -61,9 +61,9 @@ namespace sat { public: - par(solver& s); + parallel(solver& s); - ~par(); + ~parallel(); void init_solvers(solver& s, unsigned num_extra_solvers); diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 98e7fabf1..4a013a7fd 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -22,7 +22,7 @@ def_module_params('sat', ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'), ('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'), + ('threads', UINT, 1, 'number of parallel threads to use'), ('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_simplifier.cpp b/src/sat/sat_simplifier.cpp index 8bfa4bb69..3c4d784cb 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -554,7 +554,9 @@ namespace sat { literal l = c[i]; switch (value(l)) { case l_undef: - c[j] = l; + if (i != j) { + std::swap(c[j], c[i]); + } j++; break; case l_false: @@ -567,12 +569,18 @@ namespace sat { break; case l_true: r = true; - c[j] = l; + if (i != j) { + std::swap(c[j], c[i]); + } j++; break; } } - c.shrink(j); + if (j < sz) { + if (s.m_config.m_drat) s.m_drat.del(c); + c.shrink(j); + if (s.m_config.m_drat) s.m_drat.add(c, true); + } return r; } @@ -588,7 +596,9 @@ namespace sat { literal l = c[i]; switch (value(l)) { case l_undef: - c[j] = l; + if (i != j) { + std::swap(c[j], c[i]); + } j++; break; case l_false: @@ -597,7 +607,7 @@ namespace sat { return true; } } - c.shrink(j); + c.shrink(j); return false; } @@ -642,6 +652,8 @@ namespace sat { m_num_elim_lits++; insert_elim_todo(l.var()); c.elim(l); + if (s.m_config.m_drat) s.m_drat.add(c, true); + // if (s.m_config.m_drat) s.m_drat.del(c0); // can delete previous version clause_use_list & occurs = m_use_list.get(l); occurs.erase_not_removed(c); m_sub_counter -= occurs.size()/2; @@ -1418,6 +1430,7 @@ namespace sat { else s.m_stats.m_mk_clause++; clause * new_c = s.m_cls_allocator.mk_clause(m_new_cls.size(), m_new_cls.c_ptr(), false); + if (s.m_config.m_drat) s.m_drat.add(*new_c, true); s.m_clauses.push_back(new_c); m_use_list.insert(*new_c); if (m_sub_counter > 0) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index f5f9de6fc..78b10d9e1 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -212,9 +212,7 @@ namespace sat { if (m_config.m_drat && !m_drat.is_cleaned(c)) { m_drat.del(c); } - else if (!m_config.m_drat || !m_config.m_drat_check || m_drat.is_cleaned(c)) { - m_cls_allocator.del_clause(&c); - } + m_cls_allocator.del_clause(&c); m_stats.m_del_clause++; } @@ -769,7 +767,7 @@ namespace sat { pop_to_base_level(); IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";); SASSERT(at_base_lvl()); - if (m_config.m_num_parallel > 1 && !m_par) { + if (m_config.m_num_threads > 1 && !m_par) { return check_par(num_lits, lits); } flet _searching(m_searching, true); @@ -842,9 +840,9 @@ namespace sat { }; lbool solver::check_par(unsigned num_lits, literal const* lits) { - int num_threads = static_cast(m_config.m_num_parallel); + int num_threads = static_cast(m_config.m_num_threads); int num_extra_solvers = num_threads - 1; - sat::par par(*this); + sat::parallel par(*this); // par.reserve(num_threads, 1 << 16); par.reserve(num_threads, 1 << 9); par.init_solvers(*this, num_extra_solvers); @@ -956,7 +954,7 @@ namespace sat { } } - void solver::set_par(par* p, unsigned id) { + void solver::set_par(parallel* p, unsigned id) { m_par = p; m_par_num_vars = num_vars(); m_par_limit_in = 0; @@ -1662,7 +1660,9 @@ namespace sat { case l_false: break; case l_undef: - c[j] = c[i]; + if (i != j) { + std::swap(c[i], c[j]); + } j++; break; } @@ -1680,7 +1680,12 @@ namespace sat { mk_bin_clause(c[0], c[1], true); return false; default: - c.shrink(new_sz); + if (new_sz != sz) { + std::cout << "shrinking " << c << "\n"; + if (m_config.m_drat) m_drat.del(c); + c.shrink(new_sz); + if (m_config.m_drat) m_drat.add(c, true); + } attach_clause(c); return true; } @@ -1749,7 +1754,6 @@ namespace sat { if (m_ext && m_ext->resolve_conflict()) { learn_lemma_and_backjump(); - m_stats.m_conflict--; return true; } @@ -2815,7 +2819,10 @@ namespace sat { literal lit = m_trail[i]; if (lvl(lit) > level) { level = lvl(lit); - out << "level: " << level << " - "; + out << level << ": "; + } + else { + out << " "; } out << lit << " "; display_justification(out, m_justification[lit.var()]) << "\n"; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 0e8f17298..30d4ca4ad 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -34,7 +34,7 @@ Revision History: #include"sat_probing.h" #include"sat_mus.h" #include"sat_drat.h" -#include"sat_par.h" +#include"sat_parallel.h" #include"params.h" #include"statistics.h" #include"stopwatch.h" @@ -76,7 +76,7 @@ namespace sat { config m_config; stats m_stats; scoped_ptr m_ext; - par* m_par; + parallel* m_par; random_gen m_rand; clause_allocator m_cls_allocator; cleaner m_cleaner; @@ -153,7 +153,7 @@ namespace sat { friend class mus; friend class drat; friend class card_extension; - friend class par; + friend class parallel; friend struct mk_stat; public: solver(params_ref const & p, reslimit& l); @@ -260,7 +260,7 @@ namespace sat { m_num_checkpoints = 0; if (memory::get_allocation_size() > m_config.m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG); } - void set_par(par* p, unsigned id); + void set_par(parallel* p, unsigned id); bool canceled() { return !m_rlimit.inc(); } config const& get_config() { return m_config; } extension* get_extension() const { return m_ext.get(); }