z3 - z3 SMT 求解器中的不同数组值

Question

我尝试了一段时间来完成一个相当简单的要求:
我声明了一个新的数据类型
(declare-datatypes () ((A (mk_A (key Int) (var1 Int) (var2 Int)))))
哪里key应该充当数据库中的主键，即 A 的每个不同实例应该有一个不同的 key值(value)。
不同实例(函数)的容器如下所示:
(declare-const A_instances (Array Int A))
到现在为止还挺好。我试图创建一个断言，使得 A_instances 中的所有实例有一个不一样的key field 。因此，对于每个索引 i在 A_instances (key (select A_instances 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