z3 和 muZ 用于计算程序不变量答案

【问题标题】：z3 and muZ for computing program invariantsz3 和 muZ 用于计算程序不变量
【发布时间】：2013-02-05 10:30:23
【问题描述】：

我正在尝试使用 z3 (muZ) 的定点求解器，以找到程序不变量。但是，在某些时候，查询的答案是 unsat，但我不知道为什么，因为代码是可以访问的：

(declare-rel b1 (Int) interval_relation bound_relation)
(declare-rel b2 (Int) interval_relation bound_relation)
(declare-rel b3 (Int Int) interval_relation bound_relation)
(declare-rel b4 (Int Int) interval_relation bound_relation)
(declare-rel b5 (Int Int) interval_relation bound_relation)
(declare-rel b6 (Int) interval_relation bound_relation)

(declare-var i Int)
(declare-var j Int)

(rule (b1 0))
(rule (=> (and (b1 i) (< i 50)) (b2 i)))
(rule (=> (b2 i) (b3 i 0)))
(rule (=> (and (b3 i j) (< j 50)) (b4 i j)))
(rule (=> (b4 i j) (b3 (+ i 1) (+ j 1))))
(rule (=> (and (b3 i j) (>= j 50)) (b5 i j)))
(rule (=> (b5 i j) (b1 (+ 1 (- i j)))))
(rule (=> (and (b1 i) (>= i 50)) (b6 i)))

(query (b3 i j)
  :compile-with-widening true
  :unbound-compressor false
  :engine datalog
  :print-answer true
)
 ; answers unsat

(query (b4 i j)
  :compile-with-widening true
  :unbound-compressor false
  :engine datalog
  :print-answer true
)
; answers sat
; (and (<= 0 (:var 1)) (<= (:var 1) 49))
; this invariant is correct

; corresponding C program:
; int f() {
;   int i = 0;
;   int j = 0;
; 
;   while (i < 50) {  // b1
;       j = 0;
;       while (j < 50) {  // b3
;           i++;
;           j++;
;       }
;       i = i-j+1;
;   }
;   return i;
; }

有人能解释一下为什么它返回 "unsat" 吗？感谢您的帮助。

【问题讨论】：

对于未来的读者：此代码已过时，不再在 z3 中编译。

标签： z3

【解决方案1】：

这是当前 Z3 版本（muZ 部分）中的一个错误。应用时会影响数据记录引擎区间和边界域。它现在已在本地（不稳定）分支中修复。该修复程序将在下一版本中提供。

【讨论】：