鮮明的陣列值的求解器

Question

我想圍繞着一些時間來得到一個相當簡單的要求做： 我宣佈一個新的數據類型

(declare-datatypes() ((A (mk_A (key Int) (var1 Int) (var2 Int)))))

其中key應該像在數據庫中的主鍵即，A的每個不同實例應具有不同的key值。 不同的實例（功能）的容器，如下所示：

(declare-const A_instances (Array Int A))

到目前爲止好。我試圖創建一個斷言，以便A_instances中的所有實例都有不同的key字段。因此，對於A_instances (key (select A_instances i))中的每個索引i應該是不同的。但它返回unknown。

有人有什麼建議嗎？

Answer 1

一種可能的解決方案是

(declare-datatypes() ((A (mk_A (key Int) (var1 Int) (var2 Int))))) 
(declare-const A_instances (Array Int A)) 
(declare-fun j() Int) 
(assert (forall ((i Int)) (implies (distinct i j) 
          (distinct (key (select A_instances i)) 
            (key (select A_instances j)))  ) )) 
(check-sat) 

和相應的輸出是

sat