Z3 SMT-LIB2.0 循环依赖

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 的评论中所述，您可能需要考虑使用更高级别的工具来解决该问题。例如，使用 NuSMV or Spin 编码变得微不足道。

Z3 SMT-LIB2.0 循环依赖

Z3 SMT-LIB2.0 Codependent for loops

smt

z3