如何控制Z3中eval的递归函数求值深度？

控制递归求值深度的方法 #

• 调用eval时指定max_depth参数：Z3的eval函数支持通过max_depth设置递归展开的最大深度，例如eval(min_coord_expr, model, max_depth=20)。调高该值可以覆盖网格连通路径所需的递归次数，让求值器完成全展开。
• 手动实现递归展开逻辑：基于模型中的方块类型赋值，编写自定义函数遍历连通路径，逐步计算min-coord-in-cc的结果。这种方式完全可控，不受Z3默认求值深度的限制。
• 增强递归函数的终止约束：在定义min-coord-in-cc时，显式添加关于坐标可达性的终止断言（比如当当前坐标是连通分量中最小时直接返回），帮助Z3求值器更快识别终止条件，减少递归展开的复杂度。

Z3无法自动简化表达式的原因 #

• Z3模型仅记录了核心变量（方块类型）的赋值，并未预先为递归函数的所有可能调用生成显式绑定。直接求值时，求值器需要动态展开递归，但默认深度不足以覆盖整个4x2网格的连通路径，因此保留了未展开的表达式结构。
• 手动断言解的具体值后，相当于给Z3补充了完整的上下文信息，求值器可以沿着已知的方块连接关系，一步步展开递归直到终止条件触发，最终得到简化后的(mk-coord 0 0)结果。
• 递归函数的求值依赖于对连通分量的遍历，而Z3的默认求值策略优先处理简单表达式，对于需要多步遍历的递归调用，不会自动进行全路径展开，除非明确指定足够的深度或提供更明确的约束。

内容的提问来源于stack exchange，提问作者David Detlefs