2

次のコードは、2つのフィールドarray-fldと。を持つ「レコード」をエンコードしますblist-fld。これらのフィールドの更新関数を定義してから、trueである必要があるプロパティをアサートしました（ただし、z3はこれを報告しますunknown）。これはZ3バージョン4.0であり、次のように実行されz3 -smt2 -inます。

(declare-datatypes ()
                   ((mystruct (mk-mystruct
                                 (array-fld (Array Int Int))
                                 (blist-fld (List Bool))))))
(define-fun array-fld-upd ((v (Array Int Int)) (obj mystruct)) mystruct
  (mk-mystruct v (blist-fld obj)))
(define-fun blist-fld-upd ((v (List Bool)) (obj mystruct)) mystruct
  (mk-mystruct (array-fld obj) v))

(push)
(assert
 (forall ((z0 mystruct))
         (exists ((array-val (Array Int Int)))
                 (and (= array-val (array-fld z0))
                      (= (select (array-fld
                                  (array-fld-upd (store array-val 2 4) z0)) 3)
                         (select (array-fld z0) 3))))))
(check-sat)

方程式array-valバインディングを代入して、手動で実存を巻き戻し/削除すると、次のようになります。

(pop)
(assert
 (forall ((z0 mystruct))
         (= (select (array-fld (array-fld-upd (store (array-fld z0) 2 4) z0)) 3)
            (select (array-fld z0) 3))))
(check-sat)

そしてこれは喜んで解決されsatます。

これには4つの質問があります。

  1. z3を呼び出して、最初のインスタンスと2番目のインスタンスを解決する方法はありますか？
  2. レコード/構造体を別の方法でエンコードする必要がありますか？
  3. let-expressionsを別の方法でエンコードする必要がありますか（存在記号につながるのはこれらです）？
  4. または、let-expressionsを直接拡張する必要があります（これは自分で行うこともできますが、参照が多い場合は大きな用語になる可能性があります）。
4

1 に答える 1

3

適切な let 式を使用できるように質問から見えます。そうすれば、Z3 の方が簡単になります。

(declare-datatypes ()
               ((mystruct (mk-mystruct
                             (array-fld (Array Int Int))
                             (blist-fld (List Bool))))))
(define-fun array-fld-upd ((v (Array Int Int)) (obj mystruct)) mystruct
  (mk-mystruct v (blist-fld obj)))
(define-fun blist-fld-upd ((v (List Bool)) (obj mystruct)) mystruct
  (mk-mystruct (array-fld obj) v))

(push)
(assert
 (forall ((z0 mystruct))
    (let ((array-val (array-fld z0)))
                  (= (select (array-fld
                              (array-fld-upd (store array-val 2 4) z0)) 3)
                     (select (array-fld z0) 3)))))
 (check-sat)
于 2013-01-18T06:00:45.650 に答える