c++ - 在Z3中对整数位添加约束

Question

我有一个整数常量，可以这样说:

expr x = ctx.int_const("x");

我正在尝试将随机约束应用于x的各个位。但是，事实证明，您不能对整数排序使用位运算，而只能对位 vector 使用。在意识到这一点之前，我的最初方法是:

for(int i = 0; i < 32; i++){
    int mask = 0x00000001 << i;
    if(rand()%2)
        solver.add((x & mask) == 0);
    else
        solver.add((x & mask) != 0);
}

这当然不起作用，因为Z3引发异常。
在仔细研究了一下API之后，我找到了Z3_mk_int2bv函数，并想尝试一下:

for(int i = 0; i < 32; i++){
    if(rand()%2)
        solver.add(z3::expr(ctx(),Z3_mk_int2bv(ctx(), 32, v())).extract(i, i) == ctx().bv_val(0, 1));
    else
        solver.add(z3::expr(ctx(),Z3_mk_int2bv(ctx(), 32, v())).extract(i, i) != ctx().bv_val(0, 1));
}

尽管上面的求解器add调用没有声明，但实际的求解时间突然爆炸了。如此之多，以至于我还没有看到实际需要多长时间。使用位 vector 添加相似的表达式不会对SAT求解器造成重大损失，据我所知，求解器时间不到一秒钟。

我想知道上述表达式可能导致求解器性能严重下降的原因，是否有更好的方法？

Answer 1

int2bv很昂贵。造成这种情况的原因很多，但是求解器的底线现在必须在整数理论和位 vector 理论之间进行协商，而启发式方法可能并没有太大帮助。请注意，要进行正确的转换，求解器必须执行重复的除法，这是非常昂贵的。此外，从一开始就谈论数学整数的位并没有多大意义:如果它是负数怎么办？您是否假设某种无限宽度2的补码表示形式？还是其他映射？所有这些使得使用这种转换更加难以推理。由于这个原因和类似原因，很长一段时间以来int2bv在z3中都未得到解释。您可以在堆栈溢出中找到许多与此相关的帖子，例如，请参见此处:Z3 : Questions About Z3 int2bv?

最好的选择是仅使用位 vector 开始。如果您要考虑机器算术，为什么不从位 vector 开始对所有模型建模呢？

如果您坚持使用Int类型，我的建议是仅坚持使用mod函数，确保第二个参数是常量。这样可以避免某些复杂性，但是如果不考虑实际问题，就很难进一步提出意见。