Need help in understading the counter example

问题:

Can somebody please explain why I am getting a counter example with this py code.

a = Int('a')    
def X(a):
  if (a == 3): 
    return 1
  else:
    return 2

z3.prove( X(a) == If (a == 3, 1, 2) )

counterexample [a = 3]

回答1:

Your function 'X' will always return '2' for all symbolic variables. That is:

from z3 import *

a = Int('a')

def X(a):
  if (a == 3):
    return 1
  else:
    return 2

print X(a)

will always print:

2

This is precisely why Z3 provides the If function. Python's 'if' does not work for symbolic values and the tests will simply take the else branch.

Aside:

I'd call this a weakness of the Python interface to Z3, since it's really weakly typed. Ideally, this program should be rejected because of the illegal use of if-then-else, but Python isn't a sufficiently strongly-typed language to give you that level of safety. Bindings to Z3 from other languages would reject the equivalent expression as type incorrect at compile time.

回答2:

X(.) is a Python function, not a logical or Z3 function. It is evaluated when it is called. This means that the value of X(a) in

z3.prove( X(a) == If (a == 3, 1, 2) )

is determined to be 2 before z3.prove is called, because a is an Int('a') (and not 3). In this particular case, it's easy to debug such problems by simply printing the Z3 expressions, e.g.

print( X(a) == If (a == 3, 1, 2) )

reports

If(a == 3, 1, 2) == 2