mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

track clause name for debugging

Browse source
This commit is contained in:
Jakob Rath 2023-01-11 10:29:20 +01:00
parent 1d349fb0e6
commit fa036ae486
3 changed files with 15 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/clause.cpp
View file

@ -37,6 +37,7 @@ namespace polysat {
out << " \\/ ";
out << lit;
}
out << " (" << (name() ? name() : "<null>") << ")";
return out;
}

7
src/math/polysat/clause.h
View file

@ -36,6 +36,7 @@ namespace polysat {
unsigned m_ref_count = 0; // TODO: remove refcount once we confirm it's not needed anymore
bool m_redundant = redundant_default;
sat::literal_vector m_literals;
char const* m_name = "";
/* TODO: embed literals to save an indirection?
@ -64,6 +65,9 @@ namespace polysat {
sat::literal operator[](unsigned idx) const { return m_literals[idx]; }
sat::literal& operator[](unsigned idx) { return m_literals[idx]; }
sat::literal_vector& literals() { return m_literals; }
sat::literal_vector const& literals() const { return m_literals; }
using const_iterator = typename sat::literal_vector::const_iterator;
const_iterator begin() const { return m_literals.begin(); }
const_iterator end() const { return m_literals.end(); }
@ -72,6 +76,9 @@ namespace polysat {
void set_redundant(bool r) { m_redundant = r; }
bool is_redundant() const { return m_redundant; }
void set_name(char const* name) { m_name = name; }
char const* name() const { return m_name; }
};
inline std::ostream& operator<<(std::ostream& out, clause const& c) { return c.display(out); }

11
src/math/polysat/conflict.cpp
View file

@ -287,7 +287,7 @@ namespace polysat {
void conflict::insert_vars(signed_constraint c) {
for (pvar v : c->vars())
if (s.is_assigned(v))
if (s.is_assigned(v))
m_vars.insert(v);
}
@ -308,10 +308,13 @@ namespace polysat {
if (s.m_bvars.is_true(lit))
verbose_stream() << "REDUNDANT lemma " << lit << " : " << show_deref(lemma) << "\n";
LOG_H3("Lemma " << (name ? name : "<unknown>") << ": " << show_deref(lemma));
if (!name)
name = "<unknown>";
LOG_H3("Lemma " << name << ": " << show_deref(lemma));
SASSERT(lemma);
s.m_simplify_clause.apply(*lemma);
lemma->set_redundant(true);
lemma->set_name(name);
for (sat::literal lit : *lemma) {
LOG(lit_pp(s, lit));
// NOTE: it can happen that the literal's bvalue is l_true at this point.
@ -385,7 +388,7 @@ namespace polysat {
if (!has_decision) {
for (pvar v : c->vars()) {
if (s.is_assigned(v) && s.get_level(v) <= lvl) {
m_vars.insert(v);
m_vars.insert(v);
// TODO - figure out what to do with constraints from conflict lemma that disappear here.
// if (s.m_bvars.is_false(lit))
// m_resolver->infer_lemmas_for_value(v, ~c, *this);
@ -418,7 +421,7 @@ namespace polysat {
insert(s.eq(i.hi(), i.hi_val()));
}
logger().log(inf_resolve_value(s, v));
revert_pvar(v);
}