mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

no need to introduce names for zero_ext/sign_ext arguments

Browse source
This commit is contained in:
Jakob Rath 2023-08-07 15:44:06 +02:00
parent 5c53f588b7
commit 4b4f0558b4
2 changed files with 6 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -654,8 +654,7 @@ namespace polysat {
unsigned const v_sz = p_sz + extra_bits; unsigned const v_sz = p_sz + extra_bits;
if (p.is_val()) if (p.is_val())
return s.sz2pdd(v_sz).mk_val(p.val()); return s.sz2pdd(v_sz).mk_val(p.val());
pvar const p_name = s.m_names.mk_name(p); constraint_dedup::bv_ext_args const args = {{false, p, extra_bits}};
constraint_dedup::bv_ext_args const args = {false, p_name, extra_bits};
auto const it = m_dedup.m_bv_ext_expr.find_iterator(args); auto const it = m_dedup.m_bv_ext_expr.find_iterator(args);
if (it != m_dedup.m_bv_ext_expr.end()) if (it != m_dedup.m_bv_ext_expr.end())
return s.var(it->m_value); return s.var(it->m_value);
@ -663,7 +662,7 @@ namespace polysat {
pdd const V = s.var(v); pdd const V = s.var(v);
m_dedup.m_bv_ext_expr.insert(args, v); m_dedup.m_bv_ext_expr.insert(args, v);
// (1) v[|p|-1:0] = p // (1) v[|p|-1:0] = p
s.add_eq(extract(V, p_sz - 1, 0), s.var(p_name)); s.add_eq(extract(V, p_sz - 1, 0), p);
// (2) v < 2^|p| // (2) v < 2^|p|
s.add_ule(V, p.manager().max_value()); s.add_ule(V, p.manager().max_value());
return V; return V;
@ -675,15 +674,14 @@ namespace polysat {
unsigned const v_sz = p_sz + extra_bits; unsigned const v_sz = p_sz + extra_bits;
if (p.is_val()) if (p.is_val())
return s.sz2pdd(v_sz).mk_val(p.get_signed_val()); return s.sz2pdd(v_sz).mk_val(p.get_signed_val());
pdd const q = s.var(s.m_names.mk_name(p)); constraint_dedup::bv_ext_args const args = {{true, p, extra_bits}};
constraint_dedup::bv_ext_args const args = {true, q.var(), extra_bits};
auto const it = m_dedup.m_bv_ext_expr.find_iterator(args); auto const it = m_dedup.m_bv_ext_expr.find_iterator(args);
if (it != m_dedup.m_bv_ext_expr.end()) if (it != m_dedup.m_bv_ext_expr.end())
return s.var(it->m_value); return s.var(it->m_value);
pdd const v = s.var(s.add_var(v_sz, pvar_kind::internal)); pdd const v = s.var(s.add_var(v_sz, pvar_kind::internal));
m_dedup.m_bv_ext_expr.insert(args, v.var()); m_dedup.m_bv_ext_expr.insert(args, v.var());
// (1) v[|p|-1:0] = p // (1) v[|p|-1:0] = p
s.add_eq(q, extract(v, p_sz - 1, 0)); s.add_eq(extract(v, p_sz - 1, 0), p);
// (2) Let h := v[|v|-1:|p|] // (2) Let h := v[|v|-1:|p|]
pdd const h = extract(v, v_sz - 1, p_sz); pdd const h = extract(v, v_sz - 1, p_sz);
signed_constraint p_negative = s.uge(p, rational::power_of_two(p_sz - 1)); signed_constraint p_negative = s.uge(p, rational::power_of_two(p_sz - 1));

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

@ -43,11 +43,11 @@ namespace polysat {
vector<std::tuple<pdd, pdd, pvar, pvar>> m_div_rem_list; vector<std::tuple<pdd, pdd, pvar, pvar>> m_div_rem_list;
// zero_ext or sign_ext // zero_ext or sign_ext
using bv_ext_args = std::tuple<bool, pvar, unsigned>; using bv_ext_args = std::optional<std::tuple<bool, pdd, unsigned>>; // NOTE: this is only wrapped in optional because table2map requires a default constructor
using bv_ext_args_eq = default_eq<bv_ext_args>; using bv_ext_args_eq = default_eq<bv_ext_args>;
struct bv_ext_args_hash { struct bv_ext_args_hash {
unsigned operator()(bv_ext_args const& args) const { unsigned operator()(bv_ext_args const& args) const {
return mk_mix(std::get<0>(args), std::get<1>(args), std::get<2>(args)); return args ? mk_mix(std::get<0>(*args), std::get<1>(*args).hash(), std::get<2>(*args)) : 0;
} }
}; };
using bv_ext_expr_map = map<bv_ext_args, pvar, bv_ext_args_hash, bv_ext_args_eq>; using bv_ext_expr_map = map<bv_ext_args, pvar, bv_ext_args_hash, bv_ext_args_eq>;