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

Additional shortcuts for extract/concat

Browse source
This commit is contained in:
Jakob Rath 2023-08-07 15:33:51 +02:00
parent bc0119f333
commit 5c53f588b7
2 changed files with 16 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -592,6 +592,8 @@ namespace polysat {
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; unsigned const v_sz = hi - lo + 1;
if (p.power_of_2() == v_sz)
return p;
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);
@ -627,7 +629,18 @@ namespace polysat {
return args[0]; return args[0];
if (num_args == 2) if (num_args == 2)
return concat(args[0], args[1]); return concat(args[0], args[1]);
// TODO: special cases when args are values? if (std::all_of(args, args + num_args, [](pdd const& p) { return p.is_val(); })) {
rational val;
unsigned sz = 0;
for (unsigned i = num_args; i-- > 0; ) {
pdd const& p = args[i];
if (!p.is_zero())
val += p.val() * rational::power_of_two(sz);
sz += p.power_of_2();
}
return s.sz2pdd(sz).mk_val(val);
}
// TODO: special cases when some of the arguments are values?
pvar_vector pvar_args; pvar_vector pvar_args;
for (unsigned i = 0; i < num_args; ++i) for (unsigned i = 0; i < num_args; ++i)
pvar_args.push_back(s.m_names.mk_name_even_if_value(args[i])); pvar_args.push_back(s.m_names.mk_name_even_if_value(args[i]));

2
src/math/polysat/slicing.cpp
View file

@ -1031,6 +1031,8 @@ namespace polysat {
pvar slicing::mk_extract(pvar src, unsigned hi, unsigned lo) { pvar slicing::mk_extract(pvar src, unsigned hi, unsigned lo) {
LOG_H3("mk_extract: v" << src << "[" << hi << ":" << lo << "] size(v" << src << ") = " << m_solver.size(src)); LOG_H3("mk_extract: v" << src << "[" << hi << ":" << lo << "] size(v" << src << ") = " << m_solver.size(src));
if (m_solver.size(src) == hi - lo + 1)
return src;
extract_args args{src, hi, lo}; extract_args args{src, hi, lo};
auto it = m_extract_dedup.find_iterator(args); auto it = m_extract_dedup.find_iterator(args);
if (it != m_extract_dedup.end()) if (it != m_extract_dedup.end())