Code produces wrong result with ForAll, why?

Question

I am trying to use ForAll quantifier on b, so formula a * b == b with every b would give me a == 1 as result. I implemented this in the code below (Z3 python):

from z3 import *

a, b, a1 = BitVecs('a b a1', 32)

f = True
f = And(f, a1 == a * b)
f = And(f, a1 == b)

s = Solver()
s.add(ForAll(b, f))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

I expected Z3 gives me a = 1 at the output, but I got Unsat instead. Any idea on where the problem is?

(I suspect that I dont use ForAll properly, but not sure how to fix it)

Answer 1

What do you think about this:

a, b, a1 = BitVecs('a b a1', 32)

f = True
f = And(f, a1 == a * b)
g= True
g = And(f, a1 == b)

s = Solver()
s.add(ForAll(b, ForAll(a1,f == g)))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat

output:

a = 1

Other form:

a, b, a1 = BitVecs('a b a1', 32)

f = True
f = And(f, a1 == a * b)
g= True
g = And(g, a1 == b)

s = Solver()
s.add(ForAll(b, ForAll(a1,f == g)))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

output:

a = 1

Answer 2

You are asking Z3 (among other things) to find a single a1 that is equal to b for all values of b. This is not possible. Your problem is not with Z3 but with basic logic.

Answer 3

What do you think about this:

a, b = BitVecs('a b', 32)

a1 = a*b
a2 = b


s = Solver()
s.add(ForAll(b, a1 == a2))

if s.check() == sat:
     print 'a =', s.model()[a]
else:
     print 'Unsat'

the output:

a = 1

Other way:

a, b = BitVecs('a b', 32)
a1 = a*b
a2 = b
f = True
f = And(f, a1 == a2)


s = Solver()
s.add(ForAll(b, f))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

the output:

a = 1

Answer 4

If you merely want to verify the formula a * b == b for all possible b. You can use the following code.

from z3 import *

a, b = BitVecs('a b', 32)
s = Solver()
s.add(ForAll(b, a * b == b))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

This code runs in a blink of the eye, but your code overloads the solver and takes relatively a long time to complete.