时间戳

首页 > 解决方案 > Python-Z3：Python 的断言不成立

python - Python-Z3：Python 的断言不成立

问题描述

我想测试该assert语句是否适用于 z3 结果。

为此，我测试了以下语句：exists一个整数x，例如for all整数y，(x>y)。这是错误的：没有整数大于其余整数。

所以我把它翻译成 Z3py：

y_1 = Int('y_1')
x_1 = Int('x_1')
ttt = Tactic("qe")
w = Goal()
phi = Exists(x_1, ForAll (y_1, (x_1>y_1)))
w.add(phi)
result_ttt = ttt(w)
print(result_ttt)

正如预期的那样，打印结果是：[[False]]

所以我测试断言以下内容：

assert [[False]] == result_ttt

而且，令人惊讶的是，结果是assertion error！

有什么帮助吗？可能与存在的类型有关result_ttt（<class 'z3.z3.ApplyResult'>在做之后type(result_ttt）。

请注意，类似地，如果我们选择一个可满足的陈述，则该断言也不成立。

选择的语句是：for allintegers x，existsinteger y，(x>y)。这是真的。在这种情况下，结果是[[]]（因为量词消除是令人满意的）。做assert [[]] == result的时候结果是否定的。

标签： pythonz3assertassertionz3py

解决方案

当你写：

[[False]]

这意味着您有一个嵌套列表，其中包含该元素。请注意，这与 z3 无关。这是一个有效的 Python 对象。

将此与您的 进行比较result_tt，后者是Goal. 因此，您正在尝试将 aGoal与嵌套的 python 列表进行比较；这两件事永远不会相等。它们是完全不同的对象。因此断言失败。

您对这两件事以相同的方式打印这一事实感到困惑。但是检查相等性是完全不同的操作。如果您真的想比较它们“打印”相同，您可以这样说：

assert '[[False]]' == obj_to_string(result_ttt)

但是，如果 z3 开发人员决定稍后更改目标转换为字符串的方式，这当然非常难看并且很脆弱。

一般来说，您不应该尝试将目标与其他任何目标进行比较，而应使用求解器来证明它们，或使用策略来转换和消除它们。以任何其他方式使用它们都将是脆弱的，并且可能不会首先做你想做的事情。

推荐阅读