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. Consider using std::uniform_int_distribution<>(0,1) as a replacement. — user4581301
– user4581301, Commented Feb 20, 2020 at 17:42

alias · Accepted Answer · 2020-02-20 19:12:05Z

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.

edited Feb 20, 2020 at 19:12

answered Feb 20, 2020 at 19:01

alias

30.9k2 gold badges31 silver badges51 bronze badges

Sign up to request clarification or add additional context in comments.

3 Comments

squirem Over a year ago

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 Over a year ago

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.

alias Over a year ago

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.

Collectives™ on Stack Overflow

Adding constrains on integer bits in Z3

1 Answer 1

3 Comments

Your Answer

Linked

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

3 Comments

Your Answer

Sign up or log in

Post as a guest

Linked

Related