blob: abb7faf1056e1890cdb1d61d0120688e8093ed38 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
(declare-fun r1 () (Set (Tuple String Int)))
(declare-fun r2 () (Set (Tuple Int String)))
(declare-fun r () (Set (Tuple String String)))
(declare-fun s () (Set (Tuple String String)))
(declare-fun t () (Set (Tuple String Int Int String)))
(declare-fun lt1 () (Set (Tuple Int Int)))
(declare-fun lt2 () (Set (Tuple Int Int)))
(declare-fun i () Int)
(assert (= r1 (insert (mkTuple "a" 1) (mkTuple "b" 2) (mkTuple "c" 3) (singleton (mkTuple "d" 4)))))
(assert (= r2 (insert (mkTuple 1 "1") (mkTuple 2 "2") (mkTuple 3 "3") (singleton (mkTuple 17 "17")))))
(assert (= r (join r1 r2)))
(assert (= s (transpose r)))
(assert (= t (product r1 r2)))
(assert (= lt1 (insert (mkTuple 1 2) (mkTuple 2 3) (mkTuple 3 4) (singleton (mkTuple 4 5)))))
(assert (= lt2 (tclosure lt1)))
(assert (= i (card t)))
(check-sat)
|
