CODEWITHSUNDEEP
pythonz3py
Anon
Anon

Reputation: 421

s Counterexamples for invalid model for Z3

This is an extension of the question: Use Z3 to find counterexamples for a 'guess solution' to a particular CHC system?

In the below code, I am trying to use Z3 to get s counterexamples to a guess candidate for I satisfying some CHC clauses:

from z3 import *


x, xp = Ints('x xp') 

P = lambda x: x == 0
B = lambda x: x < 5
T = lambda x, xp: xp == x + 1
Q = lambda x: x == 5 

s = 10

def Check(mkConstraints, I, P , B, T , Q):
    s = Solver()
    # Add the negation of the conjunction of constraints
    s.add(Not(mkConstraints(I, P , B, T , Q)))
    r = s.check()
    if r == sat:
        return s.model()
    elif r == unsat:
        return {}
    else:
        print("Solver can't verify or disprove, it says: %s for invariant %s" %(r, I))

def System(I, P , B, T , Q):


    # P(x) -> I(x)
    c1 = Implies(P(x), I(x))

    # P(x) /\ B(x) /\ T(x,xp) -> I(xp) 
    c2 = Implies(And(B(x), I(x), T(x, xp)) , I(xp))

    # I(x) /\ ~B(x) -> Q(x)
    c3 = Implies(And(I(x), Not(B(x))), Q(x))

    return And(c1, c2, c3)


cex_List = []
I_guess = lambda x: x < 3


for i in range(s):
    cex = Check(System, I_guess, P , B , T , Q)
    I_guess = lambda t: Or(I_guess(t) , t == cex['x'])
    cex_List.append( cex[x] )

print(cex_List )

The idea is to use Z3 to learn a counterexample x0 for guess invariant I, then run Z3 to learn a counterexample for I || (x == x0) and so on till we get s counterexamples. However the following code gives 'RecursionError: maximum recursion depth exceeded '. I am confused because I am not even recursing with depth > 1 anywhere. Could anyone describe what's going wrong?

Upvotes: 0

Views: 92

Answers (1)

alias
alias

Reputation: 30418

Your problem really has nothing to do with z3; but rather a Python peculiarity. Consider this:

f = lambda x: x
f = lambda x: f(x)

print(f(5))

If you run this program, you'll also see that it falls in to the same infinite-recursion loop, since by the time you "get" to the inner f, the outer f is bound to itself again. In your case, this is exhibited in the line:

    I_guess = lambda t: Or(I_guess(t) , t == cex['x'])

which falls into the same trap by making I_guess recursive, which you did not intend.

The way to avoid this is to use an intermediate variable. It's ugly and counter-intuitive but that's the way of the python! For the example above, you'd write it as:

f = lambda x: x
g = f
f = lambda x: g(x)

print(f(5))

So, you need to do the same trick for your I_guess variable. Note that since you're updating the function iteratively, you need to make sure to remember the function in each step, instead of using the same name over and over. That is, capture the old version each time you create the new function. When applied to the above case, it'll be something like:

f = lambda x: x
f = lambda x, old_f=f: old_f(x)

print(f(5))

This'll make sure the iterations don't clobber the captured function. Applying this idea to your problem, you can code as follows:

for i in range(s):
    cex = Check(System, I_guess, P, B, T, Q)
    I_guess = lambda t, old_I_guess=I_guess: Or(old_I_guess(t), t == cex[x])
    cex_List.append(cex[x])

When run, this prints:

[2, 2, 2, 2, 2, 2, 2, 2, 2, 2]

without any infinite-recursion problem. (Whether this is the correct output or what you really wanted to do, I'm not sure. Looks to me like you need to tell z3 to give you a "different" solution, and maybe you've forgotten to do that. But that's a different question. We're really discussing a Python issue here, not z3 modeling.)

Upvotes: 3

Related Questions