Z3 C++ API如何高效比较两个表达式是否等价

Z3_is_eq_ast做的是语法层面的AST节点同一性判断，而非逻辑等价判断，不会自动应用交换律、结合律等代数规则做匹配。
你之前了解到的“等价表达式ID一致”的现象，前提是两个表达式的结构、子节点顺序完全一致：Z3内部的哈希复用机制会对结构完全相同的表达式返回同一个AST节点，这种场景下Z3_is_eq_ast才会返回true。而z1 && z2和z2 && z1因为合取操作的参数顺序不同，构造阶段生成的是两个独立的AST节点，自然会被判定为不等，这是API的预期行为，不存在实现差异。
你给出的测试代码运行后res返回false，完全符合设计逻辑：

z3::context c;
z3::expr z1 = c.bool_const("z1");
z3::expr z2 = c.bool_const("z2");
z3::expr z11 = z1 && z2;
z3::expr z22 = z2 && z1;
auto res = Z3_is_eq_ast(c, z11, z22);

全量调用默认参数的simplify会开启大量高开销的重写规则，性价比很低，可以根据业务场景选择下面开销更低的方案：

• 构造阶段轻量规范化（性能最优，首选方案）
  不需要在比对阶段做任何额外计算，只需要在生成表达式时做一层简单封装：对AND/OR/ADD/MUL这类满足交换律、结合律的运算符，先把所有操作数按AST的唯一ID（Z3_get_ast_id返回值）从小到大排序，再调用Z3的接口构造表达式。
  这种处理方式会从根源上保证“仅参数顺序不同、逻辑等价”的表达式复用同一个AST节点，后续比对直接用Z3_is_eq_ast做指针级判断即可，零额外运行时开销，额外成本仅存在于表达式构造阶段，几乎可以忽略。
• 裁剪参数的轻量化简（适合存在少量结构差异的场景）
  如果你的表达式除了参数顺序问题，还存在双重否定、冗余常量、嵌套结合律等简单结构差异，不需要调用默认的simplify。可以手动配置化简参数，关闭所有涉及复杂逻辑推理、算术重写、量词处理的高开销规则，仅开启flat_assoc（结合律扁平化）、sort_exprs（交换律排序）、elim_double_neg（消除双重否定）、constant_folding（常量折叠）这类轻量结构规范化规则，化简速度可以比默认simplify快一个数量级以上。
• 顺序无关哈希预过滤（适合存量代码改造场景）
  如果项目里已经有大量直接调用原生接口构造表达式的存量代码，不方便统一改造构造逻辑，可以给表达式实现一套和参数顺序无关的结构哈希：对交换律运算符，将所有子节点的哈希值排序后再合并计算当前节点哈希；对不满足交换律的运算符（如蕴含、减法、除法），直接按子节点顺序合并哈希。
  比对时先校验哈希值：哈希不同的表达式一定逻辑不等，可以直接返回结果；哈希相同的表达式再走后续精确判断，能过滤掉99%以上的不等场景，大幅降低整体比对开销。

内容的提问来源于stack exchange，提问作者Jiawei Ren