z3：打印一个很长的断言答案

【问题标题】：z3: print a very long assertionz3：打印一个很长的断言
【发布时间】：2020-08-06 16:42:35
【问题描述】：

以以下为例。

trues = [True] * 1000
a = z3.And(trues)

所以a 是 1000 个Trues 的合取。请注意，这不是一个实际示例，因为a 在逻辑上等同于True。

如果我们print(a)，则不会显示完整的断言。相反，结果以...) 结尾。

要打印完整的断言，我找到的一种解决方案是打印a 的s-expression。即print(a.sexpr())。这样一来，1000 个Trues 就全部显示出来了。

所以我的问题是：有没有更好的方法来打印像 a 这样的很长的断言？

【问题讨论】：

标签： z3 smt z3py

【解决方案1】：

当然。试试：

import z3

z3.set_option(max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000)

trues = [True] * 1000
a = z3.And(trues)

print(a)

您可以使用set_option 的数字来获得更适合您的用例的数字。

【讨论】：

谢谢。这正是我所需要的。