有沒有辦法使用Z3來獲取涉及集合的約束模型？

Question

我正在嘗試在Z3中對模型進行建模，以便能夠找到涉及集合的約束條件的模型 。我現在用一個數組表示一個數組。如果數組中的相應條目爲真，則元素屬於集合 。然後我有一些公理 ，我在約束中使用。

以下是SMT 2.0中的示例。

(define-sort Set (T) (Array T Bool)) 

(declare-fun |Set#Card| ((Set Int)) Int) 
(assert (forall ((s (Set Int))) 
     (! 
     (<= 0 (|Set#Card| s)) 
      :pattern ((|Set#Card| s))))) 

(declare-fun |Set#Singleton| (Int) (Set Int)) 
(assert (forall ((r Int)) 
     (! 
     (select (|Set#Singleton| r) r) 
     :pattern ((|Set#Singleton| r))))) 
(assert (forall ((r Int) (o Int)) 
     (iff (select (|Set#Singleton| r) o) (= r o)))) 
(assert (forall ((r Int)) (= (|Set#Card| (|Set#Singleton| r)) 1))) 

(declare-fun s() (Set Int)) 
(assert (= 1 (|Set#Card| s))) 
;(assert (= 1 (|Set#Card| (|Set#Singleton| 1)))) 
;(assert (not (= 1 (|Set#Card| (|Set#Singleton| 1))))) 
(check-sat) 
(get-info :reason-unknown) 
(get-model) 

我的問題是，我得到unknown，因此大多數情況下沒有模型。 我認爲我的公理化太弱。在上面的例子中，我想 喜歡得到一個包含一個元素的集合s的模型。

有誰知道如何使用Z3來獲取約束模型 涉及集？

每個答案都有幫助。也就是說，我誤解了Z3可以做什麼，並且不能做到。關於如何處理這個問題的想法也歡迎 （其他工具建議，...）。

Answer 1

的問題是，Z3將無法建立滿足斷言例如示範：

(assert (forall ((r Int) (o Int)) 
     (iff (select (|Set#Singleton| r) o) (= r o)))) 

一個可能的解決方法是，以限定|Set#Singleton|代替axiomatizing它的。 我們可以使用const數組運算符和store來定義它。這裏是一個可能的定義：

(define-fun |Set#Singleton| ((r Int)) (Set Int) 
      (store ((as const (Set Int)) false) r true)) 

Here是這一定義修改後的示例的鏈接。 Z3在使用定義後返回sat和一個模型。

在文本界面中，我們必須使用as構造來指定我們想要的常量數組的種類。 請注意，我們可以使用Z3中提供的擴展陣列理論編碼多個集合操作。 This paper有其他詳細信息。但是，這種方法不能編碼|Set#Card|函數。

另一種選擇是對unknown結果使用「候選模型」。這不是理想的解決方案，但有幾個用戶這樣做。