Z3 SMT-LIB2.0 Codependent for 循环

Question

我对使用 Z3 有点迷茫，目标是模型 2 进程都并行运行相同的循环。只要两个进程都没有完成，就会选择一个未完成的进程并执行其 10 个步骤中的下一个：

for i := 1 to 10 do
if x < 8 then x := x + i else x := i − 2x

x 是一个全局变量，i 在两个实例中都是局部变量。

另外我想将 x 初始化为 0，这在 Z3 中可以吗？

到目前为止，我得到了 unsat 的结果，代码如下：

(declare-const c Int)

(push)
(declare-const i1 Int)
(assert
(and
(>= i1 1)
(<= i1 20)
(ite (< c 5) (and (= c (+ c i1)) (>= i1 1) (<= i1 20)) (and (= c (- i1 (* 2 c))) (>= i1 1) (<= i1 20)))
))

(push)
(declare-const i2 Int)
(assert
(and
(>= i2 1)
(<= i2 20)
(ite (< c 5) (and (= c (+ c i2)) (>= i2 1) (<= i2 20)) (and (= c (- i2 (* 2 c))) (>= i2 1) (<= i2 20)))
))

(assert (= c -24))

(check-sat)
(get-model)
(pop)
(pop)

提前致谢！

Answer 1

约束

(= c (+ c i1))

始终为unsat，除非i1 等于0，但情况并非如此。

类似的考虑也适用于

(= c (- i1 (* 2 c)))

在这种情况下，只有当3c = i1 为i1 和c s.t. 选择一些值时，这才可以满足。 c > 8 和 i1 在 1..20 中，但下面的某些行要求 c 等于 -24：

(assert (= c -24))

由于i1必须是正数，所以c不能是负数，因此这个分支也是unsat。鉴于ite 的两个分支都是unsat，c s.t. 没有任何价值。该公式是可满足的，因此求解器正确回答 unsat。

注意：您可能会在玩unsat cores 时获得一些乐趣。

---

考虑这个伪代码：

int x = 0;
x = x + 1;
if (x == 1) {
    x = 2;
} else {
    x = -1;
}
assert(x == 2);

这是一种可能的（不是很有效的）编码：

(set-option:produce-models true)
(declare-fun x0 () Int)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(assert (= x0 0))                       ;; initial condition
(assert (= x1 (+ x0 1)))                ;; assignment to x
(assert (and
        (or (not (= x1 1)) (= x2 2))    ;; then branch
        (or (= x1 1) (= x2 (- 1)))      ;; else branch
))
(assert (= x2 2))                       ;; assertion
(check-sat)
(get-model)

输出是：

$ ./z3 test.smt2 
sat
(model 
  (define-fun x2 () Int
    2)
  (define-fun x1 () Int
    1)
  (define-fun x0 () Int
    0)
)

请注意，我为原始变量x 的每个赋值声明了一个新变量，以保存新值。

在您的示例中，我将首先执行 完整的循环展开，然后应用与上述相同的转换。

---

编辑：正如 Levent Erkok 在 cmets 中提到的，您可能需要考虑使用更高级别的工具来解决该问题。例如，使用 NuSMV 或 Spin 对其进行编码变得微不足道。