Python-Z3中assert断言对qe策略返回结果校验失败问题

你遇到断言失败的核心原因是参与比较的两个对象类型不匹配：
调用Z3策略（Tactic）得到的返回值是Z3自定义的z3.z3.ApplyResult类实例，不是Python原生的嵌套列表。你在控制台看到的[[False]]、[[]]只是该类重写了字符串输出方法后的显示效果，和你写的Python字面量[[False]]、[[]]本质是完全不同的对象，直接做相等比较必然返回False。

有两种常用的校验方案：

方案1：提取子目标表达式比较 #

可以先从ApplyResult中提取子目标，再调用as_expr()方法将子目标转换为Z3布尔表达式，再做比较：

• 对应你第一个假命题的场景（量化消去后得到不可满足的子目标），断言写法如下：

assert result_ttt[0].as_expr() == False

• 对应你第二个真命题的场景（量化消去后子目标无约束，恒为真），断言写法如下：

assert result_ttt[0].as_expr() == True

提示：不推荐直接将ApplyResult转成字符串和"[[False]]"这类字符串做比较，不同版本Z3的打印格式可能有差异，容易导致断言失效。

方案2：直接用求解器验证命题 #

如果你的需求只是验证命题的真假，不需要手动调用量化消去策略，更简洁的写法是直接构造求解器校验：

from z3 import *
y_1 = Int('y_1')
x_1 = Int('x_1')
phi = Exists(x_1, ForAll (y_1, (x_1>y_1)))

s = Solver()
s.add(phi)
# 假命题check结果为unsat，断言如下
assert s.check() == unsat

内容的提问来源于stack exchange，提问作者Theo Deep