为什么 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 开始。

问：SMT求解器提供的方案是否可行？ YES! （您与我们分享的部分..）

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

...

为什么 Z3 将变量保持在相同的值，即使指定不这样做

Why does Z3 keeps a variable at the same value even if it is specified not to do that

solver

smt

z3