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

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-13 17:05:56 -08:00
parent 9fa17a432a
commit 49a0266c6a
1 changed files with 16 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/sat/smt/sat_dual_solver.cpp
View file

@ -55,8 +55,8 @@ namespace sat {
return w; return w;
} }
void dual_solver::track_relevancy(bool_var v) { void dual_solver::track_relevancy(bool_var w) {
v = ext2var(v); bool_var v = ext2var(w);
if (!m_is_tracked.get(v, false)) { if (!m_is_tracked.get(v, false)) {
m_is_tracked.setx(v, true, false); m_is_tracked.setx(v, true, false);
m_tracked_vars.push_back(v); m_tracked_vars.push_back(v);
@ -80,6 +80,8 @@ 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) {
@ -123,8 +125,18 @@ 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 << " " << v1 << " " << v2 << "\n"; out << w << " " << v << " " << v1 << " " << v2 << "\n";
} }
literal_vector lits;
for (bool_var v : m_tracked_vars)
lits.push_back(literal(m_var2ext[v], l_false == s.value(m_var2ext[v])));
out << "tracked: " << lits << "\n";
lits.reset();
for (literal r : m_roots)
if (m_solver.value(r) == l_true)
lits.push_back(r);
out << "roots: " << lits << "\n";
return out; return out;
} }
} }