mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 13:23:39 +00:00
Code Activity

log justifications during conflict resolution

Browse source
This commit is contained in:
Jakob Rath 2022-01-28 15:50:14 +01:00
parent 0eb0306ae2
commit 67647433ba
3 changed files with 23 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/polysat/boolean.cpp
View file

@ -122,4 +122,13 @@ namespace polysat {
} }
return out; return out;
} }
std::ostream& bool_var_manager::display_justification(sat::literal lit, std::ostream& out) const {
out << m_kind[lit.var()];
if (is_assigned(lit))
out << " @ " << level(lit);
if (is_bool_propagation(lit))
out << " by " << show_deref(reason(lit));
return out;
}
} }

9
src/math/polysat/boolean.h
View file

@ -92,6 +92,7 @@ namespace polysat {
void unassign(sat::literal lit); void unassign(sat::literal lit);
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
std::ostream& display_justification(sat::literal lit, std::ostream& out) const;
friend std::ostream& operator<<(std::ostream& out, kind_t const& k) { friend std::ostream& operator<<(std::ostream& out, kind_t const& k) {
switch (k) { switch (k) {
@ -104,6 +105,14 @@ namespace polysat {
} }
}; };
struct bool_justification_pp {
bool_var_manager const& b;
sat::literal lit;
bool_justification_pp(bool_var_manager const& b, sat::literal lit) : b(b), lit(lit) {}
};
inline std::ostream& operator<<(std::ostream& out, bool_var_manager const& m) { return m.display(out); } inline std::ostream& operator<<(std::ostream& out, bool_var_manager const& m) { return m.display(out); }
inline std::ostream& operator<<(std::ostream& out, bool_justification_pp const& p) { return p.b.display_justification(p.lit, out); }
} }

7
src/math/polysat/solver.cpp
View file

@ -502,7 +502,8 @@ namespace polysat {
void solver::resolve_conflict() { void solver::resolve_conflict() {
LOG_H2("Resolve conflict"); LOG_H2("Resolve conflict");
LOG("\n" << *this); LOG("\n" << *this);
LOG("search state: " << m_search); LOG("Search state: " << m_search);
LOG("Assignment: " << assignments_pp(*this));
for (pvar v = 0; v < m_justification.size(); ++v) for (pvar v = 0; v < m_justification.size(); ++v)
LOG("v" << v << " " << viable::var_pp(m_viable, v)); LOG("v" << v << " " << viable::var_pp(m_viable, v));
++m_stats.m_num_conflicts; ++m_stats.m_num_conflicts;
@ -527,13 +528,13 @@ namespace polysat {
search_iterator search_it(m_search); search_iterator search_it(m_search);
while (search_it.next()) { while (search_it.next()) {
// LOG("search state: " << m_search);
auto& item = *search_it; auto& item = *search_it;
search_it.set_resolved(); search_it.set_resolved();
LOG_H2("Working on " << search_item_pp(m_search, item)); LOG_H2("Working on " << search_item_pp(m_search, item));
if (item.is_assignment()) { if (item.is_assignment()) {
// Resolve over variable assignment // Resolve over variable assignment
pvar v = item.var(); pvar v = item.var();
LOG(m_justification[v]);
if (!m_conflict.is_pmarked(v) && !m_conflict.is_bailout()) { if (!m_conflict.is_pmarked(v) && !m_conflict.is_bailout()) {
m_search.pop_assignment(); m_search.pop_assignment();
continue; continue;
@ -552,6 +553,8 @@ namespace polysat {
SASSERT(item.is_boolean()); SASSERT(item.is_boolean());
sat::literal const lit = item.lit(); sat::literal const lit = item.lit();
sat::bool_var const var = lit.var(); sat::bool_var const var = lit.var();
LOG(bool_justification_pp(m_bvars, lit));
LOG("Literal " << lit << " is " << lit2cnstr(lit));
if (!m_conflict.is_bmarked(var)) if (!m_conflict.is_bmarked(var))
continue; continue;
if (m_bvars.level(var) <= base_level()) if (m_bvars.level(var) <= base_level())