-
Notifications
You must be signed in to change notification settings - Fork 8
/
cvc4-set-tests.scm
59 lines (50 loc) · 1.25 KB
/
cvc4-set-tests.scm
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
(load "mk.scm")
(load "cvc4-driver.scm")
(load "test-check.scm")
(test "set-1"
(run* (q)
(z/ `(declare-fun ,q () (Set Int)))
(z/assert `(= ,q (singleton 1))))
'((singleton 1)))
(test "set-2"
(run* (q)
(z/ `(declare-fun ,q () (Set Int)))
(z/assert `(subset ,q (insert 2 (singleton 1)))))
'((as emptyset (Set Int))
(singleton 2)
(singleton 1)
(union [singleton 2] [singleton 1])))
(test "set-3"
(run 4 (q)
(z/ `(declare-fun ,q () (Set Int))))
'((as emptyset (Set Int))
(singleton 0)
(singleton (- 1))
(singleton (- 2))))
(test "set-4"
(run* (q)
(z/ `(declare-fun ,q () (Set Int)))
(z/assert
`(= (insert 1 2 (singleton 3))
(union ,q (insert 1 (singleton 2))))))
'((singleton 3)
(union [singleton 1] [singleton 3])
(union [singleton 2] [singleton 3])
(union [union (singleton 1) (singleton 2)] [singleton 3])))
(load "clpset.scm")
(test "subseto-1"
(run* (q)
(subseto (set ∅ 1 2) (set ∅ 1 2 3)))
'(_.0))
(test "subseto-1-not"
(run* (q)
(subseto (set ∅ 1 2 3) (set ∅ 1 2)))
'())
(test "not-subseto-1"
(run 1 (q)
(!subseto (set ∅ 1 2 3) (set ∅ 1 2)))
'(_.0))
(test "not-subseto-1-not"
(run 1 (q)
(!subseto (set ∅ 1 2) (set ∅ 1 2 3)))
'())