形式化策略的语义差异比较：基于反合一方法

一个开源引擎利用 e-graph 上的反合一技术计算形式化策略的语义差异，对共享结构只展示一次，并保留每个差异部分的两个版本。该引擎面向 SMT-LIB、Cedar、Dogwood、OpenShell 策略和 CEL 中的自动形式化输出，其中 LLM 负责生成产物，但不参与差异计算。