在 Z3 定理证明器中设置答案

【问题标题】：sets in Z3 theorem prover在 Z3 定理证明器中设置
【发布时间】：2015-07-03 16:59:12
【问题描述】：

我在合金中有一个声明

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 返回 Cards 的 (disj set) 而不是一张 Card。请问我的代码是正确的还是有不同的解决方案？

【问题讨论】：

你这是什么意思？？
我的意思是如何在 Z3 中声明一对多？
提供的答案对您有帮助和/或有用吗？如果不是，那么了解为什么不这样做以及一般的任何反馈都会很有用。如果可以，可以accept the answer吗？

标签： java z3 alloy

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

对应Alloy表达式：

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

【讨论】：