let表达式的创建由漂亮的打印机控制。试试类似的东西：
我正试图通过以下方式使用z3 Python API"简化"一些smtlib2文件：
- 读取SMTLIB2文件
- 运用一些策略&提取简化目标
- 将简化的目标添加到新的解算器
- 通过
to_smt2()打印新求解器
我有一个奇怪的用例，如果生成的smtlib文件不包含任何let表达式，那么它将是理想的。有没有办法通过python API扩展它们？
set_option(max_args=10000000, max_lines=1000000, max_depth=10000000, max_visited=1000000)
您可以使用实际数字来找到适用于您的用例的设置。从本质上讲，数字越大，共享/切断就越少。
同样重要的是参数CCD_ 3。也可以尝试将其设置为一个大数字。(默认值为10，强制let表达式。(