I'm new to SMT solving. The expression below is a very simple example.
1: (declare-const x Int)
2: (declare-const z Int)
3: (declare-const k Int)
4: (assert (= z (* x x))) ; z = x*x
5: (assert (<= z 1)) ; z <= 1, where z should be either 0 or 1
6: ; (assert (= x 1))
7: (assert (= k (- (^ 2 z) 1))) ; k = 2**z - 1
8: (check-sat)
Lines 4 and 5 narrow down the possible values of the variable z to either zero or one. The next step is to calculate 2**0 - 1 or 2**1 - 1. As a result, the variable K can be either zero or one.
However, the satisfiability in line 8 displays unknown. In my first experience of constraint solving using SMT expressions, it seems strange to me that the solver cannot solve this simple linear expression. If I uncomment line 6, the result changes to sat. However, uncommenting this line is not desired because all unknown variables should be provided by the user.
So, my question is: Can the given expressions not be resolved? Or can they be resolved by transforming them into another form somehow?
Thank you
I've written a simple example and saw the undesired result. So, I'd like to ask to experts whether this result is expected or can be resolved by refactoring.
There are two issues here. The first is that power operator creates a real-valued term. (Think of, for instance, 2^(-1). The result isn't an integer even though the arguments are.) So, you should explicitly cast:
(assert (= k (- (to_int (^ 2 z)) 1))) ; k = 2**z - 1
If you do this, you'll see that z3 answers your query as sat. (It's hard to guess why z3 isn't smart enough to deduce this, probably some "trigger" fails to fire without the cast. But hard to tell without analyzing the z3 code itself.)
The second issue, unfortunately, is harder to deal with. Exponentiation is difficult for SMT solvers: They create highly non-linear terms, and non-linear integer arithmetic is not only undecidable, the existing algorithms that deal with it (reduction to incremental bit-vectors, for instance) are necessarily very expensive. So, depending on your other constraints you might still get unknown as an answer.
But it's best to deal with each problem on its own. For each problem, there's usually an alternative way to code it to get answers, though you shouldn't expect complete push-button solutions when non-linear terms are present.