I am encountering a problem in Z3 for which I can't seem to find where it originates from and how to fix it. My goal that for a given certain iteration (for-loop) that is composed of an if-then-else statement at each step; is it possible to achieve a given value k after the loop has finished. This is done without knowing the structure of if. In other words, i need to check every possible mapping of the function (true or false) for each step. More precisely in smt2 format:
(declare-fun a(Int) Int)
(declare-fun b(Int) Int)
(assert (= 1 (a 0)))
(assert (= 1 (b 0)))
(assert (xor (and ( = (a 1) (+ (a 0) (* 2 (b 0)))) (= (b 1) (+ 1 (b 0)))) (and (= (b 1) (+ (a 0) (b 0))) (= (a 1) (+ (b 0) 1)))))
(assert (xor (and ( = (a 2) (+ (a 1) (* 2 (b 1)))) (= (b 2) (+ 2 (b 1)))) (and (= (b 2) (+ (a 1) (b 1))) (= (a 2) (+ (b 1) 2)))))
(assert (xor (and ( = (a 3) (+ (a 2) (* 2 (b 2)))) (= (b 3) (+ 3 (b 2)))) (and (= (b 3) (+ (a 2) (b 2))) (= (a 3) (+ (b 2) 3)))))
(assert (xor (and ( = (a 4) (+ (a 3) (* 2 (b 3)))) (= (b 4) (+ 4 (b 3)))) (and (= (b 4) (+ (a 3) (b 3))) (= (a 4) (+ (b 3) 4)))))
(assert (xor (and ( = (a 5) (+ (a 4) (* 2 (b 4)))) (= (b 5) (+ 5 (b 4)))) (and (= (b 5) (+ (a 4) (b 4))) (= (a 5) (+ (b 4) 5)))))
(assert (xor (and ( = (a 6) (+ (a 5) (* 2 (b 5)))) (= (b 6) (+ 6 (b 5)))) (and (= (b 6) (+ (a 5) (b 5))) (= (a 6) (+ (b 5) 6)))))
(assert (xor (and ( = (a 7) (+ (a 6) (* 2 (b 6)))) (= (b 7) (+ 7 (b 6)))) (and (= (b 7) (+ (a 6) (b 6))) (= (a 7) (+ (b 6) 7)))))
(assert (xor (and ( = (a 8) (+ (a 7) (* 2 (b 7)))) (= (b 8) (+ 8 (b 7)))) (and (= (b 8) (+ (a 7) (b 7))) (= (a 8) (+ (b 7) 8)))))
(assert (xor (and ( = (a 9) (+ (a 8) (* 2 (b 8)))) (= (b 9) (+ 9 (b 8)))) (and (= (b 9) (+ (a 8) (b 8))) (= (a 9) (+ (b 8) 9)))))
(assert (xor (and ( = (a 10) (+ (a 9) (* 2 (b 9)))) (= (b 10) (+ 10 (b 9)))) (and (= (b 10) (+ (a 9) (b 9))) (= (a 10) (+ (b 9) 10)))))
(assert (= (b 10) 461))
(check-sat)
(get-model)
The xor operator is used to check if the statement for then holds or the statement in else holds, but not both. So the the variable a or b is bounded to follow only one valid path. Somehow the values sometimes don't seem to obey this rule or they do not change, and I am unable to tell why is this happening. As for example take this output for a, for the step 2 and 3 the value doesn't change, which should not be possible:
(define-fun a ((x!0 Int)) Int
(ite (= x!0 0) 1
(ite (= x!0 1) 3
(ite (= x!0 2) 7 <--- should not be possible but keeps happening
(ite (= x!0 3) 7 <---
(ite (= x!0 4) 29
[...]
I don't know if i either am encountering a bug or my logic involved in the solution for this problem is flawed. I tried to use Bounded Model Checking. I would appreciate any help!
Issue: the problem is either in your understanding of how the loop should behave, or in the encoding of the formula implementing the logic of the loop. Since you didn't provide the original pseudo-code, I cannot guess any further.
Let's take this:
(assert (xor
(and
(= (a 1) (+ (a 0) (* 2 (b 0))))
(= (b 1) (+ 1 (b 0)))
)
(and
(= (b 1) (+ (a 0) (b 0)))
(= (a 1) (+ (b 0) 1))
)
)
)
The expression that is being unrolled is:
( -- #then-branch
a' := a + 2 * b
/\
b' := K + b
)
xor
( -- #else-branch
a' = K + b
/\
b' = a + b
)
where K depends on the current iteration, starting with 1.
Q: is the solution provided by the SMT solver feasible? YES! (the portion you have shared with us..)
a_0 := 1
b_0 := 1
-- execute #then-branch (K = 1)
a_1 := a_0 + 2 * b_0 = 1 + 2 * 1 = 3
b_1 := K + b_0 = 1 + 1 = 2
-- execute #then-branch (K = 2)
a_2 := a_1 + 2 * b_1 = 3 + 2 * 2 = 7
b_2 := K + b_1 = 2 + 2 = 4
-- execute #else-branch (K = 3)
a_3 := K + b_2 = 3 + 4 = 7
b_3 := a_2 + b_2 = 7 + 4 = 11
-- execute #then-branch (K = 4)
a_4 := a_3 + 2 * b_3 = 7 + 2 * 11 = 29
b_4 := K + b_3 = 4 + 11 = 15
...