为什么Z3保持变量不变，即使它被指定不这样做

Question

我在Z3中遇到了一个问题，似乎无法找到它的起源以及如何解决。我的目标是对于给定的特定迭代（for循环），该迭代由每个步骤中的if-then-else语句组成；循环结束后是否有可能获得给定的值k。这是在不知道if的结构的情况下完成的。换句话说，我需要为每个步骤检查功能的每个可能映射（对或错）。更精确的是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
    [...]

我不知道我是否遇到错误，或者解决该问题的逻辑是否有缺陷。我尝试使用有界模型检查。我将不胜感激任何帮助！

Answer 1

问题：问题可能出在您对循环行为的理解上，还是在于实现循环逻辑的公式的编码中。由于您没有提供原始的伪代码，因此我无法再猜测了。

---

让我们来这个：

(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))
             )
         )
 )

正在展开的表达式是：

   (                  -- #then-branch
        a' := a + 2 * b
            /\
        b' := K + b
   )
xor
   (                  -- #else-branch
        a' = K + b
            /\
        b' = a + b
   )

其中K取决于当前迭代，以1开头。

---

Q： SMT求解器提供的解决方案是否可行？ 是！（（您与我们共享的部分。。]

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

...