【发布时间】：2017-07-11 07:13:37
【问题描述】：
我有 37 个类似的 SMT2 问题，每个问题都有两个可满足的版本，我称之为 compact 和 unrolled。问题是使用增量 SMT 解决，每个 (check-sat) 返回 unsat。精简版使用 QF_AUFBV 逻辑，展开版使用 QF_ABV。我确实在 z3、yices 和 boolector 中运行了它们（但 boolector 只支持展开版本）。可在此处找到此性能评估的结果：
http://scratch.clifford.at/compact_smt2_enc_r1102.html
此示例的 SMT2 文件可从此处下载 (~10 MB)：
http://scratch.clifford.at/compact_smt2_enc_r1102.zip
我使用 :random-seed 选项的不同值运行每个求解器 5 次。 （除了不支持 :random-seed 的 boolector。所以我只需在同一输入上运行 boolector 5 次。）运行具有不同 :random-seed 的求解器时得到的变化相对较小（请参阅表中的 +/- 值最大异常值）。
求解器之间存在广泛的传播。 Boolector 和 Yices 始终比 z3 快，在某些情况下高达两个数量级。
但是，我的问题是关于“z3 vs z3”的性能。例如考虑以下数据点：
| Test Case | Z3 Median Runtime | Max Outlier |
|-------------------|-------------------|-------------|
| insn_add unrolled | 873.35 seconds | +/- 0% |
| insn_add compact | 1837.59 seconds | +/- 1% |
| insn_sub unrolled | 4395.67 seconds | +/- 16% |
| insn_sub compact | 2199.21 seconds | +/- 5% |
问题 insn_add 和 insn_sub 几乎相同。两者都是使用 Yosys 从 Verilog 生成的，唯一的区别是 insn_add 使用 this Verilog module 而 insn_sub 使用 this one 代替它。这是这两个源文件之间的差异：
--- insn_add.v 2017-01-31 15:20:47.395354732 +0100
+++ insn_sub.v 2017-01-31 15:20:47.395354732 +0100
@@ -1,6 +1,6 @@
// DO NOT EDIT -- auto-generated from generate.py
-module rvfi_insn_add (
+module rvfi_insn_sub (
input rvfi_valid,
input [ 32 - 1 : 0] rvfi_insn,
input [`RISCV_FORMAL_XLEN - 1 : 0] rvfi_pc_rdata,
@@ -29,9 +29,9 @@
wire [4:0] insn_rd = rvfi_insn[11: 7];
wire [6:0] insn_opcode = rvfi_insn[ 6: 0];
- // ADD instruction
- wire [`RISCV_FORMAL_XLEN-1:0] result = rvfi_rs1_rdata + rvfi_rs2_rdata;
- assign spec_valid = rvfi_valid && insn_funct7 == 7'b 0000000 && insn_funct3 == 3'b 000 && insn_opcode == 7'b 0110011;
+ // SUB instruction
+ wire [`RISCV_FORMAL_XLEN-1:0] result = rvfi_rs1_rdata - rvfi_rs2_rdata;
+ assign spec_valid = rvfi_valid && insn_funct7 == 7'b 0100000 && insn_funct3 == 3'b 000 && insn_opcode == 7'b 0110011;
assign spec_rs1_addr = insn_rs1;
assign spec_rs2_addr = insn_rs2;
assign spec_rd_addr = insn_rd;
但是他们在这个基准测试中的表现非常不同：总体而言，insn_sub 的性能比 insn_add 的性能差很多。此外，在 insn_add 的情况下，展开版本的运行速度大约是精简版本的两倍，但在 insn_sub 的情况下，精简版本的运行速度大约是展开版本的两倍。
这是创建中位数之前的时间。 :random-seed 设置显然似乎没有太大区别：
insn_add unrolled: 868.15 873.34 873.35 873.36 874.88
insn_add compact: 1828.70 1829.32 1837.59 1843.74 1867.13
insn_sub unrolled: 3204.06 4195.10 4395.67 4539.30 4596.05
insn_sub compact: 2003.26 2187.52 2199.21 2206.04 2209.87
由于:random-seed 的值似乎没有太大影响，我认为这些 .smt2 文件固有的某些东西使它们在 z3 上变快或变慢。 我将如何对此进行调查？我如何找出是什么让快速案例快速而慢速案例变慢，这样我就可以避免让慢速案例变慢的任何事情？（是的，我知道这是一个非常广泛的问题。抱歉。:)
这里有一些与我的主要问题类似的更具体的问题。这个问题直接受到我在（紧凑）insn_add 和 insn_sub 基准测试之间的明显差异的启发。
- 我的 SMT 输入中
(declare-..)和(define-..)语句的顺序会影响性能吗？ - 更改已声明或已定义函数的名称会影响性能吗？
- 如果我将 BV 拆分为更小的 BV，然后再次将它们串联回来，这会影响性能吗？
- 如果我比较两个 BV 是否相等，或者将 BV 拆分为单个位变量并分别比较每个位，这会影响性能吗？
- 另外：当我为
:random-seed选择不同的值时，z3 中的哪些操作实际上会发生变化？
在不改变语义的情况下对 .smt2 文件进行小的更改对于由复杂工具生成的大型测试用例来说是非常困难的。我希望我可以先尝试其他一些事情，或者也许有一些关于可能值得研究的变化的现有专家知识。或者：什么样的更改实际上等同于更改:random-seed，因此不值得研究。
（使用 git rev c67cf16 执行的测试，即在具有 make -j40 的 AWS EC2 c4.8xlarge 实例上 z3 的当前 git 头。运行时是 CPU 秒数，而不是挂钟秒数。）
编辑 2：
我现在有三个相同的测试用例（test1.smt2、test2.smt2 和test3.smt2），只是我重命名了我声明/定义的一些函数。测试用例可以在http://svn.clifford.at/handicraft/2017/z3perf/找到。
这是原始问题的变体，需要约 2 分钟而不是约 1 小时才能解决。和以前一样，更改:random-seed 的值只会产生边际效应。但是重命名一些函数而不改变其他任何东西会使运行时间改变超过 2 倍：
我现在有 opened an issue on github，认为当我重命名 SMT2 代码中的函数时，:random-seed 应该绑定到我在 z3 中随机更改的任何内容。
【问题讨论】：