指定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_sought指定的初始值是trans_assumed？

與順序相比，增量求解的模式較慢。任何更好的方法來引入初始值？

Answer 1

我認爲這是一個很好的方法，但是你可以考慮使用更多的布爾變量。現在，這是一個「全部」或「無」的方法。在你的腳本中，當執行(check-sat p)時，Z3將尋找一個模型，其中trans_assumed和trans_sought具有相同的解釋。如果這種模型不存在，它將返回包含p的不含核心。當執行(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)