7

次の単純な SMT-LIB プログラムに示すような問題を見つけました。

SMT-LIB コード:

(declare-fun isDigit (Int) Bool)
(assert (forall ((x Int))
    (=>     (isDigit x)
        (and (>= x 0) (< x 10))
    )
  )
) 

(assert (forall ((x Int))   
    (=>     (and (>= x 12) (< x 15))
        (exists ((y Int))
            (and    (>= y 1) (< y 6)
                (isHost (- x y))
            )
        )
    )
  )
)

(check-sat)
(get-model)

これにより、次の警告が表示されます。

WARNING: failed to find a pattern for quantifier (quantifier id: k!18)
sat
........
........

警告メッセージが気になります。何かが欠けていることはわかっていますが、理解できません。誰でもこの問題で私を助けることができますか?

4

1 に答える 1

3

Z3 は量指定子を処理するために異なるエンジンを使用します ( Z3 ガイドを参照)。これらのエンジンの 1 つは、パターン マッチング (E-Matching) に基づいています。Z3 は、量化された式ごとにパターンを推測しようとします。見つからない場合は、警告メッセージが発行されます。ユーザーは、各量指定子のパターンを指定することもできます。ガイドはその方法を示しています。idk!18は、Z3 によって作成されたデフォルトの id です。行番号に基づいています（あなたの場合は18行目）。量指定子に独自の ID を指定することもできます。警告は、E マッチング エンジンが指定された量指定子を処理できないことをユーザーに伝えているだけです。

于 2012-02-08T16:37:20.610 に答える