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

fix incorrect fixed_bits forbidden interval calculation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-14 12:19:04 -08:00
parent 8f3e8bd0bb
commit 05d61ed090
2 changed files with 28 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/sat/smt/polysat/fixed_bits.cpp
View file

@ -29,8 +29,15 @@ namespace polysat {
c.get_fixed_bits(v, m_fixed_slices);
}
// if x[hi:lo] = value, then
// 2^(w-hi+1)* x >=
//
// If x[hi:lo] = value, then
// let K = w - hi - 1 = w - s.length - s.offset
// 2^Kvalue <= 2^Kx < 2^K(value + 1)
// 2^Kx not in [2^K(value + 1), 2^Kvalue[
// bit-width : w - K = s.offset + s.length
//
// If y[hi:lo] = value, y[hi':lo'] = x
//
bool fixed_bits::check(rational const& val, fi_record& fi) {
unsigned sz = c.size(m_var);
rational bw = rational::power_of_two(sz);
@ -38,17 +45,21 @@ namespace polysat {
rational sbw = rational::power_of_two(s.length);
// slice is properly contained in bit-vector variable
if (s.length <= sz && s.value != mod(machine_div2k(val, s.offset), sbw)) {
SASSERT(s.offset + s.length <= sz);
rational hi_val = s.value;
rational lo_val = mod(s.value + 1, sbw);
pdd lo = c.value(rational::power_of_two(sz - s.length) * lo_val, sz);
pdd hi = c.value(rational::power_of_two(sz - s.length) * hi_val, sz);
unsigned bw = s.length + s.offset;
unsigned K = sz - bw;
pdd lo = c.value(rational::power_of_two(K) * (s.value + 1), sz);
pdd hi = c.value(rational::power_of_two(K) * s.value, sz);
rational hi_val = rational::power_of_two(s.offset) * s.value;
rational lo_val = mod(rational::power_of_two(s.offset) * s.value + 1, rational::power_of_two(bw));
fi.reset();
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
fi.deps.push_back(dependency({ m_var, s }));
fi.bit_width = s.length;
fi.deps.push_back(dependency({ m_var, s }));
fi.bit_width = bw;
fi.coeff = 1;
// verbose_stream() << "fixed bits sub: v" << m_var << " value " << val << " " << fi << "\n";
return false;
}
// slice, properly contains variable.
@ -64,6 +75,7 @@ namespace polysat {
fi.deps.push_back(dependency({ m_var, s }));
fi.bit_width = sz;
fi.coeff = 1;
verbose_stream() << "fixed bits sup: v" << m_var << " " << fi << "\n";
return false;
}
}

9
src/sat/smt/polysat/viable.cpp
View file

@ -393,8 +393,13 @@ namespace polysat {
return true;
}
else {
intersect(v, e);
TRACE("bv", tout << "fixed " << *e << "\n");
TRACE("bv", tout << "fixed " << val << " " << *e << "\n");
if (!intersect(v, e)) {
display(verbose_stream());
display_explain(verbose_stream() << "explain\n");
SASSERT(false);
}
return false;
}
}