沿等价候选到最优树路线，下载标准库执行器。运行python或python -O加文件名，都只向stdout写相同JSON；显式检查不依赖assert。
本任务的数是数学整数，程序只有纯总算术。四条规则的普遍保值由加法、乘法和dbl(z)=2z的定义证明；对−4..4的81份输入执行是实现回归，不把有限测试当作所有整数上的证明。
一、给破坏性改写与保留候选各交一条轨迹
输入为add(mul(add(x,0),2),mul(y,2))，即
((x + 0) * 2) + (y * 2)叶每个出现费1，add费2、mul费4、dbl费1。原式费用17。先去加零，再把两次乘二替换成dbl，得到add(dbl(x),dbl(y))，费用6。共同因子模式add(mul(a,c),mul(b,c))此时不再匹配。
另走“保留旧乘法形状”的路线：共同因子生成mul(add(x,y),2)，费用9，再强度削弱为dbl(add(x,y))，费用5。注意9虽然比6贵，却能通向5；只在当前形状里执行单向规则并丢弃旧候选，可能失去这条路线。
提交四条完整规则及其全称整数等式依据：add(a,0)→a、mul(a,1)→a、mul(a,2)→dbl(a)、共同因子规则。a、b、c是模式变量；x、y是待优化程序的输入变量，两种变量身份不能混用。
二、把三轮搜索逐项对到真实图上
按读、写、重建三期执行。第1轮从同一快照得到4匹配，新增4节点；第2轮5匹配，新增1节点；第3轮5匹配，新增0节点且无新合并，才报告saturated。每轮重建后有8类。
把第3轮仍有匹配但没有新事实的原因写清楚：同一右模式已经存在于目标等价类，重做它不再增长集合。不能用“匹配数不是0”判定必须继续，也不能在刚做完第一轮后臆测已经闭包。
另造dbl(add(x,0))与dbl(x)，并在两者上各包一层mul(·,2)。只合并add(x,0)与x的类后，尝试查询应报dirty。重建实际合并两个dbl类与两个外层mul类，共2次合并，连确认扫描共2遍。提交重建前后的类身份，解释父节点为何不能只靠底层union自然更新。
三、交八类费用和每条不等式
将最终图规范编号为：
0 : x | add(0,1)
1 : 0常量
2 : 2常量
3 : mul(0,2) | dbl(0)
4 : y
5 : mul(4,2) | dbl(4)
6 : add(3,5) | mul(7,2) | dbl(7) [根]
7 : add(0,4)这里add(0,1)的0是类号，不是常量0；常量0位于类1。这项区分会决定是否看见x类的自环。
按高度动态规划，初始全∞。第1轮有限项为类0/1/2/4的1；第2轮类3/5为2、类7为4；第3轮根为5。完成C=8轮，最后距离向量为
[1, 1, 1, 2, 1, 2, 5, 4]提交每个节点的d(所属类)≤节点费+孩子距离和。根处必须分别检查5≤6、5≤9、5≤5，并选择取等号的dbl(7)。继续选add(0,4)、x、y，得到有限目标dbl(add(x,y))。
只证明根费用不超过某一个候选远远不够；漏掉其余候选时，一份过高的距离也可能蒙混。把d(根)改为9，检验器应被更便宜候选拒绝；把某类距离调低却不给取等号节点，也必须拒绝。
四、迁移改变搜索集合或可生成性
- 删去共同因子规则。 重置整个图再运行，最终7类，费用6；不是把原已含费用5候选的图继续运行三条规则。规则删除不自动撤销此前已经加入的等式。
- 只给一轮预算。 仍用四规则，结果状态为iteration-limit，当前图内最优6。语义仍可靠，但没有饱和声明，也没有全部可达表达式的全局最优保证。
- 切断有限出口。 一类{loop(0),leaf}，节点费分别1/3，提取叶费3。去掉leaf，只有纯环，应返回NO_FINITE_TERM；不能返回空树费0，也不能等到任意燃料耗尽后给默认答案。
- 只改变外层增长规则。 对x×0使用mul(a,0)→mul(add(a,1),0)，三轮产生5、6、7类且一直新增，预算出口为limit。规则是正确整数等式，但这不使搜索自动终止。
另核重复模式变量：add(?v,?v)可匹配add(x类,x类)，不能匹配尚未合并的add(x类,y类)。模式有限、图可能有环，匹配仍沿模式结构前进，不按图循环反复展开。
五、迁移改变费用模型
完整图为R={pair(A,B)}，A={a,g(Q)}，B={b,h(Q)}，Q={q}。pair/g/h各费1，a/b/q各费6；语义前提a=g(q)、b=h(q)保证各类候选相等。
树费用时，a的6优于g(q)的7，b同理，最优pair(a,b)费13。改为共享DAG费用后，同一个q只算一次，pair(g(q),h(q))费9。请交两个完整对象并分别列收费节点，不能把压缩存储中的同编号默默当作计算结果可免费共享。
这个例子不要求你实现通用DAG提取器；它要求识别原最优性证明的输入/目标已经改变。若要继续求DAG最优，必须重新定义联合选择约束和证书。
六、验收算法与证据
主执行器包含12类拒绝/接口检查：dirty查询、零/负费、坏孩子、空类、重复规范节点、算子元数不一致、过高距离、无法实现的下界、虚假无项判断、非法距离及右侧未绑定模式变量。另写对照枚举500份小图的6277完整节点选择，核1465类最优值；用独立集合划分闭包核300份图的202363节点对；16个规则子集的164规范节点按稀疏多项式验证同类语义。
这些是作者自查，不代替独立审核，也不把有限案例数变成普遍证明。普遍终止来自正费用下的“最优根叶路径不重复类”，可靠性来自全部节点不等式加实现等号；搜索语义则来自有效等式与同余不变量。
最后分账：全表重建按原始节点而非只按去重后图计费；匹配与右式加入都另有工作；提取计算需C轮，教学日志保存C²距离；完整输出树有L个出现时必须支付L级输出成本。紧凑图、紧凑证书和完整表达式树是三份不同大小的对象。