Я столкнулся с проблемой в Z3, для которой я не могу найти, откуда она берется и как ее исправить. Моя цель состоит в том, чтобы для данной определенной итерации (цикла for), которая состояла из оператора if-then-else на каждом шаге;Можно ли достичь заданного значения k после завершения цикла. Это делается без знания структуры if. Другими словами, мне нужно проверить каждое возможное отображение функции (true или false) для каждого шага. Точнее в формате smt2:
(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)
Оператор xor используется, чтобы проверить, выполняется ли оператор для then или оператор в else, , но не оба ,Таким образом, переменная a или b ограничена, чтобы следовать только одному допустимому пути. Почему-то значения иногда не подчиняются этому правилу, или они не меняются, и я не могу сказать, почему это происходит. Как, например, взять этот вывод для a, для шагов 2 и 3 значение не изменяется, что не должно быть возможным:
(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
[...]
Я не знаю, если ялибо я сталкиваюсь с ошибкой, либо моя логика, связанная с решением этой проблемы, неверна. Я пытался использовать ограниченную проверку моделей. Буду признателен за любую помощь!