ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
mpmDsd.c
Go to the documentation of this file.
1
20
21#include "mpmInt.h"
22#include "misc/extra/extra.h"
23
24ABC_NAMESPACE_IMPL_START
25
29
30static Mpm_Dsd_t s_DsdClass6[595] = {
31 { 0, 0, 1, ABC_CONST(0x0000000000000000), "0" }, // 0
32 { 1, 0, 2, ABC_CONST(0xAAAAAAAAAAAAAAAA), "a" }, // 1
33 { 2, 1, 3, ABC_CONST(0x8888888888888888), "(ab)" }, // 2
34 { 2, 3, 4, ABC_CONST(0x6666666666666666), "[ab]" }, // 3
35 { 3, 2, 4, ABC_CONST(0x8080808080808080), "(abc)" }, // 4
36 { 3, 2, 4, ABC_CONST(0x7070707070707070), "(!(ab)c)" }, // 5
37 { 3, 4, 6, ABC_CONST(0x7878787878787878), "[(ab)c]" }, // 6
38 { 3, 4, 5, ABC_CONST(0x6060606060606060), "([ab]c)" }, // 7
39 { 3, 6, 8, ABC_CONST(0x9696969696969696), "[abc]" }, // 8
40 { 3, 3, 4, ABC_CONST(0xCACACACACACACACA), "<abc>" }, // 9
41 { 4, 3, 5, ABC_CONST(0x8000800080008000), "(abcd)" }, // 10
42 { 4, 3, 5, ABC_CONST(0x7F007F007F007F00), "(!(abc)d)" }, // 11
43 { 4, 5, 8, ABC_CONST(0x7F807F807F807F80), "[(abc)d]" }, // 12
44 { 4, 3, 5, ABC_CONST(0x7000700070007000), "(!(ab)cd)" }, // 13
45 { 4, 3, 5, ABC_CONST(0x8F008F008F008F00), "(!(!(ab)c)d)" }, // 14
46 { 4, 5, 8, ABC_CONST(0x8F708F708F708F70), "[(!(ab)c)d]" }, // 15
47 { 4, 5, 7, ABC_CONST(0x7800780078007800), "([(ab)c]d)" }, // 16
48 { 4, 7, 12, ABC_CONST(0x8778877887788778), "[(ab)cd]" }, // 17
49 { 4, 5, 6, ABC_CONST(0x6000600060006000), "([ab]cd)" }, // 18
50 { 4, 5, 6, ABC_CONST(0x9F009F009F009F00), "(!([ab]c)d)" }, // 19
51 { 4, 7, 10, ABC_CONST(0x9F609F609F609F60), "[([ab]c)d]" }, // 20
52 { 4, 7, 9, ABC_CONST(0x9600960096009600), "([abc]d)" }, // 21
53 { 4, 9, 16, ABC_CONST(0x6996699669966996), "[abcd]" }, // 22
54 { 4, 4, 5, ABC_CONST(0xCA00CA00CA00CA00), "(<abc>d)" }, // 23
55 { 4, 6, 8, ABC_CONST(0x35CA35CA35CA35CA), "[<abc>d]" }, // 24
56 { 4, 3, 6, ABC_CONST(0x0777077707770777), "(!(ab)!(cd))" }, // 25
57 { 4, 5, 9, ABC_CONST(0x7888788878887888), "[(ab)(cd)]" }, // 26
58 { 4, 5, 7, ABC_CONST(0x0666066606660666), "([ab]!(cd))" }, // 27
59 { 4, 7, 8, ABC_CONST(0x0660066006600660), "([ab][cd])" }, // 28
60 { 4, 4, 6, ABC_CONST(0xCAAACAAACAAACAAA), "<ab(cd)>" }, // 29
61 { 4, 6, 8, ABC_CONST(0xACCAACCAACCAACCA), "<ab[cd]>" }, // 30
62 { 4, 4, 5, ABC_CONST(0xF088F088F088F088), "<(ab)cd>" }, // 31
63 { 4, 6, 6, ABC_CONST(0xF066F066F066F066), "<[ab]cd>" }, // 32
64 { 5, 4, 6, ABC_CONST(0x8000000080000000), "(abcde)" }, // 33
65 { 5, 4, 6, ABC_CONST(0x7FFF00007FFF0000), "(!(abcd)e)" }, // 34
66 { 5, 6, 10, ABC_CONST(0x7FFF80007FFF8000), "[(abcd)e]" }, // 35
67 { 5, 4, 6, ABC_CONST(0x7F0000007F000000), "(!(abc)de)" }, // 36
68 { 5, 4, 6, ABC_CONST(0x80FF000080FF0000), "(!(!(abc)d)e)" }, // 37
69 { 5, 6, 10, ABC_CONST(0x80FF7F0080FF7F00), "[(!(abc)d)e]" }, // 38
70 { 5, 6, 9, ABC_CONST(0x7F8000007F800000), "([(abc)d]e)" }, // 39
71 { 5, 8, 16, ABC_CONST(0x807F7F80807F7F80), "[(abc)de]" }, // 40
72 { 5, 4, 6, ABC_CONST(0x7000000070000000), "(!(ab)cde)" }, // 41
73 { 5, 4, 6, ABC_CONST(0x8FFF00008FFF0000), "(!(!(ab)cd)e)" }, // 42
74 { 5, 6, 10, ABC_CONST(0x8FFF70008FFF7000), "[(!(ab)cd)e]" }, // 43
75 { 5, 4, 6, ABC_CONST(0x8F0000008F000000), "(!(!(ab)c)de)" }, // 44
76 { 5, 4, 6, ABC_CONST(0x70FF000070FF0000), "(!(!(!(ab)c)d)e)" }, // 45
77 { 5, 6, 10, ABC_CONST(0x70FF8F0070FF8F00), "[(!(!(ab)c)d)e]" }, // 46
78 { 5, 6, 9, ABC_CONST(0x8F7000008F700000), "([(!(ab)c)d]e)" }, // 47
79 { 5, 8, 16, ABC_CONST(0x708F8F70708F8F70), "[(!(ab)c)de]" }, // 48
80 { 5, 6, 8, ABC_CONST(0x7800000078000000), "([(ab)c]de)" }, // 49
81 { 5, 6, 8, ABC_CONST(0x87FF000087FF0000), "(!([(ab)c]d)e)" }, // 50
82 { 5, 8, 14, ABC_CONST(0x87FF780087FF7800), "[([(ab)c]d)e]" }, // 51
83 { 5, 8, 13, ABC_CONST(0x8778000087780000), "([(ab)cd]e)" }, // 52
84 { 5, 10, 24, ABC_CONST(0x7887877878878778), "[(ab)cde]" }, // 53
85 { 5, 6, 7, ABC_CONST(0x6000000060000000), "([ab]cde)" }, // 54
86 { 5, 6, 7, ABC_CONST(0x9FFF00009FFF0000), "(!([ab]cd)e)" }, // 55
87 { 5, 8, 12, ABC_CONST(0x9FFF60009FFF6000), "[([ab]cd)e]" }, // 56
88 { 5, 6, 7, ABC_CONST(0x9F0000009F000000), "(!([ab]c)de)" }, // 57
89 { 5, 6, 7, ABC_CONST(0x60FF000060FF0000), "(!(!([ab]c)d)e)" }, // 58
90 { 5, 8, 12, ABC_CONST(0x60FF9F0060FF9F00), "[(!([ab]c)d)e]" }, // 59
91 { 5, 8, 11, ABC_CONST(0x9F6000009F600000), "([([ab]c)d]e)" }, // 60
92 { 5, 10, 20, ABC_CONST(0x609F9F60609F9F60), "[([ab]c)de]" }, // 61
93 { 5, 8, 10, ABC_CONST(0x9600000096000000), "([abc]de)" }, // 62
94 { 5, 8, 10, ABC_CONST(0x69FF000069FF0000), "(!([abc]d)e)" }, // 63
95 { 5, 10, 18, ABC_CONST(0x69FF960069FF9600), "[([abc]d)e]" }, // 64
96 { 5, 10, 17, ABC_CONST(0x6996000069960000), "([abcd]e)" }, // 65
97 { 5, 12, 32, ABC_CONST(0x9669699696696996), "[abcde]" }, // 66
98 { 5, 5, 6, ABC_CONST(0xCA000000CA000000), "(<abc>de)" }, // 67
99 { 5, 5, 6, ABC_CONST(0x35FF000035FF0000), "(!(<abc>d)e)" }, // 68
100 { 5, 7, 10, ABC_CONST(0x35FFCA0035FFCA00), "[(<abc>d)e]" }, // 69
101 { 5, 7, 9, ABC_CONST(0x35CA000035CA0000), "([<abc>d]e)" }, // 70
102 { 5, 9, 16, ABC_CONST(0xCA3535CACA3535CA), "[<abc>de]" }, // 71
103 { 5, 4, 7, ABC_CONST(0x0777000007770000), "(!(ab)!(cd)e)" }, // 72
104 { 5, 4, 7, ABC_CONST(0xF8880000F8880000), "(!(!(ab)!(cd))e)" }, // 73
105 { 5, 6, 12, ABC_CONST(0xF8880777F8880777), "[(!(ab)!(cd))e]" }, // 74
106 { 5, 6, 10, ABC_CONST(0x7888000078880000), "([(ab)(cd)]e)" }, // 75
107 { 5, 6, 10, ABC_CONST(0x8777000087770000), "(![(ab)(cd)]e)" }, // 76
108 { 5, 8, 18, ABC_CONST(0x8777788887777888), "[(ab)(cd)e]" }, // 77
109 { 5, 6, 8, ABC_CONST(0x0666000006660000), "([ab]!(cd)e)" }, // 78
110 { 5, 6, 8, ABC_CONST(0xF9990000F9990000), "(!([ab]!(cd))e)" }, // 79
111 { 5, 8, 14, ABC_CONST(0xF9990666F9990666), "[([ab]!(cd))e]" }, // 80
112 { 5, 8, 9, ABC_CONST(0x0660000006600000), "([ab][cd]e)" }, // 81
113 { 5, 8, 9, ABC_CONST(0xF99F0000F99F0000), "(!([ab][cd])e)" }, // 82
114 { 5, 10, 16, ABC_CONST(0xF99F0660F99F0660), "[([ab][cd])e]" }, // 83
115 { 5, 5, 7, ABC_CONST(0xCAAA0000CAAA0000), "(<ab(cd)>e)" }, // 84
116 { 5, 7, 12, ABC_CONST(0x3555CAAA3555CAAA), "[<ab(cd)>e]" }, // 85
117 { 5, 7, 9, ABC_CONST(0xACCA0000ACCA0000), "(<ab[cd]>e)" }, // 86
118 { 5, 9, 16, ABC_CONST(0x5335ACCA5335ACCA), "[<ab[cd]>e]" }, // 87
119 { 5, 5, 6, ABC_CONST(0xF0880000F0880000), "(<(ab)cd>e)" }, // 88
120 { 5, 5, 6, ABC_CONST(0x0F7700000F770000), "(!<(ab)cd>e)" }, // 89
121 { 5, 7, 10, ABC_CONST(0x0F77F0880F77F088), "[<(ab)cd>e]" }, // 90
122 { 5, 7, 7, ABC_CONST(0xF0660000F0660000), "(<[ab]cd>e)" }, // 91
123 { 5, 9, 12, ABC_CONST(0x0F99F0660F99F066), "[<[ab]cd>e]" }, // 92
124 { 5, 4, 8, ABC_CONST(0x007F7F7F007F7F7F), "(!(abc)!(de))" }, // 93
125 { 5, 6, 12, ABC_CONST(0x7F8080807F808080), "[(abc)(de)]" }, // 94
126 { 5, 4, 7, ABC_CONST(0x008F8F8F008F8F8F), "(!(!(ab)c)!(de))" }, // 95
127 { 5, 6, 12, ABC_CONST(0x8F7070708F707070), "[(!(ab)c)(de)]" }, // 96
128 { 5, 6, 10, ABC_CONST(0x0078787800787878), "([(ab)c]!(de))" }, // 97
129 { 5, 6, 9, ABC_CONST(0x009F9F9F009F9F9F), "(!([ab]c)!(de))" }, // 98
130 { 5, 8, 15, ABC_CONST(0x9F6060609F606060), "[([ab]c)(de)]" }, // 99
131 { 5, 8, 13, ABC_CONST(0x0096969600969696), "([abc]!(de))" }, // 100
132 { 5, 5, 7, ABC_CONST(0x00CACACA00CACACA), "(<abc>!(de))" }, // 101
133 { 5, 7, 12, ABC_CONST(0x35CACACA35CACACA), "[<abc>(de)]" }, // 102
134 { 5, 6, 9, ABC_CONST(0x007F7F00007F7F00), "(!(abc)[de])" }, // 103
135 { 5, 6, 8, ABC_CONST(0x008F8F00008F8F00), "(!(!(ab)c)[de])" }, // 104
136 { 5, 8, 11, ABC_CONST(0x0078780000787800), "([(ab)c][de])" }, // 105
137 { 5, 8, 10, ABC_CONST(0x009F9F00009F9F00), "(!([ab]c)[de])" }, // 106
138 { 5, 10, 14, ABC_CONST(0x0096960000969600), "([abc][de])" }, // 107
139 { 5, 7, 8, ABC_CONST(0x00CACA0000CACA00), "(<abc>[de])" }, // 108
140 { 5, 5, 8, ABC_CONST(0xCAAAAAAACAAAAAAA), "<ab(cde)>" }, // 109
141 { 5, 5, 8, ABC_CONST(0xACCCAAAAACCCAAAA), "<ab(!(cd)e)>" }, // 110
142 { 5, 7, 12, ABC_CONST(0xACCCCAAAACCCCAAA), "<ab[(cd)e]>" }, // 111
143 { 5, 7, 10, ABC_CONST(0xACCAAAAAACCAAAAA), "<ab([cd]e)>" }, // 112
144 { 5, 9, 16, ABC_CONST(0xCAACACCACAACACCA), "<ab[cde]>" }, // 113
145 { 5, 6, 8, ABC_CONST(0xCCAACACACCAACACA), "<ab<cde>>" }, // 114
146 { 5, 5, 7, ABC_CONST(0xC0AAAAAAC0AAAAAA), "<a(bc)(de)>" }, // 115
147 { 5, 7, 8, ABC_CONST(0x3CAAAAAA3CAAAAAA), "<a[bc](de)>" }, // 116
148 { 5, 5, 8, ABC_CONST(0xF0888888F0888888), "<(ab)c(de)>" }, // 117
149 { 5, 7, 10, ABC_CONST(0x88F0F08888F0F088), "<(ab)c[de]>" }, // 118
150 { 5, 7, 10, ABC_CONST(0xF0666666F0666666), "<[ab]c(de)>" }, // 119
151 { 5, 9, 12, ABC_CONST(0x66F0F06666F0F066), "<[ab]c[de]>" }, // 120
152 { 5, 5, 6, ABC_CONST(0xF0008888F0008888), "<(ab)(cd)e>" }, // 121
153 { 5, 5, 6, ABC_CONST(0xF0007777F0007777), "<!(ab)(cd)e>" }, // 122
154 { 5, 7, 7, ABC_CONST(0xF0006666F0006666), "<[ab](cd)e>" }, // 123
155 { 5, 9, 8, ABC_CONST(0x0FF066660FF06666), "<[ab][cd]e>" }, // 124
156 { 5, 5, 6, ABC_CONST(0xFF008080FF008080), "<(abc)de>" }, // 125
157 { 5, 5, 6, ABC_CONST(0xFF007070FF007070), "<(!(ab)c)de>" }, // 126
158 { 5, 7, 8, ABC_CONST(0xFF007878FF007878), "<[(ab)c]de>" }, // 127
159 { 5, 7, 7, ABC_CONST(0xFF006060FF006060), "<([ab]c)de>" }, // 128
160 { 5, 9, 10, ABC_CONST(0xFF009696FF009696), "<[abc]de>" }, // 129
161 { 5, 6, 6, ABC_CONST(0xFF00CACAFF00CACA), "<<abc>de>" }, // 130
162 { 6, 5, 7, ABC_CONST(0x8000000000000000), "(abcdef)" }, // 131
163 { 6, 5, 7, ABC_CONST(0x7FFFFFFF00000000), "(!(abcde)f)" }, // 132
164 { 6, 7, 12, ABC_CONST(0x7FFFFFFF80000000), "[(abcde)f]" }, // 133
165 { 6, 5, 7, ABC_CONST(0x7FFF000000000000), "(!(abcd)ef)" }, // 134
166 { 6, 5, 7, ABC_CONST(0x8000FFFF00000000), "(!(!(abcd)e)f)" }, // 135
167 { 6, 7, 12, ABC_CONST(0x8000FFFF7FFF0000), "[(!(abcd)e)f]" }, // 136
168 { 6, 7, 11, ABC_CONST(0x7FFF800000000000), "([(abcd)e]f)" }, // 137
169 { 6, 9, 20, ABC_CONST(0x80007FFF7FFF8000), "[(abcd)ef]" }, // 138
170 { 6, 5, 7, ABC_CONST(0x7F00000000000000), "(!(abc)def)" }, // 139
171 { 6, 5, 7, ABC_CONST(0x80FFFFFF00000000), "(!(!(abc)de)f)" }, // 140
172 { 6, 7, 12, ABC_CONST(0x80FFFFFF7F000000), "[(!(abc)de)f]" }, // 141
173 { 6, 5, 7, ABC_CONST(0x80FF000000000000), "(!(!(abc)d)ef)" }, // 142
174 { 6, 5, 7, ABC_CONST(0x7F00FFFF00000000), "(!(!(!(abc)d)e)f)" }, // 143
175 { 6, 7, 12, ABC_CONST(0x7F00FFFF80FF0000), "[(!(!(abc)d)e)f]" }, // 144
176 { 6, 7, 11, ABC_CONST(0x80FF7F0000000000), "([(!(abc)d)e]f)" }, // 145
177 { 6, 9, 20, ABC_CONST(0x7F0080FF80FF7F00), "[(!(abc)d)ef]" }, // 146
178 { 6, 7, 10, ABC_CONST(0x7F80000000000000), "([(abc)d]ef)" }, // 147
179 { 6, 7, 10, ABC_CONST(0x807FFFFF00000000), "(!([(abc)d]e)f)" }, // 148
180 { 6, 9, 18, ABC_CONST(0x807FFFFF7F800000), "[([(abc)d]e)f]" }, // 149
181 { 6, 9, 17, ABC_CONST(0x807F7F8000000000), "([(abc)de]f)" }, // 150
182 { 6, 11, 32, ABC_CONST(0x7F80807F807F7F80), "[(abc)def]" }, // 151
183 { 6, 5, 7, ABC_CONST(0x7000000000000000), "(!(ab)cdef)" }, // 152
184 { 6, 5, 7, ABC_CONST(0x8FFFFFFF00000000), "(!(!(ab)cde)f)" }, // 153
185 { 6, 7, 12, ABC_CONST(0x8FFFFFFF70000000), "[(!(ab)cde)f]" }, // 154
186 { 6, 5, 7, ABC_CONST(0x8FFF000000000000), "(!(!(ab)cd)ef)" }, // 155
187 { 6, 5, 7, ABC_CONST(0x7000FFFF00000000), "(!(!(!(ab)cd)e)f)" }, // 156
188 { 6, 7, 12, ABC_CONST(0x7000FFFF8FFF0000), "[(!(!(ab)cd)e)f]" }, // 157
189 { 6, 7, 11, ABC_CONST(0x8FFF700000000000), "([(!(ab)cd)e]f)" }, // 158
190 { 6, 9, 20, ABC_CONST(0x70008FFF8FFF7000), "[(!(ab)cd)ef]" }, // 159
191 { 6, 5, 7, ABC_CONST(0x8F00000000000000), "(!(!(ab)c)def)" }, // 160
192 { 6, 5, 7, ABC_CONST(0x70FFFFFF00000000), "(!(!(!(ab)c)de)f)" }, // 161
193 { 6, 7, 12, ABC_CONST(0x70FFFFFF8F000000), "[(!(!(ab)c)de)f]" }, // 162
194 { 6, 5, 7, ABC_CONST(0x70FF000000000000), "(!(!(!(ab)c)d)ef)" }, // 163
195 { 6, 5, 7, ABC_CONST(0x8F00FFFF00000000), "(!(!(!(!(ab)c)d)e)f)" }, // 164
196 { 6, 7, 12, ABC_CONST(0x8F00FFFF70FF0000), "[(!(!(!(ab)c)d)e)f]" }, // 165
197 { 6, 7, 11, ABC_CONST(0x70FF8F0000000000), "([(!(!(ab)c)d)e]f)" }, // 166
198 { 6, 9, 20, ABC_CONST(0x8F0070FF70FF8F00), "[(!(!(ab)c)d)ef]" }, // 167
199 { 6, 7, 10, ABC_CONST(0x8F70000000000000), "([(!(ab)c)d]ef)" }, // 168
200 { 6, 7, 10, ABC_CONST(0x708FFFFF00000000), "(!([(!(ab)c)d]e)f)" }, // 169
201 { 6, 9, 18, ABC_CONST(0x708FFFFF8F700000), "[([(!(ab)c)d]e)f]" }, // 170
202 { 6, 9, 17, ABC_CONST(0x708F8F7000000000), "([(!(ab)c)de]f)" }, // 171
203 { 6, 11, 32, ABC_CONST(0x8F70708F708F8F70), "[(!(ab)c)def]" }, // 172
204 { 6, 7, 9, ABC_CONST(0x7800000000000000), "([(ab)c]def)" }, // 173
205 { 6, 7, 9, ABC_CONST(0x87FFFFFF00000000), "(!([(ab)c]de)f)" }, // 174
206 { 6, 9, 16, ABC_CONST(0x87FFFFFF78000000), "[([(ab)c]de)f]" }, // 175
207 { 6, 7, 9, ABC_CONST(0x87FF000000000000), "(!([(ab)c]d)ef)" }, // 176
208 { 6, 7, 9, ABC_CONST(0x7800FFFF00000000), "(!(!([(ab)c]d)e)f)" }, // 177
209 { 6, 9, 16, ABC_CONST(0x7800FFFF87FF0000), "[(!([(ab)c]d)e)f]" }, // 178
210 { 6, 9, 15, ABC_CONST(0x87FF780000000000), "([([(ab)c]d)e]f)" }, // 179
211 { 6, 11, 28, ABC_CONST(0x780087FF87FF7800), "[([(ab)c]d)ef]" }, // 180
212 { 6, 9, 14, ABC_CONST(0x8778000000000000), "([(ab)cd]ef)" }, // 181
213 { 6, 9, 14, ABC_CONST(0x7887FFFF00000000), "(!([(ab)cd]e)f)" }, // 182
214 { 6, 11, 26, ABC_CONST(0x7887FFFF87780000), "[([(ab)cd]e)f]" }, // 183
215 { 6, 11, 25, ABC_CONST(0x7887877800000000), "([(ab)cde]f)" }, // 184
216 { 6, 13, 48, ABC_CONST(0x8778788778878778), "[(ab)cdef]" }, // 185
217 { 6, 7, 8, ABC_CONST(0x6000000000000000), "([ab]cdef)" }, // 186
218 { 6, 7, 8, ABC_CONST(0x9FFFFFFF00000000), "(!([ab]cde)f)" }, // 187
219 { 6, 9, 14, ABC_CONST(0x9FFFFFFF60000000), "[([ab]cde)f]" }, // 188
220 { 6, 7, 8, ABC_CONST(0x9FFF000000000000), "(!([ab]cd)ef)" }, // 189
221 { 6, 7, 8, ABC_CONST(0x6000FFFF00000000), "(!(!([ab]cd)e)f)" }, // 190
222 { 6, 9, 14, ABC_CONST(0x6000FFFF9FFF0000), "[(!([ab]cd)e)f]" }, // 191
223 { 6, 9, 13, ABC_CONST(0x9FFF600000000000), "([([ab]cd)e]f)" }, // 192
224 { 6, 11, 24, ABC_CONST(0x60009FFF9FFF6000), "[([ab]cd)ef]" }, // 193
225 { 6, 7, 8, ABC_CONST(0x9F00000000000000), "(!([ab]c)def)" }, // 194
226 { 6, 7, 8, ABC_CONST(0x60FFFFFF00000000), "(!(!([ab]c)de)f)" }, // 195
227 { 6, 9, 14, ABC_CONST(0x60FFFFFF9F000000), "[(!([ab]c)de)f]" }, // 196
228 { 6, 7, 8, ABC_CONST(0x60FF000000000000), "(!(!([ab]c)d)ef)" }, // 197
229 { 6, 7, 8, ABC_CONST(0x9F00FFFF00000000), "(!(!(!([ab]c)d)e)f)" }, // 198
230 { 6, 9, 14, ABC_CONST(0x9F00FFFF60FF0000), "[(!(!([ab]c)d)e)f]" }, // 199
231 { 6, 9, 13, ABC_CONST(0x60FF9F0000000000), "([(!([ab]c)d)e]f)" }, // 200
232 { 6, 11, 24, ABC_CONST(0x9F0060FF60FF9F00), "[(!([ab]c)d)ef]" }, // 201
233 { 6, 9, 12, ABC_CONST(0x9F60000000000000), "([([ab]c)d]ef)" }, // 202
234 { 6, 9, 12, ABC_CONST(0x609FFFFF00000000), "(!([([ab]c)d]e)f)" }, // 203
235 { 6, 11, 22, ABC_CONST(0x609FFFFF9F600000), "[([([ab]c)d]e)f]" }, // 204
236 { 6, 11, 21, ABC_CONST(0x609F9F6000000000), "([([ab]c)de]f)" }, // 205
237 { 6, 13, 40, ABC_CONST(0x9F60609F609F9F60), "[([ab]c)def]" }, // 206
238 { 6, 9, 11, ABC_CONST(0x9600000000000000), "([abc]def)" }, // 207
239 { 6, 9, 11, ABC_CONST(0x69FFFFFF00000000), "(!([abc]de)f)" }, // 208
240 { 6, 11, 20, ABC_CONST(0x69FFFFFF96000000), "[([abc]de)f]" }, // 209
241 { 6, 9, 11, ABC_CONST(0x69FF000000000000), "(!([abc]d)ef)" }, // 210
242 { 6, 9, 11, ABC_CONST(0x9600FFFF00000000), "(!(!([abc]d)e)f)" }, // 211
243 { 6, 11, 20, ABC_CONST(0x9600FFFF69FF0000), "[(!([abc]d)e)f]" }, // 212
244 { 6, 11, 19, ABC_CONST(0x69FF960000000000), "([([abc]d)e]f)" }, // 213
245 { 6, 13, 36, ABC_CONST(0x960069FF69FF9600), "[([abc]d)ef]" }, // 214
246 { 6, 11, 18, ABC_CONST(0x6996000000000000), "([abcd]ef)" }, // 215
247 { 6, 11, 18, ABC_CONST(0x9669FFFF00000000), "(!([abcd]e)f)" }, // 216
248 { 6, 13, 34, ABC_CONST(0x9669FFFF69960000), "[([abcd]e)f]" }, // 217
249 { 6, 13, 33, ABC_CONST(0x9669699600000000), "([abcde]f)" }, // 218
250 { 6, 15, 64, ABC_CONST(0x6996966996696996), "[abcdef]" }, // 219
251 { 6, 6, 7, ABC_CONST(0xCA00000000000000), "(<abc>def)" }, // 220
252 { 6, 6, 7, ABC_CONST(0x35FFFFFF00000000), "(!(<abc>de)f)" }, // 221
253 { 6, 8, 12, ABC_CONST(0x35FFFFFFCA000000), "[(<abc>de)f]" }, // 222
254 { 6, 6, 7, ABC_CONST(0x35FF000000000000), "(!(<abc>d)ef)" }, // 223
255 { 6, 6, 7, ABC_CONST(0xCA00FFFF00000000), "(!(!(<abc>d)e)f)" }, // 224
256 { 6, 8, 12, ABC_CONST(0xCA00FFFF35FF0000), "[(!(<abc>d)e)f]" }, // 225
257 { 6, 8, 11, ABC_CONST(0x35FFCA0000000000), "([(<abc>d)e]f)" }, // 226
258 { 6, 10, 20, ABC_CONST(0xCA0035FF35FFCA00), "[(<abc>d)ef]" }, // 227
259 { 6, 8, 10, ABC_CONST(0x35CA000000000000), "([<abc>d]ef)" }, // 228
260 { 6, 8, 10, ABC_CONST(0xCA35FFFF00000000), "(!([<abc>d]e)f)" }, // 229
261 { 6, 10, 18, ABC_CONST(0xCA35FFFF35CA0000), "[([<abc>d]e)f]" }, // 230
262 { 6, 10, 17, ABC_CONST(0xCA3535CA00000000), "([<abc>de]f)" }, // 231
263 { 6, 12, 32, ABC_CONST(0x35CACA35CA3535CA), "[<abc>def]" }, // 232
264 { 6, 5, 8, ABC_CONST(0x0777000000000000), "(!(ab)!(cd)ef)" }, // 233
265 { 6, 5, 8, ABC_CONST(0xF888FFFF00000000), "(!(!(ab)!(cd)e)f)" }, // 234
266 { 6, 7, 14, ABC_CONST(0xF888FFFF07770000), "[(!(ab)!(cd)e)f]" }, // 235
267 { 6, 5, 8, ABC_CONST(0xF888000000000000), "(!(!(ab)!(cd))ef)" }, // 236
268 { 6, 5, 8, ABC_CONST(0x0777FFFF00000000), "(!(!(!(ab)!(cd))e)f)" }, // 237
269 { 6, 7, 14, ABC_CONST(0x0777FFFFF8880000), "[(!(!(ab)!(cd))e)f]" }, // 238
270 { 6, 7, 13, ABC_CONST(0xF888077700000000), "([(!(ab)!(cd))e]f)" }, // 239
271 { 6, 9, 24, ABC_CONST(0x0777F888F8880777), "[(!(ab)!(cd))ef]" }, // 240
272 { 6, 7, 11, ABC_CONST(0x7888000000000000), "([(ab)(cd)]ef)" }, // 241
273 { 6, 7, 11, ABC_CONST(0x8777FFFF00000000), "(!([(ab)(cd)]e)f)" }, // 242
274 { 6, 9, 20, ABC_CONST(0x8777FFFF78880000), "[([(ab)(cd)]e)f]" }, // 243
275 { 6, 7, 11, ABC_CONST(0x8777000000000000), "(![(ab)(cd)]ef)" }, // 244
276 { 6, 7, 11, ABC_CONST(0x7888FFFF00000000), "(!(![(ab)(cd)]e)f)" }, // 245
277 { 6, 9, 20, ABC_CONST(0x7888FFFF87770000), "[(![(ab)(cd)]e)f]" }, // 246
278 { 6, 9, 19, ABC_CONST(0x8777788800000000), "([(ab)(cd)e]f)" }, // 247
279 { 6, 11, 36, ABC_CONST(0x7888877787777888), "[(ab)(cd)ef]" }, // 248
280 { 6, 7, 9, ABC_CONST(0x0666000000000000), "([ab]!(cd)ef)" }, // 249
281 { 6, 7, 9, ABC_CONST(0xF999FFFF00000000), "(!([ab]!(cd)e)f)" }, // 250
282 { 6, 9, 16, ABC_CONST(0xF999FFFF06660000), "[([ab]!(cd)e)f]" }, // 251
283 { 6, 7, 9, ABC_CONST(0xF999000000000000), "(!([ab]!(cd))ef)" }, // 252
284 { 6, 7, 9, ABC_CONST(0x0666FFFF00000000), "(!(!([ab]!(cd))e)f)" }, // 253
285 { 6, 9, 16, ABC_CONST(0x0666FFFFF9990000), "[(!([ab]!(cd))e)f]" }, // 254
286 { 6, 9, 15, ABC_CONST(0xF999066600000000), "([([ab]!(cd))e]f)" }, // 255
287 { 6, 11, 28, ABC_CONST(0x0666F999F9990666), "[([ab]!(cd))ef]" }, // 256
288 { 6, 9, 10, ABC_CONST(0x0660000000000000), "([ab][cd]ef)" }, // 257
289 { 6, 9, 10, ABC_CONST(0xF99FFFFF00000000), "(!([ab][cd]e)f)" }, // 258
290 { 6, 11, 18, ABC_CONST(0xF99FFFFF06600000), "[([ab][cd]e)f]" }, // 259
291 { 6, 9, 10, ABC_CONST(0xF99F000000000000), "(!([ab][cd])ef)" }, // 260
292 { 6, 9, 10, ABC_CONST(0x0660FFFF00000000), "(!(!([ab][cd])e)f)" }, // 261
293 { 6, 11, 18, ABC_CONST(0x0660FFFFF99F0000), "[(!([ab][cd])e)f]" }, // 262
294 { 6, 11, 17, ABC_CONST(0xF99F066000000000), "([([ab][cd])e]f)" }, // 263
295 { 6, 13, 32, ABC_CONST(0x0660F99FF99F0660), "[([ab][cd])ef]" }, // 264
296 { 6, 6, 8, ABC_CONST(0xCAAA000000000000), "(<ab(cd)>ef)" }, // 265
297 { 6, 6, 8, ABC_CONST(0x3555FFFF00000000), "(!(<ab(cd)>e)f)" }, // 266
298 { 6, 8, 14, ABC_CONST(0x3555FFFFCAAA0000), "[(<ab(cd)>e)f]" }, // 267
299 { 6, 8, 13, ABC_CONST(0x3555CAAA00000000), "([<ab(cd)>e]f)" }, // 268
300 { 6, 10, 24, ABC_CONST(0xCAAA35553555CAAA), "[<ab(cd)>ef]" }, // 269
301 { 6, 8, 10, ABC_CONST(0xACCA000000000000), "(<ab[cd]>ef)" }, // 270
302 { 6, 8, 10, ABC_CONST(0x5335FFFF00000000), "(!(<ab[cd]>e)f)" }, // 271
303 { 6, 10, 18, ABC_CONST(0x5335FFFFACCA0000), "[(<ab[cd]>e)f]" }, // 272
304 { 6, 10, 17, ABC_CONST(0x5335ACCA00000000), "([<ab[cd]>e]f)" }, // 273
305 { 6, 12, 32, ABC_CONST(0xACCA53355335ACCA), "[<ab[cd]>ef]" }, // 274
306 { 6, 6, 7, ABC_CONST(0xF088000000000000), "(<(ab)cd>ef)" }, // 275
307 { 6, 6, 7, ABC_CONST(0x0F77FFFF00000000), "(!(<(ab)cd>e)f)" }, // 276
308 { 6, 8, 12, ABC_CONST(0x0F77FFFFF0880000), "[(<(ab)cd>e)f]" }, // 277
309 { 6, 6, 7, ABC_CONST(0x0F77000000000000), "(!<(ab)cd>ef)" }, // 278
310 { 6, 6, 7, ABC_CONST(0xF088FFFF00000000), "(!(!<(ab)cd>e)f)" }, // 279
311 { 6, 8, 12, ABC_CONST(0xF088FFFF0F770000), "[(!<(ab)cd>e)f]" }, // 280
312 { 6, 8, 11, ABC_CONST(0x0F77F08800000000), "([<(ab)cd>e]f)" }, // 281
313 { 6, 10, 20, ABC_CONST(0xF0880F770F77F088), "[<(ab)cd>ef]" }, // 282
314 { 6, 8, 8, ABC_CONST(0xF066000000000000), "(<[ab]cd>ef)" }, // 283
315 { 6, 8, 8, ABC_CONST(0x0F99FFFF00000000), "(!(<[ab]cd>e)f)" }, // 284
316 { 6, 10, 14, ABC_CONST(0x0F99FFFFF0660000), "[(<[ab]cd>e)f]" }, // 285
317 { 6, 10, 13, ABC_CONST(0x0F99F06600000000), "([<[ab]cd>e]f)" }, // 286
318 { 6, 12, 24, ABC_CONST(0xF0660F990F99F066), "[<[ab]cd>ef]" }, // 287
319 { 6, 5, 9, ABC_CONST(0x007F7F7F00000000), "(!(abc)!(de)f)" }, // 288
320 { 6, 5, 9, ABC_CONST(0xFF80808000000000), "(!(!(abc)!(de))f)" }, // 289
321 { 6, 7, 16, ABC_CONST(0xFF808080007F7F7F), "[(!(abc)!(de))f]" }, // 290
322 { 6, 7, 13, ABC_CONST(0x7F80808000000000), "([(abc)(de)]f)" }, // 291
323 { 6, 7, 13, ABC_CONST(0x807F7F7F00000000), "(![(abc)(de)]f)" }, // 292
324 { 6, 9, 24, ABC_CONST(0x807F7F7F7F808080), "[(abc)(de)f]" }, // 293
325 { 6, 5, 8, ABC_CONST(0x008F8F8F00000000), "(!(!(ab)c)!(de)f)" }, // 294
326 { 6, 5, 8, ABC_CONST(0xFF70707000000000), "(!(!(!(ab)c)!(de))f)" }, // 295
327 { 6, 7, 14, ABC_CONST(0xFF707070008F8F8F), "[(!(!(ab)c)!(de))f]" }, // 296
328 { 6, 7, 13, ABC_CONST(0x8F70707000000000), "([(!(ab)c)(de)]f)" }, // 297
329 { 6, 7, 13, ABC_CONST(0x708F8F8F00000000), "(![(!(ab)c)(de)]f)" }, // 298
330 { 6, 9, 24, ABC_CONST(0x708F8F8F8F707070), "[(!(ab)c)(de)f]" }, // 299
331 { 6, 7, 11, ABC_CONST(0x0078787800000000), "([(ab)c]!(de)f)" }, // 300
332 { 6, 7, 11, ABC_CONST(0xFF87878700000000), "(!([(ab)c]!(de))f)" }, // 301
333 { 6, 9, 20, ABC_CONST(0xFF87878700787878), "[([(ab)c]!(de))f]" }, // 302
334 { 6, 7, 10, ABC_CONST(0x009F9F9F00000000), "(!([ab]c)!(de)f)" }, // 303
335 { 6, 7, 10, ABC_CONST(0xFF60606000000000), "(!(!([ab]c)!(de))f)" }, // 304
336 { 6, 9, 18, ABC_CONST(0xFF606060009F9F9F), "[(!([ab]c)!(de))f]" }, // 305
337 { 6, 9, 16, ABC_CONST(0x9F60606000000000), "([([ab]c)(de)]f)" }, // 306
338 { 6, 9, 16, ABC_CONST(0x609F9F9F00000000), "(![([ab]c)(de)]f)" }, // 307
339 { 6, 11, 30, ABC_CONST(0x609F9F9F9F606060), "[([ab]c)(de)f]" }, // 308
340 { 6, 9, 14, ABC_CONST(0x0096969600000000), "([abc]!(de)f)" }, // 309
341 { 6, 9, 14, ABC_CONST(0xFF69696900000000), "(!([abc]!(de))f)" }, // 310
342 { 6, 11, 26, ABC_CONST(0xFF69696900969696), "[([abc]!(de))f]" }, // 311
343 { 6, 6, 8, ABC_CONST(0x00CACACA00000000), "(<abc>!(de)f)" }, // 312
344 { 6, 6, 8, ABC_CONST(0xFF35353500000000), "(!(<abc>!(de))f)" }, // 313
345 { 6, 8, 14, ABC_CONST(0xFF35353500CACACA), "[(<abc>!(de))f]" }, // 314
346 { 6, 8, 13, ABC_CONST(0x35CACACA00000000), "([<abc>(de)]f)" }, // 315
347 { 6, 10, 24, ABC_CONST(0xCA35353535CACACA), "[<abc>(de)f]" }, // 316
348 { 6, 7, 10, ABC_CONST(0x007F7F0000000000), "(!(abc)[de]f)" }, // 317
349 { 6, 7, 10, ABC_CONST(0xFF8080FF00000000), "(!(!(abc)[de])f)" }, // 318
350 { 6, 9, 18, ABC_CONST(0xFF8080FF007F7F00), "[(!(abc)[de])f]" }, // 319
351 { 6, 7, 9, ABC_CONST(0x008F8F0000000000), "(!(!(ab)c)[de]f)" }, // 320
352 { 6, 7, 9, ABC_CONST(0xFF7070FF00000000), "(!(!(!(ab)c)[de])f)" }, // 321
353 { 6, 9, 16, ABC_CONST(0xFF7070FF008F8F00), "[(!(!(ab)c)[de])f]" }, // 322
354 { 6, 9, 12, ABC_CONST(0x0078780000000000), "([(ab)c][de]f)" }, // 323
355 { 6, 9, 12, ABC_CONST(0xFF8787FF00000000), "(!([(ab)c][de])f)" }, // 324
356 { 6, 11, 22, ABC_CONST(0xFF8787FF00787800), "[([(ab)c][de])f]" }, // 325
357 { 6, 9, 11, ABC_CONST(0x009F9F0000000000), "(!([ab]c)[de]f)" }, // 326
358 { 6, 9, 11, ABC_CONST(0xFF6060FF00000000), "(!(!([ab]c)[de])f)" }, // 327
359 { 6, 11, 20, ABC_CONST(0xFF6060FF009F9F00), "[(!([ab]c)[de])f]" }, // 328
360 { 6, 11, 15, ABC_CONST(0x0096960000000000), "([abc][de]f)" }, // 329
361 { 6, 11, 15, ABC_CONST(0xFF6969FF00000000), "(!([abc][de])f)" }, // 330
362 { 6, 13, 28, ABC_CONST(0xFF6969FF00969600), "[([abc][de])f]" }, // 331
363 { 6, 8, 9, ABC_CONST(0x00CACA0000000000), "(<abc>[de]f)" }, // 332
364 { 6, 8, 9, ABC_CONST(0xFF3535FF00000000), "(!(<abc>[de])f)" }, // 333
365 { 6, 10, 16, ABC_CONST(0xFF3535FF00CACA00), "[(<abc>[de])f]" }, // 334
366 { 6, 6, 9, ABC_CONST(0xCAAAAAAA00000000), "(<ab(cde)>f)" }, // 335
367 { 6, 8, 16, ABC_CONST(0x35555555CAAAAAAA), "[<ab(cde)>f]" }, // 336
368 { 6, 6, 9, ABC_CONST(0xACCCAAAA00000000), "(<ab(!(cd)e)>f)" }, // 337
369 { 6, 8, 16, ABC_CONST(0x53335555ACCCAAAA), "[<ab(!(cd)e)>f]" }, // 338
370 { 6, 8, 13, ABC_CONST(0xACCCCAAA00000000), "(<ab[(cd)e]>f)" }, // 339
371 { 6, 10, 24, ABC_CONST(0x53333555ACCCCAAA), "[<ab[(cd)e]>f]" }, // 340
372 { 6, 8, 11, ABC_CONST(0xACCAAAAA00000000), "(<ab([cd]e)>f)" }, // 341
373 { 6, 10, 20, ABC_CONST(0x53355555ACCAAAAA), "[<ab([cd]e)>f]" }, // 342
374 { 6, 10, 17, ABC_CONST(0xCAACACCA00000000), "(<ab[cde]>f)" }, // 343
375 { 6, 12, 32, ABC_CONST(0x35535335CAACACCA), "[<ab[cde]>f]" }, // 344
376 { 6, 7, 9, ABC_CONST(0xCCAACACA00000000), "(<ab<cde>>f)" }, // 345
377 { 6, 9, 16, ABC_CONST(0x33553535CCAACACA), "[<ab<cde>>f]" }, // 346
378 { 6, 6, 8, ABC_CONST(0xC0AAAAAA00000000), "(<a(bc)(de)>f)" }, // 347
379 { 6, 6, 8, ABC_CONST(0x3F55555500000000), "(!<a(bc)(de)>f)" }, // 348
380 { 6, 8, 14, ABC_CONST(0x3F555555C0AAAAAA), "[<a(bc)(de)>f]" }, // 349
381 { 6, 8, 9, ABC_CONST(0x3CAAAAAA00000000), "(<a[bc](de)>f)" }, // 350
382 { 6, 10, 16, ABC_CONST(0xC35555553CAAAAAA), "[<a[bc](de)>f]" }, // 351
383 { 6, 6, 9, ABC_CONST(0xF088888800000000), "(<(ab)c(de)>f)" }, // 352
384 { 6, 6, 9, ABC_CONST(0x0F77777700000000), "(!<(ab)c(de)>f)" }, // 353
385 { 6, 8, 16, ABC_CONST(0x0F777777F0888888), "[<(ab)c(de)>f]" }, // 354
386 { 6, 8, 11, ABC_CONST(0x88F0F08800000000), "(<(ab)c[de]>f)" }, // 355
387 { 6, 8, 11, ABC_CONST(0x770F0F7700000000), "(!<(ab)c[de]>f)" }, // 356
388 { 6, 10, 20, ABC_CONST(0x770F0F7788F0F088), "[<(ab)c[de]>f]" }, // 357
389 { 6, 8, 11, ABC_CONST(0xF066666600000000), "(<[ab]c(de)>f)" }, // 358
390 { 6, 10, 20, ABC_CONST(0x0F999999F0666666), "[<[ab]c(de)>f]" }, // 359
391 { 6, 10, 13, ABC_CONST(0x66F0F06600000000), "(<[ab]c[de]>f)" }, // 360
392 { 6, 12, 24, ABC_CONST(0x990F0F9966F0F066), "[<[ab]c[de]>f]" }, // 361
393 { 6, 6, 7, ABC_CONST(0xF000888800000000), "(<(ab)(cd)e>f)" }, // 362
394 { 6, 6, 7, ABC_CONST(0x0FFF777700000000), "(!<(ab)(cd)e>f)" }, // 363
395 { 6, 8, 12, ABC_CONST(0x0FFF7777F0008888), "[<(ab)(cd)e>f]" }, // 364
396 { 6, 6, 7, ABC_CONST(0xF000777700000000), "(<!(ab)(cd)e>f)" }, // 365
397 { 6, 8, 12, ABC_CONST(0x0FFF8888F0007777), "[<!(ab)(cd)e>f]" }, // 366
398 { 6, 8, 8, ABC_CONST(0xF000666600000000), "(<[ab](cd)e>f)" }, // 367
399 { 6, 8, 8, ABC_CONST(0x0FFF999900000000), "(!<[ab](cd)e>f)" }, // 368
400 { 6, 10, 14, ABC_CONST(0x0FFF9999F0006666), "[<[ab](cd)e>f]" }, // 369
401 { 6, 10, 9, ABC_CONST(0x0FF0666600000000), "(<[ab][cd]e>f)" }, // 370
402 { 6, 12, 16, ABC_CONST(0xF00F99990FF06666), "[<[ab][cd]e>f]" }, // 371
403 { 6, 6, 7, ABC_CONST(0xFF00808000000000), "(<(abc)de>f)" }, // 372
404 { 6, 6, 7, ABC_CONST(0x00FF7F7F00000000), "(!<(abc)de>f)" }, // 373
405 { 6, 8, 12, ABC_CONST(0x00FF7F7FFF008080), "[<(abc)de>f]" }, // 374
406 { 6, 6, 7, ABC_CONST(0xFF00707000000000), "(<(!(ab)c)de>f)" }, // 375
407 { 6, 6, 7, ABC_CONST(0x00FF8F8F00000000), "(!<(!(ab)c)de>f)" }, // 376
408 { 6, 8, 12, ABC_CONST(0x00FF8F8FFF007070), "[<(!(ab)c)de>f]" }, // 377
409 { 6, 8, 9, ABC_CONST(0xFF00787800000000), "(<[(ab)c]de>f)" }, // 378
410 { 6, 10, 16, ABC_CONST(0x00FF8787FF007878), "[<[(ab)c]de>f]" }, // 379
411 { 6, 8, 8, ABC_CONST(0xFF00606000000000), "(<([ab]c)de>f)" }, // 380
412 { 6, 8, 8, ABC_CONST(0x00FF9F9F00000000), "(!<([ab]c)de>f)" }, // 381
413 { 6, 10, 14, ABC_CONST(0x00FF9F9FFF006060), "[<([ab]c)de>f]" }, // 382
414 { 6, 10, 11, ABC_CONST(0xFF00969600000000), "(<[abc]de>f)" }, // 383
415 { 6, 12, 20, ABC_CONST(0x00FF6969FF009696), "[<[abc]de>f]" }, // 384
416 { 6, 7, 7, ABC_CONST(0xFF00CACA00000000), "(<<abc>de>f)" }, // 385
417 { 6, 9, 12, ABC_CONST(0x00FF3535FF00CACA), "[<<abc>de>f]" }, // 386
418 { 6, 5, 10, ABC_CONST(0x00007FFF7FFF7FFF), "(!(abcd)!(ef))" }, // 387
419 { 6, 7, 15, ABC_CONST(0x7FFF800080008000), "[(abcd)(ef)]" }, // 388
420 { 6, 5, 8, ABC_CONST(0x000080FF80FF80FF), "(!(!(abc)d)!(ef))" }, // 389
421 { 6, 7, 15, ABC_CONST(0x80FF7F007F007F00), "[(!(abc)d)(ef)]" }, // 390
422 { 6, 7, 13, ABC_CONST(0x00007F807F807F80), "([(abc)d]!(ef))" }, // 391
423 { 6, 5, 9, ABC_CONST(0x00008FFF8FFF8FFF), "(!(!(ab)cd)!(ef))" }, // 392
424 { 6, 7, 15, ABC_CONST(0x8FFF700070007000), "[(!(ab)cd)(ef)]" }, // 393
425 { 6, 5, 9, ABC_CONST(0x000070FF70FF70FF), "(!(!(!(ab)c)d)!(ef))" }, // 394
426 { 6, 7, 15, ABC_CONST(0x70FF8F008F008F00), "[(!(!(ab)c)d)(ef)]" }, // 395
427 { 6, 7, 13, ABC_CONST(0x00008F708F708F70), "([(!(ab)c)d]!(ef))" }, // 396
428 { 6, 7, 12, ABC_CONST(0x000087FF87FF87FF), "(!([(ab)c]d)!(ef))" }, // 397
429 { 6, 9, 21, ABC_CONST(0x87FF780078007800), "[([(ab)c]d)(ef)]" }, // 398
430 { 6, 9, 19, ABC_CONST(0x0000877887788778), "([(ab)cd]!(ef))" }, // 399
431 { 6, 7, 11, ABC_CONST(0x00009FFF9FFF9FFF), "(!([ab]cd)!(ef))" }, // 400
432 { 6, 9, 18, ABC_CONST(0x9FFF600060006000), "[([ab]cd)(ef)]" }, // 401
433 { 6, 7, 10, ABC_CONST(0x000060FF60FF60FF), "(!(!([ab]c)d)!(ef))" }, // 402
434 { 6, 9, 18, ABC_CONST(0x60FF9F009F009F00), "[(!([ab]c)d)(ef)]" }, // 403
435 { 6, 9, 16, ABC_CONST(0x00009F609F609F60), "([([ab]c)d]!(ef))" }, // 404
436 { 6, 9, 15, ABC_CONST(0x000069FF69FF69FF), "(!([abc]d)!(ef))" }, // 405
437 { 6, 11, 27, ABC_CONST(0x69FF960096009600), "[([abc]d)(ef)]" }, // 406
438 { 6, 11, 25, ABC_CONST(0x0000699669966996), "([abcd]!(ef))" }, // 407
439 { 6, 6, 9, ABC_CONST(0x000035FF35FF35FF), "(!(<abc>d)!(ef))" }, // 408
440 { 6, 8, 15, ABC_CONST(0x35FFCA00CA00CA00), "[(<abc>d)(ef)]" }, // 409
441 { 6, 8, 13, ABC_CONST(0x000035CA35CA35CA), "([<abc>d]!(ef))" }, // 410
442 { 6, 5, 11, ABC_CONST(0x0000077707770777), "(!(ab)!(cd)!(ef))" }, // 411
443 { 6, 5, 9, ABC_CONST(0x0000F888F888F888), "(!(!(ab)!(cd))!(ef))" }, // 412
444 { 6, 7, 18, ABC_CONST(0xF888077707770777), "[(!(ab)!(cd))(ef)]" }, // 413
445 { 6, 7, 14, ABC_CONST(0x0000788878887888), "([(ab)(cd)]!(ef))" }, // 414
446 { 6, 7, 15, ABC_CONST(0x0000877787778777), "(![(ab)(cd)]!(ef))" }, // 415
447 { 6, 9, 27, ABC_CONST(0x8777788878887888), "[(ab)(cd)(ef)]" }, // 416
448 { 6, 7, 12, ABC_CONST(0x0000066606660666), "([ab]!(cd)!(ef))" }, // 417
449 { 6, 7, 11, ABC_CONST(0x0000F999F999F999), "(!([ab]!(cd))!(ef))" }, // 418
450 { 6, 9, 21, ABC_CONST(0xF999066606660666), "[([ab]!(cd))(ef)]" }, // 419
451 { 6, 9, 13, ABC_CONST(0x0000066006600660), "([ab][cd]!(ef))" }, // 420
452 { 6, 9, 13, ABC_CONST(0x0000F99FF99FF99F), "(!([ab][cd])!(ef))" }, // 421
453 { 6, 11, 24, ABC_CONST(0xF99F066006600660), "[([ab][cd])(ef)]" }, // 422
454 { 6, 6, 10, ABC_CONST(0x0000CAAACAAACAAA), "(<ab(cd)>!(ef))" }, // 423
455 { 6, 8, 18, ABC_CONST(0x3555CAAACAAACAAA), "[<ab(cd)>(ef)]" }, // 424
456 { 6, 8, 13, ABC_CONST(0x0000ACCAACCAACCA), "(<ab[cd]>!(ef))" }, // 425
457 { 6, 10, 24, ABC_CONST(0x5335ACCAACCAACCA), "[<ab[cd]>(ef)]" }, // 426
458 { 6, 6, 8, ABC_CONST(0x0000F088F088F088), "(<(ab)cd>!(ef))" }, // 427
459 { 6, 6, 9, ABC_CONST(0x00000F770F770F77), "(!<(ab)cd>!(ef))" }, // 428
460 { 6, 8, 15, ABC_CONST(0x0F77F088F088F088), "[<(ab)cd>(ef)]" }, // 429
461 { 6, 8, 10, ABC_CONST(0x0000F066F066F066), "(<[ab]cd>!(ef))" }, // 430
462 { 6, 10, 18, ABC_CONST(0x0F99F066F066F066), "[<[ab]cd>(ef)]" }, // 431
463 { 6, 7, 11, ABC_CONST(0x00007FFF7FFF0000), "(!(abcd)[ef])" }, // 432
464 { 6, 7, 9, ABC_CONST(0x000080FF80FF0000), "(!(!(abc)d)[ef])" }, // 433
465 { 6, 9, 14, ABC_CONST(0x00007F807F800000), "([(abc)d][ef])" }, // 434
466 { 6, 7, 10, ABC_CONST(0x00008FFF8FFF0000), "(!(!(ab)cd)[ef])" }, // 435
467 { 6, 7, 10, ABC_CONST(0x000070FF70FF0000), "(!(!(!(ab)c)d)[ef])" }, // 436
468 { 6, 9, 14, ABC_CONST(0x00008F708F700000), "([(!(ab)c)d][ef])" }, // 437
469 { 6, 9, 13, ABC_CONST(0x000087FF87FF0000), "(!([(ab)c]d)[ef])" }, // 438
470 { 6, 11, 20, ABC_CONST(0x0000877887780000), "([(ab)cd][ef])" }, // 439
471 { 6, 9, 12, ABC_CONST(0x00009FFF9FFF0000), "(!([ab]cd)[ef])" }, // 440
472 { 6, 9, 11, ABC_CONST(0x000060FF60FF0000), "(!(!([ab]c)d)[ef])" }, // 441
473 { 6, 11, 17, ABC_CONST(0x00009F609F600000), "([([ab]c)d][ef])" }, // 442
474 { 6, 11, 16, ABC_CONST(0x000069FF69FF0000), "(!([abc]d)[ef])" }, // 443
475 { 6, 13, 26, ABC_CONST(0x0000699669960000), "([abcd][ef])" }, // 444
476 { 6, 8, 10, ABC_CONST(0x000035FF35FF0000), "(!(<abc>d)[ef])" }, // 445
477 { 6, 10, 14, ABC_CONST(0x000035CA35CA0000), "([<abc>d][ef])" }, // 446
478 { 6, 7, 10, ABC_CONST(0x0000F888F8880000), "(!(!(ab)!(cd))[ef])" }, // 447
479 { 6, 9, 15, ABC_CONST(0x0000788878880000), "([(ab)(cd)][ef])" }, // 448
480 { 6, 9, 16, ABC_CONST(0x0000877787770000), "(![(ab)(cd)][ef])" }, // 449
481 { 6, 9, 12, ABC_CONST(0x0000F999F9990000), "(!([ab]!(cd))[ef])" }, // 450
482 { 6, 11, 14, ABC_CONST(0x0000066006600000), "([ab][cd][ef])" }, // 451
483 { 6, 11, 14, ABC_CONST(0x0000F99FF99F0000), "(!([ab][cd])[ef])" }, // 452
484 { 6, 8, 11, ABC_CONST(0x0000CAAACAAA0000), "(<ab(cd)>[ef])" }, // 453
485 { 6, 10, 14, ABC_CONST(0x0000ACCAACCA0000), "(<ab[cd]>[ef])" }, // 454
486 { 6, 8, 9, ABC_CONST(0x0000F088F0880000), "(<(ab)cd>[ef])" }, // 455
487 { 6, 8, 10, ABC_CONST(0x00000F770F770000), "(!<(ab)cd>[ef])" }, // 456
488 { 6, 10, 11, ABC_CONST(0x0000F066F0660000), "(<[ab]cd>[ef])" }, // 457
489 { 6, 5, 11, ABC_CONST(0x007F7F7F7F7F7F7F), "(!(abc)!(def))" }, // 458
490 { 6, 7, 16, ABC_CONST(0x7F80808080808080), "[(abc)(def)]" }, // 459
491 { 6, 5, 9, ABC_CONST(0x008F8F8F8F8F8F8F), "(!(!(ab)c)!(def))" }, // 460
492 { 6, 7, 16, ABC_CONST(0x8F70707070707070), "[(!(ab)c)(def)]" }, // 461
493 { 6, 7, 13, ABC_CONST(0x0078787878787878), "([(ab)c]!(def))" }, // 462
494 { 6, 7, 12, ABC_CONST(0x009F9F9F9F9F9F9F), "(!([ab]c)!(def))" }, // 463
495 { 6, 9, 20, ABC_CONST(0x9F60606060606060), "[([ab]c)(def)]" }, // 464
496 { 6, 9, 17, ABC_CONST(0x0096969696969696), "([abc]!(def))" }, // 465
497 { 6, 6, 9, ABC_CONST(0x00CACACACACACACA), "(<abc>!(def))" }, // 466
498 { 6, 8, 16, ABC_CONST(0x35CACACACACACACA), "[<abc>(def)]" }, // 467
499 { 6, 5, 8, ABC_CONST(0x8F0000008F8F8F8F), "(!(!(ab)c)!(!(de)f))" }, // 468
500 { 6, 7, 16, ABC_CONST(0x708F8F8F70707070), "[(!(ab)c)(!(de)f)]" }, // 469
501 { 6, 7, 11, ABC_CONST(0x7800000078787878), "([(ab)c]!(!(de)f))" }, // 470
502 { 6, 7, 10, ABC_CONST(0x9F0000009F9F9F9F), "(!([ab]c)!(!(de)f))" }, // 471
503 { 6, 9, 20, ABC_CONST(0x609F9F9F60606060), "[([ab]c)(!(de)f)]" }, // 472
504 { 6, 9, 14, ABC_CONST(0x9600000096969696), "([abc]!(!(de)f))" }, // 473
505 { 6, 6, 8, ABC_CONST(0xCA000000CACACACA), "(<abc>!(!(de)f))" }, // 474
506 { 6, 8, 16, ABC_CONST(0xCA353535CACACACA), "[<abc>(!(de)f)]" }, // 475
507 { 6, 9, 15, ABC_CONST(0x0078787878000000), "([(ab)c][(de)f])" }, // 476
508 { 6, 9, 14, ABC_CONST(0x009F9F9F9F000000), "(!([ab]c)[(de)f])" }, // 477
509 { 6, 11, 19, ABC_CONST(0x0096969696000000), "([abc][(de)f])" }, // 478
510 { 6, 8, 11, ABC_CONST(0x00CACACACA000000), "(<abc>[(de)f])" }, // 479
511 { 6, 9, 13, ABC_CONST(0x9F00009F9F9F9F9F), "(!([ab]c)!([de]f))" }, // 480
512 { 6, 11, 25, ABC_CONST(0x609F9F6060606060), "[([ab]c)([de]f)]" }, // 481
513 { 6, 11, 18, ABC_CONST(0x9600009696969696), "([abc]!([de]f))" }, // 482
514 { 6, 8, 10, ABC_CONST(0xCA0000CACACACACA), "(<abc>!([de]f))" }, // 483
515 { 6, 10, 20, ABC_CONST(0xCA3535CACACACACA), "[<abc>([de]f)]" }, // 484
516 { 6, 13, 24, ABC_CONST(0x9600009600969600), "([abc][def])" }, // 485
517 { 6, 10, 14, ABC_CONST(0xCA0000CA00CACA00), "(<abc>[def])" }, // 486
518 { 6, 7, 8, ABC_CONST(0xCACA0000CA00CA00), "(<abc><def>)" }, // 487
519 { 6, 9, 16, ABC_CONST(0x3535CACA35CA35CA), "[<abc><def>]" }, // 488
520 { 6, 6, 10, ABC_CONST(0xCAAAAAAAAAAAAAAA), "<ab(cdef)>" }, // 489
521 { 6, 6, 10, ABC_CONST(0xACCCCCCCAAAAAAAA), "<ab(!(cde)f)>" }, // 490
522 { 6, 8, 16, ABC_CONST(0xACCCCCCCCAAAAAAA), "<ab[(cde)f]>" }, // 491
523 { 6, 6, 10, ABC_CONST(0xACCCAAAAAAAAAAAA), "<ab(!(cd)ef)>" }, // 492
524 { 6, 6, 10, ABC_CONST(0xCAAACCCCAAAAAAAA), "<ab(!(!(cd)e)f)>" }, // 493
525 { 6, 8, 16, ABC_CONST(0xCAAACCCCACCCAAAA), "<ab[(!(cd)e)f]>" }, // 494
526 { 6, 8, 14, ABC_CONST(0xACCCCAAAAAAAAAAA), "<ab([(cd)e]f)>" }, // 495
527 { 6, 10, 24, ABC_CONST(0xCAAAACCCACCCCAAA), "<ab[(cd)ef]>" }, // 496
528 { 6, 8, 12, ABC_CONST(0xACCAAAAAAAAAAAAA), "<ab([cd]ef)>" }, // 497
529 { 6, 8, 12, ABC_CONST(0xCAACCCCCAAAAAAAA), "<ab(!([cd]e)f)>" }, // 498
530 { 6, 10, 20, ABC_CONST(0xCAACCCCCACCAAAAA), "<ab[([cd]e)f]>" }, // 499
531 { 6, 10, 18, ABC_CONST(0xCAACACCAAAAAAAAA), "<ab([cde]f)>" }, // 500
532 { 6, 12, 32, ABC_CONST(0xACCACAACCAACACCA), "<ab[cdef]>" }, // 501
533 { 6, 7, 10, ABC_CONST(0xCCAACACAAAAAAAAA), "<ab(<cde>f)>" }, // 502
534 { 6, 9, 16, ABC_CONST(0xAACCACACCCAACACA), "<ab[<cde>f]>" }, // 503
535 { 6, 6, 12, ABC_CONST(0xAAAAACCCACCCACCC), "<ab(!(cd)!(ef))>" }, // 504
536 { 6, 8, 18, ABC_CONST(0xACCCCAAACAAACAAA), "<ab[(cd)(ef)]>" }, // 505
537 { 6, 8, 14, ABC_CONST(0xAAAAACCAACCAACCA), "<ab([cd]!(ef))>" }, // 506
538 { 6, 10, 16, ABC_CONST(0xAAAAACCAACCAAAAA), "<ab([cd][ef])>" }, // 507
539 { 6, 7, 12, ABC_CONST(0xCCAACACACACACACA), "<ab<cd(ef)>>" }, // 508
540 { 6, 9, 16, ABC_CONST(0xCACACCAACCAACACA), "<ab<cd[ef]>>" }, // 509
541 { 6, 7, 10, ABC_CONST(0xCCCCAAAACAAACAAA), "<ab<(cd)ef>>" }, // 510
542 { 6, 9, 12, ABC_CONST(0xCCCCAAAAACCAACCA), "<ab<[cd]ef>>" }, // 511
543 { 6, 6, 9, ABC_CONST(0xC0AAAAAAAAAAAAAA), "<a(bc)(def)>" }, // 512
544 { 6, 6, 10, ABC_CONST(0xAAC0C0C0AAAAAAAA), "<a(bc)(!(de)f)>" }, // 513
545 { 6, 8, 12, ABC_CONST(0xAAC0C0AAAAAAAAAA), "<a(bc)([de]f)>" }, // 514
546 { 6, 8, 10, ABC_CONST(0x3CAAAAAAAAAAAAAA), "<a[bc](def)>" }, // 515
547 { 6, 8, 12, ABC_CONST(0xAA3C3C3CAAAAAAAA), "<a[bc](!(de)f)>" }, // 516
548 { 6, 10, 14, ABC_CONST(0xAA3C3CAAAAAAAAAA), "<a[bc]([de]f)>" }, // 517
549 { 6, 6, 8, ABC_CONST(0xC000AAAAAAAAAAAA), "<a(bcd)(ef)>" }, // 518
550 { 6, 6, 8, ABC_CONST(0x3F00AAAAAAAAAAAA), "<a(!(bc)d)(ef)>" }, // 519
551 { 6, 8, 10, ABC_CONST(0x3FC0AAAAAAAAAAAA), "<a[(bc)d](ef)>" }, // 520
552 { 6, 8, 9, ABC_CONST(0x3C00AAAAAAAAAAAA), "<a([bc]d)(ef)>" }, // 521
553 { 6, 10, 12, ABC_CONST(0xC33CAAAAAAAAAAAA), "<a[bcd](ef)>" }, // 522
554 { 6, 7, 8, ABC_CONST(0xF0CCAAAAAAAAAAAA), "<a<bcd>(ef)>" }, // 523
555 { 6, 6, 11, ABC_CONST(0xF088888888888888), "<(ab)c(def)>" }, // 524
556 { 6, 6, 10, ABC_CONST(0x88F0F0F088888888), "<(ab)c(!(de)f)>" }, // 525
557 { 6, 8, 15, ABC_CONST(0x88F0F0F0F0888888), "<(ab)c[(de)f]>" }, // 526
558 { 6, 8, 13, ABC_CONST(0x88F0F08888888888), "<(ab)c([de]f)>" }, // 527
559 { 6, 10, 20, ABC_CONST(0xF08888F088F0F088), "<(ab)c[def]>" }, // 528
560 { 6, 7, 10, ABC_CONST(0xF0F08888F088F088), "<(ab)c<def>>" }, // 529
561 { 6, 8, 14, ABC_CONST(0xF066666666666666), "<[ab]c(def)>" }, // 530
562 { 6, 8, 12, ABC_CONST(0x66F0F0F066666666), "<[ab]c(!(de)f)>" }, // 531
563 { 6, 10, 18, ABC_CONST(0x66F0F0F0F0666666), "<[ab]c[(de)f]>" }, // 532
564 { 6, 10, 16, ABC_CONST(0x66F0F06666666666), "<[ab]c([de]f)>" }, // 533
565 { 6, 12, 24, ABC_CONST(0xF06666F066F0F066), "<[ab]c[def]>" }, // 534
566 { 6, 9, 12, ABC_CONST(0xF0F06666F066F066), "<[ab]c<def>>" }, // 535
567 { 6, 6, 9, ABC_CONST(0xF000888888888888), "<(ab)(cd)(ef)>" }, // 536
568 { 6, 6, 9, ABC_CONST(0xF000777777777777), "<!(ab)(cd)(ef)>" }, // 537
569 { 6, 8, 12, ABC_CONST(0x8888F000F0008888), "<(ab)(cd)[ef]>" }, // 538
570 { 6, 8, 12, ABC_CONST(0x7777F000F0007777), "<!(ab)(cd)[ef]>" }, // 539
571 { 6, 8, 10, ABC_CONST(0x0FF0888888888888), "<(ab)[cd](ef)>" }, // 540
572 { 6, 8, 11, ABC_CONST(0xF000666666666666), "<[ab](cd)(ef)>" }, // 541
573 { 6, 10, 14, ABC_CONST(0x6666F000F0006666), "<[ab](cd)[ef]>" }, // 542
574 { 6, 10, 12, ABC_CONST(0x0FF0666666666666), "<[ab][cd](ef)>" }, // 543
575 { 6, 12, 16, ABC_CONST(0x66660FF00FF06666), "<[ab][cd][ef]>" }, // 544
576 { 6, 6, 10, ABC_CONST(0xFF00808080808080), "<(abc)d(ef)>" }, // 545
577 { 6, 8, 12, ABC_CONST(0x8080FF00FF008080), "<(abc)d[ef]>" }, // 546
578 { 6, 6, 10, ABC_CONST(0xFF00707070707070), "<(!(ab)c)d(ef)>" }, // 547
579 { 6, 8, 12, ABC_CONST(0x7070FF00FF007070), "<(!(ab)c)d[ef]>" }, // 548
580 { 6, 8, 14, ABC_CONST(0xFF00787878787878), "<[(ab)c]d(ef)>" }, // 549
581 { 6, 10, 16, ABC_CONST(0x7878FF00FF007878), "<[(ab)c]d[ef]>" }, // 550
582 { 6, 8, 12, ABC_CONST(0xFF00606060606060), "<([ab]c)d(ef)>" }, // 551
583 { 6, 10, 14, ABC_CONST(0x6060FF00FF006060), "<([ab]c)d[ef]>" }, // 552
584 { 6, 10, 18, ABC_CONST(0xFF00969696969696), "<[abc]d(ef)>" }, // 553
585 { 6, 12, 20, ABC_CONST(0x9696FF00FF009696), "<[abc]d[ef]>" }, // 554
586 { 6, 7, 10, ABC_CONST(0xFF00CACACACACACA), "<<abc>d(ef)>" }, // 555
587 { 6, 9, 12, ABC_CONST(0xCACAFF00FF00CACA), "<<abc>d[ef]>" }, // 556
588 { 6, 6, 7, ABC_CONST(0xFF00000080808080), "<(abc)(de)f>" }, // 557
589 { 6, 6, 7, ABC_CONST(0xFF0000007F7F7F7F), "<!(abc)(de)f>" }, // 558
590 { 6, 8, 8, ABC_CONST(0x00FFFF0080808080), "<(abc)[de]f>" }, // 559
591 { 6, 6, 7, ABC_CONST(0xFF00000070707070), "<(!(ab)c)(de)f>" }, // 560
592 { 6, 6, 7, ABC_CONST(0xFF0000008F8F8F8F), "<!(!(ab)c)(de)f>" }, // 561
593 { 6, 8, 8, ABC_CONST(0x00FFFF0070707070), "<(!(ab)c)[de]f>" }, // 562
594 { 6, 8, 9, ABC_CONST(0xFF00000078787878), "<[(ab)c](de)f>" }, // 563
595 { 6, 10, 10, ABC_CONST(0x00FFFF0078787878), "<[(ab)c][de]f>" }, // 564
596 { 6, 8, 8, ABC_CONST(0xFF00000060606060), "<([ab]c)(de)f>" }, // 565
597 { 6, 8, 8, ABC_CONST(0xFF0000009F9F9F9F), "<!([ab]c)(de)f>" }, // 566
598 { 6, 10, 9, ABC_CONST(0x00FFFF0060606060), "<([ab]c)[de]f>" }, // 567
599 { 6, 10, 11, ABC_CONST(0xFF00000096969696), "<[abc](de)f>" }, // 568
600 { 6, 12, 12, ABC_CONST(0x00FFFF0096969696), "<[abc][de]f>" }, // 569
601 { 6, 7, 7, ABC_CONST(0xFF000000CACACACA), "<<abc>(de)f>" }, // 570
602 { 6, 9, 8, ABC_CONST(0x00FFFF00CACACACA), "<<abc>[de]f>" }, // 571
603 { 6, 6, 7, ABC_CONST(0xFFFF000080008000), "<(abcd)ef>" }, // 572
604 { 6, 6, 7, ABC_CONST(0xFFFF00007F007F00), "<(!(abc)d)ef>" }, // 573
605 { 6, 8, 10, ABC_CONST(0xFFFF00007F807F80), "<[(abc)d]ef>" }, // 574
606 { 6, 6, 7, ABC_CONST(0xFFFF000070007000), "<(!(ab)cd)ef>" }, // 575
607 { 6, 6, 7, ABC_CONST(0xFFFF00008F008F00), "<(!(!(ab)c)d)ef>" }, // 576
608 { 6, 8, 10, ABC_CONST(0xFFFF00008F708F70), "<[(!(ab)c)d]ef>" }, // 577
609 { 6, 8, 9, ABC_CONST(0xFFFF000078007800), "<([(ab)c]d)ef>" }, // 578
610 { 6, 10, 14, ABC_CONST(0xFFFF000087788778), "<[(ab)cd]ef>" }, // 579
611 { 6, 8, 8, ABC_CONST(0xFFFF000060006000), "<([ab]cd)ef>" }, // 580
612 { 6, 8, 8, ABC_CONST(0xFFFF00009F009F00), "<(!([ab]c)d)ef>" }, // 581
613 { 6, 10, 12, ABC_CONST(0xFFFF00009F609F60), "<[([ab]c)d]ef>" }, // 582
614 { 6, 10, 11, ABC_CONST(0xFFFF000096009600), "<([abc]d)ef>" }, // 583
615 { 6, 12, 18, ABC_CONST(0xFFFF000069966996), "<[abcd]ef>" }, // 584
616 { 6, 7, 7, ABC_CONST(0xFFFF0000CA00CA00), "<(<abc>d)ef>" }, // 585
617 { 6, 9, 10, ABC_CONST(0xFFFF000035CA35CA), "<[<abc>d]ef>" }, // 586
618 { 6, 6, 8, ABC_CONST(0xFFFF000007770777), "<(!(ab)!(cd))ef>" }, // 587
619 { 6, 8, 11, ABC_CONST(0xFFFF000078887888), "<[(ab)(cd)]ef>" }, // 588
620 { 6, 8, 9, ABC_CONST(0xFFFF000006660666), "<([ab]!(cd))ef>" }, // 589
621 { 6, 10, 10, ABC_CONST(0xFFFF000006600660), "<([ab][cd])ef>" }, // 590
622 { 6, 7, 8, ABC_CONST(0xFFFF0000CAAACAAA), "<<ab(cd)>ef>" }, // 591
623 { 6, 9, 10, ABC_CONST(0xFFFF0000ACCAACCA), "<<ab[cd]>ef>" }, // 592
624 { 6, 7, 7, ABC_CONST(0xFFFF0000F088F088), "<<(ab)cd>ef>" }, // 593
625 { 6, 9, 8, ABC_CONST(0xFFFF0000F066F066), "<<[ab]cd>ef>" } // 594
626};
627
631
632
644Vec_Wrd_t * Mpm_ManGetTruthWithCnf( int Limit )
645{
646 Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 );
647 int i;
648 for ( i = 0; i < 595; i++ )
649 if ( s_DsdClass6[i].nClauses <= Limit )
650 Vec_WrdPush( vRes, s_DsdClass6[i].uTruth );
651 return vRes;
652}
653
665void Mpm_ManPrintDsdStats( Mpm_Man_t * p )
666{
667 int i, Absent = 0;
668 for ( i = 0; i < 595; i++ )
669 {
670 if ( p->nCountDsd[i] == 0 )
671 {
672 Absent++;
673 continue;
674 }
675 if ( p->pPars->fVeryVerbose )
676 {
677 printf( "%5d : ", i );
678 printf( "%-20s ", p->pDsd6[i].pStr );
679 printf( "%8d ", p->nCountDsd[i] );
680 printf( "\n" );
681 }
682 }
683 printf( "Unused classes = %d (%.2f %%). ", Absent, 100.0 * Absent / 595 );
684 printf( "Non-DSD cuts = %d (%.2f %%). ", p->nNonDsd, 100.0 * p->nNonDsd / p->nCutsMergedAll );
685 printf( "No-match cuts = %d (%.2f %%).\n", p->nNoMatch, 100.0 * p->nNoMatch / p->nCutsMergedAll );
686}
687
699Hsh_IntMan_t * Mpm_ManBuildHashTable( Vec_Int_t ** pvConfgRes )
700{
701 FILE * pFile;
702 char * pFileName = "dsdfuncs6.dat";
703 int RetValue, size = Extra_FileSize( pFileName ) / 12; // 2866420
704 Vec_Wrd_t * vTruthRes = Vec_WrdAlloc( size );
705 Vec_Int_t * vConfgRes = Vec_IntAlloc( size );
706 Hsh_IntMan_t * pHash;
707
708 pFile = fopen( pFileName, "rb" );
709 RetValue = fread( Vec_WrdArray(vTruthRes), sizeof(word), size, pFile );
710 RetValue = fread( Vec_IntArray(vConfgRes), sizeof(int), size, pFile );
711 vTruthRes->nSize = size;
712 vConfgRes->nSize = size;
713 // create hash table
714 pHash = Hsh_WrdManHashArrayStart( vTruthRes, 1 );
715 // cleanup
716 if ( pvConfgRes )
717 *pvConfgRes = vConfgRes;
718 else
719 Vec_IntFree( vConfgRes );
720 Vec_WrdFree( vTruthRes );
721// Hsh_IntManStop( pHash );
722 return pHash;
723}
724
736void Mpm_ManPrintPerm( unsigned s )
737{
738 int i;
739 for ( i = 0; i < 6; i++ )
740 printf( "%d ", (s >> (3*i)) & 7 );
741 printf( " " );
742}
743
755void Mpm_ManPrecomputePerms( Mpm_Man_t * p )
756{
757 int nVars = 6;
758 // 0(1:1) 1(2:1) 2(4:2) 3(10:6) 4(33:23) 5(131:98) 6(595:464)
759 int nClasses[7] = { 1, 2, 4, 10, 33, 131, 595 };
760 int nPerms = Extra_Factorial( nVars );
761// int nSwaps = (1 << nVars);
762 int * pComp, * pPerm;
763 int i, k, x, One, OneCopy, Num;
764 Vec_Int_t * vVars;
765 abctime clk = Abc_Clock();
766 assert( p->pDsd6 == NULL );
767 p->pDsd6 = s_DsdClass6;
768 // precompute schedules
769 pComp = Extra_GreyCodeSchedule( nVars );
770 pPerm = Extra_PermSchedule( nVars );
771 // map numbers into perms
772 p->vMap2Perm = Vec_IntStartFull( (1<<(3*nVars)) );
773 // store permutations
774 One = 0;
775 for ( x = 0; x < nVars; x++ )
776 {
777 p->Perm6[0][x] = (char)x;
778 One |= (x << (3*x));
779 }
780// Vec_IntWriteEntry( p->vMap2Perm, One, 0 );
781 OneCopy = One;
782 for ( k = 0; k < nPerms; k++ )
783 {
784 if ( k > 0 )
785 for ( x = 0; x < nVars; x++ )
786 p->Perm6[k][x] = p->Perm6[k-1][x];
787 ABC_SWAP( char, p->Perm6[k][pPerm[k]], p->Perm6[k][pPerm[k]+1] );
788
789 Num = ( (One >> (3*(pPerm[k] ))) ^ (One >> (3*(pPerm[k]+1))) ) & 7;
790 One ^= (Num << (3*(pPerm[k] )));
791 One ^= (Num << (3*(pPerm[k]+1)));
792
793 Vec_IntWriteEntry( p->vMap2Perm, One, k );
794
795// Mpm_ManPrintPerm( One );
796// for ( x = 0; x < nVars; x++ )
797// printf( "%d ", p->Perm6[k][x] );
798// printf( "\n" );
799 }
800 assert( OneCopy == One );
801 // fill in the gaps
802 vVars = Vec_IntAlloc( 6 );
803 Vec_IntForEachEntry( p->vMap2Perm, Num, i )
804 {
805 // mark used variables
806 int Count = 0;
807 One = i;
808 Vec_IntFill( vVars, 6, 0 );
809 for ( k = 0; k < nVars; k++ )
810 {
811 int iVar = ((One >> (3*k)) & 7);
812 if ( iVar >= nVars && iVar < 7 )
813 break;
814 if ( iVar != 7 )
815 {
816 if ( Vec_IntEntry( vVars, iVar ) == 1 )
817 break;
818 Vec_IntWriteEntry( vVars, iVar, 1 );
819 Count++;
820 }
821 }
822 // skip ones with dups and complete
823 if ( k < nVars || Count == nVars )
824 continue;
825 // find unused variables
826 for ( x = k = 0; k < 6; k++ )
827 if ( Vec_IntEntry(vVars, k) == 0 )
828 Vec_IntWriteEntry( vVars, x++, k );
829 Vec_IntShrink( vVars, x );
830 // fill in used variables
831 x = 0;
832 for ( k = 0; k < nVars; k++ )
833 {
834 int iVar = ((One >> (3*k)) & 7);
835 if ( iVar == 7 )
836 One ^= ((Vec_IntEntry(vVars, x++) ^ 7) << (3*k));
837 }
838 assert( x == Vec_IntSize(vVars) );
839 // save this one
840 assert( Vec_IntEntry( p->vMap2Perm, One ) != -1 );
841 Vec_IntWriteEntry( p->vMap2Perm, i, Vec_IntEntry(p->vMap2Perm, One) );
842/*
843 // mapping
844 Mpm_ManPrintPerm( i );
845 printf( "-> " );
846 Mpm_ManPrintPerm( One );
847 printf( "\n" );
848*/
849 }
850 Vec_IntFree( vVars );
851
852 // store permuted truth tables
853 assert( p->vPerm6 == NULL );
854 p->vPerm6 = Vec_WrdAlloc( nPerms * 595 );
855 for ( i = 0; i < nClasses[nVars]; i++ )
856 {
857 word uTruth = s_DsdClass6[i].uTruth;
858 for ( k = 0; k < nPerms; k++ )
859 {
860 uTruth = Abc_Tt6SwapAdjacent( uTruth, pPerm[k] );
861 Vec_WrdPush( p->vPerm6, uTruth );
862 }
863 assert( uTruth == s_DsdClass6[i].uTruth );
864 }
865 ABC_FREE( pPerm );
866 ABC_FREE( pComp );
867 // build hash table
868 p->pHash = Mpm_ManBuildHashTable( &p->vConfgRes );
869 Abc_PrintTime( 1, "Setting up DSD information", Abc_Clock() - clk );
870}
871
883word Mpm_CutTruthFromDsd( Mpm_Man_t * pMan, Mpm_Cut_t * pCut, int iClass )
884{
885 int i;
886 word uTruth = pMan->pDsd6[iClass].uTruth;
887 assert( pMan->pDsd6[iClass].nVars == (int)pCut->nLeaves );
888 for ( i = 0; i < (int)pCut->nLeaves; i++ )
889 if ( Abc_LitIsCompl(pCut->pLeaves[i]) )
890 uTruth = Abc_Tt6Flip( uTruth, i );
891 return uTruth;
892}
893
905int Mpm_CutCheckDsd6( Mpm_Man_t * p, word t )
906{
907 int fCompl, Entry, Config;
908 if ( (fCompl = (t & 1)) )
909 t = ~t;
910 Entry = *Hsh_IntManLookup( p->pHash, (unsigned *)&t );
911 if ( Entry == -1 )
912 return -1;
913 Config = Vec_IntEntry( p->vConfgRes, Entry );
914 if ( fCompl )
915 Config ^= (1 << 16);
916 return Config;
917}
918
930int Mpm_CutComputeDsd6( Mpm_Man_t * p, Mpm_Cut_t * pCut, Mpm_Cut_t * pCut0, Mpm_Cut_t * pCut1, Mpm_Cut_t * pCutC, int fCompl0, int fCompl1, int fComplC, int Type )
931{
932 int fVerbose = 0;
933 int i, Config, iClass, fCompl;
934 int pLeavesNew[6] = { -1, -1, -1, -1, -1, -1 };
935 word t = 0;
936 if ( pCutC == NULL )
937 {
938 word t0, t1;
939 int iClass0 = Abc_Lit2Var(pCut0->iFunc);
940 int iClass1 = Abc_Lit2Var(pCut1->iFunc);
941 word Truth0 = p->pDsd6[iClass0].uTruth;
942 int Perm1 = Vec_IntEntry( p->vMap2Perm, p->uPermMask[1] );
943 word Truth1p = Vec_WrdEntry( p->vPerm6, iClass1 * 720 + Perm1 );
944 if ( p->uComplMask[1] )
945 {
946 for ( i = 0; i < 6; i++ )
947 if ( (p->uComplMask[1] >> i) & 1 )
948 Truth1p = Abc_Tt6Flip( Truth1p, i );
949 }
950 t0 = (fCompl0 ^ pCut0->fCompl ^ Abc_LitIsCompl(pCut0->iFunc)) ? ~Truth0 : Truth0;
951 t1 = (fCompl1 ^ pCut1->fCompl ^ Abc_LitIsCompl(pCut1->iFunc)) ? ~Truth1p : Truth1p;
952 if ( Type == 1 )
953 t = t0 & t1;
954 else if ( Type == 2 )
955 t = t0 ^ t1;
956 else assert( 0 );
957
958if ( fVerbose )
959{
960Mpm_ManPrintPerm( p->uPermMask[1] ); printf( "\n" );
961Kit_DsdPrintFromTruth( (unsigned *)&Truth0, 6 ); printf( "\n" );
962Kit_DsdPrintFromTruth( (unsigned *)&Truth1p, 6 ); printf( "\n" );
963Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ); printf( "\n" );
964}
965 }
966 else
967 {
968 word t0, t1, tC;
969 int iClass0 = Abc_Lit2Var(pCut0->iFunc);
970 int iClass1 = Abc_Lit2Var(pCut1->iFunc);
971 int iClassC = Abc_Lit2Var(pCutC->iFunc);
972 word Truth0 = p->pDsd6[iClass0].uTruth;
973 int Perm1 = Vec_IntEntry( p->vMap2Perm, p->uPermMask[1] );
974 int PermC = Vec_IntEntry( p->vMap2Perm, p->uPermMask[2] );
975 word Truth1p = Vec_WrdEntry( p->vPerm6, iClass1 * 720 + Perm1 );
976 word TruthCp = Vec_WrdEntry( p->vPerm6, iClassC * 720 + PermC );
977 if ( p->uComplMask[1] )
978 {
979 for ( i = 0; i < 6; i++ )
980 if ( (p->uComplMask[1] >> i) & 1 )
981 Truth1p = Abc_Tt6Flip( Truth1p, i );
982 }
983 if ( p->uComplMask[2] )
984 {
985 for ( i = 0; i < 6; i++ )
986 if ( (p->uComplMask[2] >> i) & 1 )
987 TruthCp = Abc_Tt6Flip( TruthCp, i );
988 }
989 t0 = (fCompl0 ^ pCut0->fCompl ^ Abc_LitIsCompl(pCut0->iFunc)) ? ~Truth0 : Truth0;
990 t1 = (fCompl1 ^ pCut1->fCompl ^ Abc_LitIsCompl(pCut1->iFunc)) ? ~Truth1p : Truth1p;
991 tC = (fComplC ^ pCutC->fCompl ^ Abc_LitIsCompl(pCutC->iFunc)) ? ~TruthCp : TruthCp;
992 t = (tC & t1) | (~tC & t0);
993 }
994
995 // find configuration
996 Config = Mpm_CutCheckDsd6( p, t );
997 if ( Config == -1 )
998 {
999 p->nNonDsd++;
1000 return 0;
1001 }
1002
1003 // get the class
1004 iClass = Config >> 17;
1005 fCompl = (Config >> 16) & 1;
1006 Config &= 0xFFFF;
1007
1008 // check if the gate exists
1009 if ( p->pPars->fMap4Gates )
1010 {
1011 if ( Vec_IntSize(Vec_WecEntry(p->vNpnConfigs, iClass)) == 0 )
1012 {
1013 p->nNoMatch++;
1014 return 0;
1015 }
1016 }
1017
1018 // set the function
1019 pCut->iFunc = Abc_Var2Lit( iClass, fCompl );
1020
1021if ( fVerbose )
1022{
1023Mpm_CutPrint( pCut0 );
1024Mpm_CutPrint( pCut1 );
1025Mpm_CutPrint( pCut );
1026}
1027
1028 // update cut
1029 assert( (Config >> 6) < 720 );
1030 for ( i = 0; i < (int)pCut->nLeaves; i++ )
1031 pLeavesNew[(int)(p->Perm6[Config >> 6][i])] = Abc_LitNotCond( pCut->pLeaves[i], (Config >> i) & 1 );
1032 pCut->nLeaves = p->pDsd6[iClass].nVars;
1033 for ( i = 0; i < (int)pCut->nLeaves; i++ )
1034 assert( pLeavesNew[i] != -1 );
1035 for ( i = 0; i < (int)pCut->nLeaves; i++ )
1036 pCut->pLeaves[i] = pLeavesNew[i];
1037 p->nCountDsd[iClass]++;
1038 p->nSmallSupp += (int)(pCut->nLeaves < 2);
1039
1040if ( fVerbose )
1041{
1042printf( "Computed " );
1043Mpm_CutPrint( pCut );
1044printf( "\n" );
1045}
1046 return 1;
1047}
1048
1052
1053
1054ABC_NAMESPACE_IMPL_END
1055
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
p
Cube * p
Definition exorList.c:222
Extra_FileSize
int Extra_FileSize(char *pFileName)
Definition extraUtilFile.c:327
Extra_PermSchedule
int * Extra_PermSchedule(int n)
Definition extraUtilMisc.c:2206
Extra_Factorial
int Extra_Factorial(int n)
Definition extraUtilMisc.c:217
Extra_GreyCodeSchedule
int * Extra_GreyCodeSchedule(int n)
Definition extraUtilMisc.c:2170
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Kit_DsdPrintFromTruth
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition kitDsd.c:491
Mpm_ManBuildHashTable
Hsh_IntMan_t * Mpm_ManBuildHashTable(Vec_Int_t **pvConfgRes)
Definition mpmDsd.c:699
Mpm_ManGetTruthWithCnf
Vec_Wrd_t * Mpm_ManGetTruthWithCnf(int Limit)
FUNCTION DEFINITIONS ///.
Definition mpmDsd.c:644
Mpm_CutCheckDsd6
int Mpm_CutCheckDsd6(Mpm_Man_t *p, word t)
Definition mpmDsd.c:905
Mpm_ManPrintPerm
void Mpm_ManPrintPerm(unsigned s)
Definition mpmDsd.c:736
Mpm_CutComputeDsd6
int Mpm_CutComputeDsd6(Mpm_Man_t *p, Mpm_Cut_t *pCut, Mpm_Cut_t *pCut0, Mpm_Cut_t *pCut1, Mpm_Cut_t *pCutC, int fCompl0, int fCompl1, int fComplC, int Type)
Definition mpmDsd.c:930
Mpm_ManPrecomputePerms
void Mpm_ManPrecomputePerms(Mpm_Man_t *p)
Definition mpmDsd.c:755
Mpm_CutTruthFromDsd
word Mpm_CutTruthFromDsd(Mpm_Man_t *pMan, Mpm_Cut_t *pCut, int iClass)
Definition mpmDsd.c:883
Mpm_ManPrintDsdStats
void Mpm_ManPrintDsdStats(Mpm_Man_t *p)
Definition mpmDsd.c:665
Mpm_Man_t
struct Mpm_Man_t_ Mpm_Man_t
Definition mpmInt.h:94
Mpm_Dsd_t
struct Mpm_Dsd_t_ Mpm_Dsd_t
Definition mpmInt.h:84
Mpm_CutPrint
void Mpm_CutPrint(Mpm_Cut_t *pCut)
Definition mpmMap.c:103
Mpm_Cut_t
struct Mpm_Cut_t_ Mpm_Cut_t
BASIC TYPES ///.
Definition mpmInt.h:61
Mpm_Cut_t_::fCompl
unsigned fCompl
Definition mpmInt.h:66
Mpm_Cut_t_::nLeaves
unsigned nLeaves
Definition mpmInt.h:68
Mpm_Cut_t_::pLeaves
int pLeaves[1]
Definition mpmInt.h:69
Mpm_Cut_t_::iFunc
unsigned iFunc
Definition mpmInt.h:65
Mpm_Dsd_t_::uTruth
word uTruth
Definition mpmInt.h:90
Mpm_Dsd_t_::nVars
int nVars
Definition mpmInt.h:87
Mpm_Man_t_::pDsd6
Mpm_Dsd_t * pDsd6
Definition mpmInt.h:132
assert
#define assert(ex)
Definition util_old.h:213
Hsh_IntMan_t
struct Hsh_IntMan_t_ Hsh_IntMan_t
Definition vecHsh.h:66
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42