Welcome to z3.rs Discussions!

[toolCHAINZ]

👋 Welcome!

We’re using Discussions as a place to connect with other members of our community. We hope that you:

• Ask questions you’re wondering about.
• Share ideas.
• Engage with other community members.
• Welcome others and are open-minded. Remember that this is a community we
  build together 💪.

To get started, comment below with an introduction of yourself and tell us about what you do with this community.

[Evian-Zhang]

Hey I'm using this crate as the solver backend for symbolic execution (which is a program analysis algorithm to determine if certain execution path can be triggered).

I know little about the internal mechanism of SMT, while I have been using Rust for over 5 years with sufficient experience. I have just started to use this crate, and have three main concerns that I would like to help to improve:

1. Is there any MSRV (Minimum-Supported-Rust-Version) policy in this crate? If not, shall we upgrade to Rust 2024 edition? The newer edition means we can use potentially more features, and have potentially more optimization.
2. Most of the API wrappers in Rust declare themselves as no_std, which means they do not need to use platform-specific features that Rust std provides. Shall we make this crate no_std? If so, the most difference is that we need to use std like core::borrow::Borrow instead of std::borrow::Borrow.
3. There are lots of assert! across the crate. Shall we expose a feature to control whether to enable assert? This feature could be enabled by default, and optional disabled to make execution faster.

I'm happy to hear your opinion, and if you think any of the three ideas are acceptable, I'm willing to file a PR.

[Pat-Lafon]

But if you are looking for a way to help out, I think the edition change might be worth trying. Note however that the crate is 2 editions behind so it may be a little more work than you expect(though the ci does use stable rust so they aren't pinning to a specific version). If you wanted to try this, you might break it up across 2 prs for clarity. Ultimately, there might be a broader discussion to be had around msrv.

[toolCHAINZ]

On a slightly related note, yeah I had thought about bumping the MSRV as well. I don't have a good feeling for how widely this library is used, so wouldn't want to break it for anyone unnecessarily, but if edition upgrades/MSRV bumps can clean things up I'm all for it.

I've also been thinking we should consider bumping to 1.0. This library clearly does get SOME use and semantic versioning with all three numbers available would be nice. and I think actual breaking changes are fairly rare now.

[Pat-Lafon]

Yeah, I think it's pretty reasonable to avoid unnecessary breaking changes.

I would suggest waiting a little bit to see what changes shake out(as development had kinda slowed for a bit). Consider some of the discussion around whether some APIs should actually be returning Result or not. Some of the other discussions around whether arguments are passed by ownership, by reference, or by some variation like impl AsRef... I think there might be some opportunities to improve the ergonomics of this crate if you are interested(that may need breaking changes).

There is also the factor that while the crate is pre-1.0, at lot of people don't get unintentionally broken mainly because people don't/are slow to upgrade(Consider the version numbers for the download statistics on crates.io). I'm not sure if there is a demand/need for a 1.0 unless you are currently happy with the crate as it is.

[toolCHAINZ]

Oh yeah absolutely no intentions to actually push to 1.0 soon. Was just thinking about whether there would be a right time to do so and how that should be decided.

Totally agreed there's some ergonomic shortcomings in the library; I'd love to get those fixed up as well (though I don't know if I personally have the time).

[toolCHAINZ]

In a perfect world, I would want the following:

• Send (but maybe not Sync) Ast/Solver/Model Guard types that enforce translation to a new context to be used
• The elimination of the 'ctx lifetime
• A thread local "default context" like waywardmonkeys suggested

I think those three things would get the ergonomics of the library to an even higher level than the python API (because the python API has a single shared context across threads and so just segfaults if you try to do anything fancy (or else pay the ergonomic price of shipping around context handles, which are easy to forget)

Idk how realistic those goals are (especially the first two); I need to learn more about the low level api and the existing attempts at refactoring it.