mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

More failed literals

Browse source
This commit is contained in:
Miguel Neves 2017-10-13 09:15:28 -07:00
parent 56d785df94
commit 4394ce96ae
2 changed files with 69 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

95
src/sat/sat_lookahead.cpp
View file

@ -1574,19 +1574,16 @@ namespace sat {
} }
void lookahead::propagate() { void lookahead::propagate() {
while (!inconsistent() && m_qhead < m_trail.size()) { unsigned i = m_qhead;
unsigned i = m_qhead; for (; i < m_trail.size() && !inconsistent(); ++i) {
unsigned sz = m_trail.size(); literal l = m_trail[i];
for (; i < sz && !inconsistent(); ++i) { TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";);
literal l = m_trail[i]; propagate_binary(l);
TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";);
propagate_binary(l);
}
while (m_qhead < sz && !inconsistent()) {
propagate_clauses(m_trail[m_qhead++]);
}
SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size()));
} }
while (m_qhead < m_trail.size() && !inconsistent()) {
propagate_clauses(m_trail[m_qhead++]);
}
SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size()));
TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n");); TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n"););
} }
@ -1605,41 +1602,52 @@ namespace sat {
if (lit == last_changed) { if (lit == last_changed) {
break; break;
} }
if (is_fixed_at(lit, c_fixed_truth)) continue;
unsigned level = base + m_lookahead[i].m_offset;
if (m_stamp[lit.var()] >= level) {
continue;
}
if (scope_lvl() == 1) { if (scope_lvl() == 1) {
IF_VERBOSE(30, verbose_stream() << scope_lvl() << " " << lit << " binary: " << m_binary_trail.size() << " trail: " << m_trail_lim.back() << "\n";); IF_VERBOSE(30, verbose_stream() << scope_lvl() << " " << lit << " binary: " << m_binary_trail.size() << " trail: " << m_trail_lim.back() << "\n";);
} }
TRACE("sat", tout << "lookahead: " << lit << " @ " << m_lookahead[i].m_offset << "\n";); unsigned level = base + m_lookahead[i].m_offset;
reset_lookahead_reward(lit);
unsigned num_units = push_lookahead1(lit, level);
update_lookahead_reward(lit, level);
unsigned dl_lvl = level; unsigned dl_lvl = level;
num_units += do_double(lit, dl_lvl); if (is_fixed_at(lit, c_fixed_truth) || is_true_at(lit, level)) continue;
if (dl_lvl > level) { bool unsat = false;
base = dl_lvl; if (is_false_at(lit, level)) {
unsat = true;
}
else {
TRACE("sat", tout << "lookahead: " << lit << " @ " << m_lookahead[i].m_offset << "\n";);
reset_lookahead_reward(lit);
unsigned num_units = push_lookahead1(lit, level);
update_lookahead_reward(lit, level);
num_units += do_double(lit, dl_lvl);
if (dl_lvl > level) {
base = dl_lvl;
}
unsat = inconsistent();
pop_lookahead1(lit, num_units);
} }
bool unsat = inconsistent();
pop_lookahead1(lit, num_units);
if (unsat) { if (unsat) {
TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";); TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";);
lookahead_backtrack();
assign(~lit); assign(~lit);
propagate(); propagate();
change = true; change = true;
last_changed = lit; last_changed = lit;
continue;
} }
{ // if l was derived from lit and ~lit -> l, then l is a necessary assignment
// if l was derived from lit and ~lit -> l, then l is a necessary assignment literal_vector necessary_lits;
scoped_level _sl(*this, dl_lvl); for (literal l : m_binary[(~lit).index()]) {
literal_vector const& lits = m_binary[(~l).index()]; if (is_true_at(l, dl_lvl) && !is_fixed_at(l, c_fixed_truth)) {
for (literal l : lits) { necessary_lits.push_back(l);
}
}
if (!necessary_lits.empty()) {
change = true;
last_changed = lit;
lookahead_backtrack();
for (literal l : necessary_lits) {
if (inconsistent()) break; if (inconsistent()) break;
if (is_true(l) && !is_fixed_at(l, cl_fixed_truth)) { assign(l);
assign(l); propagate();
}
} }
} }
SASSERT(inconsistent() || !is_unsat()); SASSERT(inconsistent() || !is_unsat());
@ -1817,12 +1825,20 @@ namespace sat {
SASSERT(change == false); SASSERT(change == false);
break; break;
} }
if (is_fixed_at(lit, dl_truth)) continue; unsigned level = base + m_lookahead[i].m_offset;
if (base + m_lookahead.size() + m_lookahead[i].m_offset >= dl_truth) { if (level + m_lookahead.size() >= dl_truth) {
change = false; change = false;
break; break;
} }
if (push_lookahead2(lit, base + m_lookahead[i].m_offset)) { bool unsat = false;
if (is_false_at(lit, level) && !is_fixed_at(lit, dl_truth)) {
unsat = true;
}
else {
if (is_fixed_at(lit, level)) continue;
unsat = push_lookahead2(lit, level);
}
if (unsat) {
TRACE("sat", tout << "unit: " << ~lit << "\n";); TRACE("sat", tout << "unit: " << ~lit << "\n";);
++m_stats.m_double_lookahead_propagations; ++m_stats.m_double_lookahead_propagations;
SASSERT(m_level == dl_truth); SASSERT(m_level == dl_truth);
@ -1874,6 +1890,11 @@ namespace sat {
void lookahead::propagated(literal l) { void lookahead::propagated(literal l) {
assign(l); assign(l);
for (unsigned i = m_trail.size()-1; i < m_trail.size() && !inconsistent(); ++i) {
literal l = m_trail[i];
TRACE("sat", tout << "propagate " << l << " @ " << m_level << "\n";);
propagate_binary(l);
}
if (m_search_mode == lookahead_mode::lookahead1) { if (m_search_mode == lookahead_mode::lookahead1) {
m_wstack.push_back(l); m_wstack.push_back(l);
} }

18
src/sat/sat_lookahead.h
View file

@ -231,11 +231,19 @@ namespace sat {
// --------------------------------------- // ---------------------------------------
// truth values // truth values
inline bool is_fixed(literal l) const { return m_stamp[l.var()] >= m_level; }
inline bool is_fixed_at(literal l, unsigned level) const { return m_stamp[l.var()] >= level; }
inline bool is_fixed(literal l) const { return is_fixed_at(l, m_level); }
inline bool is_undef(literal l) const { return !is_fixed(l); } inline bool is_undef(literal l) const { return !is_fixed(l); }
inline bool is_undef(bool_var v) const { return m_stamp[v] < m_level; } inline bool is_undef(bool_var v) const { return m_stamp[v] < m_level; }
inline bool is_false(literal l) const { return is_fixed(l) && (bool)((m_stamp[l.var()] & 0x1) ^ l.sign()); } // even iff l.sign() inline bool is_false_at(literal l, unsigned level) const {
inline bool is_true(literal l) const { return is_fixed(l) && !(bool)((m_stamp[l.var()] & 0x1) ^ l.sign()); } return is_fixed_at(l, level) && (bool)((m_stamp[l.var()] & 0x1) ^ l.sign());
} // even iff l.sign()
inline bool is_false(literal l) const { return is_false_at(l, m_level); }
inline bool is_true_at(literal l, unsigned level) const {
return is_fixed_at(l, level) && !(bool)((m_stamp[l.var()] & 0x1) ^ l.sign());
}
inline bool is_true(literal l) const { return is_true_at(l, m_level); }
inline void set_true(literal l) { m_stamp[l.var()] = m_level + l.sign(); } inline void set_true(literal l) { m_stamp[l.var()] = m_level + l.sign(); }
inline void set_undef(literal l) { m_stamp[l.var()] = 0; } inline void set_undef(literal l) { m_stamp[l.var()] = 0; }
void set_level(literal d, literal s) { m_stamp[d.var()] = (m_stamp[s.var()] & ~0x1) + d.sign(); } void set_level(literal d, literal s) { m_stamp[d.var()] = (m_stamp[s.var()] & ~0x1) + d.sign(); }
@ -492,10 +500,6 @@ namespace sat {
void dl_disable(literal l) { m_lits[l.index()].m_double_lookahead = m_istamp_id; } void dl_disable(literal l) { m_lits[l.index()].m_double_lookahead = m_istamp_id; }
bool dl_no_overflow(unsigned base) const { return base + 2 * m_lookahead.size() * static_cast<uint64>(m_config.m_dl_max_iterations + 1) < c_fixed_truth; } bool dl_no_overflow(unsigned base) const { return base + 2 * m_lookahead.size() * static_cast<uint64>(m_config.m_dl_max_iterations + 1) < c_fixed_truth; }
bool is_fixed_at(literal lit, unsigned level) const {
return is_fixed(lit) && (!is_false(lit) || m_stamp[lit.var()] >= level);
}
unsigned do_double(literal l, unsigned& base); unsigned do_double(literal l, unsigned& base);
unsigned double_look(literal l, unsigned& base); unsigned double_look(literal l, unsigned& base);
void set_conflict() { TRACE("sat", tout << "conflict\n";); m_inconsistent = true; } void set_conflict() { TRACE("sat", tout << "conflict\n";); m_inconsistent = true; }