From bf92fa4882aeea840cfed08db4d3ea13d0e14196 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 16 Dec 2022 15:21:32 +0100 Subject: [PATCH] clause_iterator --- src/math/polysat/constraint_manager.h | 62 ++++++++++++++++++++-- src/math/polysat/solver.cpp | 75 ++++++++++++--------------- src/math/polysat/solver.h | 2 +- 3 files changed, 93 insertions(+), 46 deletions(-) diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h index 2ef2a3ca1..ae24faeb5 100644 --- a/src/math/polysat/constraint_manager.h +++ b/src/math/polysat/constraint_manager.h @@ -126,9 +126,65 @@ namespace polysat { constraint* const* begin() const { return m_constraints.data(); } constraint* const* end() const { return m_constraints.data() + m_constraints.size(); } - using clause_iterator = decltype(m_clauses)::const_iterator; - clause_iterator clauses_begin() const { return m_clauses.begin(); } - clause_iterator clauses_end() const { return m_clauses.end(); } + class clause_iterator { + friend class constraint_manager; + using storage_t = decltype(constraint_manager::m_clauses); + + using outer_iterator = storage_t::const_iterator; + outer_iterator outer_it; + outer_iterator outer_end; + + using inner_iterator = storage_t::data_t::const_iterator; + inner_iterator inner_it; + inner_iterator inner_end; + + clause_iterator(storage_t const& cls, bool begin) { + if (begin) { + outer_it = cls.begin(); + outer_end = cls.end(); + } + else { + outer_it = cls.end(); + outer_end = cls.end(); + } + begin_inner(); + } + + void begin_inner() { + if (outer_it == outer_end) { + inner_it = nullptr; + inner_end = nullptr; + } + else { + inner_it = outer_it->begin(); + inner_end = outer_it->end(); + } + } + + public: + clause const& operator*() const { + return *inner_it->get(); + } + + clause_iterator& operator++() { + ++inner_it; + while (inner_it == inner_end && outer_it != outer_end) { + ++outer_it; + begin_inner(); + } + return *this; + } + + bool operator==(clause_iterator const& other) const { + return outer_it == other.outer_it && inner_it == other.inner_it; + } + + bool operator!=(clause_iterator const& other) const { + return !operator==(other); + } + }; + clause_iterator clauses_begin() const { return clause_iterator(m_clauses, true); } + clause_iterator clauses_end() const { return clause_iterator(m_clauses, false); } class clauses_t { constraint_manager const* m_cm; diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 66c9126d5..309e5d6ae 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -587,15 +587,13 @@ namespace polysat { // Simple hack to try deciding the boolean skeleton first if (!can_bdecide()) { // enqueue all not-yet-true clauses - for (auto const& cls : m_constraints.clauses()) { - for (auto const& cl : cls) { - bool is_true = any_of(*cl, [&](sat::literal lit) { return m_bvars.is_true(lit); }); - if (is_true) - continue; - size_t undefs = count_if(*cl, [&](sat::literal lit) { return !m_bvars.is_assigned(lit); }); - if (undefs >= 2) - m_lemmas.push_back(cl.get()); - } + for (clause const& cl : m_constraints.clauses()) { + bool is_true = any_of(cl, [&](sat::literal lit) { return m_bvars.is_true(lit); }); + if (is_true) + continue; + size_t undefs = count_if(cl, [&](sat::literal lit) { return !m_bvars.is_assigned(lit); }); + if (undefs >= 2) + m_lemmas.push_back(&cl); } } #endif @@ -606,7 +604,7 @@ namespace polysat { } void solver::bdecide() { - clause& lemma = *m_lemmas[m_lemmas_qhead++]; + clause const& lemma = *m_lemmas[m_lemmas_qhead++]; on_scope_exit update_trail = [this]() { // must be done after push_level, but also if we return early. m_trail.push_back(trail_instr_t::lemma_qhead_i); @@ -1305,12 +1303,10 @@ namespace polysat { for (auto c : m_constraints) out << "\t" << c->bvar2string() << ": " << *c << "\n"; out << "Clauses:\n"; - for (auto const& cls : m_constraints.clauses()) { - for (auto const& cl : cls) { - out << "\t" << *cl << "\n"; - for (auto lit : *cl) - out << "\t\t" << lit << ": " << lit2cnstr(lit) << "\n"; - } + for (clause const& cl : m_constraints.clauses()) { + out << "\t" << cl << "\n"; + for (sat::literal lit : cl) + out << "\t\t" << lit << ": " << lit2cnstr(lit) << "\n"; } return out; } @@ -1426,23 +1422,20 @@ namespace polysat { // Check for missed boolean propagations: // - no clause should have exactly one unassigned literal, unless it is already true. // - no clause should be false - for (auto const& cls : m_constraints.clauses()) { - for (auto const& clref : cls) { - clause const& cl = *clref; - bool const is_true = any_of(cl, [&](auto lit) { return m_bvars.is_true(lit); }); - if (is_true) - continue; - size_t const undefs = count_if(cl, [&](auto lit) { return !m_bvars.is_assigned(lit); }); - if (undefs == 1) { - LOG("Missed boolean propagation of clause: " << cl); - for (sat::literal lit : cl) { - LOG(" " << lit_pp(*this, lit)); - } + for (clause const& cl : m_constraints.clauses()) { + bool const is_true = any_of(cl, [&](auto lit) { return m_bvars.is_true(lit); }); + if (is_true) + continue; + size_t const undefs = count_if(cl, [&](auto lit) { return !m_bvars.is_assigned(lit); }); + if (undefs == 1) { + LOG("Missed boolean propagation of clause: " << cl); + for (sat::literal lit : cl) { + LOG(" " << lit_pp(*this, lit)); } - SASSERT(undefs != 1); - bool const is_false = all_of(cl, [&](auto lit) { return m_bvars.is_false(lit); }); - SASSERT(!is_false); } + SASSERT(undefs != 1); + bool const is_false = all_of(cl, [&](auto lit) { return m_bvars.is_false(lit); }); + SASSERT(!is_false); } return true; } @@ -1483,19 +1476,17 @@ namespace polysat { all_ok = all_ok && ok; } } - for (auto clauses : m_constraints.clauses()) { - for (auto cl : clauses) { - bool clause_ok = false; - for (sat::literal lit : *cl) { - bool ok = lit2cnstr(lit).is_currently_true(*this); - if (ok) { - clause_ok = true; - break; - } + for (clause const& cl : m_constraints.clauses()) { + bool clause_ok = false; + for (sat::literal lit : cl) { + bool ok = lit2cnstr(lit).is_currently_true(*this); + if (ok) { + clause_ok = true; + break; } - LOG((clause_ok ? "PASS" : "FAIL") << ": " << show_deref(cl) << (cl->is_redundant() ? " (redundant)" : "")); - all_ok = all_ok && clause_ok; } + LOG((clause_ok ? "PASS" : "FAIL") << ": " << cl << (cl.is_redundant() ? " (redundant)" : "")); + all_ok = all_ok && clause_ok; } if (all_ok) LOG("All good!"); return all_ok; diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index cacb19cb5..05393a9f5 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -184,7 +184,7 @@ namespace polysat { constraints m_pwatch_trail; #endif - ptr_vector m_lemmas; ///< the non-asserting lemmas + ptr_vector m_lemmas; ///< the non-asserting lemmas unsigned m_lemmas_qhead = 0; unsigned_vector m_base_levels; // External clients can push/pop scope.