2

Z3 を使用してレコードの配列を作成することができましたが、配列に対して $\forall$ 操作を実行するために必要な構文を確認するのに苦労しています... これまでに持っている SMT-LIB2 コードのスニペット サンプルです。 .

(declare-datatypes () ((rec (mk-R5 (age Int) (area Int) (married Bool)))))
(declare-const recs (Array Int rec))
(declare-const r1 rec)
(assert(= (age r1) 15))
(assert(= (area r1) 10001))
(assert(= (married r1) true))
(declare-const r2 rec)
(assert(= (age r2) 35))
(assert(= (area r2) 2845))
(assert(= (married r2) true))
(declare-const x Int)
(declare-const y Int)
(assert (= recs (store recs x r1)))
(assert (= recs (store recs y r2)))
(assert(forall ((i rec)) (= (married i) true)))
(check-sat)
(get-model)

最後から 3 番目の行には配列への参照が必要だと思いますが、すべてを試しましたが、チュートリアルはこの問題の解決に役立ちませんでした。

ここにある配列に対して $\forall$ 操作を実行するにはどうすればよいですか?

4

1 に答える 1

3

2 つのレコードを配列に入れて、それらの要素について何かを言おうとしているようです。残念ながら、あなたのエンコーディングはそれを意味するものではありません。

最初に気付くのは、次の行の意味です。

   (declare-const recs (Array Int rec))

これは、すべての整数recsによってインデックス付けされた配列であることを示しています。つまり、ドメインはすべてのInt値のセットです。これはおそらくあなたが意図したものではありません。

また、行：

(assert (= recs (store recs x r1)))
(assert (= recs (store recs y r2)))

次のように書く方が良いです:

(assert (= (select recs x) r1))
(assert (= (select recs y) r2))

xindexとy;について知っていることを言っていると考えてください。recs書き込もうとしたときに「変更」する命令的な割り当てステートメントとは対照的です。smt-lib の値を変更するという概念はありません。構築しているモデルについて正しいとわかっていることを述べるだけです。

forall-assertion を修正する 1 つの方法は、次のように記述することです。

(assert (forall ((i Int)) 
                (implies (or (= i x) (= i y)) 
                         (= (married (select recs i)) true))))

インデックスを定量化し、インデックスがiまたはyの場合、それらのレコードにはmarried人がいると言います。これらの変更により、Z3 は次のように応答します。

sat
(model
  (define-fun r2 () rec
    (mk-R5 35 2845 true))
  (define-fun recs () (Array Int rec)
    (_ as-array k!0))
  (define-fun y () Int
    1)
  (define-fun x () Int
    0)
  (define-fun r1 () rec
    (mk-R5 15 10001 true))
  (define-fun k!0!2 ((x!0 Int)) rec
    (ite (= x!0 1) (mk-R5 35 2845 true)
      (mk-R5 15 10001 true)))
  (define-fun k!1 ((x!0 Int)) Int
    (ite (= x!0 0) 0
      1))
  (define-fun k!0 ((x!0 Int)) rec
    (k!0!2 (k!1 x!0)))
)

これは少し読みにくいですが、指定したとおりのモデルが得られます。

ただし、これは実際にモデル化しようとしていたものではないように思えます。しかし、あなたの質問からはわかりにくいです。解決しようとしている実際の問題について説明すると、回答がより役立つ場合があります。

于 2017-01-06T06:58:22.857 に答える