我有一个整数常量，可以这样说：
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));
}
尽管上面的求解器add调用没有声明，但实际的求解时间突然爆炸了。如此之多，以至于我还没有看到实际需要多长时间。使用位向量添加相似的表达式不会对SAT求解器造成重大损失，据我所知，求解器时间不到一秒钟。
我想知道上述表达式可能导致求解器性能严重下降的原因，是否有更好的方法？
int2bv太贵了。造成这种情况的原因有很多，但求解器的底线现在必须在整数理论和位向量理论之间进行协商，而启发式方法可能无济于事。请注意，要进行正确的转换，求解器必须执行重复的除法，这是非常昂贵的。此外，从一开始谈论数学整数的位并没有多大意义：如果它是负数怎么办？您是否假设某种无限宽度2的补码表示形式？还是其他映射？所有这些使得使用这种转换更加难以推理。int2bv由于这个原因和类似原因，很长一段时间以来，z3中都没有对此进行解释。您可以在堆栈溢出中找到许多与此相关的帖子，例如，请参见此处：Z3：有关Z3 int2bv的问题？
最好的选择是简单地使用位向量开始。如果您要考虑机器算术，为什么不从位向量开始对所有模型建模呢？
如果您坚持使用Int类型，我的建议是简单地坚持使用mod函数，确保第二个参数是常量。这样可以避免某些复杂性，但是如果不考虑实际问题，就很难进一步提出意见。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句