z3++
Project description
z4
z3 with some improvements:
- Change the right shift operation on
BitVec
's to be logical instead of arithmetic - Extend the
*
operation onBoolRef
's to work between twoBoolRef
's. - Add additional operations to
BoolRef
's:+
, returning an Int kind such that e.gTrue+True+False==2
&
, utilizingAnd()
|
, utilizingOr()
~
, utilizingNot()
- 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-2022.12.18.0.tar.gz
(15.2 kB
view hashes)
Built Distribution
Close
Hashes for z4_solver-2022.12.18.0-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | ba05e30b2a56cd14f3854ea8ae404452fb5221206e16ac2f88efd346d28be805 |
|
MD5 | 878ef5f0fe2fea131787d98c142dff5b |
|
BLAKE2b-256 | 3c2b02faee85f1529054ba53cf05e303cf94ae1c29eb7b24068061f9f783aa12 |