Adding constrains on integer bits in Z3

1

I have an integer constant, lets say:

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

What I'm trying to do is apply random constraints on the individual bits of x. However, it turns out you cannot use bit-wise operations with integer sorts, only bit-vectors. My initial approach before realizing this was this:

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

This of course does not work, as Z3 throws an exception. After a bit of digging through the API, I found the Z3_mk_int2bv function, and figured I'd give that a try:

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

While no assertion gets thrown on the above solver add calls, the actual solving time suddenly exploded. So much so that I have yet to see how long it actually takes. Adding similar expressions using bit-vectors does not take a major toll on the SAT solver, with the solver time being less than a second as far I can tell.

I'm wondering what it is about the above expression that could cause the solver performance to degrade so badly, and whether there's a better approach?

c++
z3
smt
z3py
sat
asked on Stack Overflow Feb 20, 2020 by squirem

1 Answer

2

int2bv is expensive. There are many reasons for this, but bottom line the solver now has to negotiate between the theory of integers and bit-vectors, and the heuristics probably don't help much. Notice that to do a proper conversion the solver has to perform repeated divisions, which is quite costly. Furthermore, talking about bits of a mathematical integer doesn't make much sense to start with: What if it's a negative number? Do you assume some sort of a infinite-width 2's complement representation? Or is it some other mapping? All this makes it harder to reason with such conversions. And for a long time int2bv was uninterpreted in z3 for this and similar reasons. You can find many posts regarding this on stack-overflow, for instance see here: Z3 : Questions About Z3 int2bv?

Your best bet would be to simply use bit-vectors to start with. If you're reasoning about machine arithmetic, why not model everything with bit-vectors to start with?

If you're stuck with the Int type, my recommendation would be to simply stick to mod function, making sure the second argument is a constant. This might avoid some of the complexity, but without looking at actual problems, it's hard to opine any further.

answered on Stack Overflow Feb 20, 2020 by alias • edited Feb 20, 2020 by alias

User contributions licensed under CC BY-SA 3.0