mirror of
https://github.com/Z3Prover/z3
synced 2025-08-19 09:40:20 +00:00
add cce
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
46fa245324
commit
9f9ae4427d
10 changed files with 259 additions and 139 deletions
|
|
@ -330,19 +330,15 @@ namespace sat {
|
|||
cs.set_end(it2);
|
||||
}
|
||||
|
||||
void simplifier::mark_all_but(clause const & c, literal l) {
|
||||
unsigned sz = c.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
if (c[i] == l)
|
||||
continue;
|
||||
mark_visited(c[i]);
|
||||
}
|
||||
void simplifier::mark_all_but(clause const & c, literal l1) {
|
||||
for (literal l2 : c)
|
||||
if (l2 != l1)
|
||||
mark_visited(l2);
|
||||
}
|
||||
|
||||
void simplifier::unmark_all(clause const & c) {
|
||||
unsigned sz = c.size();
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
unmark_visited(c[i]);
|
||||
for (literal l : c)
|
||||
unmark_visited(l);
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -952,7 +948,7 @@ namespace sat {
|
|||
}
|
||||
|
||||
bool process_var(bool_var v) {
|
||||
return !s.s.is_assumption(v) && !s.was_eliminated(v);
|
||||
return !s.s.is_assumption(v) && !s.was_eliminated(v) && !s.is_external(v);
|
||||
}
|
||||
|
||||
void operator()(unsigned num_vars) {
|
||||
|
|
@ -971,6 +967,108 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
//
|
||||
// Resolve intersection
|
||||
// Find literals that are in the intersection of all resolvents with l.
|
||||
//
|
||||
void ri(literal l, literal_vector& inter) {
|
||||
if (!process_var(l.var())) return;
|
||||
bool first = true;
|
||||
for (watched & w : s.get_wlist(~l)) {
|
||||
if (w.is_binary_non_learned_clause()) {
|
||||
literal lit = w.get_literal();
|
||||
if (s.is_marked(~lit)) continue;
|
||||
if (!first) {
|
||||
inter.reset();
|
||||
return;
|
||||
}
|
||||
first = false;
|
||||
inter.push_back(lit);
|
||||
}
|
||||
}
|
||||
clause_use_list & neg_occs = s.m_use_list.get(~l);
|
||||
clause_use_list::iterator it = neg_occs.mk_iterator();
|
||||
while (!it.at_end()) {
|
||||
bool tautology = false;
|
||||
clause & c = it.curr();
|
||||
for (literal lit : c) {
|
||||
if (s.is_marked(~lit)) {
|
||||
tautology = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (!tautology) {
|
||||
if (first) {
|
||||
for (literal lit : c) {
|
||||
if (lit != ~l) inter.push_back(lit);
|
||||
}
|
||||
first = false;
|
||||
}
|
||||
else {
|
||||
unsigned j = 0;
|
||||
unsigned sz = inter.size();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
literal lit1 = inter[i];
|
||||
for (literal lit2 : c) {
|
||||
if (lit1 == lit2) {
|
||||
inter[j++] = lit1;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
inter.shrink(j);
|
||||
if (j == 0) return;
|
||||
}
|
||||
}
|
||||
it.next();
|
||||
}
|
||||
}
|
||||
|
||||
// perform covered clause elimination.
|
||||
// first extract the covered literal addition (CLA).
|
||||
// then check whether the CLA is blocked.
|
||||
bool cce(clause& c, literal lit) {
|
||||
for (literal l : c) s.mark_visited(l);
|
||||
literal_vector added, lits;
|
||||
for (literal l : c) added.push_back(l);
|
||||
for (unsigned i = 0; i < added.size(); ++i) {
|
||||
ri(added[i], lits);
|
||||
for (literal l : lits) {
|
||||
if (!s.is_marked(l)) {
|
||||
s.mark_visited(l);
|
||||
added.push_back(l);
|
||||
}
|
||||
}
|
||||
lits.reset();
|
||||
}
|
||||
s.unmark_visited(lit);
|
||||
bool is_tautology = (added.size() > c.size()) && all_tautology(lit);
|
||||
for (literal l : added) s.unmark_visited(l);
|
||||
return is_tautology;
|
||||
}
|
||||
|
||||
bool cce(literal lit, literal l2) {
|
||||
literal_vector added, lits;
|
||||
s.mark_visited(lit);
|
||||
s.mark_visited(l2);
|
||||
added.push_back(lit);
|
||||
added.push_back(l2);
|
||||
for (unsigned i = 0; i < added.size(); ++i) {
|
||||
ri(added[i], lits);
|
||||
for (literal l : lits) {
|
||||
if (!s.is_marked(l)) {
|
||||
s.mark_visited(l);
|
||||
added.push_back(l);
|
||||
}
|
||||
}
|
||||
lits.reset();
|
||||
}
|
||||
s.unmark_visited(lit);
|
||||
bool is_tautology = added.size() > 2 && all_tautology(lit);
|
||||
for (literal l : added) s.unmark_visited(l);
|
||||
return is_tautology;
|
||||
}
|
||||
|
||||
void process(literal l) {
|
||||
TRACE("blocked_clause", tout << "processing: " << l << "\n";);
|
||||
model_converter::entry * new_entry = 0;
|
||||
|
|
@ -988,21 +1086,14 @@ namespace sat {
|
|||
SASSERT(c.contains(l));
|
||||
s.mark_all_but(c, l);
|
||||
if (all_tautology(l)) {
|
||||
TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
|
||||
if (new_entry == 0)
|
||||
new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
|
||||
m_to_remove.push_back(&c);
|
||||
block_clause(c, l, new_entry);
|
||||
s.m_num_blocked_clauses++;
|
||||
mc.insert(*new_entry, c);
|
||||
unsigned sz = c.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
literal lit = c[i];
|
||||
if (lit != l && process_var(lit.var())) {
|
||||
m_queue.decreased(~lit);
|
||||
}
|
||||
}
|
||||
s.unmark_all(c);
|
||||
}
|
||||
else if (cce(c, l)) {
|
||||
block_clause(c, l, new_entry);
|
||||
s.m_num_covered_clauses++;
|
||||
}
|
||||
s.unmark_all(c);
|
||||
it.next();
|
||||
}
|
||||
}
|
||||
|
|
@ -1024,13 +1115,12 @@ namespace sat {
|
|||
literal l2 = it->get_literal();
|
||||
s.mark_visited(l2);
|
||||
if (all_tautology(l)) {
|
||||
if (new_entry == 0)
|
||||
new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
|
||||
TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";);
|
||||
s.remove_bin_clause_half(l2, l, it->is_learned());
|
||||
block_binary(it, l, new_entry);
|
||||
s.m_num_blocked_clauses++;
|
||||
m_queue.decreased(~l2);
|
||||
mc.insert(*new_entry, l, l2);
|
||||
}
|
||||
else if (cce(l, l2)) {
|
||||
block_binary(it, l, new_entry);
|
||||
s.m_num_covered_clauses++;
|
||||
}
|
||||
else {
|
||||
*it2 = *it;
|
||||
|
|
@ -1042,6 +1132,29 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
void block_clause(clause& c, literal l, model_converter::entry *& new_entry) {
|
||||
TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
|
||||
if (new_entry == 0)
|
||||
new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
|
||||
m_to_remove.push_back(&c);
|
||||
mc.insert(*new_entry, c);
|
||||
for (literal lit : c) {
|
||||
if (lit != l && process_var(lit.var())) {
|
||||
m_queue.decreased(~lit);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
|
||||
if (new_entry == 0)
|
||||
new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
|
||||
TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";);
|
||||
literal l2 = it->get_literal();
|
||||
s.remove_bin_clause_half(l2, l, it->is_learned());
|
||||
m_queue.decreased(~l2);
|
||||
mc.insert(*new_entry, l, l2);
|
||||
}
|
||||
|
||||
bool all_tautology(literal l) {
|
||||
watch_list & wlist = s.get_wlist(l);
|
||||
m_counter -= wlist.size();
|
||||
|
|
@ -1083,9 +1196,11 @@ namespace sat {
|
|||
simplifier & m_simplifier;
|
||||
stopwatch m_watch;
|
||||
unsigned m_num_blocked_clauses;
|
||||
unsigned m_num_covered_clauses;
|
||||
blocked_cls_report(simplifier & s):
|
||||
m_simplifier(s),
|
||||
m_num_blocked_clauses(s.m_num_blocked_clauses) {
|
||||
m_num_blocked_clauses(s.m_num_blocked_clauses),
|
||||
m_num_covered_clauses(s.m_num_covered_clauses) {
|
||||
m_watch.start();
|
||||
}
|
||||
|
||||
|
|
@ -1094,6 +1209,8 @@ namespace sat {
|
|||
IF_VERBOSE(SAT_VB_LVL,
|
||||
verbose_stream() << " (sat-blocked-clauses :elim-blocked-clauses "
|
||||
<< (m_simplifier.m_num_blocked_clauses - m_num_blocked_clauses)
|
||||
<< " :elim-covered-clauses "
|
||||
<< (m_simplifier.m_num_covered_clauses - m_num_covered_clauses)
|
||||
<< mem_stat()
|
||||
<< " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << ")\n";);
|
||||
}
|
||||
|
|
@ -1379,6 +1496,7 @@ namespace sat {
|
|||
m_elim_counter -= num_pos * num_neg + before_lits;
|
||||
|
||||
// eliminate variable
|
||||
++s.m_stats.m_elim_var_res;
|
||||
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
|
||||
save_clauses(mc_entry, m_pos_cls);
|
||||
save_clauses(mc_entry, m_neg_cls);
|
||||
|
|
@ -1463,7 +1581,6 @@ namespace sat {
|
|||
order_vars_for_elim(vars);
|
||||
sat::elim_vars elim_bdd(*this);
|
||||
|
||||
std::cout << "vars to elim: " << vars.size() << "\n";
|
||||
for (bool_var v : vars) {
|
||||
checkpoint();
|
||||
if (m_elim_counter < 0)
|
||||
|
|
@ -1471,11 +1588,9 @@ namespace sat {
|
|||
if (try_eliminate(v)) {
|
||||
m_num_elim_vars++;
|
||||
}
|
||||
#if 1
|
||||
else if (elim_bdd(v)) {
|
||||
m_num_elim_vars++;
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
m_pos_cls.finalize();
|
||||
|
|
@ -1512,12 +1627,13 @@ namespace sat {
|
|||
st.update("subsumed", m_num_subsumed);
|
||||
st.update("subsumption resolution", m_num_sub_res);
|
||||
st.update("elim literals", m_num_elim_lits);
|
||||
st.update("elim bool vars", m_num_elim_vars);
|
||||
st.update("elim blocked clauses", m_num_blocked_clauses);
|
||||
st.update("elim covered clauses", m_num_covered_clauses);
|
||||
}
|
||||
|
||||
void simplifier::reset_statistics() {
|
||||
m_num_blocked_clauses = 0;
|
||||
m_num_covered_clauses = 0;
|
||||
m_num_subsumed = 0;
|
||||
m_num_sub_res = 0;
|
||||
m_num_elim_lits = 0;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue