Z3定理证明器是否提供官方语法BNF规范？

• Z3没有单独公开的专属BNF规范，它的核心输入语法完全遵循SMT-LIB2标准，你要找的AST构建逻辑和语法节点结构，和SMT-LIB2的BNF定义是一一对应的，Z3仅在此基础上做了少量功能扩展。
• 你可以直接从Z3源码中提取完整的语法规则：定位到仓库内的src/parsers目录，smt2parser的实现代码里包含了全量的语法解析规则，部分规则注释里直接标注了对应的BNF片段。
• 如果你是通过Python接口使用Z3、想学习它的Python层AST结构，可以直接查看Python绑定的z3.z3.Ast类及各个子类的源码，所有Z3底层AST节点在Python层都有对应的封装，类的属性、方法完全对应底层AST的结构字段，和你参考的Python AST类的设计逻辑是一致的。
• 另外Z3官方API文档的AST模块章节，会列出所有可用的AST节点类型、节点属性、构造和遍历方法，完全可以支撑你学习Z3 AST的构建逻辑。

内容的提问来源于stack exchange，提问作者Austin Y