Z3のソートのドメインを単一の値に制限する方法を教えてください。

Question

my Z3 programに次の規則を使用して、sに、並べ替えSの唯一の可能な値を設定しています。

Z3: ERROR: WARNING: failed to find a pattern for quantifier (quantifier id: k!8) 

特定の種類のドメインは単一の値のみを持っていることを確認するための正しい方法は何ですか？

(assert (forall ((t S)) (= t s))) 

しかし、上記の式はZ3レポート以下のエラーになりますか

Answer 1

メッセージ

Z3: ERROR: WARNING: failed to find a pattern for quantifier (quantifier id: k!8)

は誤解を招くです。これはちょうど警告であり、 "ERROR"という言葉は偶然そこにあります。これは修正され、次のリリースで利用可能になります。 警告は、E-matchingモジュールが量子を無視することをユーザーに通知するだけです。 しかし、Z3では、多くのエンジンを使用して定量化された数式を処理しています。 MBQIモジュールは、この定量化式を処理し、などの問題のために満足割り当て構築することができる：言われている、上記定量化式は、単一の要素とのソートを指定するための最良の方法ではないことを

(declare-sort S)

(declare-fun s() S)

(assert (forall ((t S)) (= t s)))

(declare-fun a() S)

(declare-fun b() S)

(assert (= a b))

(check-sat)

(model)

を。 データ型を使用して、列挙型をエンコードできます。 たとえば、次のコマンドは要素e1 ... enを持つソートSを定義します。 (declare-datatypes ((S e1 e2 … en))) 唯一の要素でソートを使用して指定することができます。 (declare-datatypes ((S e))) 次の例では、充足不能である：私はE-マッチングモジュールを無効にすると

(declare-datatypes ((S elem)))

(declare-const a S)

(declare-const b S)

(assert (not (= a b)))

(check-sat)