z3 - Z3は、制約のないUFの値に対して「何でも」出力できますか？

Question

解釈されない関数の一部の値は、検索中に制約を受けない場合があります。たとえば、smtクエリでのみf(1)が呼び出される場合f(2)、は何でもかまいませf(3)ん。どの値が解決中に使用されなかったので、何でもかまいませんかを知る方法はありますか（いくつかのオプションがあるかもしれません）？

Answer 1

数量詞のない問題の場合、へのオプション:model-partialを使用してそれを達成できますtrue。次に例を示します（ここでも入手できます）。

(set-option :model-partial true)

(declare-fun f (Int) Int)

(assert (> (f 0) 0))
(assert (< (f 1) 0))

(check-sat)
(get-model)

この例では、次の出力を取得します。

sat
(model 
  (define-fun f ((x!1 Int)) Int
    (ite (= x!1 0) 1
    (ite (= x!1 1) (- 1)
      #unspecified)))
)

ところで、次のリリース（Z3 4.3.2）では、このオプションの名前がに変更されました:model.partial。次のリリースでは、オプションはモジュールにグループ化されます。