鲜明的阵列值的求解器

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