prove-rs / z3.rs

Rust bindings for the Z3 solver.
337 stars 105 forks source link

Use an "implicit" `Context`? #261

Open waywardmonkeys opened 10 months ago

waywardmonkeys commented 10 months ago

It is tempting to move to using a thread_local!(static CONTEXT: Option<z3::Context> = None) and some helper functions to have a scoped Context ... this would let us remove a bunch (all?) of the Context parameters to the various functions in the z3 crate.

This would help make the API look more like the Python or JS APIs, while still letting people have multiple contexts if they need them.