mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-13 12:25:37 +00:00
Code Activity

Fix Homebrew/macOS build break by defining obj_map::key_data constructors (#9815)

Browse source 
Homebrew upgrade from Z3 4.15.4 to 4.16.0 failed on macOS 12 during
`src/ast/ast.cpp` compilation because `obj_map::key_data` was used with
`(key, value)` construction but only implicit constructors existed. This
surfaced at `m_poly_roots.insert(new_node, new_node)` and similar map
operations.

- **Root cause addressed**
- `obj_map<Key, Value>::key_data` relied on implicit constructors, which
are insufficient under stricter toolchains when `key_data(k, v)` /
`key_data(k)` are instantiated via `obj_map` helpers.

- **Code change (minimal, targeted)**
- Added explicit struct constructors in `src/util/obj_hashtable.h` for:
    - default initialization
    - key-only construction (`key_data(Key* k)`)
    - key + lvalue value (`key_data(Key* k, Value const& v)`)
    - key + rvalue value (`key_data(Key* k, Value&& v)`)
- No behavioral changes to map semantics; this only makes existing call
sites well-formed across compilers.

- **Example of the change**
  ```c++
  struct key_data {
      Key * m_key = nullptr;
      Value m_value;
      key_data() = default;
      key_data(Key* k): m_key(k) {}
      key_data(Key* k, Value const& v): m_key(k), m_value(v) {}
      key_data(Key* k, Value&& v): m_key(k), m_value(std::move(v)) {}
      // ...
  };
  ```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-06-11 23:09:07 -07:00 • committed by GitHub
parent 05c9ece3d2
commit 054d71455d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/util/obj_hashtable.h
View file

@ -62,6 +62,10 @@ public:
struct key_data {
Key * m_key = nullptr;
Value m_value;
key_data() = default;
key_data(Key* k): m_key(k) {}
key_data(Key* k, Value const& v): m_key(k), m_value(v) {}
key_data(Key* k, Value&& v): m_key(k), m_value(std::move(v)) {}
Value const & get_value() const { return m_value; }
Key & get_key () const { return *m_key; }
unsigned hash() const { return m_key->hash(); }
@ -239,5 +243,3 @@ void erase_dealloc_value(obj_map<Key, Value*> & m, Key * k) {
dealloc(v);
}
}