z3 with some improvements:
- Change the right shift operation on
BitVec's to be logical instead of arithmetic
- Add the
- Some helper methods for solving:
- Add some helper functions for z3 variables/constants:
pip install z4-solver.
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")
[b = 4, a = 15, div0 = [else -> 3], mod0 = [else -> 3]] [b = 8, a = 11, div0 = [else -> 1], mod0 = [else -> 3]]
Release history Release notifications | RSS feed
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Hashes for z4_solver-2021.12.25.1-py3-none-any.whl