我试了一段时间来完成一个相当简单的要求:
我声明了一种新的数据类型
(declare-datatypes()((A(mk_A(key Int)(var1 Int)(var2 Int)))))
其中key应该像数据库中的主键一样,即A的每个不同实例应该具有不同的键值.
不同实例(函数)的容器如下所示:
(declare-const A_instances(Array Int A))
到现在为止还挺好.我尝试创建一个断言,以便A_instances中的所有实例都有不同的键字段.因此,对于A_instances中的每个索引i(key(select A_instances i))应该是不同的.然而,它返回未知.
有人有什么建议吗?
最佳答案 一种可能的解决方案是
(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