Z3の未解釈関数の表現について

Question

私は簡単な質問があります。私は単純なプログラム（Z3 NET APIを使用して）を書いて、次のように出力を得ました。

プログラム（一部）：

 Sort[] domain = new Sort[3]; 
     domain[0] = intT; 
     domain[1] = intT;   
     domain[2] = intT; 
     FPolicy = z3.MkFuncDecl("FPolicy", domain, boolT);  

     Term[] args = new Term[3]; 
     args[0] = z3.MkNumeral(0, intT); 
     args[1] = z3.MkNumeral(1, intT); 
     args[2] = z3.MkNumeral(30, intT); 
     z3.AssertCnstr(z3.MkApp(FPolicy, args)); 

     args[1] = z3.MkNumeral(2, intT); 
     args[2] = z3.MkNumeral(20, intT); 
     z3.AssertCnstr(z3.MkApp(FPolicy, args)); 

出力：私は、私が作ることが疑問に思って

FPolicy -> { 
    0 1 30 -> true 
    0 2 20 -> true  
    else -> true 
} 

- 偽として "他>真"（すなわち、 "他 - >偽"） 。

Answer 1

:-)より良いソリューションを見るのを楽しみにしています

、Z3（3.2）rangeでより頻繁に発生しelse値を選択します。 rangeここでは、Z3が特定の有限集合の入力値に割り当てられた有限集合の値を意味します。この例ではrangeにはtrueしか発生していません。したがって、trueがelse値として選択されます。

数値限定子のフリー（および配列のない）問題の場合、オプション:model-compact trueを使用しない場合、elseの値は重要ではありません。 つまり、式Fが充足可能であれば、Z3はMというモデルを生成します。次に、elseの値をMに変更すると、結果のモデルM’はまだFのモデルです。 を無視するか、入力式Fが数量化されていない場合はFは配列理論を使用せず、:model-compact trueは使用しません。 このプロパティは現在Z3で実装されているアルゴリズムに基づいており、将来変更される可能性があります。 対照的に、mhsによって提供されるソリューションは、Z3の実装の変更によって影響を受けません。エンコーディングでは、SMTソルバ（モデルの作成に成功したソルバ）は、限定子の前件で指定されていないすべての点で、関数の値としてfalseを使用する必要があります。

もう1つの方法は、default演算子を使用し、配列を使用して問題をエンコードすることです。 default演算子を使用する場合は、配列をペアとして表示する必要があります（実際の配列、デフォルト値）。 このデフォルト値は、モデル構築中にelse値を提供するために使用されます。 Z3には、storeとmapの演算子にデフォルト値を伝播させるための組み込み公理もいくつかあります。 このアプローチを使用してエンコードされた問題は次のとおりです。

(set-option :produce-models true) 
(declare-const FPolicy (Array Int Int Int Bool)) 

(assert (select FPolicy 0 1 30)) 
(assert (select FPolicy 0 2 20)) 
(assert (not (default FPolicy))) 

(check-sat) 
(get-model) 

Answer 2

次のようになります（）？

(set-option :MBQI true) 

(declare-fun FPolicy (Int Int Int) Bool) 

(assert (forall ((x1 Int) (x2 Int) (x3 Int)) (! 
    (implies 
    (not 
     (or 
     (and (= x1 0) (= x2 1) (= x3 30)) 
     (and (= x1 0) (= x2 2) (= x3 20)))) 
     (= (FPolicy x1 x2 x3) false)) 
    :pattern (FPolicy x1 x2 x3)))) 

(assert (FPolicy 0 1 30)) 
(assert (FPolicy 0 2 20)) 

(check-sat) 
(get-model) 

私が見ることができる利点は、forall-constraintに触れずにFPolicy（0 1 30）== falseに変更できることです。 明白な欠点は、基本的にすべての引数タプルを2回言及し、作成されたモデルがむしろ複雑であることです。私は数量詞の自由の問題について