mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

fix bit width of extract on constants

Browse source
This commit is contained in:
Jakob Rath 2023-08-04 11:10:49 +02:00
parent d62aa82762
commit 2a2015f61d
2 changed files with 11 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -591,10 +591,11 @@ namespace polysat {
pdd constraint_manager::extract(pdd const& p, unsigned hi, unsigned lo) { pdd constraint_manager::extract(pdd const& p, unsigned hi, unsigned lo) {
SASSERT(hi >= lo); SASSERT(hi >= lo);
SASSERT(p.power_of_2() > hi); SASSERT(p.power_of_2() > hi);
unsigned const v_sz = hi - lo + 1;
if (p.is_val()) { if (p.is_val()) {
// p[hi:lo] = (p >> lo) % 2^(hi - lo + 1) // p[hi:lo] = (p >> lo) % 2^(hi - lo + 1)
rational q = mod2k(machine_div2k(p.val(), lo), hi - lo + 1); rational q = mod2k(machine_div2k(p.val(), lo), hi - lo + 1);
return p.manager().mk_val(q); return s.sz2pdd(v_sz).mk_val(q);
} }
if (lo == hi) { if (lo == hi) {
// could turn it into a single-bit constraint... unclear if that is useful // could turn it into a single-bit constraint... unclear if that is useful
@ -604,6 +605,7 @@ namespace polysat {
} }
pvar const src = s.m_names.mk_name(p); pvar const src = s.m_names.mk_name(p);
pvar const v = s.m_slicing.mk_extract(src, hi, lo); pvar const v = s.m_slicing.mk_extract(src, hi, lo);
SASSERT_EQ(s.var(v).power_of_2(), v_sz);
return s.var(v); return s.var(v);
} }

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

@ -184,6 +184,7 @@ namespace bv {
unsigned const lo = bv.get_extract_low(e); unsigned const lo = bv.get_extract_low(e);
auto const src = expr2pdd(e->get_arg(0)); auto const src = expr2pdd(e->get_arg(0));
auto const p = m_polysat.extract(src, hi, lo); auto const p = m_polysat.extract(src, hi, lo);
SASSERT_EQ(p.power_of_2(), hi - lo + 1);
polysat_set(e, p); polysat_set(e, p);
} }
@ -258,6 +259,10 @@ namespace bv {
force_push(); force_push();
pdd p = var2pdd(v1); pdd p = var2pdd(v1);
pdd q = var2pdd(v2); pdd q = var2pdd(v2);
// LOG("expr(v1) = " << mk_ismt2_pp(var2enode(v1)->get_expr(), m));
// LOG("expr(v2) = " << mk_ismt2_pp(var2enode(v2)->get_expr(), m));
// LOG("polysat_merge_eh: size(v1) = " << get_bv_size(v1) << ", size(v2) = " << get_bv_size(v2));
// LOG("polysat_merge_eh: " << p << " (width " << p.power_of_2() << ") " << q << " (width " << q.power_of_2() << ")");
auto sc = m_polysat.eq(p, q); auto sc = m_polysat.eq(p, q);
m_var_eqs.setx(m_var_eqs_head, std::make_pair(v1, v2), std::make_pair(v1, v2)); m_var_eqs.setx(m_var_eqs_head, std::make_pair(v1, v2), std::make_pair(v1, v2));
ctx.push(value_trail<unsigned>(m_var_eqs_head)); ctx.push(value_trail<unsigned>(m_var_eqs_head));
@ -364,9 +369,10 @@ namespace bv {
#ifndef NDEBUG #ifndef NDEBUG
IF_VERBOSE(8, IF_VERBOSE(8,
expr* e = var2enode(v)->get_expr(); expr* e = var2enode(v)->get_expr();
verbose_stream() << "polysat_set: " << expr_ref(e, m) << " -> " << p << std::endl; verbose_stream() << "polysat_set: " << expr_ref(e, m) << " [bv size " << get_bv_size(v) << "] -> " << p << " [pdd size " << p.power_of_2() << "]" << std::endl;
); );
#endif #endif
SASSERT_EQ(get_bv_size(v), p.power_of_2());
m_var2pdd.reserve(get_num_vars(), p); m_var2pdd.reserve(get_num_vars(), p);
m_var2pdd_valid.reserve(get_num_vars(), false); m_var2pdd_valid.reserve(get_num_vars(), false);
ctx.push(set_bitvector_trail(m_var2pdd_valid, v)); ctx.push(set_bitvector_trail(m_var2pdd_valid, v));