Skip to content

Make z3_ctx pub #341

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jun 22, 2025
Merged

Make z3_ctx pub #341

merged 2 commits into from
Jun 22, 2025

Conversation

toolCHAINZ
Copy link
Contributor

@toolCHAINZ toolCHAINZ commented Mar 30, 2025

I'm working on writing Python bindings for some code that I have that uses z3.rs. I would like my bindings to be able to work seamlessly with python's z3 library (producing terms and assertions to be used in python's handle to a solver for instance). I'm writing an opinionated API around the assumption that Python is always "driving" and that we are ALWAYS using Python's global Z3 context (allocated once on first use, never dropped or moved).

Pyo3 has the requirement that any Rust type passing into Python cannot have a lifetime other than 'static, and all my structs have the z3.rs 'ctx lifetime.

I'm working around this by pulling in a pointer to Python's global Z3_Context and storing it in a thread_local RefCell<Z3_Context>. I have a second thread_local with a 'static reference to the contents of the RefCell.

If Context is #[repr(transparent)] then I believe I can safely transmute this reference into a &'static Context, which I can then use for all my FFI types.

I've already tried this and it seems to work fine, but to actually do this, I need the guarantee of transparent.

I don't think that making this change would break anything. I assume this is also a less dangerous change for z3.rs to make than allowing for constructing Context structs out of raw pointers in the high-level API.

@waywardmonkeys
Copy link
Contributor

If the field was pub, would you be able to use it?

@toolCHAINZ
Copy link
Contributor Author

Yes, that would work as well and be less gross! I'd just assumed there was a reason you didn't want to expose that.

@toolCHAINZ toolCHAINZ changed the title Mark Context as transparent Make z3_ctx pub Mar 30, 2025
@toolCHAINZ
Copy link
Contributor Author

I've changed the PR to just make it pub, as that seems a lot cleaner.

@waywardmonkeys waywardmonkeys merged commit c884dbc into prove-rs:master Jun 22, 2025
11 checks passed
@toolCHAINZ toolCHAINZ deleted the patch-1 branch June 23, 2025 09:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants