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

【问题标题】：Distinct Array values in z3 SMT solverz3 SMT 求解器中的不同数组值
【发布时间】：2014-10-23 06:01:22
【问题描述】：

我尝试了一段时间来完成一个相当简单的要求：我声明了一个新的数据类型

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

有人有什么建议吗？

【问题讨论】：

标签： z3 smt

【解决方案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

【讨论】：