выполнимость формулы, имеющий FORALL квантора

Question

Это мой код Python:

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' 

В этом коде, я написал следующую формулу в Z3Py синтаксисе:

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

Когда я запускаю этот скрипт, находит модель, в то время как я думаю, что это должно быть unsat. Как это возможно? Я что-то упускаю?

Answer 1

Вы забыли связать b и c:

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

После связывания b, c, то результат unsat. Если вы не связываете b, c, то они рассматриваются как свободные константы, и существует модель формулы.