0

プログラムの不変条件を見つけるために、z3（muZ）の不動点ソルバーで遊んでみようとしています。ただし、ある時点で、クエリは不満に答えますが、コードが到達可能であるため、理由はわかりません。

(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」を返すのか誰かが私に説明できますか？ご協力いただきありがとうございます。

4

1 に答える 1

0

これは、Z3の現在のリリース（muZ部分）のバグです。間隔ドメインと境界ドメインを適用すると、データログエンジンに影響します。現在、ローカル（不安定）ブランチで修正されています。この修正は、次のリリースで利用できるようになります。

于 2013-02-05T16:16:25.920 に答える