在 Z3 中对整数位添加约束

Question

我有一个整数常量，比如说：

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

我要做的是对 x 的各个位应用随机约束。但是，事实证明，您不能将按位运算与整数排序一起使用，而只能使用位向量。在意识到这一点之前，我最初的做法是这样的：

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));
}

虽然没有在上述求解器添加调用上引发任何断言，但实际求解时间突然爆炸式增长。如此之多，以至于我还没有看到实际需要多长时间。使用位向量添加类似的表达式不会对 SAT 求解器造成重大影响，据我所知，求解器的时间不到一秒。

我想知道上面的表达式是什么导致求解器性能如此糟糕地下降，是否有更好的方法？

Answer 1

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

您最好的选择是简单地使用位向量开始。如果您正在推理机器算术，为什么不用位向量对所有内容进行建模呢？

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