наборы в средстве доказательства теорем Z3

У меня есть декларация в 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) карт вместо одной карты. Мой код правильный или есть другое решение, пожалуйста?


java z3 alloy
person Lola Alole    schedule 03.07.2015    source источник
comment
что вы имеете ввиду под чем??   -  person Lola Alole    schedule 03.07.2015
comment
Я имею в виду, как объявить один ко многим в Z3?   -  person Lola Alole    schedule 03.07.2015
comment
Был ли предоставленный ответ полезным и/или полезным для вас? Если нет, то было бы полезно услышать, почему нет, а также любые отзывы в целом. Если да, можете ли вы принять ответ?   -  person ivcha    schedule 02.09.2016

Ответы (1)


arrow_upward
0
arrow_downward

Вы можете закодировать отношение с помощью функции, которая возвращает набор:

(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
person ivcha    schedule 08.12.2015