mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

collect_fixed

Browse source
This commit is contained in:
Jakob Rath 2023-07-26 15:07:53 +02:00
parent 6cb84dc4cd
commit 1e528e264f
1 changed files with 23 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -485,7 +485,7 @@ namespace polysat {
} }
rational slicing::get_value(enode* s) const { rational slicing::get_value(enode* s) const {
SASSERT(s->interpreted()); SASSERT(is_value(s));
rational val; rational val;
VERIFY(try_get_value(s, val)); VERIFY(try_get_value(s, val));
return val; return val;
@ -1166,6 +1166,28 @@ namespace polysat {
SASSERT(all_of(m_egraph.nodes(), [](enode* n) { return !n->is_marked1(); })); SASSERT(all_of(m_egraph.nodes(), [](enode* n) { return !n->is_marked1(); }));
} }
void slicing::collect_fixed(pvar v, rational& mask, rational& value) {
enode_vector& base = m_tmp2;
SASSERT(base.empty());
get_base(var2slice(v), base);
mask = 0;
value = 0;
rational a;
unsigned lo = 0;
for (auto it = base.rbegin(); it != base.rend(); ++it) {
enode* n = *it;
enode* r = n->get_root();
unsigned const w = width(n);
if (try_get_value(r, a)) {
rational const factor = rational::power_of_two(lo);
// TODO: probably better to return vector of {w, lo, a} instead
mask += (rational::power_of_two(w) - 1) * factor;
value += a * factor;
}
lo += w;
}
}
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) {