mirror of
https://github.com/Z3Prover/z3
synced 2025-07-20 19:32:04 +00:00
fix relevancy tracking in new solver
This commit is contained in:
parent
36e9412252
commit
85a20791db
2 changed files with 12 additions and 8 deletions
|
@ -72,6 +72,7 @@ namespace sat {
|
||||||
}
|
}
|
||||||
|
|
||||||
void dual_solver::add_root(unsigned sz, literal const* clause) {
|
void dual_solver::add_root(unsigned sz, literal const* clause) {
|
||||||
|
TRACE("dual", tout << "root: " << literal_vector(sz, clause) << "\n";);
|
||||||
if (sz == 1) {
|
if (sz == 1) {
|
||||||
m_units.push_back(clause[0]);
|
m_units.push_back(clause[0]);
|
||||||
return;
|
return;
|
||||||
|
@ -80,11 +81,10 @@ namespace sat {
|
||||||
for (unsigned i = 0; i < sz; ++i)
|
for (unsigned i = 0; i < sz; ++i)
|
||||||
m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
|
m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
|
||||||
m_roots.push_back(~root);
|
m_roots.push_back(~root);
|
||||||
if (root.var() == 5350)
|
|
||||||
std::cout << "root clause " << literal_vector(sz, clause) << "\n";
|
|
||||||
}
|
}
|
||||||
|
|
||||||
void dual_solver::add_aux(unsigned sz, literal const* clause) {
|
void dual_solver::add_aux(unsigned sz, literal const* clause) {
|
||||||
|
TRACE("dual", tout << "aux: " << literal_vector(sz, clause) << "\n";);
|
||||||
m_lits.reset();
|
m_lits.reset();
|
||||||
for (unsigned i = 0; i < sz; ++i)
|
for (unsigned i = 0; i < sz; ++i)
|
||||||
m_lits.push_back(ext2lit(clause[i]));
|
m_lits.push_back(ext2lit(clause[i]));
|
||||||
|
@ -106,8 +106,8 @@ namespace sat {
|
||||||
for (literal lit : m_solver.get_core())
|
for (literal lit : m_solver.get_core())
|
||||||
m_core.push_back(lit2ext(lit));
|
m_core.push_back(lit2ext(lit));
|
||||||
if (is_sat == l_true) {
|
if (is_sat == l_true) {
|
||||||
IF_VERBOSE(0, display(s, verbose_stream()));
|
TRACE("dual", display(s, tout); s.display(tout););
|
||||||
s.display(verbose_stream());
|
IF_VERBOSE(0, verbose_stream() << "unexpected SAT\n");
|
||||||
UNREACHABLE();
|
UNREACHABLE();
|
||||||
return false;
|
return false;
|
||||||
}
|
}
|
||||||
|
@ -125,7 +125,8 @@ namespace sat {
|
||||||
lbool v2 = s.value(w);
|
lbool v2 = s.value(w);
|
||||||
if (v1 == v2 || v2 == l_undef)
|
if (v1 == v2 || v2 == l_undef)
|
||||||
continue;
|
continue;
|
||||||
out << w << " " << v << " " << v1 << " " << v2 << "\n";
|
out << "ext: " << w << " " << v2 << "\n";
|
||||||
|
out << "int: " << v << " " << v1 << "\n";
|
||||||
}
|
}
|
||||||
literal_vector lits;
|
literal_vector lits;
|
||||||
for (bool_var v : m_tracked_vars)
|
for (bool_var v : m_tracked_vars)
|
||||||
|
|
|
@ -115,18 +115,21 @@ struct goal2sat::imp : public sat::sat_internalizer {
|
||||||
return sat::status::th(m_is_redundant, m.get_basic_family_id());
|
return sat::status::th(m_is_redundant, m.get_basic_family_id());
|
||||||
}
|
}
|
||||||
|
|
||||||
|
bool relevancy_enabled() {
|
||||||
|
return m_euf && ensure_euf()->relevancy_enabled();
|
||||||
|
}
|
||||||
|
|
||||||
bool top_level_relevant() {
|
bool top_level_relevant() {
|
||||||
return m_top_level && m_euf && ensure_euf()->relevancy_enabled();
|
return m_top_level && relevancy_enabled();
|
||||||
}
|
}
|
||||||
|
|
||||||
void add_dual_def(unsigned n, sat::literal const* lits) {
|
void add_dual_def(unsigned n, sat::literal const* lits) {
|
||||||
if (top_level_relevant())
|
if (relevancy_enabled())
|
||||||
ensure_euf()->add_aux(n, lits);
|
ensure_euf()->add_aux(n, lits);
|
||||||
}
|
}
|
||||||
|
|
||||||
void add_dual_root(unsigned n, sat::literal const* lits) {
|
void add_dual_root(unsigned n, sat::literal const* lits) {
|
||||||
if (top_level_relevant())
|
if (relevancy_enabled())
|
||||||
ensure_euf()->add_root(n, lits);
|
ensure_euf()->add_root(n, lits);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue