Неожиданный результат проверки утверждения с квантором Exists

Question

Я новичок в Z3Py (и Z3). Следующий код возвращает unsat, как и ожидалось:

from z3 import Ints, Tactic, Exists, And, Implies, ForAll, Bool, Solver, IntSort, BoolSort, Function 

s = Solver() 
t, a, t0 = Ints('t a t0') 
p = Function('p', IntSort(), IntSort(), BoolSort()) 
facts = [ 
    t >= 1, 
    t <= 2, 
    Implies(And([t>0, t <= 1]), p(t, 1) == False), 
    Implies(And([t>1, t <= 2]), p(t, 1) == True), 
] 
query = Implies(t == 2, Exists(t0, And([t0 == t, t0 >= 1, t0 <= 2, p(t0, 1) == True]))) 
f = Implies(And(facts), query) 
s.add(Tactic('qe')(Not(f)).as_expr()) 
print s.check() # unsat means f is valid 

Если я теперь изменить query к

query = Implies(t == 1, Exists(t0, And([t0 > t, t0 >= 1, t0 <= 2, p(t0, 1) == True]))) 

печатает sat, хотя я ожидал unsat, как t0 == 2 является искомым свидетелем квантора. Поблагодарите за понимание, спасибо.

Answer 1

Ответил на мой вопрос. Мои предположения были слишком слабыми. Следующая редакция: facts выполняет:

facts = [ 
    t >= 1, 
    t <= 2, 
    ForAll(t, Implies(And([t>0, t <= 1]), p(t, 1) == False)), 
    ForAll(t, Implies(And([t>1, t <= 2]), p(t, 1) == True)), 
]