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

fixup fixedbits again

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-14 14:38:44 -08:00
parent ff637a3989
commit 79a2c86c05
3 changed files with 9 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -36,7 +36,6 @@ namespace polysat {
// 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);
@ -49,22 +48,22 @@ namespace polysat {
SASSERT(s.offset + s.length <= 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);
pdd lo = c.value(rational::power_of_two(sz - s.length) * (s.value + 1), sz);
pdd hi = c.value(rational::power_of_two(sz - s.length) * 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));
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 = bw;
fi.coeff = 1;
// verbose_stream() << "fixed bits sub: v" << m_var << " value " << val << " " << fi << "\n";
// verbose_stream() << "fixed bits sub: v" << m_var << " " << sz << " value " << val << " " << fi << "\n";
return false;
}
// slice, properly contains variable.
// s.offset refers to offset in containing value.
if (s.length > sz && mod(machine_div2k(s.value, s.offset), bw) != val) {
if (false && s.length > sz && mod(machine_div2k(s.value, s.offset), bw) != val) {
rational hi_val = mod(machine_div2k(s.value, s.offset), bw);
rational lo_val = mod(hi_val + 1, bw);

1
src/sat/smt/polysat/ule_constraint.cpp
View file

@ -323,6 +323,7 @@ namespace polysat {
// Evaluate lhs <= rhs
lbool ule_constraint::eval(pdd const& lhs, pdd const& rhs) {
// NOTE: don't assume simplifications here because we also call this on partially substituted constraints
if (lhs.is_zero())
return l_true; // 0 <= p
if (lhs == rhs)

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

@ -655,6 +655,7 @@ namespace polysat {
// a < x <= b <=>
// a + 1 <= x < b + 1
// x - a - 1 < b - a
auto vlo = c.value(mod((e.value - 1) * p2eb + 1, p2b), bw);
auto vhi = c.value(mod(e.value * p2eb + 1, p2b), bw);
@ -666,6 +667,7 @@ namespace polysat {
verbose_stream() << "before bw " << ebw << " " << bw << " " << *e.e << "\nafter bw " << abw << " " << aw << " " << *after.e << "\n";
if (!t.is_val())
IF_VERBOSE(0, verbose_stream() << "symbolic t : " << t << "\n");
verbose_stream() << t - vlo << " " << vhi - vlo << "\n";
#endif
auto sc = cs.ult(t - vlo, vhi - vlo);
@ -676,6 +678,7 @@ namespace polysat {
deps.push_back(c.propagate(sc, c.explain_weak_eval(sc)));
t.reset(lo.manager());
t = c.value(mod(e.value, rational::power_of_two(aw)), aw);
// verbose_stream() << "after " << t << "\n";
}
if (abw < aw)