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

expose extract roots as separate

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-31 11:56:44 -08:00
parent a326ad4cd9
commit 62bb234251
2 changed files with 25 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/sat/sat_scc.cpp
View file

@ -67,15 +67,8 @@ namespace sat {
} }
}; };
unsigned scc::operator()() { bool scc::extract_roots(literal_vector& roots, bool_var_vector& to_elim) {
if (m_solver.m_inconsistent) literal_vector lits;
return 0;
if (!m_scc)
return 0;
CASSERT("scc_bug", m_solver.check_invariant());
report rpt(*this);
TRACE("scc", m_solver.display(tout););
TRACE("scc_details", m_solver.display_watches(tout););
unsigned_vector index; unsigned_vector index;
unsigned_vector lowlink; unsigned_vector lowlink;
unsigned_vector s; unsigned_vector s;
@ -84,11 +77,9 @@ namespace sat {
index.resize(num_lits, UINT_MAX); index.resize(num_lits, UINT_MAX);
lowlink.resize(num_lits, UINT_MAX); lowlink.resize(num_lits, UINT_MAX);
in_s.resize(num_lits, false); in_s.resize(num_lits, false);
literal_vector roots, lits;
roots.resize(m_solver.num_vars(), null_literal); roots.resize(m_solver.num_vars(), null_literal);
unsigned next_index = 0; unsigned next_index = 0;
svector<frame> frames; svector<frame> frames;
bool_var_vector to_elim;
for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) { for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
if (index[l_idx] != UINT_MAX) if (index[l_idx] != UINT_MAX)
@ -182,7 +173,7 @@ namespace sat {
j--; j--;
if (to_literal(l2_idx) == ~l) { if (to_literal(l2_idx) == ~l) {
m_solver.set_conflict(); m_solver.set_conflict();
return 0; return false;
} }
if (m_solver.is_external(to_literal(l2_idx).var())) { if (m_solver.is_external(to_literal(l2_idx).var())) {
r = to_literal(l2_idx); r = to_literal(l2_idx);
@ -226,6 +217,23 @@ namespace sat {
roots[i] = literal(i, false); roots[i] = literal(i, false);
} }
} }
return true;
}
unsigned scc::operator()() {
if (m_solver.m_inconsistent)
return 0;
if (!m_scc)
return 0;
CASSERT("scc_bug", m_solver.check_invariant());
report rpt(*this);
TRACE("scc", m_solver.display(tout););
TRACE("scc_details", m_solver.display_watches(tout););
literal_vector roots;
bool_var_vector to_elim;
if (!extract_roots(roots, to_elim))
return 0;
TRACE("scc", for (unsigned i = 0; i < roots.size(); i++) { tout << i << " -> " << roots[i] << "\n"; } TRACE("scc", for (unsigned i = 0; i < roots.size(); i++) { tout << i << " -> " << roots[i] << "\n"; }
tout << "to_elim: "; for (unsigned v : to_elim) tout << v << " "; tout << "\n";); tout << "to_elim: "; for (unsigned v : to_elim) tout << v << " "; tout << "\n";);
m_num_elim += to_elim.size(); m_num_elim += to_elim.size();
@ -234,9 +242,8 @@ namespace sat {
TRACE("scc_detail", m_solver.display(tout);); TRACE("scc_detail", m_solver.display(tout););
CASSERT("scc_bug", m_solver.check_invariant()); CASSERT("scc_bug", m_solver.check_invariant());
if (m_scc_tr) { if (m_scc_tr)
reduce_tr(); reduce_tr();
}
TRACE("scc_detail", m_solver.display(tout);); TRACE("scc_detail", m_solver.display(tout););
return to_elim.size(); return to_elim.size();
} }

4
src/sat/sat_scc.h
View file

@ -41,9 +41,13 @@ namespace sat {
void reduce_tr(); void reduce_tr();
unsigned reduce_tr(bool learned); unsigned reduce_tr(bool learned);
public: public:
scc(solver & s, params_ref const & p); scc(solver & s, params_ref const & p);
bool extract_roots(literal_vector& roots, bool_var_vector& lits);
unsigned operator()(); unsigned operator()();
void updt_params(params_ref const & p); void updt_params(params_ref const & p);