mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

testing bdd for elim-vars

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-18 17:37:38 -07:00
parent 6155362571
commit dc6ed64da1
9 changed files with 254 additions and 133 deletions
Download patch file Download diff file Expand all files Collapse all files

76
src/sat/sat_lookahead.cpp
View file

@ -412,11 +412,17 @@ namespace sat {
for (literal l1 : m_trail) {
SASSERT(is_true(l1));
for (literal l2 : m_binary[l1.index()]) {
VERIFY(is_true(l2));
if (is_undef(l2)) return true;
}
unsigned sz = m_ternary_count[(~l1).index()];
for (binary b : m_ternary[(~l1).index()]) {
if (sz-- == 0) break;
if (!(is_true(b.m_u) || is_true(b.m_v) || (is_undef(b.m_v) && is_undef(b.m_u)))) {
std::cout << b.m_u << " " << b.m_v << "\n";
std::cout << get_level(b.m_u) << " " << get_level(b.m_v) << " level: " << m_level << "\n";
UNREACHABLE();
}
if ((is_false(b.m_u) && is_undef(b.m_v)) || (is_false(b.m_v) && is_undef(b.m_u)))
return true;
}
@ -424,6 +430,7 @@ namespace sat {
for (nary * n : m_nary_clauses) {
if (n->size() == 1 && !is_true(n->get_head())) {
for (literal lit : *n) {
VERIFY(!is_undef(lit));
if (is_undef(lit)) return true;
}
}
@ -1743,74 +1750,10 @@ namespace sat {
bool lookahead::check_autarky(literal l, unsigned level) {
return false;
#if 0
// no propagations are allowed to reduce clauses.
for (nary * cp : m_nary[(~l).index()]) {
clause& c = *cp;
unsigned sz = c.size();
bool found = false;
for (unsigned i = 0; !found && i < sz; ++i) {
found = is_true(c[i]);
if (found) {
TRACE("sat", tout << c[i] << " is true in " << c << "\n";);
}
}
IF_VERBOSE(2, verbose_stream() << "skip autarky " << l << "\n";);
if (!found) return false;
}
//
// bail out if there is a pending binary propagation.
// In general, we would have to check, recursively that
// a binary propagation does not create reduced clauses.
//
literal_vector const& lits = m_binary[l.index()];
TRACE("sat", tout << l << ": " << lits << "\n";);
for (unsigned i = 0; i < lits.size(); ++i) {
literal l2 = lits[i];
if (is_true(l2)) continue;
SASSERT(!is_false(l2));
return false;
}
return true;
#endif
}
void lookahead::update_lookahead_reward(literal l, unsigned level) {
if (m_lookahead_reward == 0) {
if (!check_autarky(l, level)) {
// skip
}
else if (get_lookahead_reward(l) == 0) {
++m_stats.m_autarky_propagations;
IF_VERBOSE(1, verbose_stream() << "(sat.lookahead autarky " << l << ")\n";);
TRACE("sat", tout << "autarky: " << l << " @ " << m_stamp[l.var()]
<< " "
<< (!m_binary[l.index()].empty() || m_nary_count[l.index()] != 0) << "\n";);
lookahead_backtrack();
assign(l);
propagate();
}
else {
++m_stats.m_autarky_equivalences;
// l => p is known, but p => l is possibly not.
// add p => l.
// justification: any consequence of l
// that is not a consequence of p does not
// reduce the clauses.
literal p = get_parent(l);
SASSERT(p != null_literal);
if (m_stamp[p.var()] > m_stamp[l.var()]) {
TRACE("sat", tout << "equivalence " << l << " == " << p << "\n"; display(tout););
IF_VERBOSE(1, verbose_stream() << "(sat.lookahead equivalence " << l << " == " << p << ")\n";);
add_binary(~l, p);
set_level(l, p);
}
}
}
else {
void lookahead::update_lookahead_reward(literal l, unsigned level) {
if (m_lookahead_reward != 0) {
inc_lookahead_reward(l, m_lookahead_reward);
}
}
@ -1852,7 +1795,6 @@ namespace sat {
literal last_changed = null_literal;
unsigned num_iterations = 0;
while (change && num_iterations < m_config.m_dl_max_iterations && !inconsistent()) {
change = false;
num_iterations++;
for (unsigned i = 0; !inconsistent() && i < m_lookahead.size(); ++i) {
literal lit = m_lookahead[i].m_lit;