0

This is my Python code:

s = z3.Solver()

f = z3.Function('f', z3.IntSort(), z3.IntSort())
g = z3.Function('g', z3.IntSort(), z3.IntSort())
h = z3.Function('h', z3.IntSort(), z3.IntSort())

a, b, c = z3.Ints('a b c')

imp_a = z3.And(f(a) == b, g(a) == c)
imp_b = h(c) == b
ax = z3.ForAll(a, z3.Implies(imp_a, imp_b))

l = [
    ax,
    f(1) == 5,
    g(1) == 2,
    h(2) != 5
]
s.add(l)

if s.check() == z3.sat:
    print s.model()
else:
    print 'Unsat'

In this code, I have written the following formula in Z3Py syntax:

forall a, (f(a) == b and g(a) == c) => h(c) == b

When I run this script it finds a model, while I think it should be unsat. How could it be possible? Am I missing something?

4

1 回答 1

2

You forgot to bind b and c:

ax = z3.ForAll([a,b,c], z3.Implies(imp_a, imp_b))

After binding b, c, then the result is unsat. If you don't bind b,c, then they are treated as free constants and there is a model of the formula.

于 2016-06-08T15:37:58.137 回答