How can I check only existence in z3?

I need some temporary variables in z3, I don't need the value to be calculated just need to check it exists is enough.

This is (simple form of) what I'm working on:

import z3

def maj(a, b, c):
    return (a & b) ^ (a & c) ^ (b & c)

def func(a, b, c):
    a = z3.RotateRight(a, 5) ^ z3.BitVecVal(0xafaf, 16)
    b = z3.RotateRight(b, 2) ^ z3.RotateRight(b, 7)
    c = z3.RotateRight(c, 11) ^ z3.LShR(c, 3)
    return a + c, b + c, maj(a + b, a + c, b + c)

solver = z3.SolverFor('QF_BV')
some_var = 0x0000
_x = z3.BitVec('x', 16)
x = _x
y = z3.BitVecVal(some_var, 16)
c = z3.BitVec('c', 16)
for i in range(16):
    x, y, c = func(x, y, c)
solver.add(c == z3.BitVecVal(0xff00, 16))
print(solver.check())
model = solver.model()
print(model[_x].as_long())

I need value of x but don't need value of c just knowing there is some variable is enough. If I pass some fixed constant for c it runs much faster (but it might be unsat)

Also using z3.Var(1, z3.BitVecSort(16)) gives unknown as answer.

Is there any way for it?

Solution

Your question is a bit ambiguous: I take it that you do care that the final value of c to be 0xff00, but you don't care what its initial value is? Since you keep mutating c, it isn't clear which one you want to constrain.

If that's the case, i.e., if you want the final value of c to be 0xff00 and don't care what the initial value is, then what you did is just fine. You just shouldn't expect the solver to come up with a solution quickly. This looks a lot like some sort of encryption/scrambler routine, and SMT solvers--or any other solver for that matter--isn't good at dealing with such problems by design. They tend to encode one-way functions, so you shouldn't expect an out-of-the-box general constraint solver to reverse-engineer it with ease. It can be done, but it won't be fast.

In the off-chance that you actually don't care what the final value of c is (which is an odd thing to do, but I suppose there might be a use case for it), then the typical way to deal with this would be to use a quantifier. It kind of follows from your requirement: "There is some c, I don't care what it is." So, let's code that. We need to make a few changes. First, we need quantifiers, so set the solver appropriately:

solver = z3.SolverFor('BV')

Then:

final_c = z3.BitVec('final_c', 16)
solver.add(z3.Exists([final_c], c == final_c))

Note that the declaration of final_c is a technicality. You won't be able to access its value. It's just to make sure that there exists some final value of c that's reachable. (i.e., the whole thing isn't unsat.)

With these changes, if you run the program you'll see it says:

Traceback (most recent call last):
  File "/Users/leventerkok/qq/b.py", line 27, in <module>
    print(model[_x].as_long())
AttributeError: 'NoneType' object has no attribute 'as_long'

This is because the model didn't even care for _x; it noticed that this is satisfiable and didn't bother to compute _x. But we can ask it to give us a value like this:

model = solver.model()
print(model.evaluate(_x, model_completion=True))

This prints:

sat
0

So, there's a way to run your equations and it all works out starting with x = 0. Well, that wasn't very interesting, but without any additional constraints it does make sense: Starting with x = 0, and an appropriate y/c, you can indeed unroll this calculation.

Finally, don't use z3.Var(1, BitVecSort(16)). Those are lambda-vars, that you should never reach out for. (It's a design flaw in my mind that z3 exposes them to the end-user, but not everything is perfect!)