Z3の初期モデル値の指定

Question

モデルの初期 'ソフト'値の指定方法は？この初期モデルは、同様のクエリを解決した結果であり、このモデルが正しい部分を持つか、または現在のクエリで真実である可能性があります。

は現在、私は、増分解決やhard/soft constraintsでこれをシミュレートしています：

(define-fun trans_assumed ((a Int)) Int 
; an initial model, which may be (partially) true 
) 

(declare-fun trans_sought ((a Int)) Int) 

(declare-const p Bool) 
(assert (=> p (forall ((a Int)) (= (trans_assumed a) (trans_sought a))))) 
(check-sat p) ; in hope that trans_assumed values will be used as initial below 

; add here the main constraints for trans_sought function 

(check-sat) ; Z3 will use trans_assumed as a starting point for trans_sought 

これは本当にtrans_assumedするtrans_soughtの初期値を指定していますか？

解決のインクリメンタルモードは、シーケンシャルと比較して遅いです。初期値を導入するより良い方法はありますか？

Answer 1

これは良いアプローチだと思っていますが、より多くのブール変数を使用することを検討することもできます。今、それは「すべて」または「何もない」アプローチです。あなたのスクリプトで、(check-sat p)が実行されると、Z3はtrans_assumedとtrans_soughtが同じ解釈を持つモデルを探します。そのようなモデルが存在しない場合は、pを含むunsatコアを返します。 (check)が実行されるとき、Z3はpをfalseに割り当てることが自由であり、ユニバーサル量限定子は本質的に無関心である。つまり、trans_assumedとtrans_soughtは全く異なる場合があります。

複数のブール変数を使用してtrans_soughtの解釈を制御すると、柔軟性が増します。 問題の残りの部分が数量化されていない場合は、汎用量子を削除することを検討する必要があります。これは、有限個の点でtrans_soughtの値だけを気にしている場合に実行できます。

trans_assumed(0) = 1とtrans_assumed(1) = 10があるとします。その後、我々は書くことができます。このエンコーディングで

assert (=> p0 (= (trans_sought 0) 1))) 
assert (=> p1 (= (trans_sought 1) 10))) 

を、私たちは(check-sat p0 p1)、(check-sat p0)、(check-sat p1)