A tiny example of PyExZ3 usage that I came up with did not work as expected. Here is the example:
def d1(x,y):
if y < x - 2 :
return 7
else :
return 2
def d2(x,y):
if y > 3 :
return 10
else:
return 50
def d3(x,y):
if y < -x + 3 :
return 100
else :
return 200
def yolo(a,b):
return d1(a,b)+d2(a,b)+d3(a,b)
def expected_result():
return [ 112, 157, 152, 217, 212, 257, 252]
The above content is saved in FILE.py and tested (on Windows) with .\pyexz3.py FILE.py --start yolo.
I was expecting 7 paths but only 6 unique are found. One (resulting in 251) is listed twice.
Are my expectations wrong or does pyexz3 return incorrect results?
Looks like PyExZ3 is no longer maintained; so it's impossible to say if this is a bug in PyExZ3 or some incompatibility as z3 evolved over time. If you want to investigate that, you'll have to run it with a version of z3 that they claim to support; a release of z3 from around 2015. However, I'm not sure what good that'll do, as I doubt PyExZ3 will be "fixed" or revamped anytime soon.
If you're willing to use regular z3 programming, however, you can easily solve this problem with just regular z3 features. Of course, this requires you to "rewrite" the Python code to be z3-aware; a task that can be daunting in general, depending on what kind of Python programs you want to work with. The example you have given, however, is trivial to rewrite in this style:
from z3 import *
def d1(x, y): return If(y < x - 2 , 7, 2)
def d2(x, y): return If(y > 3 , 10, 50)
def d3(x, y): return If(y < -x + 3, 100, 200)
def yolo(a, b): return d1(a, b) + d2(a, b) + d3(a, b)
Once you have this, you can create a constraint for the resulting value based on symbolic inputs for a and b:
s = Solver()
a, b, r = Ints('a b r')
s.add(r == yolo(a, b))
With this set-up, we need one more ingredient. The all_smt function from Section 5.1 of https://theory.stanford.edu/~nikolaj/programmingz3.html. (The one right before the start of Section 5.2.) Once you have that included, it's easy to get all possible (and different) values for r with a simple iteration:
for i, m in enumerate(all_smt(s, [r])):
print(f"{i+1}. a = {m[a].as_long():>2d}, b = {m[b].as_long():>2d}, r = {m[r]}")
This prints:
1. a = 0, b = 0, r = 152
2. a = 7, b = 4, r = 217
3. a = 3, b = -1, r = 157
4. a = 4, b = 0, r = 257
5. a = 0, b = 4, r = 212
6. a = 1, b = 3, r = 252
7. a = -2, b = 4, r = 112
which I believe is the result you've been looking for.
For completeness, here's the whole script, including the all_smt function referred above:
from z3 import *
def d1(x, y): return If(y < x - 2 , 7, 2)
def d2(x, y): return If(y > 3 , 10, 50)
def d3(x, y): return If(y < -x + 3, 100, 200)
def yolo(a, b): return d1(a, b) + d2(a, b) + d3(a ,b)
s = Solver()
a, b, r = Ints('a b r')
s.add(r == yolo(a, b))
def all_smt(s, initial_terms):
def block_term(s, m, t):
s.add(t != m.eval(t, model_completion=True))
def fix_term(s, m, t):
s.add(t == m.eval(t, model_completion=True))
def all_smt_rec(terms):
if sat == s.check():
m = s.model()
yield m
for i in range(len(terms)):
s.push()
block_term(s, m, terms[i])
for j in range(i):
fix_term(s, m, terms[j])
yield from all_smt_rec(terms[i:])
s.pop()
yield from all_smt_rec(list(initial_terms))
for i, m in enumerate(all_smt(s, [r])):
print(f"{i+1}. a = {m[a].as_long():>2d}, b = {m[b].as_long():>2d}, r = {m[r]}")
While Python is a fine choice for scripting z3, it's not always the best choice for doing program-analysis tasks. For these sorts of problems functional languages like Haskell provide a better platform. In particular Haskell's SBV package comes with a "batteries included" approach to addressing these sorts of problems, taking advantage of the excellent features of the Haskell ecosystem for program analysis. So, if that's something that can fit into your environment, I'd recommend investigating using Haskell for such problems.
As an example, here's how we'd solve this very same problem in Haskell using the SBV library, which calls z3 (or other SMT solvers) under the hood:
import Data.SBV
d1, d2, d3, yolo :: (SInteger, SInteger) -> SInteger
d1 (x, y) = ite (y .< x - 2 ) 7 2
d2 (x, y) = ite (y .> 3 ) 10 50
d3 (x, y) = ite (y .< -x + 3) 100 200
yolo (a, b) = d1 (a, b) + d2 (a, b) + d3 (a, b)
paths :: IO AllSatResult
paths = allSat $ do
a <- sInteger "a"
b <- sInteger "b"
partition "r" $ yolo (a, b)
In this case, the code-complexity of the Python and Haskell versions is quite comparable, but for larger programs I think you'll find Haskell fares better. This prints:
Solution #1:
a = -2 :: Integer
b = 4 :: Integer
r = 112 :: Integer
Solution #2:
a = 0 :: Integer
b = 3 :: Integer
r = 252 :: Integer
Solution #3:
a = -1 :: Integer
b = 4 :: Integer
r = 212 :: Integer
Solution #4:
a = 3 :: Integer
b = 0 :: Integer
r = 257 :: Integer
Solution #5:
a = 2 :: Integer
b = -1 :: Integer
r = 157 :: Integer
Solution #6:
a = 7 :: Integer
b = 4 :: Integer
r = 217 :: Integer
Solution #7:
a = 0 :: Integer
b = 0 :: Integer
r = 152 :: Integer
Found 7 different solutions.