mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 13:54:53 +00:00
Code Activity

Add clarifying comments for hash matrix overflow safety and cache validity

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-02 21:16:46 +00:00
parent cfea2db8bf
commit fbd3d445e2
2 changed files with 8 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -289,6 +289,10 @@ namespace euf {
static const unsigned HASH_BASE = 31;
// Compute a 2x2 polynomial hash matrix for associativity-respecting hashing.
// Unsigned overflow is intentional and well-defined (mod 2^32).
// M[0][0] tracks HASH_BASE^(num_leaves), which is always nonzero since
// HASH_BASE is odd. M[0][1] is the actual hash value.
void sgraph::compute_hash_matrix(snode* n) {
if (n->is_empty()) {
// identity matrix: concat with empty is identity
@ -310,6 +314,7 @@ 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;
n->m_hash_matrix[0][0] = HASH_BASE;
n->m_hash_matrix[0][1] = v;

4
src/ast/euf/euf_snode.h
View file

@ -109,7 +109,9 @@ namespace euf {
unsigned level() const { return m_level; }
unsigned length() const { return m_length; }
// associativity-respecting hash: cached if the 2x2 matrix is non-zero
// associativity-respecting hash: cached if the 2x2 matrix is non-zero.
// M[0][0] = HASH_BASE^(num_leaves) which is always nonzero since HASH_BASE
// is odd and gcd(odd, 2^32) = 1, so the check is safe.
bool has_cached_hash() const { return m_hash_matrix[0][0] != 0; }
unsigned assoc_hash() const { return m_hash_matrix[0][1]; }