-
Notifications
You must be signed in to change notification settings - Fork 0
/
set.sats
88 lines (76 loc) · 3.12 KB
/
set.sats
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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
datasort Set = (* hook into smt2 *)
sortdef set = Set
stacst set_emp: set = "ext#smt_set_emp"
stacst set_add: (set, int) -> set = "ext#smt_set_add"
stacst set_del: (set, int) -> set = "ext#smt_set_del"
stacst set_cap: (set, set) -> set = "ext#smt_set_cap"
stacst set_cup: (set, set) -> set = "ext#smt_set_cup"
stacst set_dif: (set, set) -> set = "ext#smt_set_dif"
stacst set_com: (set) -> set = "ext#smt_set_com"
stacst set_mem: (set, int) -> bool = "ext#smt_set_mem"
stacst set_sub: (set, set) -> bool = "ext#smt_set_sub"
stacst set_sup: (set, set) -> bool = "ext#smt_set_sup"
stacst set_eq: (set, set) -> bool = "ext#smt_set_eq"
stadef emp = set_emp
stadef + (e:int, s:set) = set_add (s, e)
stadef + = set_add
stadef - = set_del
stadef + = set_cup
stadef * = set_cap
stadef - = set_dif
stadef ~ = set_com
stadef mem = set_mem
stadef sub = set_sub
stadef < = set_sub
stadef sup = set_sup
stadef > = set_sup
stadef == = set_eq
stadef disj (a:set, b:set) = a * b == emp
(* An naive natural number bit set. *)
%{#
#ifndef LIBSS_SET
#define LIBSS_SET
#include <unistd.h>
#include <stdlib.h>
#include <stdint.h>
#define libss_set_emp() (0)
#define libss_set_add(s, n) ((s) | (1 << (n)))
#define libss_set_del(s, n) ((s) & ~(1 << n))
#define libss_set_cap(a, b) ((a) & (b))
#define libss_set_cup(a, b) ((a) | (b))
#define libss_set_dif(a, b) ((a) & ~(b))
#define libss_set_mem(s, n) (((a) & (1 << (n))) > 0)
#define libss_set_sub(a, b) ((a) | (b) == (b))
#define libss_set_sup(a, b) ((a) | (b) == (a))
#define libss_set_eq(a, b) ((a) == (b))
#define libss_set_disj(a, b) ((a) & (b) == 0)
#define libss_set_show(s) for(unsigned int mask=0x8000;mask;mask>>=1){printf("%d",!!(mask & s));}
#endif
%}
abst@ype set (set) = $extype "int32_t"
#define ATS_EXTERN_PREFIX "libss_"
fun set_emp (): set emp = "mac#%"
fun set_add {s:set} {n:int} (set s, int n): set (s + n) = "mac#%"
fun set_del {s:set} {n:int} (set s, int n): set (s - n) = "mac#%"
fun set_cap {s1,s2:set} (set s1, set s2): set (s1 * s2) = "mac#%"
fun set_cup {s1,s2:set} (set s1, set s2): set (s1 + s2) = "mac#%"
fun set_dif {s1,s2:set} (set s1, set s2): set (s1 - s2) = "mac#%"
fun set_mem {s:set} {n:int} (set s, int n): bool (mem (s, n)) = "mac#%"
fun set_sub {s1,s2:set} (set s1, set s2): bool (s1 < s2) = "mac#%"
fun set_sup {s1,s2:set} (set s1, set s2): bool (s1 > s2) = "mac#%"
fun set_eq {s1,s2:set} (set s1, set s2): bool (s1 == s2) = "mac#%"
fun set_disj {s1,s2:set} (set s1, set s2): bool (disj (s1, s2)) = "mac#%"
fun set_show {s:set} (set s): void = "mac#%"
overload + with set_add
overload - with set_del
overload + with set_cup
overload * with set_cap
overload - with set_dif
overload = with set_eq
overload emp with set_emp
overload mem with set_mem
overload sub with set_sub
overload < with set_sub
overload sup with set_sup
overload > with set_sup
overload disj with set_disj