mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

n/a

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-08-14 14:12:14 +02:00
parent cd838e5cf4
commit 94d83b7be9
2 changed files with 81 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

104
src/sat/sat_bceq.cpp
View file

@ -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<clause>& 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<clause*>& 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<bool> 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<clause*> clauses(m_L), new_clauses;
literal_vector blits(m_L_blits), new_blits;
svector<clause*>& 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;
}

19
src/sat/sat_bceq.h
View file

@ -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> clause_use_list;
class use_list {
vector<ptr_vector<clause> > 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<clause>& get(literal lit);
};
typedef std::pair<literal, literal> bin_clause;
typedef svector<bin_clause> bin_clauses;
solver & m_solver;
@ -49,13 +57,14 @@ namespace sat {
svector<bool> m_marked;
svector<bool> 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<clause*>& clauses);
void pure_decompose(ptr_vector<clause>& uses, svector<clause*>& clauses);
void post_decompose();
literal find_blocked(clause const& cls);
bool bce(clause& cls);