在 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 上找到很多关于这个的帖子，例如在这里看到：

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

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

在 Z3 中添加对整数位的约束

Adding constrains on integer bits in Z3

c++

z3

smt

z3py

sat