z3 - pyZ3：扩展 smt2 输出中的 let 表达式？

Question

我正在尝试通过以下方式使用 z3 Python API 来“简化”一些 smtlib2 文件：

1. 读取 SMTLIB2 文件
2. 应用一些策略并提取一个简化的目标
3. 将简化目标添加到新求解器
4. 通过打印新的求解器to_smt2()

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

标签： z3z3py

Answer 1

let 表达式的创建由漂亮的打印机控制。尝试类似：

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

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

同样重要的是参数min_alias_size。也尝试将其设置为一个很大的数字。（默认值为 10，强制使用 let 表达式。）