Merge prove-rs/z3 master #2
Open
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* Add basic support for vcpkg. Use vcpkg-rs to manage z3 instead. A non-default feature vcpkg is added.
This is faster than having it do a build of Z3 as it does now and by running it on macOS against the brew installed Z3, it is going to be a more recent version of Z3 than what the system Z3 on Linux would be.
Instead of building the lib and then doing the tests, just do the tests. Otherwise, we end up building the lib twice. This also: * No longer uses `-vv` for very verbose output. * Uses `--workspace` instead of `--all`.
This is always on now.
This moves the code for linking against the C++ stdlib from just happening for a bundled build to happening for any build. It also adds a case for the Android C++ stdlib and hooks up re-running the build script if the `CXXSTDLIB` env var changes.
This uses the import of `std::env` in more places to shorten code and fixes some things pointed out by clippy. Also, since a const was only used in a single function, move it inside that function.
This is in addition to running them against it on Linux.
The return value was missing a lifetime annotation connecting it to the context's lifetime `'ctx`, this left the Rust compiler to tie it to the lifetime of the `Solver` reference, which was too short. Fixes #262.
This renames the `static-link-z3` build feature to `bundled` but leaves a bit around for now to maintain compatibility. It also improves the README's discussion a little bit to mention `vcpkg`.
This is from the C API (where I had added it in 2019).
This was added after we'd generated the bindings and so it needed to be added by hand.
Expose API to convert solver into SMT-LIB2 format
This adds support for `Z3_mk_re_allchars`, `Z3_mk_re_diff`, and `Z3_mk_re_power`.
This helps find the lib and includes more accurately than not using it. This builds on previous work by @poscat0x04 and @wtdcode.
The answer varies between versions of Z3.
An update to emscripten brought a newer compiler and that found a longstanding bug in Z3 that broke compilation. For now, use a slightly older version until a new version of Z3 (after 4.13.0) is released with the fix. See Z3Prover/z3#7235 for the Z3 fix.
This fixes an issue when using a more recent set of cmake policies with linking debug builds on Windows.
Update bundled Z3 to z3 4.12.3.
* Add new regexp operations * Z3_mk_re_option typo? * Attempt at testing Regexp * Use from_str instead of new_const
Add some missing optimize APIs
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.