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

fix zero/sign extension

Browse source
This commit is contained in:
Jakob Rath 2023-07-21 14:32:22 +02:00
parent e7c9112beb
commit f14c3c3cb4
4 changed files with 20 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/math/polysat/constraint_manager.cpp
View file

@ -640,14 +640,16 @@ namespace polysat {
return s.var(v);
}
pdd constraint_manager::zero_ext(pdd const& p, unsigned bit_width) {
SASSERT(bit_width > p.power_of_2());
pdd constraint_manager::zero_ext(pdd const& p, unsigned extra_bits) {
SASSERT(extra_bits > 0);
unsigned const p_sz = p.power_of_2();
unsigned const v_sz = p_sz + extra_bits;
pdd const q = s.var(s.m_names.mk_name(p));
constraint_dedup::bv_ext_args const args = {false, q.var(), bit_width};
constraint_dedup::bv_ext_args const args = {false, q.var(), extra_bits};
auto const it = m_dedup.m_bv_ext_expr.find_iterator(args);
if (it != m_dedup.m_bv_ext_expr.end())
return s.var(it->m_value);
pdd const v = s.var(s.add_var(bit_width));
pdd const v = s.var(s.add_var(v_sz));
m_dedup.m_bv_ext_expr.insert(args, v.var());
// (1) v[|p|-1:0] = p
s.add_eq(q, extract(v, p.power_of_2() - 1, 0));
@ -656,20 +658,21 @@ namespace polysat {
return v;
}
pdd constraint_manager::sign_ext(pdd const& p, unsigned bit_width) {
pdd constraint_manager::sign_ext(pdd const& p, unsigned extra_bits) {
SASSERT(extra_bits > 0);
unsigned const p_sz = p. power_of_2();
SASSERT(bit_width > p_sz);
unsigned const v_sz = p_sz + extra_bits;
pdd const q = s.var(s.m_names.mk_name(p));
constraint_dedup::bv_ext_args const args = {true, q.var(), bit_width};
constraint_dedup::bv_ext_args const args = {true, q.var(), extra_bits};
auto const it = m_dedup.m_bv_ext_expr.find_iterator(args);
if (it != m_dedup.m_bv_ext_expr.end())
return s.var(it->m_value);
pdd const v = s.var(s.add_var(bit_width));
pdd const v = s.var(s.add_var(v_sz));
m_dedup.m_bv_ext_expr.insert(args, v.var());
// (1) v[|p|-1:0] = p
s.add_eq(q, extract(v, p_sz - 1, 0));
// (2) Let h := v[bit_width-1:|p|]
pdd const h = extract(v, bit_width - 1, p_sz);
// (2) Let h := v[|v|-1:|p|]
pdd const h = extract(v, v_sz - 1, p_sz);
signed_constraint p_negative = s.uge(p, rational::power_of_two(p_sz - 1));
// (3) p < 2^(|p|-1) ==> h = 0
s.add_clause(p_negative, s.eq(h), false);

4
src/math/polysat/constraint_manager.h
View file

@ -172,8 +172,8 @@ namespace polysat {
pdd concat(pdd const& p, pdd const& q);
pdd concat(unsigned num_args, pdd const* args);
pdd zero_ext(pdd const& p, unsigned bit_width);
pdd sign_ext(pdd const& p, unsigned bit_width);
pdd zero_ext(pdd const& p, unsigned extra_bits);
pdd sign_ext(pdd const& p, unsigned extra_bits);
constraint* const* begin() const { return m_constraints.data(); }
constraint* const* end() const { return m_constraints.data() + m_constraints.size(); }

4
src/math/polysat/solver.h
View file

@ -419,10 +419,10 @@ namespace polysat {
pdd concat(unsigned num_args, pdd const* args) { return m_constraints.concat(num_args, args); }
/** Create expression for zero-extension of p */
pdd zero_ext(pdd const& p, unsigned bit_width) { return m_constraints.zero_ext(p, bit_width); }
pdd zero_ext(pdd const& p, unsigned extra_bits) { return m_constraints.zero_ext(p, extra_bits); }
/** Create expression for signed-extension of p */
pdd sign_ext(pdd const& p, unsigned bit_width) { return m_constraints.sign_ext(p, bit_width); }
pdd sign_ext(pdd const& p, unsigned extra_bits) { return m_constraints.sign_ext(p, extra_bits); }
/**
* Create terms for unsigned quot-rem

6
src/sat/smt/bv_polysat.cpp
View file

@ -89,10 +89,10 @@ namespace bv {
case OP_BSREM0: break;
case OP_BUREM0: break;
case OP_BSMOD0: break;
// TODO: what about those naked breaks above? is this handled elsewhere?
case OP_EXTRACT: polysat_extract(a); break;
case OP_CONCAT: polysat_concat(a); break;
case OP_ZERO_EXT: polysat_par_unary(a, [&](pdd const& p, unsigned sz) { return m_polysat.zero_ext(p, sz); }); break;
case OP_SIGN_EXT: polysat_par_unary(a, [&](pdd const& p, unsigned sz) { return m_polysat.sign_ext(p, sz); }); break;
@ -199,8 +199,8 @@ namespace bv {
void solver::polysat_par_unary(app* e, std::function<polysat::pdd(polysat::pdd,unsigned)> const& fn) {
pdd const p = expr2pdd(e->get_arg(0));
unsigned const sz = e->get_parameter(0).get_int();
polysat_set(e, fn(p, sz));
unsigned const par = e->get_parameter(0).get_int();
polysat_set(e, fn(p, par));
}
void solver::polysat_binary(app* e, std::function<polysat::pdd(polysat::pdd, polysat::pdd)> const& fn) {