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

slicing::explain_simple_overlap

Browse source
This commit is contained in:
Jakob Rath 2023-12-01 13:13:59 +01:00
parent cf9b7bed0c
commit 828f74db73
2 changed files with 46 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1490,6 +1490,7 @@ namespace polysat {
SASSERT_EQ(sub_lo(p), n); // otherwise not a candidate
// check if base of sub_hi(p) matches the base of v
enode_vector& p_hi_base = m_tmp3;
SASSERT(p_hi_base.empty());
get_base(sub_hi(p), p_hi_base);
auto p_it = p_hi_base.rbegin();
bool ok = true;
@ -1519,6 +1520,48 @@ namespace polysat {
SASSERT(all_of(m_egraph.nodes(), [](enode* n) { return !n->is_marked1(); }));
}
void slicing::explain_simple_overlap(pvar v, pvar x, std::function<void(sat::literal)> const& on_lit) {
SASSERT(width(var2slice(x)) <= width(var2slice(v)));
SASSERT(m_marked_lits.empty());
SASSERT(m_tmp_deps.empty());
enode_vector& v_base = m_tmp4;
SASSERT(v_base.empty());
get_base(var2slice(v), v_base);
enode_vector& x_base = m_tmp5;
SASSERT(x_base.empty());
get_base(var2slice(x), x_base);
auto v_it = v_base.rbegin();
auto x_it = x_base.rbegin();
while (x_it != x_base.rend()) {
SASSERT(v_it != v_base.rend());
enode* nv = *v_it; ++v_it;
enode* nx = *x_it; ++x_it;
SASSERT_EQ(nv->get_root(), nx->get_root());
explain_equal(nv, nx, 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::collect_fixed(pvar v, justified_fixed_bits_vector& out) {
enode_vector& base = m_tmp2;
SASSERT(base.empty());

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

@ -280,6 +280,8 @@ namespace polysat {
mutable enode_vector m_tmp1;
mutable enode_vector m_tmp2;
mutable enode_vector m_tmp3;
mutable enode_vector m_tmp4;
mutable enode_vector m_tmp5;
ptr_vector<void> m_tmp_deps;
sat::literal_set m_marked_lits;
@ -362,6 +364,7 @@ namespace polysat {
/** For a given variable v, find the set of variables w such that w = v[|w|:0]. */
void collect_simple_overlaps(pvar v, pvar_vector& out);
void explain_simple_overlap(pvar v, pvar x, std::function<void(sat::literal)> const& on_lit);
struct justified_fixed_bits : public fixed_bits {
enode* just;