smtlib-v0.3.0

This release changes how terms are stored. In 0.2.0 terms where all stored with 'static, making them Copy and easy to move around. The downside was that any constructed term would stick around forever. To mitigate this memory leak, while retaining Copy semantics 0.3.0 introduces the concept of Storage. Essentially this means that terms are allocated in a shared buffer, arena style. This swaps out &'static with &'st, meaning that all terms now carry around a lifetime of their storage binding them to live exactly as long as that, and allowing the storage to be dropped and memory reclaimed as needed. The downside is that now one needs lifetime allocation and to pass a storage. The first downside is inevitable if we want statically enforced lifetimes, but we've tried to mitigate the second by storing pointers to storage in convenient places, allowing for writing stuff like x + 2 and having the resulting term be allocated seamlessly. An upside of using arena allocation, is that we open the possibility to interning terms, strings and slices plus arranging things more compactly in memory.

This update does contain quite a lot of breaking changes, but as a starting point for migration one we refer to this commit to give an idea of what's involved in updating.

smtlib-v0.2.0

Documentation

• Update backend doc links

Features

• [breaking] Remove async-trait crate and async, z3, cvc5 features
• [breaking] Remove Async{Driver,Solver} in favor of Tokio{Driver,Solver}

Miscellaneous Tasks

• Skip formatting generated files

Refactor

• Generate logics.rs in xtask rather than build.rs
• Generate ast.rs in xtask rather than build.rs

Misc

• Move some crate versions to root Cargo.toml