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

remove stale functionality, finish implementation for super-slices

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-01-11 10:18:52 -08:00
parent 6b12bd6dcd
commit 0d3a465e75
2 changed files with 18 additions and 178 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -33,15 +33,16 @@ namespace polysat {
// 2^(w-hi+1)* x >=
bool fixed_bits::check(rational const& val, fi_record& fi) {
unsigned sz = c.size(m_var);
rational bw = rational::power_of_two(sz);
for (auto const& s : m_fixed_slices) {
rational bw = rational::power_of_two(s.length);
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 + 1), bw)) {
if (s.length <= sz && s.value != mod(machine_div2k(val, s.offset + 1), sbw)) {
SASSERT(s.offset + s.length <= sz);
rational hi_val = s.value;
rational lo_val = mod(s.value + 1, bw);
pdd lo = c.value(rational::power_of_two(sz - s.offset - s.length) * lo_val, c.size(m_var));
pdd hi = c.value(rational::power_of_two(sz - s.offset - s.length) * hi_val, c.size(m_var));
rational lo_val = mod(s.value + 1, sbw);
pdd lo = c.value(rational::power_of_two(sz - s.offset - s.length) * lo_val, sz);
pdd hi = c.value(rational::power_of_two(sz - s.offset - s.length) * hi_val, sz);
fi.reset();
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
fi.deps.push_back(dependency({ m_var, s }));
@ -51,8 +52,17 @@ namespace polysat {
}
// slice, properly contains variable.
// s.offset refers to offset in containing value.
if (s.length > sz) {
NOT_IMPLEMENTED_YET();
if (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);
pdd lo = c.value(lo_val, sz);
pdd hi = c.value(hi_val, sz);
fi.reset();
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
fi.deps.push_back(dependency({ m_var, s }));
fi.bit_width = sz;
fi.coeff = 1;
return false;
}
}
return true;
@ -62,167 +72,6 @@ namespace polysat {
for (auto const& s : m_fixed_slices)
out << s.value << "[" << s.length << "]@" << s.offset << "\n";
return out;
}
/**
* 2^k * x = 2^k * b
* ==> x[N-k-1:0] = b[N-k-1:0]
*/
bool get_eq_fixed_lsb(pdd const& p, fixed_slice& out) {
SASSERT(!p.is_val());
unsigned const N = p.power_of_2();
// Recognize p = 2^k * a * x - 2^k * b
if (!p.hi().is_val())
return false;
if (!p.lo().is_val())
return false;
// p = c * x - d
rational const c = p.hi().val();
rational const d = (-p.lo()).val();
SASSERT(!c.is_zero());
#if 1
// NOTE: ule_constraint::simplify removes odd factors of the leading term
unsigned k;
VERIFY(c.is_power_of_two(k));
if (d.parity(N) < k)
return false;
rational const b = machine_div2k(d, k);
out = fixed_slice(b, 0, N - k);
SASSERT_EQ(d, b * rational::power_of_two(k));
SASSERT_EQ(p, (p.manager().mk_var(p.var()) - out.value) * rational::power_of_two(k));
return true;
#else
// branch if we want to support non-simplifed constraints (not recommended)
//
// 2^k * a * x = 2^k * b
// ==> x[N-k-1:0] = a^-1 * b[N-k-1:0]
// for odd a
unsigned k = c.parity(N);
if (d.parity(N) < k)
return false;
rational const a = machine_div2k(c, k);
SASSERT(a.is_odd());
SASSERT(a.is_one()); // TODO: ule-simplify will multiply with a_inv already, so we can drop the check here.
rational a_inv;
VERIFY(a.mult_inverse(N, a_inv));
rational const b = machine_div2k(d, k);
out.hi = N - k - 1;
out.lo = 0;
out.value = a_inv * b;
SASSERT_EQ(p, (p.manager().mk_var(p.var()) - out.value) * a * rational::power_of_two(k));
return true;
#endif
}
bool get_eq_fixed_slice(pdd const& p, fixed_slice& out) {
if (get_eq_fixed_lsb(p, out))
return true;
return false;
}
/**
* Constraint lhs <= rhs.
*
* -2^(k - 2) * x > 2^(k - 1)
* <=> 2 + x[1:0] > 2 (mod 4)
* ==> x[1:0] = 1
* -- TODO: Generalize [the obvious solution does not work]
*/
bool get_ule_fixed_lsb(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_slice& out) {
return false;
}
/**
* Constraint lhs <= rhs.
*
* x <= 2^k - 1 ==> x[N-1:k] = 0
* x < 2^k ==> x[N-1:k] = 0
*/
bool get_ule_fixed_msb(pdd const& p, pdd const& q, bool is_positive, fixed_slice& out) {
SASSERT(!q.is_zero()); // equalities are handled elsewhere
unsigned const N = p.power_of_2();
pdd const& lhs = is_positive ? p : q;
pdd const& rhs = is_positive ? q : p;
bool const is_strict = !is_positive;
if (lhs.is_var() && rhs.is_val()) {
// x <= c
// find smallest k such that c <= 2^k - 1, i.e., c+1 <= 2^k
// ==> x <= 2^k - 1 ==> x[N-1:k] = 0
//
// x < c
// find smallest k such that c <= 2^k
// ==> x < 2^k ==> x[N-1:k] = 0
rational const c = is_strict ? rhs.val() : (rhs.val() + 1);
unsigned const k = c.next_power_of_two();
if (k < N) {
out.length = N - k;
out.offset = k;
out.value = 0;
return true;
}
}
return false;
}
// 2^(N-1) <= 2^(N-1-i) * x
bool get_ule_fixed_bit(pdd const& p, pdd const& q, bool is_positive, fixed_slice& out) {
return false;
}
bool get_ule_fixed_slice(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_slice& out) {
SASSERT(ule_constraint::is_simplified(lhs, rhs));
if (rhs.is_zero())
return is_positive ? get_eq_fixed_slice(lhs, out) : false;
if (get_ule_fixed_msb(lhs, rhs, is_positive, out))
return true;
if (get_ule_fixed_lsb(lhs, rhs, is_positive, out))
return true;
if (get_ule_fixed_bit(lhs, rhs, is_positive, out))
return true;
return false;
}
bool get_fixed_slice(signed_constraint c, fixed_slice& out) {
SASSERT_EQ(c.vars().size(), 1); // this only makes sense for univariate constraints
if (c.is_ule())
return get_ule_fixed_slice(c.to_ule().lhs(), c.to_ule().rhs(), c.is_positive(), out);
// if (c->is_op())
// ; // TODO: x & constant = constant ==> bitmask ... but we have trouble recognizing that because we introduce a new variable for '&' before we see the equality.
return false;
}
/*
// 2^(k - d) * x = m * 2^(k - d)
// Special case [still seems to occur frequently]: -2^(k - 2) * x > 2^(k - 1) - TODO: Generalize [the obvious solution does not work] => lsb(x, 2) = 1
bool get_lsb(pdd lhs, pdd rhs, pdd& p, trailing_bits& info, bool pos) {
SASSERT(lhs.is_univariate() && lhs.degree() <= 1);
SASSERT(rhs.is_univariate() && rhs.degree() <= 1);
else { // inequality - check for special case
if (pos || lhs.power_of_2() < 3)
return false;
auto it = lhs.begin();
if (it == lhs.end())
return false;
if (it->vars.size() != 1)
return false;
rational coeff = it->coeff;
it++;
if (it != lhs.end())
return false;
if ((mod2k(-coeff, lhs.power_of_2())) != rational::power_of_two(lhs.power_of_2() - 2))
return false;
p = lhs.div(coeff);
SASSERT(p.is_var());
info.bits = 1;
info.length = 2;
info.positive = true; // this is a conjunction
return true;
}
}
*/
}
} // namespace polysat

9
src/sat/smt/polysat/fixed_bits.h
View file

@ -20,15 +20,6 @@ namespace polysat {
class core;
bool get_eq_fixed_lsb(pdd const& p, fixed_slice& out);
bool get_eq_fixed_slice(pdd const& p, fixed_slice& out);
bool get_ule_fixed_lsb(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_slice& out);
bool get_ule_fixed_msb(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_slice& out);
bool get_ule_fixed_bit(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_slice& out);
bool get_ule_fixed_slice(pdd const& lhs, pdd const& rhs, bool is_positive, fixed_slice& out);
bool get_fixed_slice(signed_constraint c, fixed_slice& out);
class fixed_bits {
core& c;
pvar m_var = null_var;