问题:

I'm getting unexpected results with some script using Python API of Z3. I think that I'm misunderstanding some process or simply using some command wrong. For example, suppose I have the following script:

from z3 import *

x = Int('x')

def g(x):
    if x == 0:
       return 1
    elif x > 0:
       return x**(x+1)

s = Solver()
s.add(g(x) > x)
print s.check()
if s.check()== sat:
    m = s.model()
    m.evaluate(x, model_completion=True)
    print m

This will return the following output:

sat
[x = 0]

That it's OK, but if I substitute s.add(g(x) > x) by s.add(x > 1, g(x) > x), this returns unsat. I was expecting something like:

sat
[x = 2]

Can anybody help me to understand what's going on?

回答1:

Python's if-then-else does not translate to Z3's if-then-else. You have to use the "If" function. See here: https://github.com/Z3Prover/z3/blob/master/src/api/python/z3.py#L1092

回答2:

My Python skills are slightly underdeveloped, but I think the crucial concept underlying this problem is that Python functions do not translate to Z3 functions, e.g., if x == 0: ... will not create a Z3 function that checks all possible values of x. The easiest way to check is to just print the solver, so that it will show you the constraints, just add print s. In your unsatisfiable case, I get [x > 1, x < 1], which is indeed unsatisfiable.