Skip to content

tyilo/z4

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

21 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

z4

PyPI

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 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.

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

Releases

No releases published

Packages

No packages published

Languages