Z3正时变化 [英] Z3 timing variation
问题描述
自从升级到 Z3 的开源版本(最新的 git master)以来，我注意到使用 C API 重复运行几乎相同的 SMT 查询(从 2 到 122 秒之间的任何时间)之间存在显着的时间差异.查询之间的唯一区别是数组的命名(在 QF_AUFBV 逻辑中).
Since upgrading to the open source release of Z3 (latest git master), I've noticed a significant timing variation between repeated runs of nearly-identical SMT queries using the C API (anywhere from 2-122s). The only difference between the queries is the naming of arrays (in the QF_AUFBV logic).
我们按如下方式分配数组:
We're allocating arrays as follows:
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).用其他名称(例如，a"或arr51_0x2628008")替换arr51"会显着改变查询的持续时间，最多两个数量级.在不改变阵列名称的情况下重复运行不会表现出显着的时序变化.
Below is an example query (converted to SMT-LIB). Replacing "arr51" with other names (e.g., "a" or "arr51_0x2628008") significantly changes the duration of the query, by up to two orders of magnitude. Repeated runs without varying the array name don't exhibit a significant timing variation.
有趣的是，Z3 3.2 的旧二进制版本似乎不受数组命名的影响(并且对于我们的大多数查询运行速度更快).
Interestingly, the old binary release of Z3 3.2 doesn't seem to be affected by array naming (and runs faster for most of our queries).
(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
)
我已经尝试明确设置随机种子，但这(不出所料)没有帮助:
I've tried explicitly setting the random seeds, but this (unsurprisingly) hasn't helped:
Z3_set_param_value(z3_config, "ARITH_RANDOM_SEED", "0");
Z3_set_param_value(z3_config, "RANDOM_SEED", "0");
Z3 仅通过更改符号名称来显示如此显着的时序变化是否正常?
Is it normal for Z3 to display such significant timing variation just by changing the names of symbols?
此外，是否有任何数组命名方案可以全面减少求解器时间?
Also, is there any array naming scheme that would reduce solver time across the board?
谢谢！
推荐答案
我们在包含表单表达式的基准测试中观察到这种差异
We observe this kind of discrepancy in benchmarks that contain expressions of the form
(bvadd t_1 ... t_n)，或(bvmul t_1 ... t_n)
基准可能未明确包含此类术语.例如，术语 (bvadd a (bvsub b (bvadd c d)) 被简化为一元和.
The benchmark may not explicitly contain this kind of term. For example, the term (bvadd a (bvsub b (bvadd c d)) is simplified to a nary sum.
在许多情况下，术语t_is 的顺序对性能有显着影响.变量名称会影响这些术语的顺序.Z3 有两个公式简化器.
In many instances, the order of the terms t_is have a dramatic effect on performance. The variable names affect the order of these terms. Z3 has two formula simplifiers.
旧的(位于 src/ast/simplifier)使用与每个表达式关联的内部 id 对 AC 运算符的参数进行排序.这种方法不受名称更改的影响，但它有另一个令人讨厌的副作用:我们创建表达式的顺序会影响内部 id 分配，从而影响术语 t_i 的顺序.这是许多 Z3 应用程序中的一个问题.
The old one (located at src/ast/simplifier) uses the internal ids associated with each expression to sort arguments of AC operators. This approach is not affected by name changes, but it has another nasty side-effect: the order we create expressions affect the internal id assignment, and consequently the order of the terms t_i. This was an issue in many Z3 applications.
新的简化器(位于 src/ast/rewriter)使用了不同的方法.它使用基于表达式结构的总顺序对表达式进行排序.在这种新方法中，我们创建表达式的顺序无关紧要，但名称很重要.新代码使用这个新的公式简化器.但是，我们仍然有使用旧简化器的旧代码.
The new simplifier (located at src/ast/rewriter) uses a different approach. It sorts expressions using a total order based on the structure of expressions. In this new approach, the order we create expressions does not matter, but the names do. New code uses this new formula simplifier. However, we still have old code that uses the old simplifier.
对于 QF_AUFBV 基准测试，两个公式简化器都被使用.在我们用新的简化器替换所有出现的旧简化器之后，这将在未来发生变化.
For QF_AUFBV benchmarks, both formula simplifiers are used. This will change in the future, after we replace all occurrences of the old simplifier with the new one.
最后，如果您能将您遇到性能问题的基准集发送给我们，那就太好了.这将有助于我们改进 Z3.
Finally, it would be great if you could send us the set of benchmarks where you are having performance problems. It would help us to improve Z3.
编辑
我想强调，主要问题是(bvadd t_1 ... t_n)形式的表达式的出现.其次，对于 QF_AUFBV 基准测试，使用了两个简化器.在当前版本中，很难避免这种时间波动.例如，如果我们重新排列假设，我们还应该观察时间波动.
I'd like to emphasize that the main issue is the occurrence of expressions of the form (bvadd t_1 ... t_n). Second, for QF_AUFBV benchmarks both simplifiers are used. In the current version, it is hard to avoid this timing fluctuations. For example, we should also observe timing fluctuations if we reorder the assumptions.
这里描述了您的实例中发生的情况，以及名称影响行为的原因.这有点技术性，但它应该澄清发生了什么.
Here is a description of what happens in your instance, and why the name affects the behavior. It is a little bit technical, but it should clarify what is going on.
1- 执行新的简化程序.此简化器使用哈希表缓存中间结果.AST 的哈希码取决于用于常量和函数符号的名称.
1- The new simplifier is executed. This simplifier caches intermediate results using a hashtable. The hashcode of an AST depends on the names used for constants and function symbols.
2- 新的简化器完成后，缓存被删除.我们遍历存储在缓存中的 AST 并递减它们的引用计数器.如果计数器为零，则删除 AST.重要提示:散列表中 AST 的顺序取决于它们的散列代码.因此，哈希码(以及名称)可能会影响删除 AST 的顺序.
2- After the new simplifier is done, the cache is deleted. We traverse the ASTs stored in the cache and decrement their reference counters. If the counter is zero, the AST is deleted. IMPORTANT: the order of the ASTs in the hashtable depends on their hash code. So, the hash code (and consequently the names) may affect the order ASTs are deleted.
3- Z3 中的 AST 管理器为每个 AST 节点分配一个内部 ID.当一个 AST 节点被删除时，它的 ID 会被回收.也就是说，可以将 ID 分配给新的 AST 节点.我们这样做是因为我们不想用完 ID.
3- The AST manager in Z3 assigns an internal ID to each AST node. When an AST node is deleted, its ID is recycled. That is, the ID can be assigned to new AST nodes. We do that because we don't want to run out of IDs.
4- 执行旧的简化程序时，它会创建新的 AST，并将回收的 ID 分配给这些新的 AST.
4- When the old simplifier is executed, it will create new ASTs, and recycled IDs are assigned to these new ASTs.
5- 由于旧的简化器使用 ID 对 bvadd 的参数进行排序，因此当我们更改变量名称时，我们可以获得不同的顺序.
5- Since, the old simplifier uses IDs to sort the arguments of bvadd, we can get a different order when we change the name of a variable.
总结
名称不同 ==> Hash 不同 ==> Hashtable 中的顺序不同 ==> 删除顺序不同 ==> 回收的 ID 以不同的顺序重用 ==> 具有不同 ID 的新 AST ==> 影响旧的简化器命令 bvadd
Different name ==> Different Hash ==> Different order in the Hashtable ==> Different deletion order ==> Recycled IDs are reused in different order ==> new ASTs with different IDs ==> Affects how the old simplifier orders the arguments of bvadd
这篇关于Z3正时变化的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
