如何测量Z3中公式大小？验证simplify操作是否修改公式

内置大小计算方法 #

Z3提供了内置的公式大小度量接口，以常用的Python绑定为例：

• 调用phi.size()可获取公式的抽象语法树（AST）节点总数，这是Z3默认的公式大小定义。
• 对简化后的公式phi_simp = simplify(phi)，同样用phi_simp.size()获取其大小，对比两者数值即可快速判断简化操作是否带来结构上的规模变化。

示例代码：

from z3 import *

# 替换为你的大规模公式
x, y = Bools('x y')
phi = Or(Not(y), And(y, Not(x)))
phi_simp = simplify(phi)

print(f"原公式节点数: {phi.size()}")
print(f"简化后公式节点数: {phi_simp.size()}")

验证公式是否被修改 #

若需直接确认simplify是否修改了公式结构，可使用语法等价判断：

• 调用phi.eq(phi_simp)，返回True说明原公式与简化后公式的AST结构完全一致，简化操作未做修改；返回False则表示公式结构已被调整。
• 注：该判断基于语法结构，而非语义等价，但足以满足你确认simplify是否产生修改的需求。

补充说明 #

Z3的simplify行为受多种参数（如:elim_and、:pull_cheap_ite等）控制，即使公式节点数未变化，也可能在语义等价的前提下调整了AST结构，eq()方法可准确捕捉这类结构变化。若需自定义大小度量（如统计原子公式数量、特定运算符出现次数），可自行遍历AST实现，但内置的size()方法已能覆盖绝大多数快速分析场景。

内容的提问来源于stack exchange，提问作者Theo Deep