From f3f83d04457cdca1c924ba5164c964b3aeb12edb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 Jul 2021 13:42:22 -0700 Subject: [PATCH] #5429 --- src/sat/sat_drat.cpp | 61 +++++++++++++++------------------ src/sat/sat_solver.cpp | 3 +- src/sat/sat_solver.h | 5 +++ src/sat/smt/sat_dual_solver.cpp | 4 --- src/sat/smt/sat_dual_solver.h | 3 -- 5 files changed, 34 insertions(+), 42 deletions(-) diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 982b6bb9b..f0ca7132f 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -37,9 +37,8 @@ namespace sat { if (s.get_config().m_drat && s.get_config().m_drat_file.is_non_empty_string()) { auto mode = s.get_config().m_drat_binary ? (std::ios_base::binary | std::ios_base::out | std::ios_base::trunc) : std::ios_base::out; m_out = alloc(std::ofstream, s.get_config().m_drat_file.str(), mode); - if (s.get_config().m_drat_binary) { - std::swap(m_out, m_bout); - } + if (s.get_config().m_drat_binary) + std::swap(m_out, m_bout); } } @@ -50,9 +49,8 @@ namespace sat { dealloc(m_bout); for (unsigned i = 0; i < m_proof.size(); ++i) { clause* c = m_proof[i]; - if (c) { - m_alloc.del_clause(c); - } + if (c) + m_alloc.del_clause(c); } m_proof.reset(); m_out = nullptr; @@ -93,6 +91,7 @@ namespace sat { unsigned len = 0; + if (st.is_deleted()) { buffer[len++] = 'd'; buffer[len++] = ' '; @@ -133,7 +132,7 @@ namespace sat { memcpy(buffer + len, d, lastd - d); len += static_cast(lastd - d); buffer[len++] = ' '; - if (len + 50 > sizeof(buffer)) { + if (static_cast(len) + 50 > sizeof(buffer)) { m_out->write(buffer, len); len = 0; } @@ -208,15 +207,14 @@ namespace sat { declare(l); IF_VERBOSE(20, trace(verbose_stream(), 1, &l, st);); - if (st.is_redundant() && st.is_sat()) { + if (st.is_redundant() && st.is_sat()) verify(1, &l); - } - if (st.is_deleted()) { + + if (st.is_deleted()) return; - } - if (m_check_unsat) { - assign_propagate(l); - } + + if (m_check_unsat) + assign_propagate(l); m_units.push_back(l); } @@ -233,9 +231,9 @@ namespace sat { // don't record binary as deleted. } else { - if (st.is_redundant() && st.is_sat()) { + if (st.is_redundant() && st.is_sat()) verify(2, lits); - } + clause* c = m_alloc.mk_clause(2, lits, st.is_redundant()); m_proof.push_back(c); m_status.push_back(st); @@ -245,15 +243,12 @@ namespace sat { 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; - } - else if (value(l1) == l_false) { - assign_propagate(l2); - } - else if (value(l2) == l_false) { - assign_propagate(l1); - } + if (value(l1) == l_false && value(l2) == l_false) + m_inconsistent = true; + else if (value(l1) == l_false) + assign_propagate(l2); + else if (value(l2) == l_false) + assign_propagate(l1); } } @@ -403,16 +398,14 @@ namespace sat { if (n == 0) return false; unsigned num_units = m_units.size(); - for (unsigned i = 0; !m_inconsistent && i < n; ++i) { + for (unsigned i = 0; !m_inconsistent && i < n; ++i) assign_propagate(~c[i]); - } - if (!m_inconsistent) { - DEBUG_CODE(validate_propagation();); - } + + DEBUG_CODE(if (!m_inconsistent) validate_propagation();); DEBUG_CODE( - for (literal u : m_units) { + for (literal u : m_units) SASSERT(m_assignment[u.var()] != l_undef); - }); + ); #if 0 if (!m_inconsistent) { @@ -465,9 +458,9 @@ namespace sat { } #endif - for (unsigned i = num_units; i < m_units.size(); ++i) { + for (unsigned i = num_units; i < m_units.size(); ++i) m_assignment[m_units[i].var()] = l_undef; - } + m_units.shrink(num_units); bool ok = m_inconsistent; m_inconsistent = false; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index d923014c1..3c4569907 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1304,7 +1304,8 @@ namespace sat { flet _searching(m_searching, true); m_clone = nullptr; if (m_mc.empty() && gparams::get_ref().get_bool("model_validate", false)) { - m_clone = alloc(solver, m_params, m_rlimit); + + m_clone = alloc(solver, m_no_drat_params, m_rlimit); m_clone->copy(*this); m_clone->set_extension(nullptr); } diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 10e5bd06d..a5d83f273 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -82,6 +82,10 @@ namespace sat { void reset(); void collect_statistics(statistics & st) const; }; + + struct no_drat_params : public params_ref { + no_drat_params() { set_sym("drat.file", symbol()); } + }; class solver : public solver_core { public: @@ -183,6 +187,7 @@ namespace sat { scoped_limit_trail m_vars_lim; stopwatch m_stopwatch; params_ref m_params; + no_drat_params m_no_drat_params; scoped_ptr m_clone; // for debugging purposes literal_vector m_assumptions; // additional assumptions during check literal_set m_assumption_set; // set of enabled assumptions diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp index 1e2068707..e16b09ed1 100644 --- a/src/sat/smt/sat_dual_solver.cpp +++ b/src/sat/smt/sat_dual_solver.cpp @@ -18,10 +18,6 @@ Author: namespace sat { - dual_solver::no_drat_params::no_drat_params() { - set_sym("drat.file", symbol()); - } - dual_solver::dual_solver(reslimit& l): m_solver(m_params, l) { diff --git a/src/sat/smt/sat_dual_solver.h b/src/sat/smt/sat_dual_solver.h index 9c9b2568e..d0465ac32 100644 --- a/src/sat/smt/sat_dual_solver.h +++ b/src/sat/smt/sat_dual_solver.h @@ -23,9 +23,6 @@ Author: namespace sat { class dual_solver { - struct no_drat_params : public params_ref { - no_drat_params(); - }; no_drat_params m_params; solver m_solver; lim_svector m_units, m_roots;