z3++
Project description
z4
z3 with some improvements:
- Change the right shift operation on
BitVec
's to be logical instead of arithmetic - Add the
ByteVec
class - Some helper methods for solving:
easy_solve
find_all_solutions
easy_prove
- Add some helper functions for z3 variables/constants:
BoolToInt
Sgn
Abs
TruncDiv
Usage
Install with pip install z4-solver
.
Standard usage:
import z4
a, b = z4.Ints("a b")
print(*z4.find_all_solutions([a > 0, b > 0, a % b == 3, a > b, a + b == 19]), sep="\n")
Output:
[b = 4, a = 15, div0 = [else -> 3], mod0 = [else -> 3]]
[b = 8, a = 11, div0 = [else -> 1], mod0 = [else -> 3]]
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
z4-solver-2021.12.25.1.tar.gz
(15.0 kB
view hashes)
Built Distribution
Close
Hashes for z4_solver-2021.12.25.1-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | dc03e224463dd54b4d789f1880bf3a742cc00c32e33765e0970e0503ff9e5123 |
|
MD5 | 80192cd25102771c9783e00e03f6bec9 |
|
BLAKE2b-256 | 255cc68e6ba2e237ab737e03d7867ba3f00f99de34e633642c1c64675e50958d |