mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 19:52:29 +00:00
compress elimination stack representation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
e0e7836c12
commit
8811d78415
3 changed files with 108 additions and 54 deletions
|
|
@ -38,16 +38,15 @@ namespace sat {
|
|||
return *this;
|
||||
}
|
||||
|
||||
void model_converter::process_stack(model & m, literal_vector const& stack) const {
|
||||
void model_converter::process_stack(model & m, literal_vector const& c, elim_stackv const& stack) const {
|
||||
SASSERT(!stack.empty());
|
||||
unsigned sz = stack.size();
|
||||
SASSERT(stack[sz - 1] == null_literal);
|
||||
for (unsigned i = sz - 1; i-- > 0; ) {
|
||||
literal lit = stack[i]; // this is the literal that is pivoted on. It is repeated
|
||||
for (unsigned i = sz; i-- > 0; ) {
|
||||
unsigned csz = stack[i].first;
|
||||
literal lit = stack[i].second;
|
||||
bool sat = false;
|
||||
for (; i > 0 && stack[--i] != null_literal;) {
|
||||
if (sat) continue;
|
||||
sat = value_at(stack[i], m) == l_true;
|
||||
for (unsigned j = 0; !sat && j < csz; ++j) {
|
||||
sat = value_at(c[j], m) == l_true;
|
||||
}
|
||||
if (!sat) {
|
||||
m[lit.var()] = lit.sign() ? l_false : l_true;
|
||||
|
|
@ -66,6 +65,7 @@ namespace sat {
|
|||
bool sat = false;
|
||||
bool var_sign = false;
|
||||
unsigned index = 0;
|
||||
literal_vector clause;
|
||||
for (literal l : it->m_clauses) {
|
||||
if (l == null_literal) {
|
||||
// end of clause
|
||||
|
|
@ -74,13 +74,15 @@ namespace sat {
|
|||
}
|
||||
elim_stack* s = it->m_elim_stack[index];
|
||||
if (s) {
|
||||
process_stack(m, s->stack());
|
||||
process_stack(m, clause, s->stack());
|
||||
}
|
||||
sat = false;
|
||||
++index;
|
||||
clause.reset();
|
||||
continue;
|
||||
}
|
||||
|
||||
clause.push_back(l);
|
||||
if (sat)
|
||||
continue;
|
||||
bool sign = l.sign();
|
||||
|
|
@ -190,13 +192,13 @@ namespace sat {
|
|||
// TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";);
|
||||
}
|
||||
|
||||
void model_converter::insert(entry & e, literal_vector const& c, literal_vector const& elims) {
|
||||
void model_converter::insert(entry & e, literal_vector const& c, elim_stackv const& elims) {
|
||||
SASSERT(c.contains(literal(e.var(), false)) || c.contains(literal(e.var(), true)));
|
||||
SASSERT(m_entries.begin() <= &e);
|
||||
SASSERT(&e < m_entries.end());
|
||||
for (literal l : c) e.m_clauses.push_back(l);
|
||||
e.m_clauses.push_back(null_literal);
|
||||
e.m_elim_stack.push_back(alloc(elim_stack, elims));
|
||||
e.m_elim_stack.push_back(elims.empty() ? nullptr : alloc(elim_stack, elims));
|
||||
TRACE("sat_mc_bug", tout << "adding: " << c << "\n";);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -39,18 +39,20 @@ namespace sat {
|
|||
class model_converter {
|
||||
|
||||
public:
|
||||
typedef svector<std::pair<unsigned, literal>> elim_stackv;
|
||||
|
||||
class elim_stack {
|
||||
unsigned m_refcount;
|
||||
literal_vector m_stack;
|
||||
elim_stackv m_stack;
|
||||
public:
|
||||
elim_stack(literal_vector const& stack):
|
||||
elim_stack(elim_stackv const& stack):
|
||||
m_refcount(0),
|
||||
m_stack(stack) {
|
||||
}
|
||||
~elim_stack() { }
|
||||
void inc_ref() { ++m_refcount; }
|
||||
void dec_ref() { if (0 == --m_refcount) dealloc(this); }
|
||||
literal_vector const& stack() const { return m_stack; }
|
||||
elim_stackv const& stack() const { return m_stack; }
|
||||
};
|
||||
|
||||
enum kind { ELIM_VAR = 0, BLOCK_LIT };
|
||||
|
|
@ -74,7 +76,7 @@ namespace sat {
|
|||
private:
|
||||
vector<entry> m_entries;
|
||||
|
||||
void process_stack(model & m, literal_vector const& stack) const;
|
||||
void process_stack(model & m, literal_vector const& clause, elim_stackv const& stack) const;
|
||||
|
||||
public:
|
||||
model_converter();
|
||||
|
|
@ -86,7 +88,7 @@ namespace sat {
|
|||
void insert(entry & e, clause const & c);
|
||||
void insert(entry & e, literal l1, literal l2);
|
||||
void insert(entry & e, clause_wrapper const & c);
|
||||
void insert(entry & c, literal_vector const& covered_clause, literal_vector const& elim_stack);
|
||||
void insert(entry & c, literal_vector const& covered_clause, elim_stackv const& elim_stack);
|
||||
|
||||
bool empty() const { return m_entries.empty(); }
|
||||
|
||||
|
|
|
|||
|
|
@ -965,6 +965,7 @@ namespace sat {
|
|||
literal l = m_queue.next();
|
||||
process(l);
|
||||
}
|
||||
cce();
|
||||
}
|
||||
|
||||
//
|
||||
|
|
@ -1027,55 +1028,106 @@ namespace sat {
|
|||
|
||||
literal_vector m_covered_clause;
|
||||
literal_vector m_intersection;
|
||||
literal_vector m_elim_stack;
|
||||
sat::model_converter::elim_stackv m_elim_stack;
|
||||
unsigned m_ala_qhead;
|
||||
|
||||
bool cla(literal lit) {
|
||||
/*
|
||||
* C \/ l l \/ lit
|
||||
* -------------------
|
||||
* C \/ l \/ ~lit
|
||||
*/
|
||||
void add_ala() {
|
||||
for (; m_ala_qhead < m_covered_clause.size(); ++m_ala_qhead) {
|
||||
literal l = m_covered_clause[m_ala_qhead];
|
||||
for (watched & w : s.get_wlist(~l)) {
|
||||
if (w.is_binary_clause()) {
|
||||
literal lit = w.get_literal();
|
||||
if (!s.is_marked(lit) && !s.is_marked(~lit)) {
|
||||
//std::cout << "ALA " << ~lit << "\n";
|
||||
m_covered_clause.push_back(~lit);
|
||||
s.mark_visited(~lit);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool add_cla(literal& blocked) {
|
||||
for (unsigned i = 0; i < m_covered_clause.size(); ++i) {
|
||||
m_intersection.reset();
|
||||
if (ri(m_covered_clause[i], m_intersection)) {
|
||||
blocked = m_covered_clause[i];
|
||||
return true;
|
||||
}
|
||||
for (literal l : m_intersection) {
|
||||
if (!s.is_marked(l)) {
|
||||
s.mark_visited(l);
|
||||
m_covered_clause.push_back(l);
|
||||
}
|
||||
}
|
||||
if (!m_intersection.empty()) {
|
||||
m_elim_stack.push_back(std::make_pair(m_covered_clause.size(), m_covered_clause[i]));
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool cla(literal& blocked) {
|
||||
bool is_tautology = false;
|
||||
for (literal l : m_covered_clause) s.mark_visited(l);
|
||||
unsigned num_iterations = 0, sz;
|
||||
m_elim_stack.reset();
|
||||
m_ala_qhead = 0;
|
||||
do {
|
||||
++num_iterations;
|
||||
sz = m_covered_clause.size();
|
||||
for (unsigned i = 0; i < m_covered_clause.size(); ++i) {
|
||||
m_intersection.reset();
|
||||
if (ri(m_covered_clause[i], m_intersection) && m_covered_clause[i] == lit) {
|
||||
is_tautology = true;
|
||||
break;
|
||||
}
|
||||
for (literal l : m_intersection) {
|
||||
if (!s.is_marked(l)) {
|
||||
s.mark_visited(l);
|
||||
m_covered_clause.push_back(l);
|
||||
}
|
||||
}
|
||||
if (!m_intersection.empty()) {
|
||||
m_elim_stack.append(m_covered_clause); // the current clause
|
||||
m_elim_stack.push_back(m_covered_clause[i]); // the pivot literal
|
||||
m_elim_stack.push_back(null_literal); // null demarcation
|
||||
}
|
||||
do {
|
||||
++num_iterations;
|
||||
sz = m_covered_clause.size();
|
||||
is_tautology = add_cla(blocked);
|
||||
}
|
||||
while (m_covered_clause.size() > sz && !is_tautology);
|
||||
break;
|
||||
//if (is_tautology) break;
|
||||
//sz = m_covered_clause.size();
|
||||
// unsound? add_ala();
|
||||
}
|
||||
while (m_covered_clause.size() > sz && !is_tautology);
|
||||
while (m_covered_clause.size() > sz);
|
||||
for (literal l : m_covered_clause) s.unmark_visited(l);
|
||||
if (is_tautology) std::cout << "taut: " << num_iterations << "\n";
|
||||
// if (is_tautology) std::cout << "taut: " << num_iterations << " " << m_covered_clause.size() << " " << m_elim_stack.size() << "\n";
|
||||
return is_tautology;
|
||||
}
|
||||
|
||||
// perform covered clause elimination.
|
||||
// first extract the covered literal addition (CLA).
|
||||
// then check whether the CLA is blocked.
|
||||
bool cce(clause& c, literal lit) {
|
||||
bool cce(clause& c, literal& blocked) {
|
||||
m_covered_clause.reset();
|
||||
for (literal l : c) m_covered_clause.push_back(l);
|
||||
return cla(lit);
|
||||
return cla(blocked);
|
||||
}
|
||||
|
||||
bool cce(literal lit, literal l2) {
|
||||
bool cce(literal lit, literal l2, literal& blocked) {
|
||||
m_covered_clause.reset();
|
||||
m_covered_clause.push_back(lit);
|
||||
m_covered_clause.push_back(l2);
|
||||
return cla(lit);
|
||||
return cla(blocked);
|
||||
}
|
||||
|
||||
void cce() {
|
||||
m_to_remove.reset();
|
||||
literal blocked;
|
||||
for (clause* cp : s.s.m_clauses) {
|
||||
clause& c = *cp;
|
||||
if (c.was_removed()) continue;
|
||||
if (cce(c, blocked)) {
|
||||
model_converter::entry * new_entry = 0;
|
||||
block_covered_clause(c, blocked, new_entry);
|
||||
s.m_num_covered_clauses++;
|
||||
}
|
||||
}
|
||||
for (clause* c : m_to_remove) {
|
||||
s.remove_clause(*c);
|
||||
}
|
||||
m_to_remove.reset();
|
||||
}
|
||||
|
||||
void process(literal l) {
|
||||
|
|
@ -1085,6 +1137,7 @@ namespace sat {
|
|||
return;
|
||||
}
|
||||
|
||||
literal blocked = null_literal;
|
||||
m_to_remove.reset();
|
||||
{
|
||||
clause_use_list & occs = s.m_use_list.get(l);
|
||||
|
|
@ -1095,14 +1148,10 @@ namespace sat {
|
|||
SASSERT(c.contains(l));
|
||||
s.mark_all_but(c, l);
|
||||
if (all_tautology(l)) {
|
||||
s.unmark_all(c);
|
||||
block_clause(c, l, new_entry);
|
||||
s.m_num_blocked_clauses++;
|
||||
}
|
||||
else if (cce(c, l)) {
|
||||
block_covered_clause(c, l, new_entry);
|
||||
s.m_num_covered_clauses++;
|
||||
}
|
||||
s.unmark_all(c);
|
||||
it.next();
|
||||
}
|
||||
}
|
||||
|
|
@ -1127,8 +1176,9 @@ namespace sat {
|
|||
block_binary(it, l, new_entry);
|
||||
s.m_num_blocked_clauses++;
|
||||
}
|
||||
else if (cce(l, l2)) {
|
||||
block_covered_binary(it, l, new_entry);
|
||||
else if (cce(l, l2, blocked)) {
|
||||
model_converter::entry * blocked_entry = 0;
|
||||
block_covered_binary(it, l, blocked, blocked_entry);
|
||||
s.m_num_covered_clauses++;
|
||||
}
|
||||
else {
|
||||
|
|
@ -1163,9 +1213,9 @@ namespace sat {
|
|||
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
|
||||
}
|
||||
|
||||
void prepare_block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
|
||||
void prepare_block_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) {
|
||||
if (new_entry == 0)
|
||||
new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
|
||||
new_entry = &(mc.mk(model_converter::BLOCK_LIT, blocked.var()));
|
||||
literal l2 = it->get_literal();
|
||||
TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";);
|
||||
s.remove_bin_clause_half(l2, l, it->is_learned());
|
||||
|
|
@ -1173,12 +1223,12 @@ namespace sat {
|
|||
}
|
||||
|
||||
void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
|
||||
prepare_block_binary(it, l, new_entry);
|
||||
prepare_block_binary(it, l, l, new_entry);
|
||||
mc.insert(*new_entry, l, it->get_literal());
|
||||
}
|
||||
|
||||
void block_covered_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
|
||||
prepare_block_binary(it, l, new_entry);
|
||||
void block_covered_binary(watch_list::iterator it, literal l, literal blocked, model_converter::entry *& new_entry) {
|
||||
prepare_block_binary(it, l, blocked, new_entry);
|
||||
mc.insert(*new_entry, m_covered_clause, m_elim_stack);
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue