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
(check (= 0 (& 10 0)))
(check (= 8 (& 8 10)))
(check (= 10 (| 8 10)))
(check (= 2 (^ 8 10)))
(check (= 8 (<< 1 3)))
(check (= 1 (>> 8 3)))
(check (= 2 (% 8 3)))
(check (= 2 (/ 8 3)))
(check (= -1 (not-i64 0)))
; bitsets
;(function bs-union (i64 i64) i64)
;(rewrite (bs-union a b) (| a b))
;(function bs-inter (i64 i64) i64)
;(rewrite (bs-inter a b) (& a b))
;(function bs-comp (i64) i64)
;(rewrite (bs-comp a) (bvnot a))
; singleton set
;(function bs-sing (i64) i64)
;(rewrite (bs-sing a) (1 << a))
;(function bs-insert (i64 i64) i64)
;(rewrite (bs-insert s x) (| s (1 << a))
;(function bs-diff (i64 i64) i64)
;(rewrite (bs-diff a b) (^ a (bs-inter a b))
;(let bs-empty 0)
;(let bs-subset (i64 i64) bool)
;(rewrite (bs-subset x y) (is-zero (bs-diff x y)))
;(let bs-is-elem (i64 i64) bool)
;(rewrite (bs-is-elem s x) (not (is-zero (bs-inter s (sing x)))))