從模型中獲取具體數組值

Question

我正在使用Z3檢查數組屬性片段中公式的可滿足性。 Z3返回的數組變量的模型通常使用其他if-expressions，if-then-else案例分析等來表達。我想以某種方式解析Z3輸出的模型並創建數組，以滿足輸入SMT-LIB公式，明確地。

例如，我希望能夠以某種方式總是簡化Z3輸出以下形式的模型：

A -> { 
    1 -> 3 
    2 -> 4 
    else -> 6 
} 

有一些簡單的方法來遍歷模型（？使用C API），並創建一個顯式數組代表模型？

Answer 1

不幸的是，消息中描述的輸出格式不足以描述數組屬性片段中每個可滿足公式的模型。例如，請考慮以下簡單示例。

(declare-fun f (Int) Int) 
(declare-const a Int) 
(declare-const b Int) 

(assert (forall ((i Int) (j Int)) (=> (<= i j) (<= (f i) (f j))))) 
(assert (< (f a) (f b))) 

(check-sat) 
(get-model) 

公式f被非遞減，它有兩個點a和b S.T. f(a) < f(b)。在任何模型中，我們必須對所有值i <= a,f(i) <= f(a)以及所有值j >= b,f(b) <= f(j)都具有該值。也就是，

f(i) <= f(a) < f(b) <= f(j)。

單個else不起作用。 Z3產生對f的解釋，該解釋本質上是「階梯函數」。你可以嘗試上面的例子here。