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

slicing equivalent vars + explain

Browse source
This commit is contained in:
Jakob Rath 2023-08-18 16:21:59 +02:00
parent e09636065b
commit b4902f374b
2 changed files with 44 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/math/polysat/slicing.cpp
View file

@ -625,6 +625,30 @@ namespace polysat {
explain_equal(var2slice(x), var2slice(y), out_deps); explain_equal(var2slice(x), var2slice(y), out_deps);
} }
void slicing::explain_equal(pvar x, pvar y, std::function<void(sat::literal)> const& on_lit) {
SASSERT(m_marked_lits.empty());
SASSERT(m_tmp_deps.empty());
explain_equal(x, y, m_tmp_deps);
for (void* dp : m_tmp_deps) {
dep_t const d = dep_t::decode(dp);
if (d.is_null())
continue;
if (d.is_lit()) {
sat::literal lit = d.lit();
if (m_marked_lits.contains(lit))
continue;
m_marked_lits.insert(lit);
on_lit(d.lit());
}
else {
// equivalence between to variables cannot be due to value assignment
UNREACHABLE();
}
}
m_marked_lits.reset();
m_tmp_deps.reset();
}
void slicing::explain(ptr_vector<void>& out_deps) { void slicing::explain(ptr_vector<void>& out_deps) {
SASSERT(is_conflict()); SASSERT(is_conflict());
m_egraph.begin_explain(); m_egraph.begin_explain();
@ -1530,6 +1554,16 @@ namespace polysat {
explain_value(n, on_lit, on_var); explain_value(n, on_lit, on_var);
} }
pvar_vector slicing::equivalent_vars(pvar v) const {
pvar_vector xs;
for (enode* n : euf::enode_class(var2slice(v))) {
pvar const x = slice2var(n);
if (x != null_var)
xs.push_back(x);
}
return xs;
}
std::ostream& slicing::display(std::ostream& out) const { std::ostream& slicing::display(std::ostream& out) const {
enode_vector base; enode_vector base;
for (pvar v = 0; v < m_var2slice.size(); ++v) { for (pvar v = 0; v < m_var2slice.size(); ++v) {

10
src/math/polysat/slicing.h
View file

@ -375,6 +375,16 @@ namespace polysat {
void collect_fixed(pvar v, justified_fixed_bits_vector& out); void collect_fixed(pvar v, justified_fixed_bits_vector& out);
void explain_fixed(enode* just, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var); void explain_fixed(enode* just, std::function<void(sat::literal)> const& on_lit, std::function<void(pvar)> const& on_var);
/**
* Collect variables that are equivalent to v (including v itself)
*
* NOTE: this might miss some variables that are equal due to equivalent base slices. With 'polysat.slicing.congruence=true' and after propagate(), it should return all equal variables.
*/
pvar_vector equivalent_vars(pvar v) const;
/** Explain why variables x and y are equivalent */
void explain_equal(pvar x, pvar y, std::function<void(sat::literal)> const& on_lit);
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
std::ostream& display_tree(std::ostream& out) const; std::ostream& display_tree(std::ostream& out) const;
}; };