Adding constrains on integer bits in Z3

Question

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?

unrelated: `if(rand()%2)` is likely slightly biased, and in general, [`rand` sucks](https://channel9.msdn.com/Events/GoingNative/2013/rand-Considered-Harmful). Consider using [`std::uniform_int_distribution<>(0,1)`](https://en.cppreference.com/w/cpp/numeric/random/uniform_int_distribution) as a replacement. — user4581301, Feb 20 '20 at 17:42

alias · Accepted Answer · 2020-02-20T19:12:05.513

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.

I made the assumption that integer constants were internally represented as 32-bit integers, similar to gecode. Regardless, I needed a way to randomize the bits, whether it was signed or not. Thanks for the answer and tips. — squirem, Feb 20 '20 at 19:31
Just tried your answer, it works perfect. Solver time is negligible. For the sign, I randomized between the integer being greater than or equal to 0, or less than 0. — squirem, Feb 20 '20 at 19:50
As you found out, SMTLib's `Int` type is unbounded. It's a true mathematical integer; not some machine representation of limited width. Glad it worked out for you. — alias, Feb 20 '20 at 21:53

Adding constrains on integer bits in Z3

1 Answers1