5

Z3のオープンソースリリース（最新のgitマスター）にアップグレードしてから、C API（2〜122のどこか）を使用してほぼ同一のSMTクエリを繰り返し実行する際のタイミングに大きな違いがあることに気付きました。クエリ間の唯一の違いは、（QF_AUFBVロジックでの）配列の命名です。

次のように配列を割り当てています。

Z3_symbol s = Z3_mk_string_symbol(z3_context, arrayName);
Z3_mk_const(z3_context, s,
            Z3_mk_array_sort(z3_context, getSort(32), getSort(8)));

以下は、クエリの例です（SMT-LIBに変換されます）。「arr51」を他の名前（「a」や「arr51_0x2628008」など）に置き換えると、クエリの期間が最大2桁大きく変わります。アレイ名を変更せずに繰り返し実行しても、タイミングに大きな変動はありません。

興味深いことに、Z3 3.2の古いバイナリリリースは、配列の命名の影響を受けていないようです（そして、ほとんどのクエリでより高速に実行されます）。

(benchmark klee
:status unsat
:logic QF_AUFBV
:extrafuns ((arr51 Array[32:8]))
:assumption
(let (?x13 (concat (select arr51 bv58[32]) (concat (select arr51 bv57[32]) (select arr51 bv56[32]))))
(let (?x16 (concat (select arr51 bv59[32]) ?x13))
(let (?x23 (concat bv0[32] ?x16))
(let (?x34 (bvsub (bvadd (concat (extract[33:0] ?x23) bv0[30]) (concat (extract[35:0] ?x23) bv0[28])) (concat (extract[40:0] ?x23) bv0[23])))
(let (?x42 (bvadd (bvadd ?x34 (concat (extract[44:0] ?x23) bv0[19])) (concat (extract[45:0] ?x23) bv0[18])))
(let (?x50 (bvadd (bvsub ?x42 (concat (extract[47:0] ?x23) bv0[16])) (concat (extract[49:0] ?x23) bv0[14])))
(let (?x58 (bvsub (bvadd ?x50 (concat (extract[50:0] ?x23) bv0[13])) (concat (extract[52:0] ?x23) bv0[11])))
(let (?x66 (bvadd (bvadd ?x58 (concat (extract[56:0] ?x23) bv0[7])) (concat (extract[59:0] ?x23) bv0[4])))
(let (?x68 (extract[63:32] (bvsub ?x66 ?x23)))
(flet ($x79 (= bv1[32] bv30[32]))
(let (?x80 (ite $x79 (concat bv0[30] (extract[31:30] (bvsub ?x16 ?x68))) (ite (= bv1[32] bv31[32]) (concat bv0[31] (extract[31:31] (bvsub ?x16 ?x68))) bv0[32])))
(flet ($x85 (= bv1[32] bv29[32]))
(flet ($x90 (= bv1[32] bv28[32]))
(let (?x91 (ite $x90 (concat bv0[28] (extract[31:28] (bvsub ?x16 ?x68))) (ite $x85 (concat bv0[29] (extract[31:29] (bvsub ?x16 ?x68))) ?x80)))
(flet ($x96 (= bv1[32] bv27[32]))
(flet ($x102 (= bv1[32] bv26[32]))
(let (?x103 (ite $x102 (concat bv0[26] (extract[31:26] (bvsub ?x16 ?x68))) (ite $x96 (concat bv0[27] (extract[31:27] (bvsub ?x16 ?x68))) ?x91)))
(flet ($x108 (= bv1[32] bv25[32]))
(flet ($x114 (= bv1[32] bv24[32]))
(let (?x115 (ite $x114 (concat bv0[24] (extract[31:24] (bvsub ?x16 ?x68))) (ite $x108 (concat bv0[25] (extract[31:25] (bvsub ?x16 ?x68))) ?x103)))
(flet ($x119 (= bv1[32] bv23[32]))
(flet ($x125 (= bv1[32] bv22[32]))
(let (?x126 (ite $x125 (concat bv0[22] (extract[31:22] (bvsub ?x16 ?x68))) (ite $x119 (concat bv0[23] (extract[31:23] (bvsub ?x16 ?x68))) ?x115)))
(flet ($x131 (= bv1[32] bv21[32]))
(flet ($x137 (= bv1[32] bv20[32]))
(let (?x138 (ite $x137 (concat bv0[20] (extract[31:20] (bvsub ?x16 ?x68))) (ite $x131 (concat bv0[21] (extract[31:21] (bvsub ?x16 ?x68))) ?x126)))
(flet ($x142 (= bv1[32] bv19[32]))
(flet ($x147 (= bv1[32] bv18[32]))
(let (?x148 (ite $x147 (concat bv0[18] (extract[31:18] (bvsub ?x16 ?x68))) (ite $x142 (concat bv0[19] (extract[31:19] (bvsub ?x16 ?x68))) ?x138)))
(flet ($x153 (= bv1[32] bv17[32]))
(flet ($x157 (= bv1[32] bv16[32]))
(let (?x158 (ite $x157 (concat bv0[16] (extract[31:16] (bvsub ?x16 ?x68))) (ite $x153 (concat bv0[17] (extract[31:17] (bvsub ?x16 ?x68))) ?x148)))
(flet ($x163 (= bv1[32] bv15[32]))
(flet ($x168 (= bv1[32] bv14[32]))
(let (?x169 (ite $x168 (concat bv0[14] (extract[31:14] (bvsub ?x16 ?x68))) (ite $x163 (concat bv0[15] (extract[31:15] (bvsub ?x16 ?x68))) ?x158)))
(flet ($x173 (= bv1[32] bv13[32]))
(flet ($x179 (= bv1[32] bv12[32]))
(let (?x180 (ite $x179 (concat bv0[12] (extract[31:12] (bvsub ?x16 ?x68))) (ite $x173 (concat bv0[13] (extract[31:13] (bvsub ?x16 ?x68))) ?x169)))
(flet ($x184 (= bv1[32] bv11[32]))
(flet ($x190 (= bv1[32] bv10[32]))
(let (?x191 (ite $x190 (concat bv0[10] (extract[31:10] (bvsub ?x16 ?x68))) (ite $x184 (concat bv0[11] (extract[31:11] (bvsub ?x16 ?x68))) ?x180)))
(flet ($x196 (= bv1[32] bv9[32]))
(flet ($x202 (= bv1[32] bv8[32]))
(let (?x203 (ite $x202 (concat bv0[8] (extract[31:8] (bvsub ?x16 ?x68))) (ite $x196 (concat bv0[9] (extract[31:9] (bvsub ?x16 ?x68))) ?x191)))
(flet ($x207 (= bv1[32] bv7[32]))
(flet ($x213 (= bv1[32] bv6[32]))
(let (?x214 (ite $x213 (concat bv0[6] (extract[31:6] (bvsub ?x16 ?x68))) (ite $x207 (concat bv0[7] (extract[31:7] (bvsub ?x16 ?x68))) ?x203)))
(flet ($x219 (= bv1[32] bv5[32]))
(flet ($x224 (= bv1[32] bv4[32]))
(let (?x225 (ite $x224 (concat bv0[4] (extract[31:4] (bvsub ?x16 ?x68))) (ite $x219 (concat bv0[5] (extract[31:5] (bvsub ?x16 ?x68))) ?x214)))
(flet ($x230 (= bv1[32] bv3[32]))
(flet ($x236 (= bv1[32] bv2[32]))
(let (?x237 (ite $x236 (concat bv0[2] (extract[31:2] (bvsub ?x16 ?x68))) (ite $x230 (concat bv0[3] (extract[31:3] (bvsub ?x16 ?x68))) ?x225)))
(flet ($x241 (= bv1[32] bv1[32]))
(let (?x69 (bvsub ?x16 ?x68))
(flet ($x243 (= bv1[32] bv0[32]))
(let (?x245 (bvadd (ite $x243 ?x69 (ite $x241 (concat bv0[1] (extract[31:1] ?x69)) ?x237)) ?x68))
(let (?x253 (ite (= bv16[32] bv30[32]) (concat bv0[30] (extract[31:30] ?x245)) (ite (= bv16[32] bv31[32]) (concat bv0[31] (extract[31:31] ?x245)) bv0[32])))
(let (?x261 (ite (= bv16[32] bv28[32]) (concat bv0[28] (extract[31:28] ?x245)) (ite (= bv16[32] bv29[32]) (concat bv0[29] (extract[31:29] ?x245)) ?x253)))
(let (?x269 (ite (= bv16[32] bv26[32]) (concat bv0[26] (extract[31:26] ?x245)) (ite (= bv16[32] bv27[32]) (concat bv0[27] (extract[31:27] ?x245)) ?x261)))
(let (?x277 (ite (= bv16[32] bv24[32]) (concat bv0[24] (extract[31:24] ?x245)) (ite (= bv16[32] bv25[32]) (concat bv0[25] (extract[31:25] ?x245)) ?x269)))
(let (?x285 (ite (= bv16[32] bv22[32]) (concat bv0[22] (extract[31:22] ?x245)) (ite (= bv16[32] bv23[32]) (concat bv0[23] (extract[31:23] ?x245)) ?x277)))
(let (?x293 (ite (= bv16[32] bv20[32]) (concat bv0[20] (extract[31:20] ?x245)) (ite (= bv16[32] bv21[32]) (concat bv0[21] (extract[31:21] ?x245)) ?x285)))
(let (?x301 (ite (= bv16[32] bv18[32]) (concat bv0[18] (extract[31:18] ?x245)) (ite (= bv16[32] bv19[32]) (concat bv0[19] (extract[31:19] ?x245)) ?x293)))
(let (?x309 (ite (= bv16[32] bv16[32]) (concat bv0[16] (extract[31:16] ?x245)) (ite (= bv16[32] bv17[32]) (concat bv0[17] (extract[31:17] ?x245)) ?x301)))
(let (?x317 (ite (= bv16[32] bv14[32]) (concat bv0[14] (extract[31:14] ?x245)) (ite (= bv16[32] bv15[32]) (concat bv0[15] (extract[31:15] ?x245)) ?x309)))
(let (?x325 (ite (= bv16[32] bv12[32]) (concat bv0[12] (extract[31:12] ?x245)) (ite (= bv16[32] bv13[32]) (concat bv0[13] (extract[31:13] ?x245)) ?x317)))
(let (?x333 (ite (= bv16[32] bv10[32]) (concat bv0[10] (extract[31:10] ?x245)) (ite (= bv16[32] bv11[32]) (concat bv0[11] (extract[31:11] ?x245)) ?x325)))
(let (?x341 (ite (= bv16[32] bv8[32]) (concat bv0[8] (extract[31:8] ?x245)) (ite (= bv16[32] bv9[32]) (concat bv0[9] (extract[31:9] ?x245)) ?x333)))
(let (?x349 (ite (= bv16[32] bv6[32]) (concat bv0[6] (extract[31:6] ?x245)) (ite (= bv16[32] bv7[32]) (concat bv0[7] (extract[31:7] ?x245)) ?x341)))
(let (?x357 (ite (= bv16[32] bv4[32]) (concat bv0[4] (extract[31:4] ?x245)) (ite (= bv16[32] bv5[32]) (concat bv0[5] (extract[31:5] ?x245)) ?x349)))
(let (?x365 (ite (= bv16[32] bv2[32]) (concat bv0[2] (extract[31:2] ?x245)) (ite (= bv16[32] bv3[32]) (concat bv0[3] (extract[31:3] ?x245)) ?x357)))
(let (?x371 (ite (= bv16[32] bv0[32]) ?x245 (ite (= bv16[32] bv1[32]) (concat bv0[1] (extract[31:1] ?x245)) ?x365)))
(let (?x372 (concat bv0[32] ?x371))
(let (?x380 (bvsub (bvadd (concat (extract[32:0] ?x372) bv0[31]) (concat (extract[34:0] ?x372) bv0[29])) (concat (extract[36:0] ?x372) bv0[27])))
(let (?x386 (bvsub (bvadd ?x380 (concat (extract[38:0] ?x372) bv0[25])) (concat (extract[40:0] ?x372) bv0[23])))
(let (?x392 (bvsub (bvadd ?x386 (concat (extract[42:0] ?x372) bv0[21])) (concat (extract[44:0] ?x372) bv0[19])))
(let (?x398 (bvsub (bvadd ?x392 (concat (extract[46:0] ?x372) bv0[17])) (concat (extract[48:0] ?x372) bv0[15])))
(let (?x404 (bvsub (bvadd ?x398 (concat (extract[50:0] ?x372) bv0[13])) (concat (extract[52:0] ?x372) bv0[11])))
(let (?x410 (bvsub (bvadd ?x404 (concat (extract[54:0] ?x372) bv0[9])) (concat (extract[56:0] ?x372) bv0[7])))
(let (?x416 (bvsub (bvadd ?x410 (concat (extract[58:0] ?x372) bv0[5])) (concat (extract[60:0] ?x372) bv0[3])))
(let (?x420 (extract[63:32] (bvadd ?x416 (concat (extract[62:0] ?x372) bv0[1]))))
(let (?x427 (ite $x79 (concat bv0[30] (extract[31:30] (bvsub ?x371 ?x420))) (ite (= bv1[32] bv31[32]) (concat bv0[31] (extract[31:31] (bvsub ?x371 ?x420))) bv0[32])))
(let (?x433 (ite $x90 (concat bv0[28] (extract[31:28] (bvsub ?x371 ?x420))) (ite $x85 (concat bv0[29] (extract[31:29] (bvsub ?x371 ?x420))) ?x427)))
(let (?x439 (ite $x102 (concat bv0[26] (extract[31:26] (bvsub ?x371 ?x420))) (ite $x96 (concat bv0[27] (extract[31:27] (bvsub ?x371 ?x420))) ?x433)))
(let (?x445 (ite $x114 (concat bv0[24] (extract[31:24] (bvsub ?x371 ?x420))) (ite $x108 (concat bv0[25] (extract[31:25] (bvsub ?x371 ?x420))) ?x439)))
(let (?x451 (ite $x125 (concat bv0[22] (extract[31:22] (bvsub ?x371 ?x420))) (ite $x119 (concat bv0[23] (extract[31:23] (bvsub ?x371 ?x420))) ?x445)))
(let (?x457 (ite $x137 (concat bv0[20] (extract[31:20] (bvsub ?x371 ?x420))) (ite $x131 (concat bv0[21] (extract[31:21] (bvsub ?x371 ?x420))) ?x451)))
(let (?x463 (ite $x147 (concat bv0[18] (extract[31:18] (bvsub ?x371 ?x420))) (ite $x142 (concat bv0[19] (extract[31:19] (bvsub ?x371 ?x420))) ?x457)))
(let (?x469 (ite $x157 (concat bv0[16] (extract[31:16] (bvsub ?x371 ?x420))) (ite $x153 (concat bv0[17] (extract[31:17] (bvsub ?x371 ?x420))) ?x463)))
(let (?x475 (ite $x168 (concat bv0[14] (extract[31:14] (bvsub ?x371 ?x420))) (ite $x163 (concat bv0[15] (extract[31:15] (bvsub ?x371 ?x420))) ?x469)))
(let (?x481 (ite $x179 (concat bv0[12] (extract[31:12] (bvsub ?x371 ?x420))) (ite $x173 (concat bv0[13] (extract[31:13] (bvsub ?x371 ?x420))) ?x475)))
(let (?x487 (ite $x190 (concat bv0[10] (extract[31:10] (bvsub ?x371 ?x420))) (ite $x184 (concat bv0[11] (extract[31:11] (bvsub ?x371 ?x420))) ?x481)))
(let (?x493 (ite $x202 (concat bv0[8] (extract[31:8] (bvsub ?x371 ?x420))) (ite $x196 (concat bv0[9] (extract[31:9] (bvsub ?x371 ?x420))) ?x487)))
(let (?x499 (ite $x213 (concat bv0[6] (extract[31:6] (bvsub ?x371 ?x420))) (ite $x207 (concat bv0[7] (extract[31:7] (bvsub ?x371 ?x420))) ?x493)))
(let (?x505 (ite $x224 (concat bv0[4] (extract[31:4] (bvsub ?x371 ?x420))) (ite $x219 (concat bv0[5] (extract[31:5] (bvsub ?x371 ?x420))) ?x499)))
(let (?x511 (ite $x236 (concat bv0[2] (extract[31:2] (bvsub ?x371 ?x420))) (ite $x230 (concat bv0[3] (extract[31:3] (bvsub ?x371 ?x420))) ?x505)))
(let (?x421 (bvsub ?x371 ?x420))
(let (?x516 (bvadd (ite $x243 ?x421 (ite $x241 (concat bv0[1] (extract[31:1] ?x421)) ?x511)) ?x420))
(let (?x524 (ite (= bv3[32] bv30[32]) (concat bv0[30] (extract[31:30] ?x516)) (ite (= bv3[32] bv31[32]) (concat bv0[31] (extract[31:31] ?x516)) bv0[32])))
(let (?x532 (ite (= bv3[32] bv28[32]) (concat bv0[28] (extract[31:28] ?x516)) (ite (= bv3[32] bv29[32]) (concat bv0[29] (extract[31:29] ?x516)) ?x524)))
(let (?x540 (ite (= bv3[32] bv26[32]) (concat bv0[26] (extract[31:26] ?x516)) (ite (= bv3[32] bv27[32]) (concat bv0[27] (extract[31:27] ?x516)) ?x532)))
(let (?x548 (ite (= bv3[32] bv24[32]) (concat bv0[24] (extract[31:24] ?x516)) (ite (= bv3[32] bv25[32]) (concat bv0[25] (extract[31:25] ?x516)) ?x540)))
(let (?x556 (ite (= bv3[32] bv22[32]) (concat bv0[22] (extract[31:22] ?x516)) (ite (= bv3[32] bv23[32]) (concat bv0[23] (extract[31:23] ?x516)) ?x548)))
(let (?x564 (ite (= bv3[32] bv20[32]) (concat bv0[20] (extract[31:20] ?x516)) (ite (= bv3[32] bv21[32]) (concat bv0[21] (extract[31:21] ?x516)) ?x556)))
(let (?x572 (ite (= bv3[32] bv18[32]) (concat bv0[18] (extract[31:18] ?x516)) (ite (= bv3[32] bv19[32]) (concat bv0[19] (extract[31:19] ?x516)) ?x564)))
(let (?x580 (ite (= bv3[32] bv16[32]) (concat bv0[16] (extract[31:16] ?x516)) (ite (= bv3[32] bv17[32]) (concat bv0[17] (extract[31:17] ?x516)) ?x572)))
(let (?x588 (ite (= bv3[32] bv14[32]) (concat bv0[14] (extract[31:14] ?x516)) (ite (= bv3[32] bv15[32]) (concat bv0[15] (extract[31:15] ?x516)) ?x580)))
(let (?x596 (ite (= bv3[32] bv12[32]) (concat bv0[12] (extract[31:12] ?x516)) (ite (= bv3[32] bv13[32]) (concat bv0[13] (extract[31:13] ?x516)) ?x588)))
(let (?x604 (ite (= bv3[32] bv10[32]) (concat bv0[10] (extract[31:10] ?x516)) (ite (= bv3[32] bv11[32]) (concat bv0[11] (extract[31:11] ?x516)) ?x596)))
(let (?x612 (ite (= bv3[32] bv8[32]) (concat bv0[8] (extract[31:8] ?x516)) (ite (= bv3[32] bv9[32]) (concat bv0[9] (extract[31:9] ?x516)) ?x604)))
(let (?x620 (ite (= bv3[32] bv6[32]) (concat bv0[6] (extract[31:6] ?x516)) (ite (= bv3[32] bv7[32]) (concat bv0[7] (extract[31:7] ?x516)) ?x612)))
(let (?x628 (ite (= bv3[32] bv4[32]) (concat bv0[4] (extract[31:4] ?x516)) (ite (= bv3[32] bv5[32]) (concat bv0[5] (extract[31:5] ?x516)) ?x620)))
(let (?x636 (ite (= bv3[32] bv2[32]) (concat bv0[2] (extract[31:2] ?x516)) (ite (= bv3[32] bv3[32]) (concat bv0[3] (extract[31:3] ?x516)) ?x628)))
(let (?x642 (ite (= bv3[32] bv0[32]) ?x516 (ite (= bv3[32] bv1[32]) (concat bv0[1] (extract[31:1] ?x516)) ?x636)))
(let (?x648 (bvsub ?x371 (bvadd (concat (extract[28:0] ?x642) bv0[3]) (concat (extract[30:0] ?x642) bv0[1]))))
(= bv253[8] (extract[7:0] ?x648))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
:assumption
(let (?x13 (concat (select arr51 bv58[32]) (concat (select arr51 bv57[32]) (select arr51 bv56[32]))))
(let (?x16 (concat (select arr51 bv59[32]) ?x13))
(not (= bv4294967295[32] ?x16))))
:assumption
(let (?x13 (concat (select arr51 bv58[32]) (concat (select arr51 bv57[32]) (select arr51 bv56[32]))))
(let (?x16 (concat (select arr51 bv59[32]) ?x13))
(bvule bv100000[32] ?x16)))
:assumption
(let (?x13 (concat (select arr51 bv58[32]) (concat (select arr51 bv57[32]) (select arr51 bv56[32]))))
(let (?x16 (concat (select arr51 bv59[32]) ?x13))
(bvule ?x16 bv999999[32])))
:assumption
(let (?x13 (concat (select arr51 bv58[32]) (concat (select arr51 bv57[32]) (select arr51 bv56[32]))))
(let (?x16 (concat (select arr51 bv59[32]) ?x13))
(let (?x17 (sign_extend[32] ?x16))
(bvsle bv0[64] ?x17))))
:formula
true
)

ランダムシードを明示的に設定しようとしましたが、これは（当然のことながら）役に立ちませんでした：

Z3_set_param_value(z3_config, "ARITH_RANDOM_SEED", "0");
Z3_set_param_value(z3_config, "RANDOM_SEED", "0");

シンボルの名前を変更するだけで、Z3がこのような大きなタイミング変動を表示するのは正常ですか？

また、全体的なソルバー時間を短縮する配列命名スキームはありますか？

ありがとう！

4

1 に答える 1

6

フォームの表現を含むベンチマークでは、この種の不一致が見られます

  • (bvadd t_1 ... t_n)、 また
  • (bvmul t_1 ... t_n)

ベンチマークには、この種の用語が明示的に含まれていない場合があります。たとえば、この用語(bvadd a (bvsub b (bvadd c d))は単純化されて合計になります。

多くの場合、用語t_iの順序はパフォーマンスに劇的な影響を及ぼします。変数名は、これらの用語の順序に影響します。Z3には2つの数式単純化子があります。

古いもの（にありますsrc/ast/simplifier）は、各式に関連付けられた内部IDを使用して、AC演算子の引数を並べ替えます。このアプローチは名前の変更の影響を受けませんが、別の厄介な副作用があります。式を作成する順序が内部IDの割り当てに影響し、その結果、用語の順序に影響しt_iます。これは、多くのZ3アプリケーションで問題でした。

新しいシンプリファイア（にありますsrc/ast/rewriter）は別のアプローチを使用します。式の構造に基づいた全順序を使用して式を並べ替えます。この新しいアプローチでは、式を作成する順序は重要ではありませんが、名前は重要です。新しいコードは、この新しい数式の簡略化を使用します。ただし、古いシンプリファイアを使用する古いコードはまだあります。

QF_AUFBVベンチマークには、両方の式の簡略化子が使用されます。これは、古いシンプリファイアのすべてのオカレンスを新しいシンプリファイアに置き換えた後、将来変更されます。

最後に、パフォーマンスの問題が発生しているベンチマークのセットを送っていただければ幸いです。Z3の改善に役立ちます。

編集

主な問題は、フォームの表現の出現であることを強調したいと思い(bvadd t_1 ... t_n)ます。次に、QF_AUFBVベンチマークには両方の単純化子が使用されます。現在のバージョンでは、このタイミングの変動を回避することは困難です。たとえば、仮定を並べ替える場合は、タイミングの変動も観察する必要があります。

これは、インスタンスで何が起こるか、および名前が動作に影響を与える理由の説明です。少し技術的ですが、何が起こっているのかを明確にする必要があります。

1-新しいシンプリファイアが実行されます。このシンプリファイアは、ハッシュテーブルを使用して中間結果をキャッシュします。ASTのハッシュコードは、定数と関数シンボルに使用される名前によって異なります。

2-新しい単純化が行われた後、キャッシュは削除されます。キャッシュに格納されているASTをトラバースし、それらの参照カウンターをデクリメントします。カウンターがゼロの場合、ASTは削除されます。重要：ハッシュテーブル内のASTの順序は、ハッシュコードによって異なります。そのため、ハッシュコード（およびその結果として名前）は、ASTが削除される順序に影響を与える可能性があります。

3- Z3のASTマネージャーは、各ASTノードに内部IDを割り当てます。ASTノードが削除されると、そのIDがリサイクルされます。つまり、IDを新しいASTノードに割り当てることができます。IDを使い果たしたくないので、これを行います。

4-古いシンプリファイアが実行されると、新しいASTが作成され、リサイクルされたIDがこれらの新しいASTに割り当てられます。

5-古い単純化子はIDを使用しての引数をソートするbvaddため、変数の名前を変更すると異なる順序を取得できます。

概要

異なる名前==>異なるハッシュ==>ハッシュテーブル内の異なる順序==>異なる削除順序==>リサイクルされたIDは異なる順序で再利用されます==>異なるIDを持つ新しいAST==>古い単純化子が引数を順序付ける方法に影響しますのbvadd

于 2013-03-26T00:39:15.480 に答える