mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

refactor creation of concat nodes

Browse source
This commit is contained in:
Jakob Rath 2023-07-20 17:11:01 +02:00
parent 4b3cfa8c50
commit e45d13ffdf
2 changed files with 26 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -231,20 +231,31 @@ namespace polysat {
return alloc_enode(a, 0, nullptr, var);
}
slicing::enode* slicing::mk_concat_node(enode_vector const& slices) {
ptr_vector<expr> args;
for (enode* n : slices)
args.push_back(n->get_expr());
app_ref a(m_ast.mk_app(mk_concat_decl(args), args), m_ast);
return find_or_alloc_enode(a, slices.size(), slices.data(), null_var);
}
void slicing::add_concat_node(enode* s, enode* concat) {
SASSERT(slice2var(s) != null_var); // all concat nodes should point to a variable node
SASSERT(is_app(concat->get_expr()));
slice_info& concat_info = m_info[concat->get_id()];
SASSERT(!concat_info.slice); // not yet set
concat_info.slice = s;
m_egraph.merge(s, concat, encode_dep(dep_t()));
}
void slicing::add_congruence(pvar v) {
enode_vector& base = m_tmp2;
SASSERT(base.empty());
enode* sv = var2slice(v);
get_base(sv, base);
// Add equation v == concat(s1, ..., sn)
ptr_vector<expr> args;
for (enode* n : base)
args.push_back(n->get_expr());
app* a = m_ast.mk_app(mk_concat_decl(args), args);
enode* concat = find_or_alloc_enode(a, base.size(), base.data(), null_var);
info(concat).slice = sv;
add_concat_node(sv, mk_concat_node(base));
base.clear();
m_egraph.merge(sv, concat, encode_dep(dep_t()));
}
void slicing::add_congruence_if_needed(pvar v) {
@ -394,7 +405,7 @@ namespace polysat {
slicing::enode* slicing::mk_value_slice(rational const& val, unsigned bit_width) {
SASSERT(0 <= val && val < rational::power_of_two(bit_width));
app* a = m_bv->mk_numeral(val, bit_width);
app_ref a(m_bv->mk_numeral(val, bit_width), m_ast);
enode* s = find_or_alloc_enode(a, 0, nullptr, null_var);
s->mark_interpreted();
SASSERT(s->interpreted());
@ -881,6 +892,10 @@ namespace polysat {
if (is_slice(s) && !has_sub(s)) {
VERIFY(all_of(euf::enode_class(s), [&](enode* n) { return is_slice(n); }));
}
// all concat nodes point to a variable slice
if (is_concat(s)) {
VERIFY(slice2var(s) != null_var);
}
// properties below only matter for representatives
if (!s->is_root())
continue;

3
src/math/polysat/slicing.h
View file

@ -110,6 +110,9 @@ namespace polysat {
void add_congruence_if_needed(pvar v);
func_decl* mk_concat_decl(ptr_vector<expr> const& args);
enode* mk_concat_node(enode_vector const& slices);
// Add s = concat(s1, ..., sn)
void add_concat_node(enode* s, enode* concat);
static void* encode_dep(dep_t d);
static dep_t decode_dep(void* d);