1

私はこの次の主張を書きました：

(assert (!
    (forall ((A Set) (B Set))
        (= 
            (= A B) 
            (and (subset A B)(subset B A)))
:no-pattern)))

エラー " " が表示されるのはなぜinvalid expression, unexpected inputですか? 構文エラーをチェックするために、ガイドから例をコピーし、を に置き換えました。それもエラーになります。:pattern (…):no-pattern

4

1 に答える 1

2

注釈:no-patternは、引数として式を想定しています。普遍的に量化された数式Fにパターンの注釈が付けられていない場合、Z3 はヒューリスティックに のパターンを選択しますF。注釈:no-patternは、Z3 に、発生する部分式をパターンとして使用してFはならないことを指示します。これがあなたの例です（http://rise4fun.com/Z3/KfO5でも入手できます）：

(declare-sort Set)
(declare-fun mysubset (Set Set) Bool)

(assert 
    (forall ((A Set) (B Set))
        (! (= 
            (= A B) 
            (and (mysubset A B) (mysubset B A)))
           :no-pattern (mysubset A B))))

(check-sat)

注意: 方程式 ( など(= A B)) は、Z3 によってパターンとして選択されることはありません。

他の例http://rise4fun.com/Z3/njVuへのリンクを次に示します。

ところで、注釈:patternは 2 種類の引数を受け入れます。または式のリスト。Z3 ガイドには、次の注釈:pattern ((f (g x))があります。((f (g x))は、式 を含む長さ 1 のリストです(f (g x))。に置き換える:patternと:no-pattern、 は式ではないため、エラーが発生します((f (g x))。一方、:no-pattern (f (g x)有効な:no-pattern注釈です。

最後に、:patternZ3 はマルチパターン ( guide ) をサポートしているため、式のリストを受け入れます。

于 2012-11-23T19:27:54.430 に答える