使用 Exists 量词检查断言的意外结果

Question

我是 Z3Py（和 Z3）的新手。以下代码 returns 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)),
]

使用 Exists 量词检查断言的意外结果

Unexpected result checking an assertion with an Exists quantifier

z3

z3py