4

ゴールとサブゴールではなく、z3で定義された未解釈の関数に簡略化を適用する方法はありますか？

私は次のz3コードを持っています：

(declare-fun f (Bool Bool) Bool)
(assert (forall ((b1 Bool) (b2 Bool))
        (implies b2 (f b1 b2))))
(assert (exists ((b1 Bool) (b2 Bool))
        (not (f b1 b2))))
(check-sat)
(get-model)

そして、次の出力が得られます。

sat
(model 
(define-fun b1!1 () Bool
  false)
(define-fun b2!0 () Bool
  false)
(define-fun k!7 ((x!1 Bool)) Bool
  false)
(define-fun f!8 ((x!1 Bool) (x!2 Bool)) Bool
  (ite (and (= x!1 false) (= x!2 true)) true
  false))
(define-fun k!6 ((x!1 Bool)) Bool
  (ite (= x!1 false) false
  true))
(define-fun f ((x!1 Bool) (x!2 Bool)) Bool
  (f!8 (k!7 x!1) (k!6 x!2)))
)

fの定義に書き換え規則を適用することにより、次の導出によってfが2番目の引数（x！2）に等しいことがわかります。

(f!8 (k!7 x!1) (k!6 x!2))
= (f!8 false (k!6 x!2))
= (f!8 false x!2)
=(x!2)

z3に次の定義を自動的に生成させる方法はありますか？

(define-fun f ((x!1 Bool) (x!2 Bool)) Bool
  (x!2))

ご協力いただきありがとうございます。よろしく、オズワルド。

4

1 に答える 1

4

1つのオプションは、Z3に式を評価するように依頼することです。(f x y)ここでx、およびyは新しいブール定数です。evalコマンドは現在のモデルで評価され(f x y)、y例で生成されます。これが完全な例です（ここからオンラインでも入手できます）：

(declare-fun f (Bool Bool) Bool)

; x and y are free Boolean constants that will be used to create the expression (f x y)
(declare-const x Bool)
(declare-const y Bool)

(assert (forall ((b1 Bool) (b2 Bool))
        (implies b2 (f b1 b2))))
(assert (exists ((b1 Bool) (b2 Bool))
        (not (f b1 b2))))
(check-sat)

(eval (f x y))
于 2013-03-11T20:21:55.620 に答える