z3++
Project description
z4
z3 with some improvements:
-
BitVec
:- Change the right shift operation to be logical instead of arithmetic
-
Add the
ByteVec
class -
Add some helper methods for solving:
easy_solve
find_all_solutions
easy_prove
-
Add some helper methods for optimizing:
maximize
minimize
-
Add some helper functions for z3 variables/constants:
BoolToInt
Sgn
TruncDiv
Features implemented upstream
These features were first provided by z4, before z3 included these features. They have now been removed from z4.
-
BoolRef
: -
Helper functions:
Abs
cf08cdf
Usage
Install with pip install z4-solver
.
easy_solve
import z4
a, b = z4.Ints("a b")
print(z4.easy_solve([a <= 10, b <= 10, a + b == 15]))
Output:
[b = 5, a = 10]
find_all_solutions
import z4
a, b = z4.Ints("a b")
print(*z4.find_all_solutions([a <= 10, b <= 10, a + b == 15]), sep="\n")
Output:
[b = 5, a = 10]
[b = 6, a = 9]
[b = 7, a = 8]
[b = 8, a = 7]
[b = 9, a = 6]
[b = 10, a = 5]
easy_prove
Let's try and prove that 2 * a >= a
for all integers a
:
import z4
a = z4.Int("a")
print(z4.easy_prove(2 * a >= a))
Output
Traceback (most recent call last):
...
z4.Z3CounterExample: [a = -1]
This isn't true so we get an exception with the counter-example a = -1
. Of course 2 * -1 = -2
which is less than -1
.
Let's try again with the assumption that a
must be non-negative:
print(z4.easy_prove(z4.Implies(a >= 0, 2 * a >= a)))
Output:
True
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
Built Distribution
File details
Details for the file z4_solver-2024.12.14.1.tar.gz
.
File metadata
- Download URL: z4_solver-2024.12.14.1.tar.gz
- Upload date:
- Size: 24.0 kB
- Tags: Source
- Uploaded using Trusted Publishing? No
- Uploaded via: uv/0.5.9
File hashes
Algorithm | Hash digest | |
---|---|---|
SHA256 |
fb7bc4de7309162b02f5ada3e2e872fe2b2adc8931ef732b868f55cb97242d3a
|
|
MD5 |
37fd0194646be468db9fab1d6fc2a4d6
|
|
BLAKE2b-256 |
1fcc13844191feac88cf273175b009cf783728c63c09e283f8860f8c43ab23ba
|
File details
Details for the file z4_solver-2024.12.14.1-py3-none-any.whl
.
File metadata
- Download URL: z4_solver-2024.12.14.1-py3-none-any.whl
- Upload date:
- Size: 16.4 kB
- Tags: Python 3
- Uploaded using Trusted Publishing? No
- Uploaded via: uv/0.5.9
File hashes
Algorithm | Hash digest | |
---|---|---|
SHA256 |
d5ca36cb1709583880ecce6ee73eae9efd6bf30b5a210ddedf188d90769c24f4
|
|
MD5 |
5e42ce07ea072fcc81ecff6ea40c5567
|
|
BLAKE2b-256 |
0186527549af900f7034b0cba141be987f5b1e5096e6399d5c0b490c6892e563
|