pyZ3:在smt2输出中展开let-表达式？

Question

我试图通过以下方法使用Python“简化”一些smtlib2文件：

在solver

• printing文件中读取

1. 应用一些策略&提取简化的目标
2. ，通过to_smt2()

将简化的目标添加到新的SMTLIB2中，新的求解器

我有一个奇怪的用例，如果生成的smtlib文件不包含任何let表达式，则非常理想。有没有办法通过python扩展它们？

Answer 1

let-表达式的创建由漂亮的打印机控制.试一试如下：

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

您可以使用实际数字来查找适合您的用例的设置。从本质上说，数字越大，共享/切断的数量就越少。

同样重要的是参数min_alias_size。还可以尝试将其设置为一个大的数字。(默认值为10，这会强制let-表达式。)