From 94d83b7be97683f90de092760b3690a1b1457898 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 14 Aug 2015 14:12:14 +0200 Subject: [PATCH] n/a Signed-off-by: Nikolaj Bjorner --- src/sat/sat_bceq.cpp | 104 ++++++++++++++++++++++++++++--------------- src/sat/sat_bceq.h | 19 +++++--- 2 files changed, 81 insertions(+), 42 deletions(-) diff --git a/src/sat/sat_bceq.cpp b/src/sat/sat_bceq.cpp index 48145010f..179749dac 100644 --- a/src/sat/sat_bceq.cpp +++ b/src/sat/sat_bceq.cpp @@ -26,6 +26,29 @@ Revision History: namespace sat { + void bceq::use_list::init(unsigned num_vars) { + m_clauses.reset(); + m_clauses.resize(2*num_vars); + } + + void bceq::use_list::insert(clause& c) { + unsigned sz = c.size(); + for (unsigned i = 0; i < sz; i++) { + m_clauses[c[i].index()].push_back(&c); + } + } + + void bceq::use_list::erase(clause& c) { + unsigned sz = c.size(); + for (unsigned i = 0; i < sz; i++) { + m_clauses[c[i].index()].erase(&c); + } + } + + ptr_vector& bceq::use_list::get(literal lit) { + return m_clauses[lit.index()]; + } + bceq::bceq(solver & s): m_solver(s) { } @@ -45,7 +68,7 @@ namespace sat { m_R.reset(); m_L_blits.reset(); m_R_blits.reset(); - m_bce_use_list.finalize(); + m_bce_use_list.reset(); clause * const* it = m_solver.begin_clauses(); clause * const* end = m_solver.end_clauses(); for (; it != end; ++it) { @@ -120,14 +143,13 @@ namespace sat { } void bceq::pure_decompose(clause_use_list& uses, svector& clauses) { - clause_use_list::iterator it = uses.mk_iterator(); - while (!it.at_end()) { - clause& cls = it.curr(); + unsigned sz = uses.size(); + for (unsigned i = 0; i < sz; ++i) { + clause& cls = *uses[i]; if (!cls.was_removed() && m_clauses[cls.id()]) { clauses.push_back(&cls); m_clauses[cls.id()] = 0; } - it.next(); } } @@ -177,50 +199,59 @@ namespace sat { m_use_list = save; } + + // Note: replay blocked clause elimination: + // Suppose C u { c1 } is blocked. + // annotate each clause by blocking literal. + // for new clause c2, check if C u { c2 } is blocked. + // For each c in C record which literal it is blocked. + // (Order the clauses in C by block ordering) + // l | c is blocked, + // -> c2 contains ~l => check if c c2 is blocked + // bool bceq::bce(clause& cls0) { IF_VERBOSE(1, verbose_stream() << "bce " << m_L.size() << " " << m_R.size() << " " << cls0 << "\n";); - svector live_clauses; + unsigned_vector& live_clauses = m_live_clauses; + live_clauses.reset(); m_use_list = &m_bce_use_list; m_bce_use_list.insert(cls0); - svector clauses(m_L), new_clauses; - literal_vector blits(m_L_blits), new_blits; + svector& clauses = m_L; + literal_vector& blits = m_L_blits; clauses.push_back(&cls0); blits.push_back(null_literal); bool removed = false; m_removed.reset(); - do { + for (unsigned i = 0; i < clauses.size(); ++i) { + clause& cls1 = *clauses[i]; + literal lit = find_blocked(cls1); + if (lit == null_literal) { + live_clauses.push_back(i); + } + else { + m_removed.setx(cls1.id(), true, false); + removed = true; + } + } + while (removed) { removed = false; - for (unsigned i = 0; i < clauses.size(); ++i) { - clause& cls1 = *clauses[i]; + //std::cout << live_clauses.size() << " "; + for (unsigned i = 0; i < live_clauses.size(); ++i) { + clause& cls1 = *clauses[live_clauses[i]]; literal lit = find_blocked(cls1); - if (lit == null_literal) { - m_bce_use_list.erase(cls1); - } - else { - IF_VERBOSE(2, verbose_stream() << "; remove " << cls1 << "\n";); + if (lit != null_literal) { m_removed.setx(cls1.id(), true, false); - new_clauses.push_back(&cls1); - new_blits.push_back(lit); removed = true; - clauses[i] = clauses.back(); - blits[i] = blits.back(); - clauses.pop_back(); - blits.pop_back(); + live_clauses[i] = live_clauses.back(); + live_clauses.pop_back(); --i; } } } - while (removed); - if (clauses.empty()) { - m_L.reset(); - m_L_blits.reset(); - new_clauses.reverse(); - new_blits.reverse(); - m_L.append(new_clauses); - m_L_blits.append(new_blits); - } - IF_VERBOSE(1, if (!clauses.empty()) verbose_stream() << "; clauses left after BCE: " << clauses.size() << "\n";); - return clauses.empty(); + //std::cout << "\n"; + m_bce_use_list.erase(cls0); + clauses.pop_back(); + blits.pop_back(); + return live_clauses.empty(); } literal bceq::find_blocked(clause const& cls) { @@ -247,9 +278,9 @@ namespace sat { bool bceq::is_blocked(literal lit) const { clause_use_list& uses = m_use_list->get(~lit); - clause_use_list::iterator it = uses.mk_iterator(); - while (!it.at_end()) { - clause const& cls = it.curr(); + unsigned sz = uses.size(); + for (unsigned i = 0; i < sz; ++i) { + clause const& cls = *uses[i]; unsigned sz = cls.size(); bool is_axiom = m_removed.get(cls.id(), false); for (unsigned i = 0; !is_axiom && i < sz; ++i) { @@ -260,7 +291,6 @@ namespace sat { if (!is_axiom) { return false; } - it.next(); } return true; } diff --git a/src/sat/sat_bceq.h b/src/sat/sat_bceq.h index cd18ee456..c9d01e78b 100644 --- a/src/sat/sat_bceq.h +++ b/src/sat/sat_bceq.h @@ -20,16 +20,24 @@ Revision History: #define SAT_BCEQ_H_ #include"sat_types.h" -#include "union_find.h" -#include "sat_simplifier.h" +#include"union_find.h" namespace sat { class solver; - class use_list; - class clause_use_list; class bceq { + typedef ptr_vector clause_use_list; + class use_list { + vector > m_clauses; + public: + use_list() {} + void init(unsigned num_vars); + void reset() { m_clauses.reset(); } + void erase(clause& c); + void insert(clause& c); + ptr_vector& get(literal lit); + }; typedef std::pair bin_clause; typedef svector bin_clauses; solver & m_solver; @@ -49,13 +57,14 @@ namespace sat { svector m_marked; svector m_removed; // set of clauses removed (not considered in clause set during BCE) union_find_default_ctx m_union_find_ctx; + unsigned_vector m_live_clauses; void init(); void register_clause(clause* cls); void unregister_clause(clause* cls); void pure_decompose(); void pure_decompose(literal lit); - void pure_decompose(clause_use_list& uses, svector& clauses); + void pure_decompose(ptr_vector& uses, svector& clauses); void post_decompose(); literal find_blocked(clause const& cls); bool bce(clause& cls);