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
.
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
z4_solver-2022.12.18.1.tar.gz
(15.6 kB
view hashes)
Built Distribution
Close
Hashes for z4_solver-2022.12.18.1-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | fc1f36058a282e3f6d8dcd7033bbaa549bd7b4681d80736a2cc1e962445bda14 |
|
MD5 | 8e5513c8e273d47ad7abec8e8c0e1e7b |
|
BLAKE2b-256 | 14f335efa4fb25ff920b80b929e13b5442413799b3c470558f5a6c815a66b5f6 |