Python-Z3: Python 的断言不成立
Python-Z3: Python's assertion is not holding
我想测试 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 all 整数 x、exists 整数 y、(x>y)。这是真的。在这种情况下，结果是 [[]]（因为量词消除是令人满意的）。当做 assert [[]] == result 结果是否定的。
当你写：
[[False]]
这意味着您有一个包含该元素的嵌套列表。请注意，这与 z3 无关。这是一个有效的 Python 对象。
将此与您的 result_tt 进行比较，后者是 Goal。因此，您正在尝试将 Goal 与嵌套的 python 列表进行比较；这两件事永远不会相等。它们是完全不同的对象。因此断言失败。
您对这两个东西的打印方式相同感到困惑。但是检查相等性是一个完全不同的操作。如果你真的想比较它们“打印”的相同，你可以这样说：
assert '[[False]]' == obj_to_string(result_ttt)
当然，如果 z3 开发人员以后决定更改将目标转换为字符串的方式，那当然是非常丑陋和脆弱的。
一般来说，你不应该试图将目标与其他任何东西进行比较，而是使用求解器来证明它们，或者使用策略来转化和消除它们。以任何其他方式使用它们都会很脆弱，并且很可能不会做你想做的事情。
我想测试 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 all 整数 x、exists 整数 y、(x>y)。这是真的。在这种情况下，结果是 [[]]（因为量词消除是令人满意的）。当做 assert [[]] == result 结果是否定的。
当你写：
[[False]]
这意味着您有一个包含该元素的嵌套列表。请注意，这与 z3 无关。这是一个有效的 Python 对象。
将此与您的 result_tt 进行比较，后者是 Goal。因此，您正在尝试将 Goal 与嵌套的 python 列表进行比较；这两件事永远不会相等。它们是完全不同的对象。因此断言失败。
您对这两个东西的打印方式相同感到困惑。但是检查相等性是一个完全不同的操作。如果你真的想比较它们“打印”的相同，你可以这样说：
assert '[[False]]' == obj_to_string(result_ttt)
当然，如果 z3 开发人员以后决定更改将目标转换为字符串的方式，那当然是非常丑陋和脆弱的。
一般来说，你不应该试图将目标与其他任何东西进行比较，而是使用求解器来证明它们，或者使用策略来转化和消除它们。以任何其他方式使用它们都会很脆弱，并且很可能不会做你想做的事情。