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 z4solver
.
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 counterexample a = 1
. Of course 2 * 1 = 2
which is less than 1
.
Let's try again with the assumption that a
must be nonnegative:
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_solver2022.12.18.1.tar.gz
(15.6 kB
view hashes)
Built Distribution
Close
Hashes for z4_solver2022.12.18.1py3noneany.whl
Algorithm  Hash digest  

SHA256  fc1f36058a282e3f6d8dcd7033bbaa549bd7b4681d80736a2cc1e962445bda14 

MD5  8e5513c8e273d47ad7abec8e8c0e1e7b 

BLAKE2b256  14f335efa4fb25ff920b80b929e13b5442413799b3c470558f5a6c815a66b5f6 