2

(get-assignment) コマンドは、シンボルのリストと、ブール型の場合はその true/false 値を返す必要があります。私の理解では、これは :produce-assignments が true に設定されていて、(check-sat) が sat を返す場合にのみ実行できます。ただし、Z3 でこれをテストするために小さなスクリプトを実行すると、(get-assignment) は () - 空白を返すだけです。これが私のスクリプトです：

(set-option :produce-assignments true)
(set-logic QF_UF)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (= a b )) 
(check-sat)
(get-assignment)
4

1 に答える 1

2

のセマンティクスget-assignmentは直感的ではありません。サブフォーミュラの値を表示しますnamed。SMT 2.0 リファレンス(62 ページ)から:

get-assignment (29) 既に説明した他のいくつかのコマンド (get-proof など) と同様に、このコマンドを発行することができます。デフォルトでは false である Produce-assignments オプションが true に設定されている場合のみ (以下のセクション 5.1.7 を参照)。このオプションをサポートするためにソルバーは必要ありません。get-value と同様に、sat を報告する check-sat コマンド、または任意で、assertion-set コマンドを介さずに不明を報告するコマンドの後にのみ発行できます。このコマンドは、すべてのペア (fb) のシーケンスを返します。ここで、b は true または false であり、f は、すべてのアサーションのセット内の (t という名前の f) という形式の (サブ) 項のラベルであり、t はブール型です。get-value と同様に、

2 つの名前付きサブフォーミュラを使用した同じ例を次に示します (ここでもオンラインで入手できます)。

(set-option :produce-assignments true)
(set-logic QF_UF)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (! (= (! a :named a_val) b ) :named eq_val)) 
(check-sat)
(get-assignment)
于 2013-05-08T14:22:27.603 に答える