Z3能否爲UF的無約束值輸出「任何東西」？

Question

在搜索過程中，未解釋函數的某些值可能不受限制。例如，如果在smt查詢中只有f(1)被調用，那麼f(2),f(3)可以是任何東西。有沒有辦法（有些選項可能）知道在解決過程中哪些值沒有被使用，因此可以是任何東西？

Answer 1

對於無量詞的問題，可以使用選項:model-partial至true來實現。 下面是一個例子（也可here）：

(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))) 
) 

順便說一句，在下一版本（4.3.2 Z3），這個選項改名爲:model.partial。在下一個版本中，這些選項分組在模塊中。