1

Z3 を使用して未知の射影関数を含む方程式を解き、方程式を満たす関数の有効な解釈を見つけようとしています。たとえば、方程式の場合:snd . f = g . fst有効な解釈はf = \(x,y) -> (y,x)とg = idです。Z3 が高次でないことはわかっているので、問題を一次形式でエンコードしようとしています。たとえば、次のf = g.fstように使用します。

(declare-datatypes (T) ((Tree (leaf (value T)) (node (children TreeList)))
                        (TreeList nil (cons (head Tree) (tail TreeList)))))
(define-fun fst ((x (Tree Int))) (Tree Int) (head (children x)))
(define-fun snd ((x (Tree Int))) (Tree Int) (head (tail (children x))))
(declare-fun f ((Tree Int)) (Tree Int))
(declare-fun g ((Tree Int)) (Tree Int))
(assert (forall ((x (Tree Int))) (= (f x) (g (fst x)))))
(check-sat)
(get-model)

どのような種類の作品が戻ってきますか:

(define-fun g ((x!1 (Tree Int))) (Tree Int)
  (leaf 0))
(define-fun f ((x!1 (Tree Int))) (Tree Int)
  (g (head (children x!1))))

ただし、snd . f = g . fst（ツリーをペアに単純化して試してみました）：

(declare-datatypes (T) ((Pair (leaf (value T)) (pair (fst Pair) (snd Pair)))))
(declare-fun f ((Pair Int)) (Pair Int))
(declare-fun g ((Pair Int)) (Pair Int))
(assert (forall ((x (Pair Int))) (= (snd (f x)) (g (fst x)))))

私は得るunknown。

また、ブール値または整数をパラメーターとして使用するだけでADTを使用せずに同様の問題をエンコードしようとしましたが、モデルは関数に定数値を割り当てるだけです。また、関数定数、恒等関数、ペアワイズおよびシーケンシャル コンポジション用の単純な ADT を定義してから、 のような式を単純化できる「equals」関数を定義しようとしましたf.id = fが、これには次のような再帰関数が含まれます。

(declare-datatypes () (
  (Fun id 
       (fun (funnum Int))
       (seq (after Fun) (before Fun))
       (pair (fst Fun) (snd Fun)) )))
(define-fun eq ((x Fun) (y Fun)) Bool (or
    (= x y)
      (eq x (seq y id)) ; id neutral for seq
      (eq x (seq id y))
      (eq y (seq x id))
      (eq y (seq id x))))
(declare-const f Fun)
(declare-const g Fun)
(assert (eq f (seq id g)))
(check-sat)
(get-model)

これは明らかに無効です。または、解釈されていない関数を使用すると、「eq」が定数関数になります。

(declare-fun eq (Fun Fun) Bool)
(assert (forall ((x Fun) (y Fun))  ; semantic equality
    (= (eq x y) (or
      (= x y) ; syntactic eq
      (eq x (seq y id)) ; id neutral for seq
      (eq x (seq id y))
      (eq y (seq x id))
      (eq y (seq id x))
    ))
))
=>
(define-fun eq ((x!1 Fun) (x!2 Fun)) Bool
    true)

Int -> Int 型の関数を含む方程式と同様に、これは f と g の定数関数を返します。

(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (forall ((x Int)) (= (+ (f x) 1) (+ (g x) 2)) ))

これらのタイムアウトを追加します。

(assert (forall ((x Int) (y Int)) (=> 
  (not (= x y)) 
  (not (= (g x) (g y))))))
(assert (forall ((x Int) (y Int)) (=> 
  (not (= x y)) 
  (not (= (f x) (f y))))))

この種のことを機能させる方法はありますか？

どうもありがとう！

4

1 に答える 1

1

Z3 は本質的に有限モデルを検索するため、関数方程式を直接解くのにはあまり適していません。この種のモデルを見つけるための主なトリックは、構成可能な関数の代替解釈の有限セットを提供することによって、式を強化することです。たとえば、f(x) を恒等、順列、または x または y の繰り返しにするか、フィールドの 1 つで定数値を返すことができます。これは、単純な算術演算を実行する関数で構成できます。許可する構成の数を制限する必要があります。g のテンプレートの同様のセットをアサートします。これまでのところ、これはビットベクトルに最適です。このような解釈の検索スペースは、簡単に圧倒されてしまいます。代数データ型とテンプレートを使用して例を試しました。この場合、Z3 は解釈を見つけることができません。

于 2014-10-03T16:47:07.400 に答える