Z3定理证明器中的集合

Question

我在Alloy 中有一个声明

sig Card{}
sig ATM {card :  disj  set Card}

我把它转换成Z3，就像这样：

1- (declare-sort ATM) 
2- (declare-fun isATM (ATM) Bool)
3- (declare-sort Card)
4- (declare-fun isCard (Card) Bool)
5- (declare-fun card (ATM Card) Bool)
6- (assert(forall ((c Card) (atm ATM)) (=> (card atm c) (and(isATM atm) (isCard c))))) 
7- (declare-fun disjSetCard (ATM) Card)
8- (assert(forall ((atm ATM) (c Card))  (=> (card atm c)(= c(disjSetCard atm)))))
check sat

问题是，在第7行中，如何使函数disjSetCard返回卡片的(disj set)，而不是一张卡片。请问我的代码是正确的还是有不同的解决方案？

Answer 1

您可以使用返回集合的函数对关系进行编码：

(define-sort Set (T) (Array T Bool))    
(declare-sort ATM)     
(declare-sort Card)    
(declare-fun ATMtoCard (ATM) (Set Card))

并将ATM的不同成员的字段值约束为不相交，其中：

(forall ((a Card) (x ATM) (y ATM))
(=>
  (and (select (ATMtoCard x) a) (select (ATMtoCard y) a))
  (= x y)
))

对应合金表达式：

all a: Card | all x, y: ATM |
a in x.card && a in y.card implies x = y