mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

mk_concat

Browse source
This commit is contained in:
Jakob Rath 2023-07-20 17:27:55 +02:00
parent b725b61c57
commit 3e23742bcf
1 changed files with 22 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -729,30 +729,29 @@ namespace polysat {
} }
pvar slicing::mk_concat(unsigned num_args, pvar const* args) { pvar slicing::mk_concat(unsigned num_args, pvar const* args) {
NOT_IMPLEMENTED_YET(); enode_vector& slices = m_tmp3;
return null_var; SASSERT(slices.empty());
#if 0 unsigned total_width = 0;
// v := p ++ q (new variable of size |p| + |q|) for (unsigned i = 0; i < num_args; ++i) {
// v[:|q|] = p enode* s = var2slice(args[i]);
// v[|q|:] = q slices.push_back(s);
unsigned const p_sz = p.power_of_2(); total_width += width(s);
unsigned const q_sz = q.power_of_2();
unsigned const v_sz = p_sz + q_sz;
if (p.is_val() && q.is_val()) {
rational const val = p.val() * rational::power_of_two(q_sz) + q.val();
return m_solver.sz2pdd(v_sz).mk_val(val);
} }
if (p.is_val()) { // NOTE: we use concat nodes to deduplicate (syntactically equal) concat expressions.
} // we might end up reusing variables that are not introduced by mk_concat (if we enable the variable re-use optimizatio in mk_extract),
if (q.is_val()) { // but because such congruence nodes are only added over direct descendants, we do not get unwanted dependencies from this re-use.
} // (but note that the nodes from mk_concat are not only over direct descendants)
pvar const v = m_solver.add_var(v_sz); enode* concat = mk_concat_node(slices);
enode_vector tmp; pvar v = slice2var(concat);
tmp.push_back(pdd2slice(p)); if (v != null_var)
tmp.push_back(pdd2slice(q)); return v;
VERIFY(merge(tmp, var2slice(v), dep_t())); v = m_solver.add_var(total_width);
return m_solver.var(v); enode* sv = var2slice(v);
#endif VERIFY(merge(slices, sv, dep_t()));
// NOTE: add_concat_node must be done after merge to preserve the invariant: "a base slice is never equivalent to a congruence node".
add_concat_node(sv, concat);
slices.reset();
return v;
} }
pvar slicing::mk_concat(std::initializer_list<pvar> args) { pvar slicing::mk_concat(std::initializer_list<pvar> args) {