mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

fix alias bug

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-03-02 10:15:14 -08:00
parent 657aaf9a0f
commit 531bda39ac
3 changed files with 33 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/ast/sls/bv_sls_eval.cpp
View file

@ -1043,8 +1043,16 @@ namespace bv {
if (b.is_zero()) {
a.get_variant(m_tmp, m_rand);
return a.set_repair(random_bool(), m_tmp);
}
}
#if 0
verbose_stream() << "solve for " << e << "\n";
rational r = e.get_value(e.nw);
rational root;
verbose_stream() << r.is_int_perfect_square(root) << "\n";
#endif
auto& x = m_tmp;
auto& y = m_tmp2;
@ -1055,7 +1063,8 @@ namespace bv {
auto& nexta = m_nexta;
auto& nextb = m_nextb;
auto& aux = m_aux;
auto bw = b.bw;
// x*ta + y*tb = x
@ -1071,10 +1080,11 @@ namespace bv {
y[a.nw] = 0;
x[a.nw] = 0;
a.set_bw((a.nw + 1)* 8 * sizeof(digit_t));
y.set_bw(a.bw); // enable comparisons
a.set_zero(x);
x.set(b.bw, true); // x = 2 ^ b.bw
x.set(bw, true); // x = 2 ^ b.bw
a.set_one(ta);
a.set_zero(tb);
@ -1099,11 +1109,10 @@ namespace bv {
a.set(tb, aux); // tb := aux
}
a.set_bw(b.bw);
a.set_bw(bw);
y.set_bw(0);
// x*a + y*b = 1
tb.set_bw(b.bw);
tb.set_bw(0);
#if Z3DEBUG
b.get(y);

24
src/ast/sls/sls_valuation.cpp
View file

@ -74,6 +74,15 @@ namespace bv {
return out;
}
rational bvect::get_value(unsigned nw) const {
rational p(1), r(0);
for (unsigned i = 0; i < nw; ++i) {
r += p * rational((*this)[i]);
p *= rational::power_of_two(8 * sizeof(digit_t));
}
return r;
}
sls_valuation::sls_valuation(unsigned bw) {
set_bw(bw);
m_lo.set_bw(bw);
@ -347,7 +356,7 @@ namespace bv {
dst.set(i, true);
}
else {
for (unsigned i = 0; i < bw && !in_range(dst); ++i)
for (unsigned i = 0; !in_range(dst) && i < bw; ++i)
if (!fixed.get(i) && !dst.get(i))
dst.set(i, true);
for (unsigned i = bw; !in_range(dst) && i-- > 0;)
@ -398,15 +407,6 @@ namespace bv {
clear_overflow_bits(bits);
}
rational sls_valuation::get_value(bvect const& bits) const {
rational p(1), r(0);
for (unsigned i = 0; i < nw; ++i) {
r += p * rational(bits[i]);
p *= rational::power_of_two(8 * sizeof(digit_t));
}
return r;
}
void sls_valuation::get(bvect& dst) const {
m_bits.copy_to(nw, dst);
}
@ -479,8 +479,8 @@ namespace bv {
set_value(m_hi, h);
}
else {
auto old_lo = get_value(m_lo);
auto old_hi = get_value(m_hi);
auto old_lo = lo();
auto old_hi = hi();
if (old_lo < old_hi) {
if (old_lo < l && l < old_hi)
set_value(m_lo, l),

11
src/ast/sls/sls_valuation.h
View file

@ -60,6 +60,8 @@ namespace bv {
return bw;
}
rational get_value(unsigned nw) const;
friend bool operator==(bvect const& a, bvect const& b);
friend bool operator<(bvect const& a, bvect const& b);
friend bool operator>(bvect const& a, bvect const& b);
@ -96,7 +98,6 @@ namespace bv {
bvect m_lo, m_hi; // range assignment to bit-vector, as wrap-around interval
unsigned mask;
rational get_value(bvect const& bits) const;
bool round_up(bvect& dst) const;
bool round_down(bvect& dst) const;
@ -131,10 +132,10 @@ namespace bv {
void set_value(bvect& bits, rational const& r);
rational get_value() const { return get_value(m_bits); }
rational get_eval() const { return get_value(eval); }
rational lo() const { return get_value(m_lo); }
rational hi() const { return get_value(m_hi); }
rational get_value() const { return m_bits.get_value(nw); }
rational get_eval() const { return eval.get_value(nw); }
rational lo() const { return m_lo.get_value(nw); }
rational hi() const { return m_hi.get_value(nw); }
void get(bvect& dst) const;