litex/builtin_code/
set_operators.rs

1// Set unions, intersections, subset, finite_set count, etc.
2
3pub const BUILTIN_ENV_CODE_FOR_SET_OPERATORS: &str = r#"
4
5prop in_intersect_is_in_both(z set, A set, B set):
6    $in(z, A)
7    $in(z, B)
8
9prop in_set_minus_is_in_first_operand(z set, A set, B set):
10    $in(z, A)
11
12prop in_set_minus_is_not_in_second_operand(z set, A set, B set):
13    not $in(z, B)
14
15prop in_cup_via_member_set(z set, F set, Y set):
16    $in(z, cup(F))
17
18know:
19    forall z set, A set, B set:
20        $in(z, A)
21        =>:
22            $in(z, union(A, B))
23
24    forall z set, A set, B set:
25        $in(z, B)
26        =>:
27            $in(z, union(A, B))
28
29    forall z set, A set, B set:
30        $in(z, union(A, B))
31        =>:
32            $in(z, A) or $in(z, B)
33
34    forall z set, A set, B set:
35        $in(z, A)
36        $in(z, B)
37        =>:
38            $in(z, intersect(A, B))
39
40    forall z set, A set, B set:
41        $in(z, intersect(A, B))
42        =>:
43            $in_intersect_is_in_both(z, A, B)
44
45    forall z set, A set, B set:
46        not $in(z, A)
47        =>:
48            not $in(z, intersect(A, B))
49
50    forall z set, A set, B set:
51        not $in(z, B)
52        =>:
53            not $in(z, intersect(A, B))
54
55    forall A, B set:
56        intersect(A, B) $subset A
57
58    forall A, B set:
59        intersect(A, B) $subset B
60
61    forall A, B set:
62        A $subset union(A, B)
63
64    forall A, B set:
65        B $subset union(A, B)
66
67    forall A, B set:
68        union(A, B) = union(B, A)
69
70    forall A, B set:
71        intersect(A, B) = intersect(B, A)
72
73    forall A, B, C set:
74        union(union(A, B), C) = union(A, union(B, C))
75
76    forall A, B, C set:
77        intersect(intersect(A, B), C) = intersect(A, intersect(B, C))
78
79    forall A, B set:
80        union(A, intersect(A, B)) = A
81
82    forall A, B set:
83        intersect(A, union(A, B)) = A
84
85    forall A set:
86        union(A, A) = A
87
88    forall A set:
89        intersect(A, A) = A
90
91    forall A set:
92        union(A, {}) = A
93
94    forall A set:
95        intersect(A, {}) = {}
96
97    forall A, B, C set:
98        intersect(A, union(B, C)) = union(intersect(A, B), intersect(A, C))
99
100    forall A, B, C set:
101        union(A, intersect(B, C)) = intersect(union(A, B), union(A, C))
102
103    forall z set, A set, B set:
104        $in(z, A)
105        not $in(z, B)
106        =>:
107            $in(z, set_minus(A, B))
108
109    forall z set, A set, B set:
110        $in(z, set_minus(A, B))
111        =>:
112            $in_set_minus_is_in_first_operand(z, A, B)
113
114    forall z set, A set, B set:
115        $in(z, set_minus(A, B))
116        =>:
117            $in_set_minus_is_not_in_second_operand(z, A, B)
118
119    forall A, B set:
120        set_minus(A, B) $subset A
121
122    forall A, B set:
123        set_diff(A, B) = union(set_minus(A, B), set_minus(B, A))
124
125    forall z set, F set, Y set:
126        $in(Y, F)
127        $in(z, Y)
128        =>:
129            $in_cup_via_member_set(z, F, Y)
130
131    forall A, B finite_set:
132        A $subset B
133        =>:
134            count(A) <= count(B)
135
136    forall A, B finite_set:
137        A $superset B
138        =>:
139            count(A) >= count(B)
140"#;
litex/builtin_code/set_operators.rs

litex/builtin_code/
set_operators.rs
