mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-11 17:46:20 +00:00
Code Activity

Different slices of the same variable have the same hash

Browse source
This commit is contained in:
CEisenhofer 2026-06-28 14:36:35 +02:00
parent 79cdc91a75
commit cc42304f60
4 changed files with 56 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/ast/euf/euf_sgraph.cpp
View file

@ -28,6 +28,8 @@ namespace euf {
m(m),
m_seq(m),
m_rewriter(m),
m_th_rewriter(m),
m_sk(m, m_th_rewriter),
m_egraph(eg),
m_str_sort(m_seq.str.mk_string_sort(), m),
m_pin(m) {
@ -305,7 +307,7 @@ namespace euf {
}
}
static const unsigned HASH_BASE = 31;
static constexpr unsigned HASH_BASE = 31;
// Compute a 2x2 polynomial hash matrix for associativity-respecting hashing.
// Unsigned overflow is intentional and well-defined (mod 2^32).
@ -333,7 +335,20 @@ namespace euf {
else {
// leaf/token: [[HASH_BASE, value], [0, 1]]
// +1 avoids zero hash values; wraps safely on unsigned overflow
unsigned v = n->get_expr() ? n->get_expr()->get_id() + 1 : n->id() + 1;
// for slices it is the same as its parent
expr* e = n->get_expr();
SASSERT(e);
unsigned v;
if (m_sk.is_slice(e)) {
do {
// get root variable
e = to_app(e)->get_arg(0);
} while (m_sk.is_slice(e));
v = e->get_id();
}
else
v = e->get_id() + 1;
n->m_hash_matrix[0][0] = HASH_BASE;
n->m_hash_matrix[0][1] = v;
n->m_hash_matrix[1][0] = 0;

2
src/ast/euf/euf_sgraph.h
View file

@ -83,6 +83,8 @@ namespace euf {
ast_manager& m;
seq_util m_seq;
seq_rewriter m_rewriter;
th_rewriter m_th_rewriter;
seq::skolem m_sk;
egraph& m_egraph;
region m_region;
snode_vector m_nodes;

48
src/smt/seq/seq_nielsen.cpp
View file

@ -2124,13 +2124,14 @@ namespace seq {
return reason_is_string_only(n->m_reason);
}
std::vector<unsigned> nielsen_graph::compute_node_signature(nielsen_node const* n) const {
std::vector<unsigned> nielsen_graph::compute_node_signature(nielsen_node const* n) {
std::vector<unsigned> sig;
// string equalities (order-independent)
{
std::vector<std::pair<unsigned,unsigned>> v;
for (auto const& e : n->str_eqs())
for (auto const& e : n->str_eqs()) {
v.emplace_back(e.m_lhs->id(), e.m_rhs->id());
}
std::sort(v.begin(), v.end());
sig.push_back(static_cast<unsigned>(v.size()));
for (auto const& [a,b] : v) { sig.push_back(a); sig.push_back(b); }
@ -2139,9 +2140,10 @@ namespace seq {
// string disequalities
{
std::vector<std::pair<unsigned,unsigned>> v;
for (auto const& d : n->str_deqs())
for (auto const& d : n->str_deqs()) {
v.emplace_back(d.m_lhs->id(), d.m_rhs->id());
std::sort(v.begin(), v.end());
}
std::ranges::sort(v);
sig.push_back(static_cast<unsigned>(v.size()));
for (auto const& [a,b] : v) { sig.push_back(a); sig.push_back(b); }
}
@ -2154,9 +2156,13 @@ namespace seq {
static_cast<unsigned>(mm.m_kind),
mm.m_root ? mm.m_root->id() : UINT_MAX,
mm.m_nu, mm.m_discharged ? 1u : 0u });
std::sort(v.begin(), v.end());
std::ranges::sort(v);
sig.push_back(static_cast<unsigned>(v.size()));
for (auto const& a : v) for (unsigned x : a) sig.push_back(x);
for (auto const& a : v) {
for (unsigned x : a) {
sig.push_back(x);
}
}
}
sig.push_back(UINT_MAX);
// character-range constraints (per symbolic unit)
@ -2165,22 +2171,38 @@ namespace seq {
for (auto const& [uid, cr] : n->char_ranges()) {
std::vector<unsigned> entry;
entry.push_back(uid);
for (auto const& rg : cr.first.ranges()) { entry.push_back(rg.m_lo); entry.push_back(rg.m_hi); }
for (auto const& rg : cr.first.ranges()) {
entry.push_back(rg.m_lo);
entry.push_back(rg.m_hi);
}
v.push_back(std::move(entry));
}
std::sort(v.begin(), v.end());
sig.push_back(static_cast<unsigned>(v.size()));
for (auto const& e : v) { sig.push_back(static_cast<unsigned>(e.size())); for (unsigned x : e) sig.push_back(x); }
for (auto const& e : v) {
sig.push_back(static_cast<unsigned>(e.size()));
for (unsigned x : e) {
sig.push_back(x);
}
}
}
return sig;
}
dep_tracker nielsen_graph::node_all_deps(nielsen_node const* n) {
dep_tracker nielsen_graph::node_all_deps(nielsen_node const* n) const {
dep_tracker d = nullptr;
for (auto const& e : n->str_eqs()) d = m_dep_mgr.mk_join(d, e.m_dep);
for (auto const& q : n->str_deqs()) d = m_dep_mgr.mk_join(d, q.m_dep);
for (auto const& mm : n->str_mems()) d = m_dep_mgr.mk_join(d, mm.m_dep);
for (auto const& [uid, cr] : n->char_ranges()) d = m_dep_mgr.mk_join(d, cr.second);
for (auto const& e : n->str_eqs()) {
d = m_dep_mgr.mk_join(d, e.m_dep);
}
for (auto const& q : n->str_deqs()) {
d = m_dep_mgr.mk_join(d, q.m_dep);
}
for (auto const& mm : n->str_mems()) {
d = m_dep_mgr.mk_join(d, mm.m_dep);
}
for (auto const& [uid, cr] : n->char_ranges()) {
d = m_dep_mgr.mk_join(d, cr.second);
}
return d;
}

4
src/smt/seq/seq_nielsen.h
View file

@ -1066,9 +1066,9 @@ namespace seq {
// Canonical structural signature of a node (string equalities,
// disequalities, memberships incl. view/guard metadata, char ranges).
// Two nodes with equal signatures have identical string constraints.
std::vector<unsigned> compute_node_signature(nielsen_node const* n) const;
static std::vector<unsigned> compute_node_signature(nielsen_node const* n);
// Union of all constraint deps of a node (sound over-approx conflict).
dep_tracker node_all_deps(nielsen_node const* n);
dep_tracker node_all_deps(nielsen_node const* n) const;
// True iff the node's UNSAT depends only on string/regex constraints.
bool node_unsat_string_only(nielsen_node const* n) const;