如何在Z3 SMT2语法中使用tactics、处理goals及查询相关文档

goals结果的处理规则 #

你调用apply <战术名>执行自定义化简/求解步骤时，返回的(goals ...)结构是战术执行后的子问题集合，每个goal对应原问题经过战术转换、拆分后的一个独立约束分支，处理逻辑如下：

• 先逐个检查每个goal的标记位：
  • 若goal标记为unsat，说明该分支约束存在矛盾，直接判定该分支不可满足，无需后续处理
  • 若goal为空（没有剩余约束），说明该分支不存在任何约束限制，天然可满足
  • 若goal包含剩余有效约束，说明该分支还未完成求解，可以选择两种后续操作：
    • 对单个goal继续叠加其他战术做进一步处理，比如组合simplify、solve-eqs、对应理论的求解战术（比如整数问题用lia）逐步化简
    • 跳过手动战术流程，直接执行(check-sat)，Z3的默认求解引擎会自动处理所有拆分出的goal，完成整体求解
      针对你给出的示例，两个合取的上界约束4p+3q ≤ r-10和4p+3q ≤ r-12经过simplify战术处理后，会自动剔除冗余的宽松上界约束，最终返回的goals列表只会有1个有效goal，内容为(<= (+ (* 4 p) (* 3 q)) (- r 12))，不存在其他分支。

注意：apply是Z3战术编程的暴露接口，用于手动控制求解流程做性能调优或者特殊求解逻辑定制。如果不需要精细控制求解步骤，写完断言后直接执行(check-sat)、(get-model)即可，Z3会在内部完成所有化简、分支拆分、求解步骤，不会返回中间goals结构。

相关参考资料查阅渠道 #

• Z3官方文档的Strategies & Tactics章节：完整说明SMT2接口下战术的设计逻辑、goals结构的字段定义、不同战术的适用场景和输出规则
• Z3 SMT2命令参考手册：明确apply命令的语法规范、返回值格式，对goals结构中每个属性（比如求解精度、依赖假设、不可满足标记）都有明确定义
• Z3内置帮助：在SMT2交互界面直接执行(help-tactic)命令，即可打印当前安装版本Z3支持的所有内置战术列表、参数说明和使用示例，无需查阅外部资料

内容的提问来源于stack exchange，提问作者Artem Yu