abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
extraUtilDsd.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [extraUtilDsd.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [extra]
8 
9  Synopsis [File management utilities.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: extraUtilDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include <stdio.h>
22 #include <stdlib.h>
23 #include <string.h>
24 #include <assert.h>
25 
26 #include "extra.h"
27 #include "misc/vec/vec.h"
28 #include "misc/vec/vecHsh.h"
29 #include "misc/util/utilTruth.h"
30 #include "bool/rsb/rsb.h"
31 
32 ABC_NAMESPACE_IMPL_START
33 
34 ////////////////////////////////////////////////////////////////////////
35 /// DECLARATIONS ///
36 ////////////////////////////////////////////////////////////////////////
37 
38 typedef struct Sdm_Dsd_t_ Sdm_Dsd_t;
39 struct Sdm_Dsd_t_
40 {
41  int nVars; // support size
42  int nAnds; // the number of AND gates
43  int nClauses; // the number of CNF clauses
44  word uTruth; // truth table
45  char * pStr; // description
46 };
47 
48 #define DSD_CLASS_NUM 595
49 
50 static Sdm_Dsd_t s_DsdClass6[DSD_CLASS_NUM] = {
51  { 0, 0, 1, ABC_CONST(0x0000000000000000), "0" }, // 0
52  { 1, 0, 2, ABC_CONST(0xAAAAAAAAAAAAAAAA), "a" }, // 1
53  { 2, 1, 3, ABC_CONST(0x8888888888888888), "(ab)" }, // 2
54  { 2, 3, 4, ABC_CONST(0x6666666666666666), "[ab]" }, // 3
55  { 3, 2, 4, ABC_CONST(0x8080808080808080), "(abc)" }, // 4
56  { 3, 2, 4, ABC_CONST(0x7070707070707070), "(!(ab)c)" }, // 5
57  { 3, 4, 6, ABC_CONST(0x7878787878787878), "[(ab)c]" }, // 6
58  { 3, 4, 5, ABC_CONST(0x6060606060606060), "([ab]c)" }, // 7
59  { 3, 6, 8, ABC_CONST(0x9696969696969696), "[abc]" }, // 8
60  { 3, 3, 4, ABC_CONST(0xCACACACACACACACA), "<abc>" }, // 9
61  { 4, 3, 5, ABC_CONST(0x8000800080008000), "(abcd)" }, // 10
62  { 4, 3, 5, ABC_CONST(0x7F007F007F007F00), "(!(abc)d)" }, // 11
63  { 4, 5, 8, ABC_CONST(0x7F807F807F807F80), "[(abc)d]" }, // 12
64  { 4, 3, 5, ABC_CONST(0x7000700070007000), "(!(ab)cd)" }, // 13
65  { 4, 3, 5, ABC_CONST(0x8F008F008F008F00), "(!(!(ab)c)d)" }, // 14
66  { 4, 5, 8, ABC_CONST(0x8F708F708F708F70), "[(!(ab)c)d]" }, // 15
67  { 4, 5, 7, ABC_CONST(0x7800780078007800), "([(ab)c]d)" }, // 16
68  { 4, 7, 12, ABC_CONST(0x8778877887788778), "[(ab)cd]" }, // 17
69  { 4, 5, 6, ABC_CONST(0x6000600060006000), "([ab]cd)" }, // 18
70  { 4, 5, 6, ABC_CONST(0x9F009F009F009F00), "(!([ab]c)d)" }, // 19
71  { 4, 7, 10, ABC_CONST(0x9F609F609F609F60), "[([ab]c)d]" }, // 20
72  { 4, 7, 9, ABC_CONST(0x9600960096009600), "([abc]d)" }, // 21
73  { 4, 9, 16, ABC_CONST(0x6996699669966996), "[abcd]" }, // 22
74  { 4, 4, 5, ABC_CONST(0xCA00CA00CA00CA00), "(<abc>d)" }, // 23
75  { 4, 6, 8, ABC_CONST(0x35CA35CA35CA35CA), "[<abc>d]" }, // 24
76  { 4, 3, 6, ABC_CONST(0x0777077707770777), "(!(ab)!(cd))" }, // 25
77  { 4, 5, 9, ABC_CONST(0x7888788878887888), "[(ab)(cd)]" }, // 26
78  { 4, 5, 7, ABC_CONST(0x0666066606660666), "([ab]!(cd))" }, // 27
79  { 4, 7, 8, ABC_CONST(0x0660066006600660), "([ab][cd])" }, // 28
80  { 4, 4, 6, ABC_CONST(0xCAAACAAACAAACAAA), "<ab(cd)>" }, // 29
81  { 4, 6, 8, ABC_CONST(0xACCAACCAACCAACCA), "<ab[cd]>" }, // 30
82  { 4, 4, 5, ABC_CONST(0xF088F088F088F088), "<(ab)cd>" }, // 31
83  { 4, 6, 6, ABC_CONST(0xF066F066F066F066), "<[ab]cd>" }, // 32
84  { 5, 4, 6, ABC_CONST(0x8000000080000000), "(abcde)" }, // 33
85  { 5, 4, 6, ABC_CONST(0x7FFF00007FFF0000), "(!(abcd)e)" }, // 34
86  { 5, 6, 10, ABC_CONST(0x7FFF80007FFF8000), "[(abcd)e]" }, // 35
87  { 5, 4, 6, ABC_CONST(0x7F0000007F000000), "(!(abc)de)" }, // 36
88  { 5, 4, 6, ABC_CONST(0x80FF000080FF0000), "(!(!(abc)d)e)" }, // 37
89  { 5, 6, 10, ABC_CONST(0x80FF7F0080FF7F00), "[(!(abc)d)e]" }, // 38
90  { 5, 6, 9, ABC_CONST(0x7F8000007F800000), "([(abc)d]e)" }, // 39
91  { 5, 8, 16, ABC_CONST(0x807F7F80807F7F80), "[(abc)de]" }, // 40
92  { 5, 4, 6, ABC_CONST(0x7000000070000000), "(!(ab)cde)" }, // 41
93  { 5, 4, 6, ABC_CONST(0x8FFF00008FFF0000), "(!(!(ab)cd)e)" }, // 42
94  { 5, 6, 10, ABC_CONST(0x8FFF70008FFF7000), "[(!(ab)cd)e]" }, // 43
95  { 5, 4, 6, ABC_CONST(0x8F0000008F000000), "(!(!(ab)c)de)" }, // 44
96  { 5, 4, 6, ABC_CONST(0x70FF000070FF0000), "(!(!(!(ab)c)d)e)" }, // 45
97  { 5, 6, 10, ABC_CONST(0x70FF8F0070FF8F00), "[(!(!(ab)c)d)e]" }, // 46
98  { 5, 6, 9, ABC_CONST(0x8F7000008F700000), "([(!(ab)c)d]e)" }, // 47
99  { 5, 8, 16, ABC_CONST(0x708F8F70708F8F70), "[(!(ab)c)de]" }, // 48
100  { 5, 6, 8, ABC_CONST(0x7800000078000000), "([(ab)c]de)" }, // 49
101  { 5, 6, 8, ABC_CONST(0x87FF000087FF0000), "(!([(ab)c]d)e)" }, // 50
102  { 5, 8, 14, ABC_CONST(0x87FF780087FF7800), "[([(ab)c]d)e]" }, // 51
103  { 5, 8, 13, ABC_CONST(0x8778000087780000), "([(ab)cd]e)" }, // 52
104  { 5, 10, 24, ABC_CONST(0x7887877878878778), "[(ab)cde]" }, // 53
105  { 5, 6, 7, ABC_CONST(0x6000000060000000), "([ab]cde)" }, // 54
106  { 5, 6, 7, ABC_CONST(0x9FFF00009FFF0000), "(!([ab]cd)e)" }, // 55
107  { 5, 8, 12, ABC_CONST(0x9FFF60009FFF6000), "[([ab]cd)e]" }, // 56
108  { 5, 6, 7, ABC_CONST(0x9F0000009F000000), "(!([ab]c)de)" }, // 57
109  { 5, 6, 7, ABC_CONST(0x60FF000060FF0000), "(!(!([ab]c)d)e)" }, // 58
110  { 5, 8, 12, ABC_CONST(0x60FF9F0060FF9F00), "[(!([ab]c)d)e]" }, // 59
111  { 5, 8, 11, ABC_CONST(0x9F6000009F600000), "([([ab]c)d]e)" }, // 60
112  { 5, 10, 20, ABC_CONST(0x609F9F60609F9F60), "[([ab]c)de]" }, // 61
113  { 5, 8, 10, ABC_CONST(0x9600000096000000), "([abc]de)" }, // 62
114  { 5, 8, 10, ABC_CONST(0x69FF000069FF0000), "(!([abc]d)e)" }, // 63
115  { 5, 10, 18, ABC_CONST(0x69FF960069FF9600), "[([abc]d)e]" }, // 64
116  { 5, 10, 17, ABC_CONST(0x6996000069960000), "([abcd]e)" }, // 65
117  { 5, 12, 32, ABC_CONST(0x9669699696696996), "[abcde]" }, // 66
118  { 5, 5, 6, ABC_CONST(0xCA000000CA000000), "(<abc>de)" }, // 67
119  { 5, 5, 6, ABC_CONST(0x35FF000035FF0000), "(!(<abc>d)e)" }, // 68
120  { 5, 7, 10, ABC_CONST(0x35FFCA0035FFCA00), "[(<abc>d)e]" }, // 69
121  { 5, 7, 9, ABC_CONST(0x35CA000035CA0000), "([<abc>d]e)" }, // 70
122  { 5, 9, 16, ABC_CONST(0xCA3535CACA3535CA), "[<abc>de]" }, // 71
123  { 5, 4, 7, ABC_CONST(0x0777000007770000), "(!(ab)!(cd)e)" }, // 72
124  { 5, 4, 7, ABC_CONST(0xF8880000F8880000), "(!(!(ab)!(cd))e)" }, // 73
125  { 5, 6, 12, ABC_CONST(0xF8880777F8880777), "[(!(ab)!(cd))e]" }, // 74
126  { 5, 6, 10, ABC_CONST(0x7888000078880000), "([(ab)(cd)]e)" }, // 75
127  { 5, 6, 10, ABC_CONST(0x8777000087770000), "(![(ab)(cd)]e)" }, // 76
128  { 5, 8, 18, ABC_CONST(0x8777788887777888), "[(ab)(cd)e]" }, // 77
129  { 5, 6, 8, ABC_CONST(0x0666000006660000), "([ab]!(cd)e)" }, // 78
130  { 5, 6, 8, ABC_CONST(0xF9990000F9990000), "(!([ab]!(cd))e)" }, // 79
131  { 5, 8, 14, ABC_CONST(0xF9990666F9990666), "[([ab]!(cd))e]" }, // 80
132  { 5, 8, 9, ABC_CONST(0x0660000006600000), "([ab][cd]e)" }, // 81
133  { 5, 8, 9, ABC_CONST(0xF99F0000F99F0000), "(!([ab][cd])e)" }, // 82
134  { 5, 10, 16, ABC_CONST(0xF99F0660F99F0660), "[([ab][cd])e]" }, // 83
135  { 5, 5, 7, ABC_CONST(0xCAAA0000CAAA0000), "(<ab(cd)>e)" }, // 84
136  { 5, 7, 12, ABC_CONST(0x3555CAAA3555CAAA), "[<ab(cd)>e]" }, // 85
137  { 5, 7, 9, ABC_CONST(0xACCA0000ACCA0000), "(<ab[cd]>e)" }, // 86
138  { 5, 9, 16, ABC_CONST(0x5335ACCA5335ACCA), "[<ab[cd]>e]" }, // 87
139  { 5, 5, 6, ABC_CONST(0xF0880000F0880000), "(<(ab)cd>e)" }, // 88
140  { 5, 5, 6, ABC_CONST(0x0F7700000F770000), "(!<(ab)cd>e)" }, // 89
141  { 5, 7, 10, ABC_CONST(0x0F77F0880F77F088), "[<(ab)cd>e]" }, // 90
142  { 5, 7, 7, ABC_CONST(0xF0660000F0660000), "(<[ab]cd>e)" }, // 91
143  { 5, 9, 12, ABC_CONST(0x0F99F0660F99F066), "[<[ab]cd>e]" }, // 92
144  { 5, 4, 8, ABC_CONST(0x007F7F7F007F7F7F), "(!(abc)!(de))" }, // 93
145  { 5, 6, 12, ABC_CONST(0x7F8080807F808080), "[(abc)(de)]" }, // 94
146  { 5, 4, 7, ABC_CONST(0x008F8F8F008F8F8F), "(!(!(ab)c)!(de))" }, // 95
147  { 5, 6, 12, ABC_CONST(0x8F7070708F707070), "[(!(ab)c)(de)]" }, // 96
148  { 5, 6, 10, ABC_CONST(0x0078787800787878), "([(ab)c]!(de))" }, // 97
149  { 5, 6, 9, ABC_CONST(0x009F9F9F009F9F9F), "(!([ab]c)!(de))" }, // 98
150  { 5, 8, 15, ABC_CONST(0x9F6060609F606060), "[([ab]c)(de)]" }, // 99
151  { 5, 8, 13, ABC_CONST(0x0096969600969696), "([abc]!(de))" }, // 100
152  { 5, 5, 7, ABC_CONST(0x00CACACA00CACACA), "(<abc>!(de))" }, // 101
153  { 5, 7, 12, ABC_CONST(0x35CACACA35CACACA), "[<abc>(de)]" }, // 102
154  { 5, 6, 9, ABC_CONST(0x007F7F00007F7F00), "(!(abc)[de])" }, // 103
155  { 5, 6, 8, ABC_CONST(0x008F8F00008F8F00), "(!(!(ab)c)[de])" }, // 104
156  { 5, 8, 11, ABC_CONST(0x0078780000787800), "([(ab)c][de])" }, // 105
157  { 5, 8, 10, ABC_CONST(0x009F9F00009F9F00), "(!([ab]c)[de])" }, // 106
158  { 5, 10, 14, ABC_CONST(0x0096960000969600), "([abc][de])" }, // 107
159  { 5, 7, 8, ABC_CONST(0x00CACA0000CACA00), "(<abc>[de])" }, // 108
160  { 5, 5, 8, ABC_CONST(0xCAAAAAAACAAAAAAA), "<ab(cde)>" }, // 109
161  { 5, 5, 8, ABC_CONST(0xACCCAAAAACCCAAAA), "<ab(!(cd)e)>" }, // 110
162  { 5, 7, 12, ABC_CONST(0xACCCCAAAACCCCAAA), "<ab[(cd)e]>" }, // 111
163  { 5, 7, 10, ABC_CONST(0xACCAAAAAACCAAAAA), "<ab([cd]e)>" }, // 112
164  { 5, 9, 16, ABC_CONST(0xCAACACCACAACACCA), "<ab[cde]>" }, // 113
165  { 5, 6, 8, ABC_CONST(0xCCAACACACCAACACA), "<ab<cde>>" }, // 114
166  { 5, 5, 7, ABC_CONST(0xC0AAAAAAC0AAAAAA), "<a(bc)(de)>" }, // 115
167  { 5, 7, 8, ABC_CONST(0x3CAAAAAA3CAAAAAA), "<a[bc](de)>" }, // 116
168  { 5, 5, 8, ABC_CONST(0xF0888888F0888888), "<(ab)c(de)>" }, // 117
169  { 5, 7, 10, ABC_CONST(0x88F0F08888F0F088), "<(ab)c[de]>" }, // 118
170  { 5, 7, 10, ABC_CONST(0xF0666666F0666666), "<[ab]c(de)>" }, // 119
171  { 5, 9, 12, ABC_CONST(0x66F0F06666F0F066), "<[ab]c[de]>" }, // 120
172  { 5, 5, 6, ABC_CONST(0xF0008888F0008888), "<(ab)(cd)e>" }, // 121
173  { 5, 5, 6, ABC_CONST(0xF0007777F0007777), "<!(ab)(cd)e>" }, // 122
174  { 5, 7, 7, ABC_CONST(0xF0006666F0006666), "<[ab](cd)e>" }, // 123
175  { 5, 9, 8, ABC_CONST(0x0FF066660FF06666), "<[ab][cd]e>" }, // 124
176  { 5, 5, 6, ABC_CONST(0xFF008080FF008080), "<(abc)de>" }, // 125
177  { 5, 5, 6, ABC_CONST(0xFF007070FF007070), "<(!(ab)c)de>" }, // 126
178  { 5, 7, 8, ABC_CONST(0xFF007878FF007878), "<[(ab)c]de>" }, // 127
179  { 5, 7, 7, ABC_CONST(0xFF006060FF006060), "<([ab]c)de>" }, // 128
180  { 5, 9, 10, ABC_CONST(0xFF009696FF009696), "<[abc]de>" }, // 129
181  { 5, 6, 6, ABC_CONST(0xFF00CACAFF00CACA), "<<abc>de>" }, // 130
182  { 6, 5, 7, ABC_CONST(0x8000000000000000), "(abcdef)" }, // 131
183  { 6, 5, 7, ABC_CONST(0x7FFFFFFF00000000), "(!(abcde)f)" }, // 132
184  { 6, 7, 12, ABC_CONST(0x7FFFFFFF80000000), "[(abcde)f]" }, // 133
185  { 6, 5, 7, ABC_CONST(0x7FFF000000000000), "(!(abcd)ef)" }, // 134
186  { 6, 5, 7, ABC_CONST(0x8000FFFF00000000), "(!(!(abcd)e)f)" }, // 135
187  { 6, 7, 12, ABC_CONST(0x8000FFFF7FFF0000), "[(!(abcd)e)f]" }, // 136
188  { 6, 7, 11, ABC_CONST(0x7FFF800000000000), "([(abcd)e]f)" }, // 137
189  { 6, 9, 20, ABC_CONST(0x80007FFF7FFF8000), "[(abcd)ef]" }, // 138
190  { 6, 5, 7, ABC_CONST(0x7F00000000000000), "(!(abc)def)" }, // 139
191  { 6, 5, 7, ABC_CONST(0x80FFFFFF00000000), "(!(!(abc)de)f)" }, // 140
192  { 6, 7, 12, ABC_CONST(0x80FFFFFF7F000000), "[(!(abc)de)f]" }, // 141
193  { 6, 5, 7, ABC_CONST(0x80FF000000000000), "(!(!(abc)d)ef)" }, // 142
194  { 6, 5, 7, ABC_CONST(0x7F00FFFF00000000), "(!(!(!(abc)d)e)f)" }, // 143
195  { 6, 7, 12, ABC_CONST(0x7F00FFFF80FF0000), "[(!(!(abc)d)e)f]" }, // 144
196  { 6, 7, 11, ABC_CONST(0x80FF7F0000000000), "([(!(abc)d)e]f)" }, // 145
197  { 6, 9, 20, ABC_CONST(0x7F0080FF80FF7F00), "[(!(abc)d)ef]" }, // 146
198  { 6, 7, 10, ABC_CONST(0x7F80000000000000), "([(abc)d]ef)" }, // 147
199  { 6, 7, 10, ABC_CONST(0x807FFFFF00000000), "(!([(abc)d]e)f)" }, // 148
200  { 6, 9, 18, ABC_CONST(0x807FFFFF7F800000), "[([(abc)d]e)f]" }, // 149
201  { 6, 9, 17, ABC_CONST(0x807F7F8000000000), "([(abc)de]f)" }, // 150
202  { 6, 11, 32, ABC_CONST(0x7F80807F807F7F80), "[(abc)def]" }, // 151
203  { 6, 5, 7, ABC_CONST(0x7000000000000000), "(!(ab)cdef)" }, // 152
204  { 6, 5, 7, ABC_CONST(0x8FFFFFFF00000000), "(!(!(ab)cde)f)" }, // 153
205  { 6, 7, 12, ABC_CONST(0x8FFFFFFF70000000), "[(!(ab)cde)f]" }, // 154
206  { 6, 5, 7, ABC_CONST(0x8FFF000000000000), "(!(!(ab)cd)ef)" }, // 155
207  { 6, 5, 7, ABC_CONST(0x7000FFFF00000000), "(!(!(!(ab)cd)e)f)" }, // 156
208  { 6, 7, 12, ABC_CONST(0x7000FFFF8FFF0000), "[(!(!(ab)cd)e)f]" }, // 157
209  { 6, 7, 11, ABC_CONST(0x8FFF700000000000), "([(!(ab)cd)e]f)" }, // 158
210  { 6, 9, 20, ABC_CONST(0x70008FFF8FFF7000), "[(!(ab)cd)ef]" }, // 159
211  { 6, 5, 7, ABC_CONST(0x8F00000000000000), "(!(!(ab)c)def)" }, // 160
212  { 6, 5, 7, ABC_CONST(0x70FFFFFF00000000), "(!(!(!(ab)c)de)f)" }, // 161
213  { 6, 7, 12, ABC_CONST(0x70FFFFFF8F000000), "[(!(!(ab)c)de)f]" }, // 162
214  { 6, 5, 7, ABC_CONST(0x70FF000000000000), "(!(!(!(ab)c)d)ef)" }, // 163
215  { 6, 5, 7, ABC_CONST(0x8F00FFFF00000000), "(!(!(!(!(ab)c)d)e)f)" }, // 164
216  { 6, 7, 12, ABC_CONST(0x8F00FFFF70FF0000), "[(!(!(!(ab)c)d)e)f]" }, // 165
217  { 6, 7, 11, ABC_CONST(0x70FF8F0000000000), "([(!(!(ab)c)d)e]f)" }, // 166
218  { 6, 9, 20, ABC_CONST(0x8F0070FF70FF8F00), "[(!(!(ab)c)d)ef]" }, // 167
219  { 6, 7, 10, ABC_CONST(0x8F70000000000000), "([(!(ab)c)d]ef)" }, // 168
220  { 6, 7, 10, ABC_CONST(0x708FFFFF00000000), "(!([(!(ab)c)d]e)f)" }, // 169
221  { 6, 9, 18, ABC_CONST(0x708FFFFF8F700000), "[([(!(ab)c)d]e)f]" }, // 170
222  { 6, 9, 17, ABC_CONST(0x708F8F7000000000), "([(!(ab)c)de]f)" }, // 171
223  { 6, 11, 32, ABC_CONST(0x8F70708F708F8F70), "[(!(ab)c)def]" }, // 172
224  { 6, 7, 9, ABC_CONST(0x7800000000000000), "([(ab)c]def)" }, // 173
225  { 6, 7, 9, ABC_CONST(0x87FFFFFF00000000), "(!([(ab)c]de)f)" }, // 174
226  { 6, 9, 16, ABC_CONST(0x87FFFFFF78000000), "[([(ab)c]de)f]" }, // 175
227  { 6, 7, 9, ABC_CONST(0x87FF000000000000), "(!([(ab)c]d)ef)" }, // 176
228  { 6, 7, 9, ABC_CONST(0x7800FFFF00000000), "(!(!([(ab)c]d)e)f)" }, // 177
229  { 6, 9, 16, ABC_CONST(0x7800FFFF87FF0000), "[(!([(ab)c]d)e)f]" }, // 178
230  { 6, 9, 15, ABC_CONST(0x87FF780000000000), "([([(ab)c]d)e]f)" }, // 179
231  { 6, 11, 28, ABC_CONST(0x780087FF87FF7800), "[([(ab)c]d)ef]" }, // 180
232  { 6, 9, 14, ABC_CONST(0x8778000000000000), "([(ab)cd]ef)" }, // 181
233  { 6, 9, 14, ABC_CONST(0x7887FFFF00000000), "(!([(ab)cd]e)f)" }, // 182
234  { 6, 11, 26, ABC_CONST(0x7887FFFF87780000), "[([(ab)cd]e)f]" }, // 183
235  { 6, 11, 25, ABC_CONST(0x7887877800000000), "([(ab)cde]f)" }, // 184
236  { 6, 13, 48, ABC_CONST(0x8778788778878778), "[(ab)cdef]" }, // 185
237  { 6, 7, 8, ABC_CONST(0x6000000000000000), "([ab]cdef)" }, // 186
238  { 6, 7, 8, ABC_CONST(0x9FFFFFFF00000000), "(!([ab]cde)f)" }, // 187
239  { 6, 9, 14, ABC_CONST(0x9FFFFFFF60000000), "[([ab]cde)f]" }, // 188
240  { 6, 7, 8, ABC_CONST(0x9FFF000000000000), "(!([ab]cd)ef)" }, // 189
241  { 6, 7, 8, ABC_CONST(0x6000FFFF00000000), "(!(!([ab]cd)e)f)" }, // 190
242  { 6, 9, 14, ABC_CONST(0x6000FFFF9FFF0000), "[(!([ab]cd)e)f]" }, // 191
243  { 6, 9, 13, ABC_CONST(0x9FFF600000000000), "([([ab]cd)e]f)" }, // 192
244  { 6, 11, 24, ABC_CONST(0x60009FFF9FFF6000), "[([ab]cd)ef]" }, // 193
245  { 6, 7, 8, ABC_CONST(0x9F00000000000000), "(!([ab]c)def)" }, // 194
246  { 6, 7, 8, ABC_CONST(0x60FFFFFF00000000), "(!(!([ab]c)de)f)" }, // 195
247  { 6, 9, 14, ABC_CONST(0x60FFFFFF9F000000), "[(!([ab]c)de)f]" }, // 196
248  { 6, 7, 8, ABC_CONST(0x60FF000000000000), "(!(!([ab]c)d)ef)" }, // 197
249  { 6, 7, 8, ABC_CONST(0x9F00FFFF00000000), "(!(!(!([ab]c)d)e)f)" }, // 198
250  { 6, 9, 14, ABC_CONST(0x9F00FFFF60FF0000), "[(!(!([ab]c)d)e)f]" }, // 199
251  { 6, 9, 13, ABC_CONST(0x60FF9F0000000000), "([(!([ab]c)d)e]f)" }, // 200
252  { 6, 11, 24, ABC_CONST(0x9F0060FF60FF9F00), "[(!([ab]c)d)ef]" }, // 201
253  { 6, 9, 12, ABC_CONST(0x9F60000000000000), "([([ab]c)d]ef)" }, // 202
254  { 6, 9, 12, ABC_CONST(0x609FFFFF00000000), "(!([([ab]c)d]e)f)" }, // 203
255  { 6, 11, 22, ABC_CONST(0x609FFFFF9F600000), "[([([ab]c)d]e)f]" }, // 204
256  { 6, 11, 21, ABC_CONST(0x609F9F6000000000), "([([ab]c)de]f)" }, // 205
257  { 6, 13, 40, ABC_CONST(0x9F60609F609F9F60), "[([ab]c)def]" }, // 206
258  { 6, 9, 11, ABC_CONST(0x9600000000000000), "([abc]def)" }, // 207
259  { 6, 9, 11, ABC_CONST(0x69FFFFFF00000000), "(!([abc]de)f)" }, // 208
260  { 6, 11, 20, ABC_CONST(0x69FFFFFF96000000), "[([abc]de)f]" }, // 209
261  { 6, 9, 11, ABC_CONST(0x69FF000000000000), "(!([abc]d)ef)" }, // 210
262  { 6, 9, 11, ABC_CONST(0x9600FFFF00000000), "(!(!([abc]d)e)f)" }, // 211
263  { 6, 11, 20, ABC_CONST(0x9600FFFF69FF0000), "[(!([abc]d)e)f]" }, // 212
264  { 6, 11, 19, ABC_CONST(0x69FF960000000000), "([([abc]d)e]f)" }, // 213
265  { 6, 13, 36, ABC_CONST(0x960069FF69FF9600), "[([abc]d)ef]" }, // 214
266  { 6, 11, 18, ABC_CONST(0x6996000000000000), "([abcd]ef)" }, // 215
267  { 6, 11, 18, ABC_CONST(0x9669FFFF00000000), "(!([abcd]e)f)" }, // 216
268  { 6, 13, 34, ABC_CONST(0x9669FFFF69960000), "[([abcd]e)f]" }, // 217
269  { 6, 13, 33, ABC_CONST(0x9669699600000000), "([abcde]f)" }, // 218
270  { 6, 15, 64, ABC_CONST(0x6996966996696996), "[abcdef]" }, // 219
271  { 6, 6, 7, ABC_CONST(0xCA00000000000000), "(<abc>def)" }, // 220
272  { 6, 6, 7, ABC_CONST(0x35FFFFFF00000000), "(!(<abc>de)f)" }, // 221
273  { 6, 8, 12, ABC_CONST(0x35FFFFFFCA000000), "[(<abc>de)f]" }, // 222
274  { 6, 6, 7, ABC_CONST(0x35FF000000000000), "(!(<abc>d)ef)" }, // 223
275  { 6, 6, 7, ABC_CONST(0xCA00FFFF00000000), "(!(!(<abc>d)e)f)" }, // 224
276  { 6, 8, 12, ABC_CONST(0xCA00FFFF35FF0000), "[(!(<abc>d)e)f]" }, // 225
277  { 6, 8, 11, ABC_CONST(0x35FFCA0000000000), "([(<abc>d)e]f)" }, // 226
278  { 6, 10, 20, ABC_CONST(0xCA0035FF35FFCA00), "[(<abc>d)ef]" }, // 227
279  { 6, 8, 10, ABC_CONST(0x35CA000000000000), "([<abc>d]ef)" }, // 228
280  { 6, 8, 10, ABC_CONST(0xCA35FFFF00000000), "(!([<abc>d]e)f)" }, // 229
281  { 6, 10, 18, ABC_CONST(0xCA35FFFF35CA0000), "[([<abc>d]e)f]" }, // 230
282  { 6, 10, 17, ABC_CONST(0xCA3535CA00000000), "([<abc>de]f)" }, // 231
283  { 6, 12, 32, ABC_CONST(0x35CACA35CA3535CA), "[<abc>def]" }, // 232
284  { 6, 5, 8, ABC_CONST(0x0777000000000000), "(!(ab)!(cd)ef)" }, // 233
285  { 6, 5, 8, ABC_CONST(0xF888FFFF00000000), "(!(!(ab)!(cd)e)f)" }, // 234
286  { 6, 7, 14, ABC_CONST(0xF888FFFF07770000), "[(!(ab)!(cd)e)f]" }, // 235
287  { 6, 5, 8, ABC_CONST(0xF888000000000000), "(!(!(ab)!(cd))ef)" }, // 236
288  { 6, 5, 8, ABC_CONST(0x0777FFFF00000000), "(!(!(!(ab)!(cd))e)f)" }, // 237
289  { 6, 7, 14, ABC_CONST(0x0777FFFFF8880000), "[(!(!(ab)!(cd))e)f]" }, // 238
290  { 6, 7, 13, ABC_CONST(0xF888077700000000), "([(!(ab)!(cd))e]f)" }, // 239
291  { 6, 9, 24, ABC_CONST(0x0777F888F8880777), "[(!(ab)!(cd))ef]" }, // 240
292  { 6, 7, 11, ABC_CONST(0x7888000000000000), "([(ab)(cd)]ef)" }, // 241
293  { 6, 7, 11, ABC_CONST(0x8777FFFF00000000), "(!([(ab)(cd)]e)f)" }, // 242
294  { 6, 9, 20, ABC_CONST(0x8777FFFF78880000), "[([(ab)(cd)]e)f]" }, // 243
295  { 6, 7, 11, ABC_CONST(0x8777000000000000), "(![(ab)(cd)]ef)" }, // 244
296  { 6, 7, 11, ABC_CONST(0x7888FFFF00000000), "(!(![(ab)(cd)]e)f)" }, // 245
297  { 6, 9, 20, ABC_CONST(0x7888FFFF87770000), "[(![(ab)(cd)]e)f]" }, // 246
298  { 6, 9, 19, ABC_CONST(0x8777788800000000), "([(ab)(cd)e]f)" }, // 247
299  { 6, 11, 36, ABC_CONST(0x7888877787777888), "[(ab)(cd)ef]" }, // 248
300  { 6, 7, 9, ABC_CONST(0x0666000000000000), "([ab]!(cd)ef)" }, // 249
301  { 6, 7, 9, ABC_CONST(0xF999FFFF00000000), "(!([ab]!(cd)e)f)" }, // 250
302  { 6, 9, 16, ABC_CONST(0xF999FFFF06660000), "[([ab]!(cd)e)f]" }, // 251
303  { 6, 7, 9, ABC_CONST(0xF999000000000000), "(!([ab]!(cd))ef)" }, // 252
304  { 6, 7, 9, ABC_CONST(0x0666FFFF00000000), "(!(!([ab]!(cd))e)f)" }, // 253
305  { 6, 9, 16, ABC_CONST(0x0666FFFFF9990000), "[(!([ab]!(cd))e)f]" }, // 254
306  { 6, 9, 15, ABC_CONST(0xF999066600000000), "([([ab]!(cd))e]f)" }, // 255
307  { 6, 11, 28, ABC_CONST(0x0666F999F9990666), "[([ab]!(cd))ef]" }, // 256
308  { 6, 9, 10, ABC_CONST(0x0660000000000000), "([ab][cd]ef)" }, // 257
309  { 6, 9, 10, ABC_CONST(0xF99FFFFF00000000), "(!([ab][cd]e)f)" }, // 258
310  { 6, 11, 18, ABC_CONST(0xF99FFFFF06600000), "[([ab][cd]e)f]" }, // 259
311  { 6, 9, 10, ABC_CONST(0xF99F000000000000), "(!([ab][cd])ef)" }, // 260
312  { 6, 9, 10, ABC_CONST(0x0660FFFF00000000), "(!(!([ab][cd])e)f)" }, // 261
313  { 6, 11, 18, ABC_CONST(0x0660FFFFF99F0000), "[(!([ab][cd])e)f]" }, // 262
314  { 6, 11, 17, ABC_CONST(0xF99F066000000000), "([([ab][cd])e]f)" }, // 263
315  { 6, 13, 32, ABC_CONST(0x0660F99FF99F0660), "[([ab][cd])ef]" }, // 264
316  { 6, 6, 8, ABC_CONST(0xCAAA000000000000), "(<ab(cd)>ef)" }, // 265
317  { 6, 6, 8, ABC_CONST(0x3555FFFF00000000), "(!(<ab(cd)>e)f)" }, // 266
318  { 6, 8, 14, ABC_CONST(0x3555FFFFCAAA0000), "[(<ab(cd)>e)f]" }, // 267
319  { 6, 8, 13, ABC_CONST(0x3555CAAA00000000), "([<ab(cd)>e]f)" }, // 268
320  { 6, 10, 24, ABC_CONST(0xCAAA35553555CAAA), "[<ab(cd)>ef]" }, // 269
321  { 6, 8, 10, ABC_CONST(0xACCA000000000000), "(<ab[cd]>ef)" }, // 270
322  { 6, 8, 10, ABC_CONST(0x5335FFFF00000000), "(!(<ab[cd]>e)f)" }, // 271
323  { 6, 10, 18, ABC_CONST(0x5335FFFFACCA0000), "[(<ab[cd]>e)f]" }, // 272
324  { 6, 10, 17, ABC_CONST(0x5335ACCA00000000), "([<ab[cd]>e]f)" }, // 273
325  { 6, 12, 32, ABC_CONST(0xACCA53355335ACCA), "[<ab[cd]>ef]" }, // 274
326  { 6, 6, 7, ABC_CONST(0xF088000000000000), "(<(ab)cd>ef)" }, // 275
327  { 6, 6, 7, ABC_CONST(0x0F77FFFF00000000), "(!(<(ab)cd>e)f)" }, // 276
328  { 6, 8, 12, ABC_CONST(0x0F77FFFFF0880000), "[(<(ab)cd>e)f]" }, // 277
329  { 6, 6, 7, ABC_CONST(0x0F77000000000000), "(!<(ab)cd>ef)" }, // 278
330  { 6, 6, 7, ABC_CONST(0xF088FFFF00000000), "(!(!<(ab)cd>e)f)" }, // 279
331  { 6, 8, 12, ABC_CONST(0xF088FFFF0F770000), "[(!<(ab)cd>e)f]" }, // 280
332  { 6, 8, 11, ABC_CONST(0x0F77F08800000000), "([<(ab)cd>e]f)" }, // 281
333  { 6, 10, 20, ABC_CONST(0xF0880F770F77F088), "[<(ab)cd>ef]" }, // 282
334  { 6, 8, 8, ABC_CONST(0xF066000000000000), "(<[ab]cd>ef)" }, // 283
335  { 6, 8, 8, ABC_CONST(0x0F99FFFF00000000), "(!(<[ab]cd>e)f)" }, // 284
336  { 6, 10, 14, ABC_CONST(0x0F99FFFFF0660000), "[(<[ab]cd>e)f]" }, // 285
337  { 6, 10, 13, ABC_CONST(0x0F99F06600000000), "([<[ab]cd>e]f)" }, // 286
338  { 6, 12, 24, ABC_CONST(0xF0660F990F99F066), "[<[ab]cd>ef]" }, // 287
339  { 6, 5, 9, ABC_CONST(0x007F7F7F00000000), "(!(abc)!(de)f)" }, // 288
340  { 6, 5, 9, ABC_CONST(0xFF80808000000000), "(!(!(abc)!(de))f)" }, // 289
341  { 6, 7, 16, ABC_CONST(0xFF808080007F7F7F), "[(!(abc)!(de))f]" }, // 290
342  { 6, 7, 13, ABC_CONST(0x7F80808000000000), "([(abc)(de)]f)" }, // 291
343  { 6, 7, 13, ABC_CONST(0x807F7F7F00000000), "(![(abc)(de)]f)" }, // 292
344  { 6, 9, 24, ABC_CONST(0x807F7F7F7F808080), "[(abc)(de)f]" }, // 293
345  { 6, 5, 8, ABC_CONST(0x008F8F8F00000000), "(!(!(ab)c)!(de)f)" }, // 294
346  { 6, 5, 8, ABC_CONST(0xFF70707000000000), "(!(!(!(ab)c)!(de))f)" }, // 295
347  { 6, 7, 14, ABC_CONST(0xFF707070008F8F8F), "[(!(!(ab)c)!(de))f]" }, // 296
348  { 6, 7, 13, ABC_CONST(0x8F70707000000000), "([(!(ab)c)(de)]f)" }, // 297
349  { 6, 7, 13, ABC_CONST(0x708F8F8F00000000), "(![(!(ab)c)(de)]f)" }, // 298
350  { 6, 9, 24, ABC_CONST(0x708F8F8F8F707070), "[(!(ab)c)(de)f]" }, // 299
351  { 6, 7, 11, ABC_CONST(0x0078787800000000), "([(ab)c]!(de)f)" }, // 300
352  { 6, 7, 11, ABC_CONST(0xFF87878700000000), "(!([(ab)c]!(de))f)" }, // 301
353  { 6, 9, 20, ABC_CONST(0xFF87878700787878), "[([(ab)c]!(de))f]" }, // 302
354  { 6, 7, 10, ABC_CONST(0x009F9F9F00000000), "(!([ab]c)!(de)f)" }, // 303
355  { 6, 7, 10, ABC_CONST(0xFF60606000000000), "(!(!([ab]c)!(de))f)" }, // 304
356  { 6, 9, 18, ABC_CONST(0xFF606060009F9F9F), "[(!([ab]c)!(de))f]" }, // 305
357  { 6, 9, 16, ABC_CONST(0x9F60606000000000), "([([ab]c)(de)]f)" }, // 306
358  { 6, 9, 16, ABC_CONST(0x609F9F9F00000000), "(![([ab]c)(de)]f)" }, // 307
359  { 6, 11, 30, ABC_CONST(0x609F9F9F9F606060), "[([ab]c)(de)f]" }, // 308
360  { 6, 9, 14, ABC_CONST(0x0096969600000000), "([abc]!(de)f)" }, // 309
361  { 6, 9, 14, ABC_CONST(0xFF69696900000000), "(!([abc]!(de))f)" }, // 310
362  { 6, 11, 26, ABC_CONST(0xFF69696900969696), "[([abc]!(de))f]" }, // 311
363  { 6, 6, 8, ABC_CONST(0x00CACACA00000000), "(<abc>!(de)f)" }, // 312
364  { 6, 6, 8, ABC_CONST(0xFF35353500000000), "(!(<abc>!(de))f)" }, // 313
365  { 6, 8, 14, ABC_CONST(0xFF35353500CACACA), "[(<abc>!(de))f]" }, // 314
366  { 6, 8, 13, ABC_CONST(0x35CACACA00000000), "([<abc>(de)]f)" }, // 315
367  { 6, 10, 24, ABC_CONST(0xCA35353535CACACA), "[<abc>(de)f]" }, // 316
368  { 6, 7, 10, ABC_CONST(0x007F7F0000000000), "(!(abc)[de]f)" }, // 317
369  { 6, 7, 10, ABC_CONST(0xFF8080FF00000000), "(!(!(abc)[de])f)" }, // 318
370  { 6, 9, 18, ABC_CONST(0xFF8080FF007F7F00), "[(!(abc)[de])f]" }, // 319
371  { 6, 7, 9, ABC_CONST(0x008F8F0000000000), "(!(!(ab)c)[de]f)" }, // 320
372  { 6, 7, 9, ABC_CONST(0xFF7070FF00000000), "(!(!(!(ab)c)[de])f)" }, // 321
373  { 6, 9, 16, ABC_CONST(0xFF7070FF008F8F00), "[(!(!(ab)c)[de])f]" }, // 322
374  { 6, 9, 12, ABC_CONST(0x0078780000000000), "([(ab)c][de]f)" }, // 323
375  { 6, 9, 12, ABC_CONST(0xFF8787FF00000000), "(!([(ab)c][de])f)" }, // 324
376  { 6, 11, 22, ABC_CONST(0xFF8787FF00787800), "[([(ab)c][de])f]" }, // 325
377  { 6, 9, 11, ABC_CONST(0x009F9F0000000000), "(!([ab]c)[de]f)" }, // 326
378  { 6, 9, 11, ABC_CONST(0xFF6060FF00000000), "(!(!([ab]c)[de])f)" }, // 327
379  { 6, 11, 20, ABC_CONST(0xFF6060FF009F9F00), "[(!([ab]c)[de])f]" }, // 328
380  { 6, 11, 15, ABC_CONST(0x0096960000000000), "([abc][de]f)" }, // 329
381  { 6, 11, 15, ABC_CONST(0xFF6969FF00000000), "(!([abc][de])f)" }, // 330
382  { 6, 13, 28, ABC_CONST(0xFF6969FF00969600), "[([abc][de])f]" }, // 331
383  { 6, 8, 9, ABC_CONST(0x00CACA0000000000), "(<abc>[de]f)" }, // 332
384  { 6, 8, 9, ABC_CONST(0xFF3535FF00000000), "(!(<abc>[de])f)" }, // 333
385  { 6, 10, 16, ABC_CONST(0xFF3535FF00CACA00), "[(<abc>[de])f]" }, // 334
386  { 6, 6, 9, ABC_CONST(0xCAAAAAAA00000000), "(<ab(cde)>f)" }, // 335
387  { 6, 8, 16, ABC_CONST(0x35555555CAAAAAAA), "[<ab(cde)>f]" }, // 336
388  { 6, 6, 9, ABC_CONST(0xACCCAAAA00000000), "(<ab(!(cd)e)>f)" }, // 337
389  { 6, 8, 16, ABC_CONST(0x53335555ACCCAAAA), "[<ab(!(cd)e)>f]" }, // 338
390  { 6, 8, 13, ABC_CONST(0xACCCCAAA00000000), "(<ab[(cd)e]>f)" }, // 339
391  { 6, 10, 24, ABC_CONST(0x53333555ACCCCAAA), "[<ab[(cd)e]>f]" }, // 340
392  { 6, 8, 11, ABC_CONST(0xACCAAAAA00000000), "(<ab([cd]e)>f)" }, // 341
393  { 6, 10, 20, ABC_CONST(0x53355555ACCAAAAA), "[<ab([cd]e)>f]" }, // 342
394  { 6, 10, 17, ABC_CONST(0xCAACACCA00000000), "(<ab[cde]>f)" }, // 343
395  { 6, 12, 32, ABC_CONST(0x35535335CAACACCA), "[<ab[cde]>f]" }, // 344
396  { 6, 7, 9, ABC_CONST(0xCCAACACA00000000), "(<ab<cde>>f)" }, // 345
397  { 6, 9, 16, ABC_CONST(0x33553535CCAACACA), "[<ab<cde>>f]" }, // 346
398  { 6, 6, 8, ABC_CONST(0xC0AAAAAA00000000), "(<a(bc)(de)>f)" }, // 347
399  { 6, 6, 8, ABC_CONST(0x3F55555500000000), "(!<a(bc)(de)>f)" }, // 348
400  { 6, 8, 14, ABC_CONST(0x3F555555C0AAAAAA), "[<a(bc)(de)>f]" }, // 349
401  { 6, 8, 9, ABC_CONST(0x3CAAAAAA00000000), "(<a[bc](de)>f)" }, // 350
402  { 6, 10, 16, ABC_CONST(0xC35555553CAAAAAA), "[<a[bc](de)>f]" }, // 351
403  { 6, 6, 9, ABC_CONST(0xF088888800000000), "(<(ab)c(de)>f)" }, // 352
404  { 6, 6, 9, ABC_CONST(0x0F77777700000000), "(!<(ab)c(de)>f)" }, // 353
405  { 6, 8, 16, ABC_CONST(0x0F777777F0888888), "[<(ab)c(de)>f]" }, // 354
406  { 6, 8, 11, ABC_CONST(0x88F0F08800000000), "(<(ab)c[de]>f)" }, // 355
407  { 6, 8, 11, ABC_CONST(0x770F0F7700000000), "(!<(ab)c[de]>f)" }, // 356
408  { 6, 10, 20, ABC_CONST(0x770F0F7788F0F088), "[<(ab)c[de]>f]" }, // 357
409  { 6, 8, 11, ABC_CONST(0xF066666600000000), "(<[ab]c(de)>f)" }, // 358
410  { 6, 10, 20, ABC_CONST(0x0F999999F0666666), "[<[ab]c(de)>f]" }, // 359
411  { 6, 10, 13, ABC_CONST(0x66F0F06600000000), "(<[ab]c[de]>f)" }, // 360
412  { 6, 12, 24, ABC_CONST(0x990F0F9966F0F066), "[<[ab]c[de]>f]" }, // 361
413  { 6, 6, 7, ABC_CONST(0xF000888800000000), "(<(ab)(cd)e>f)" }, // 362
414  { 6, 6, 7, ABC_CONST(0x0FFF777700000000), "(!<(ab)(cd)e>f)" }, // 363
415  { 6, 8, 12, ABC_CONST(0x0FFF7777F0008888), "[<(ab)(cd)e>f]" }, // 364
416  { 6, 6, 7, ABC_CONST(0xF000777700000000), "(<!(ab)(cd)e>f)" }, // 365
417  { 6, 8, 12, ABC_CONST(0x0FFF8888F0007777), "[<!(ab)(cd)e>f]" }, // 366
418  { 6, 8, 8, ABC_CONST(0xF000666600000000), "(<[ab](cd)e>f)" }, // 367
419  { 6, 8, 8, ABC_CONST(0x0FFF999900000000), "(!<[ab](cd)e>f)" }, // 368
420  { 6, 10, 14, ABC_CONST(0x0FFF9999F0006666), "[<[ab](cd)e>f]" }, // 369
421  { 6, 10, 9, ABC_CONST(0x0FF0666600000000), "(<[ab][cd]e>f)" }, // 370
422  { 6, 12, 16, ABC_CONST(0xF00F99990FF06666), "[<[ab][cd]e>f]" }, // 371
423  { 6, 6, 7, ABC_CONST(0xFF00808000000000), "(<(abc)de>f)" }, // 372
424  { 6, 6, 7, ABC_CONST(0x00FF7F7F00000000), "(!<(abc)de>f)" }, // 373
425  { 6, 8, 12, ABC_CONST(0x00FF7F7FFF008080), "[<(abc)de>f]" }, // 374
426  { 6, 6, 7, ABC_CONST(0xFF00707000000000), "(<(!(ab)c)de>f)" }, // 375
427  { 6, 6, 7, ABC_CONST(0x00FF8F8F00000000), "(!<(!(ab)c)de>f)" }, // 376
428  { 6, 8, 12, ABC_CONST(0x00FF8F8FFF007070), "[<(!(ab)c)de>f]" }, // 377
429  { 6, 8, 9, ABC_CONST(0xFF00787800000000), "(<[(ab)c]de>f)" }, // 378
430  { 6, 10, 16, ABC_CONST(0x00FF8787FF007878), "[<[(ab)c]de>f]" }, // 379
431  { 6, 8, 8, ABC_CONST(0xFF00606000000000), "(<([ab]c)de>f)" }, // 380
432  { 6, 8, 8, ABC_CONST(0x00FF9F9F00000000), "(!<([ab]c)de>f)" }, // 381
433  { 6, 10, 14, ABC_CONST(0x00FF9F9FFF006060), "[<([ab]c)de>f]" }, // 382
434  { 6, 10, 11, ABC_CONST(0xFF00969600000000), "(<[abc]de>f)" }, // 383
435  { 6, 12, 20, ABC_CONST(0x00FF6969FF009696), "[<[abc]de>f]" }, // 384
436  { 6, 7, 7, ABC_CONST(0xFF00CACA00000000), "(<<abc>de>f)" }, // 385
437  { 6, 9, 12, ABC_CONST(0x00FF3535FF00CACA), "[<<abc>de>f]" }, // 386
438  { 6, 5, 10, ABC_CONST(0x00007FFF7FFF7FFF), "(!(abcd)!(ef))" }, // 387
439  { 6, 7, 15, ABC_CONST(0x7FFF800080008000), "[(abcd)(ef)]" }, // 388
440  { 6, 5, 8, ABC_CONST(0x000080FF80FF80FF), "(!(!(abc)d)!(ef))" }, // 389
441  { 6, 7, 15, ABC_CONST(0x80FF7F007F007F00), "[(!(abc)d)(ef)]" }, // 390
442  { 6, 7, 13, ABC_CONST(0x00007F807F807F80), "([(abc)d]!(ef))" }, // 391
443  { 6, 5, 9, ABC_CONST(0x00008FFF8FFF8FFF), "(!(!(ab)cd)!(ef))" }, // 392
444  { 6, 7, 15, ABC_CONST(0x8FFF700070007000), "[(!(ab)cd)(ef)]" }, // 393
445  { 6, 5, 9, ABC_CONST(0x000070FF70FF70FF), "(!(!(!(ab)c)d)!(ef))" }, // 394
446  { 6, 7, 15, ABC_CONST(0x70FF8F008F008F00), "[(!(!(ab)c)d)(ef)]" }, // 395
447  { 6, 7, 13, ABC_CONST(0x00008F708F708F70), "([(!(ab)c)d]!(ef))" }, // 396
448  { 6, 7, 12, ABC_CONST(0x000087FF87FF87FF), "(!([(ab)c]d)!(ef))" }, // 397
449  { 6, 9, 21, ABC_CONST(0x87FF780078007800), "[([(ab)c]d)(ef)]" }, // 398
450  { 6, 9, 19, ABC_CONST(0x0000877887788778), "([(ab)cd]!(ef))" }, // 399
451  { 6, 7, 11, ABC_CONST(0x00009FFF9FFF9FFF), "(!([ab]cd)!(ef))" }, // 400
452  { 6, 9, 18, ABC_CONST(0x9FFF600060006000), "[([ab]cd)(ef)]" }, // 401
453  { 6, 7, 10, ABC_CONST(0x000060FF60FF60FF), "(!(!([ab]c)d)!(ef))" }, // 402
454  { 6, 9, 18, ABC_CONST(0x60FF9F009F009F00), "[(!([ab]c)d)(ef)]" }, // 403
455  { 6, 9, 16, ABC_CONST(0x00009F609F609F60), "([([ab]c)d]!(ef))" }, // 404
456  { 6, 9, 15, ABC_CONST(0x000069FF69FF69FF), "(!([abc]d)!(ef))" }, // 405
457  { 6, 11, 27, ABC_CONST(0x69FF960096009600), "[([abc]d)(ef)]" }, // 406
458  { 6, 11, 25, ABC_CONST(0x0000699669966996), "([abcd]!(ef))" }, // 407
459  { 6, 6, 9, ABC_CONST(0x000035FF35FF35FF), "(!(<abc>d)!(ef))" }, // 408
460  { 6, 8, 15, ABC_CONST(0x35FFCA00CA00CA00), "[(<abc>d)(ef)]" }, // 409
461  { 6, 8, 13, ABC_CONST(0x000035CA35CA35CA), "([<abc>d]!(ef))" }, // 410
462  { 6, 5, 11, ABC_CONST(0x0000077707770777), "(!(ab)!(cd)!(ef))" }, // 411
463  { 6, 5, 9, ABC_CONST(0x0000F888F888F888), "(!(!(ab)!(cd))!(ef))" }, // 412
464  { 6, 7, 18, ABC_CONST(0xF888077707770777), "[(!(ab)!(cd))(ef)]" }, // 413
465  { 6, 7, 14, ABC_CONST(0x0000788878887888), "([(ab)(cd)]!(ef))" }, // 414
466  { 6, 7, 15, ABC_CONST(0x0000877787778777), "(![(ab)(cd)]!(ef))" }, // 415
467  { 6, 9, 27, ABC_CONST(0x8777788878887888), "[(ab)(cd)(ef)]" }, // 416
468  { 6, 7, 12, ABC_CONST(0x0000066606660666), "([ab]!(cd)!(ef))" }, // 417
469  { 6, 7, 11, ABC_CONST(0x0000F999F999F999), "(!([ab]!(cd))!(ef))" }, // 418
470  { 6, 9, 21, ABC_CONST(0xF999066606660666), "[([ab]!(cd))(ef)]" }, // 419
471  { 6, 9, 13, ABC_CONST(0x0000066006600660), "([ab][cd]!(ef))" }, // 420
472  { 6, 9, 13, ABC_CONST(0x0000F99FF99FF99F), "(!([ab][cd])!(ef))" }, // 421
473  { 6, 11, 24, ABC_CONST(0xF99F066006600660), "[([ab][cd])(ef)]" }, // 422
474  { 6, 6, 10, ABC_CONST(0x0000CAAACAAACAAA), "(<ab(cd)>!(ef))" }, // 423
475  { 6, 8, 18, ABC_CONST(0x3555CAAACAAACAAA), "[<ab(cd)>(ef)]" }, // 424
476  { 6, 8, 13, ABC_CONST(0x0000ACCAACCAACCA), "(<ab[cd]>!(ef))" }, // 425
477  { 6, 10, 24, ABC_CONST(0x5335ACCAACCAACCA), "[<ab[cd]>(ef)]" }, // 426
478  { 6, 6, 8, ABC_CONST(0x0000F088F088F088), "(<(ab)cd>!(ef))" }, // 427
479  { 6, 6, 9, ABC_CONST(0x00000F770F770F77), "(!<(ab)cd>!(ef))" }, // 428
480  { 6, 8, 15, ABC_CONST(0x0F77F088F088F088), "[<(ab)cd>(ef)]" }, // 429
481  { 6, 8, 10, ABC_CONST(0x0000F066F066F066), "(<[ab]cd>!(ef))" }, // 430
482  { 6, 10, 18, ABC_CONST(0x0F99F066F066F066), "[<[ab]cd>(ef)]" }, // 431
483  { 6, 7, 11, ABC_CONST(0x00007FFF7FFF0000), "(!(abcd)[ef])" }, // 432
484  { 6, 7, 9, ABC_CONST(0x000080FF80FF0000), "(!(!(abc)d)[ef])" }, // 433
485  { 6, 9, 14, ABC_CONST(0x00007F807F800000), "([(abc)d][ef])" }, // 434
486  { 6, 7, 10, ABC_CONST(0x00008FFF8FFF0000), "(!(!(ab)cd)[ef])" }, // 435
487  { 6, 7, 10, ABC_CONST(0x000070FF70FF0000), "(!(!(!(ab)c)d)[ef])" }, // 436
488  { 6, 9, 14, ABC_CONST(0x00008F708F700000), "([(!(ab)c)d][ef])" }, // 437
489  { 6, 9, 13, ABC_CONST(0x000087FF87FF0000), "(!([(ab)c]d)[ef])" }, // 438
490  { 6, 11, 20, ABC_CONST(0x0000877887780000), "([(ab)cd][ef])" }, // 439
491  { 6, 9, 12, ABC_CONST(0x00009FFF9FFF0000), "(!([ab]cd)[ef])" }, // 440
492  { 6, 9, 11, ABC_CONST(0x000060FF60FF0000), "(!(!([ab]c)d)[ef])" }, // 441
493  { 6, 11, 17, ABC_CONST(0x00009F609F600000), "([([ab]c)d][ef])" }, // 442
494  { 6, 11, 16, ABC_CONST(0x000069FF69FF0000), "(!([abc]d)[ef])" }, // 443
495  { 6, 13, 26, ABC_CONST(0x0000699669960000), "([abcd][ef])" }, // 444
496  { 6, 8, 10, ABC_CONST(0x000035FF35FF0000), "(!(<abc>d)[ef])" }, // 445
497  { 6, 10, 14, ABC_CONST(0x000035CA35CA0000), "([<abc>d][ef])" }, // 446
498  { 6, 7, 10, ABC_CONST(0x0000F888F8880000), "(!(!(ab)!(cd))[ef])" }, // 447
499  { 6, 9, 15, ABC_CONST(0x0000788878880000), "([(ab)(cd)][ef])" }, // 448
500  { 6, 9, 16, ABC_CONST(0x0000877787770000), "(![(ab)(cd)][ef])" }, // 449
501  { 6, 9, 12, ABC_CONST(0x0000F999F9990000), "(!([ab]!(cd))[ef])" }, // 450
502  { 6, 11, 14, ABC_CONST(0x0000066006600000), "([ab][cd][ef])" }, // 451
503  { 6, 11, 14, ABC_CONST(0x0000F99FF99F0000), "(!([ab][cd])[ef])" }, // 452
504  { 6, 8, 11, ABC_CONST(0x0000CAAACAAA0000), "(<ab(cd)>[ef])" }, // 453
505  { 6, 10, 14, ABC_CONST(0x0000ACCAACCA0000), "(<ab[cd]>[ef])" }, // 454
506  { 6, 8, 9, ABC_CONST(0x0000F088F0880000), "(<(ab)cd>[ef])" }, // 455
507  { 6, 8, 10, ABC_CONST(0x00000F770F770000), "(!<(ab)cd>[ef])" }, // 456
508  { 6, 10, 11, ABC_CONST(0x0000F066F0660000), "(<[ab]cd>[ef])" }, // 457
509  { 6, 5, 11, ABC_CONST(0x007F7F7F7F7F7F7F), "(!(abc)!(def))" }, // 458
510  { 6, 7, 16, ABC_CONST(0x7F80808080808080), "[(abc)(def)]" }, // 459
511  { 6, 5, 9, ABC_CONST(0x008F8F8F8F8F8F8F), "(!(!(ab)c)!(def))" }, // 460
512  { 6, 7, 16, ABC_CONST(0x8F70707070707070), "[(!(ab)c)(def)]" }, // 461
513  { 6, 7, 13, ABC_CONST(0x0078787878787878), "([(ab)c]!(def))" }, // 462
514  { 6, 7, 12, ABC_CONST(0x009F9F9F9F9F9F9F), "(!([ab]c)!(def))" }, // 463
515  { 6, 9, 20, ABC_CONST(0x9F60606060606060), "[([ab]c)(def)]" }, // 464
516  { 6, 9, 17, ABC_CONST(0x0096969696969696), "([abc]!(def))" }, // 465
517  { 6, 6, 9, ABC_CONST(0x00CACACACACACACA), "(<abc>!(def))" }, // 466
518  { 6, 8, 16, ABC_CONST(0x35CACACACACACACA), "[<abc>(def)]" }, // 467
519  { 6, 5, 8, ABC_CONST(0x8F0000008F8F8F8F), "(!(!(ab)c)!(!(de)f))" }, // 468
520  { 6, 7, 16, ABC_CONST(0x708F8F8F70707070), "[(!(ab)c)(!(de)f)]" }, // 469
521  { 6, 7, 11, ABC_CONST(0x7800000078787878), "([(ab)c]!(!(de)f))" }, // 470
522  { 6, 7, 10, ABC_CONST(0x9F0000009F9F9F9F), "(!([ab]c)!(!(de)f))" }, // 471
523  { 6, 9, 20, ABC_CONST(0x609F9F9F60606060), "[([ab]c)(!(de)f)]" }, // 472
524  { 6, 9, 14, ABC_CONST(0x9600000096969696), "([abc]!(!(de)f))" }, // 473
525  { 6, 6, 8, ABC_CONST(0xCA000000CACACACA), "(<abc>!(!(de)f))" }, // 474
526  { 6, 8, 16, ABC_CONST(0xCA353535CACACACA), "[<abc>(!(de)f)]" }, // 475
527  { 6, 9, 15, ABC_CONST(0x0078787878000000), "([(ab)c][(de)f])" }, // 476
528  { 6, 9, 14, ABC_CONST(0x009F9F9F9F000000), "(!([ab]c)[(de)f])" }, // 477
529  { 6, 11, 19, ABC_CONST(0x0096969696000000), "([abc][(de)f])" }, // 478
530  { 6, 8, 11, ABC_CONST(0x00CACACACA000000), "(<abc>[(de)f])" }, // 479
531  { 6, 9, 13, ABC_CONST(0x9F00009F9F9F9F9F), "(!([ab]c)!([de]f))" }, // 480
532  { 6, 11, 25, ABC_CONST(0x609F9F6060606060), "[([ab]c)([de]f)]" }, // 481
533  { 6, 11, 18, ABC_CONST(0x9600009696969696), "([abc]!([de]f))" }, // 482
534  { 6, 8, 10, ABC_CONST(0xCA0000CACACACACA), "(<abc>!([de]f))" }, // 483
535  { 6, 10, 20, ABC_CONST(0xCA3535CACACACACA), "[<abc>([de]f)]" }, // 484
536  { 6, 13, 24, ABC_CONST(0x9600009600969600), "([abc][def])" }, // 485
537  { 6, 10, 14, ABC_CONST(0xCA0000CA00CACA00), "(<abc>[def])" }, // 486
538  { 6, 7, 8, ABC_CONST(0xCACA0000CA00CA00), "(<abc><def>)" }, // 487
539  { 6, 9, 16, ABC_CONST(0x3535CACA35CA35CA), "[<abc><def>]" }, // 488
540  { 6, 6, 10, ABC_CONST(0xCAAAAAAAAAAAAAAA), "<ab(cdef)>" }, // 489
541  { 6, 6, 10, ABC_CONST(0xACCCCCCCAAAAAAAA), "<ab(!(cde)f)>" }, // 490
542  { 6, 8, 16, ABC_CONST(0xACCCCCCCCAAAAAAA), "<ab[(cde)f]>" }, // 491
543  { 6, 6, 10, ABC_CONST(0xACCCAAAAAAAAAAAA), "<ab(!(cd)ef)>" }, // 492
544  { 6, 6, 10, ABC_CONST(0xCAAACCCCAAAAAAAA), "<ab(!(!(cd)e)f)>" }, // 493
545  { 6, 8, 16, ABC_CONST(0xCAAACCCCACCCAAAA), "<ab[(!(cd)e)f]>" }, // 494
546  { 6, 8, 14, ABC_CONST(0xACCCCAAAAAAAAAAA), "<ab([(cd)e]f)>" }, // 495
547  { 6, 10, 24, ABC_CONST(0xCAAAACCCACCCCAAA), "<ab[(cd)ef]>" }, // 496
548  { 6, 8, 12, ABC_CONST(0xACCAAAAAAAAAAAAA), "<ab([cd]ef)>" }, // 497
549  { 6, 8, 12, ABC_CONST(0xCAACCCCCAAAAAAAA), "<ab(!([cd]e)f)>" }, // 498
550  { 6, 10, 20, ABC_CONST(0xCAACCCCCACCAAAAA), "<ab[([cd]e)f]>" }, // 499
551  { 6, 10, 18, ABC_CONST(0xCAACACCAAAAAAAAA), "<ab([cde]f)>" }, // 500
552  { 6, 12, 32, ABC_CONST(0xACCACAACCAACACCA), "<ab[cdef]>" }, // 501
553  { 6, 7, 10, ABC_CONST(0xCCAACACAAAAAAAAA), "<ab(<cde>f)>" }, // 502
554  { 6, 9, 16, ABC_CONST(0xAACCACACCCAACACA), "<ab[<cde>f]>" }, // 503
555  { 6, 6, 12, ABC_CONST(0xAAAAACCCACCCACCC), "<ab(!(cd)!(ef))>" }, // 504
556  { 6, 8, 18, ABC_CONST(0xACCCCAAACAAACAAA), "<ab[(cd)(ef)]>" }, // 505
557  { 6, 8, 14, ABC_CONST(0xAAAAACCAACCAACCA), "<ab([cd]!(ef))>" }, // 506
558  { 6, 10, 16, ABC_CONST(0xAAAAACCAACCAAAAA), "<ab([cd][ef])>" }, // 507
559  { 6, 7, 12, ABC_CONST(0xCCAACACACACACACA), "<ab<cd(ef)>>" }, // 508
560  { 6, 9, 16, ABC_CONST(0xCACACCAACCAACACA), "<ab<cd[ef]>>" }, // 509
561  { 6, 7, 10, ABC_CONST(0xCCCCAAAACAAACAAA), "<ab<(cd)ef>>" }, // 510
562  { 6, 9, 12, ABC_CONST(0xCCCCAAAAACCAACCA), "<ab<[cd]ef>>" }, // 511
563  { 6, 6, 9, ABC_CONST(0xC0AAAAAAAAAAAAAA), "<a(bc)(def)>" }, // 512
564  { 6, 6, 10, ABC_CONST(0xAAC0C0C0AAAAAAAA), "<a(bc)(!(de)f)>" }, // 513
565  { 6, 8, 12, ABC_CONST(0xAAC0C0AAAAAAAAAA), "<a(bc)([de]f)>" }, // 514
566  { 6, 8, 10, ABC_CONST(0x3CAAAAAAAAAAAAAA), "<a[bc](def)>" }, // 515
567  { 6, 8, 12, ABC_CONST(0xAA3C3C3CAAAAAAAA), "<a[bc](!(de)f)>" }, // 516
568  { 6, 10, 14, ABC_CONST(0xAA3C3CAAAAAAAAAA), "<a[bc]([de]f)>" }, // 517
569  { 6, 6, 8, ABC_CONST(0xC000AAAAAAAAAAAA), "<a(bcd)(ef)>" }, // 518
570  { 6, 6, 8, ABC_CONST(0x3F00AAAAAAAAAAAA), "<a(!(bc)d)(ef)>" }, // 519
571  { 6, 8, 10, ABC_CONST(0x3FC0AAAAAAAAAAAA), "<a[(bc)d](ef)>" }, // 520
572  { 6, 8, 9, ABC_CONST(0x3C00AAAAAAAAAAAA), "<a([bc]d)(ef)>" }, // 521
573  { 6, 10, 12, ABC_CONST(0xC33CAAAAAAAAAAAA), "<a[bcd](ef)>" }, // 522
574  { 6, 7, 8, ABC_CONST(0xF0CCAAAAAAAAAAAA), "<a<bcd>(ef)>" }, // 523
575  { 6, 6, 11, ABC_CONST(0xF088888888888888), "<(ab)c(def)>" }, // 524
576  { 6, 6, 10, ABC_CONST(0x88F0F0F088888888), "<(ab)c(!(de)f)>" }, // 525
577  { 6, 8, 15, ABC_CONST(0x88F0F0F0F0888888), "<(ab)c[(de)f]>" }, // 526
578  { 6, 8, 13, ABC_CONST(0x88F0F08888888888), "<(ab)c([de]f)>" }, // 527
579  { 6, 10, 20, ABC_CONST(0xF08888F088F0F088), "<(ab)c[def]>" }, // 528
580  { 6, 7, 10, ABC_CONST(0xF0F08888F088F088), "<(ab)c<def>>" }, // 529
581  { 6, 8, 14, ABC_CONST(0xF066666666666666), "<[ab]c(def)>" }, // 530
582  { 6, 8, 12, ABC_CONST(0x66F0F0F066666666), "<[ab]c(!(de)f)>" }, // 531
583  { 6, 10, 18, ABC_CONST(0x66F0F0F0F0666666), "<[ab]c[(de)f]>" }, // 532
584  { 6, 10, 16, ABC_CONST(0x66F0F06666666666), "<[ab]c([de]f)>" }, // 533
585  { 6, 12, 24, ABC_CONST(0xF06666F066F0F066), "<[ab]c[def]>" }, // 534
586  { 6, 9, 12, ABC_CONST(0xF0F06666F066F066), "<[ab]c<def>>" }, // 535
587  { 6, 6, 9, ABC_CONST(0xF000888888888888), "<(ab)(cd)(ef)>" }, // 536
588  { 6, 6, 9, ABC_CONST(0xF000777777777777), "<!(ab)(cd)(ef)>" }, // 537
589  { 6, 8, 12, ABC_CONST(0x8888F000F0008888), "<(ab)(cd)[ef]>" }, // 538
590  { 6, 8, 12, ABC_CONST(0x7777F000F0007777), "<!(ab)(cd)[ef]>" }, // 539
591  { 6, 8, 10, ABC_CONST(0x0FF0888888888888), "<(ab)[cd](ef)>" }, // 540
592  { 6, 8, 11, ABC_CONST(0xF000666666666666), "<[ab](cd)(ef)>" }, // 541
593  { 6, 10, 14, ABC_CONST(0x6666F000F0006666), "<[ab](cd)[ef]>" }, // 542
594  { 6, 10, 12, ABC_CONST(0x0FF0666666666666), "<[ab][cd](ef)>" }, // 543
595  { 6, 12, 16, ABC_CONST(0x66660FF00FF06666), "<[ab][cd][ef]>" }, // 544
596  { 6, 6, 10, ABC_CONST(0xFF00808080808080), "<(abc)d(ef)>" }, // 545
597  { 6, 8, 12, ABC_CONST(0x8080FF00FF008080), "<(abc)d[ef]>" }, // 546
598  { 6, 6, 10, ABC_CONST(0xFF00707070707070), "<(!(ab)c)d(ef)>" }, // 547
599  { 6, 8, 12, ABC_CONST(0x7070FF00FF007070), "<(!(ab)c)d[ef]>" }, // 548
600  { 6, 8, 14, ABC_CONST(0xFF00787878787878), "<[(ab)c]d(ef)>" }, // 549
601  { 6, 10, 16, ABC_CONST(0x7878FF00FF007878), "<[(ab)c]d[ef]>" }, // 550
602  { 6, 8, 12, ABC_CONST(0xFF00606060606060), "<([ab]c)d(ef)>" }, // 551
603  { 6, 10, 14, ABC_CONST(0x6060FF00FF006060), "<([ab]c)d[ef]>" }, // 552
604  { 6, 10, 18, ABC_CONST(0xFF00969696969696), "<[abc]d(ef)>" }, // 553
605  { 6, 12, 20, ABC_CONST(0x9696FF00FF009696), "<[abc]d[ef]>" }, // 554
606  { 6, 7, 10, ABC_CONST(0xFF00CACACACACACA), "<<abc>d(ef)>" }, // 555
607  { 6, 9, 12, ABC_CONST(0xCACAFF00FF00CACA), "<<abc>d[ef]>" }, // 556
608  { 6, 6, 7, ABC_CONST(0xFF00000080808080), "<(abc)(de)f>" }, // 557
609  { 6, 6, 7, ABC_CONST(0xFF0000007F7F7F7F), "<!(abc)(de)f>" }, // 558
610  { 6, 8, 8, ABC_CONST(0x00FFFF0080808080), "<(abc)[de]f>" }, // 559
611  { 6, 6, 7, ABC_CONST(0xFF00000070707070), "<(!(ab)c)(de)f>" }, // 560
612  { 6, 6, 7, ABC_CONST(0xFF0000008F8F8F8F), "<!(!(ab)c)(de)f>" }, // 561
613  { 6, 8, 8, ABC_CONST(0x00FFFF0070707070), "<(!(ab)c)[de]f>" }, // 562
614  { 6, 8, 9, ABC_CONST(0xFF00000078787878), "<[(ab)c](de)f>" }, // 563
615  { 6, 10, 10, ABC_CONST(0x00FFFF0078787878), "<[(ab)c][de]f>" }, // 564
616  { 6, 8, 8, ABC_CONST(0xFF00000060606060), "<([ab]c)(de)f>" }, // 565
617  { 6, 8, 8, ABC_CONST(0xFF0000009F9F9F9F), "<!([ab]c)(de)f>" }, // 566
618  { 6, 10, 9, ABC_CONST(0x00FFFF0060606060), "<([ab]c)[de]f>" }, // 567
619  { 6, 10, 11, ABC_CONST(0xFF00000096969696), "<[abc](de)f>" }, // 568
620  { 6, 12, 12, ABC_CONST(0x00FFFF0096969696), "<[abc][de]f>" }, // 569
621  { 6, 7, 7, ABC_CONST(0xFF000000CACACACA), "<<abc>(de)f>" }, // 570
622  { 6, 9, 8, ABC_CONST(0x00FFFF00CACACACA), "<<abc>[de]f>" }, // 571
623  { 6, 6, 7, ABC_CONST(0xFFFF000080008000), "<(abcd)ef>" }, // 572
624  { 6, 6, 7, ABC_CONST(0xFFFF00007F007F00), "<(!(abc)d)ef>" }, // 573
625  { 6, 8, 10, ABC_CONST(0xFFFF00007F807F80), "<[(abc)d]ef>" }, // 574
626  { 6, 6, 7, ABC_CONST(0xFFFF000070007000), "<(!(ab)cd)ef>" }, // 575
627  { 6, 6, 7, ABC_CONST(0xFFFF00008F008F00), "<(!(!(ab)c)d)ef>" }, // 576
628  { 6, 8, 10, ABC_CONST(0xFFFF00008F708F70), "<[(!(ab)c)d]ef>" }, // 577
629  { 6, 8, 9, ABC_CONST(0xFFFF000078007800), "<([(ab)c]d)ef>" }, // 578
630  { 6, 10, 14, ABC_CONST(0xFFFF000087788778), "<[(ab)cd]ef>" }, // 579
631  { 6, 8, 8, ABC_CONST(0xFFFF000060006000), "<([ab]cd)ef>" }, // 580
632  { 6, 8, 8, ABC_CONST(0xFFFF00009F009F00), "<(!([ab]c)d)ef>" }, // 581
633  { 6, 10, 12, ABC_CONST(0xFFFF00009F609F60), "<[([ab]c)d]ef>" }, // 582
634  { 6, 10, 11, ABC_CONST(0xFFFF000096009600), "<([abc]d)ef>" }, // 583
635  { 6, 12, 18, ABC_CONST(0xFFFF000069966996), "<[abcd]ef>" }, // 584
636  { 6, 7, 7, ABC_CONST(0xFFFF0000CA00CA00), "<(<abc>d)ef>" }, // 585
637  { 6, 9, 10, ABC_CONST(0xFFFF000035CA35CA), "<[<abc>d]ef>" }, // 586
638  { 6, 6, 8, ABC_CONST(0xFFFF000007770777), "<(!(ab)!(cd))ef>" }, // 587
639  { 6, 8, 11, ABC_CONST(0xFFFF000078887888), "<[(ab)(cd)]ef>" }, // 588
640  { 6, 8, 9, ABC_CONST(0xFFFF000006660666), "<([ab]!(cd))ef>" }, // 589
641  { 6, 10, 10, ABC_CONST(0xFFFF000006600660), "<([ab][cd])ef>" }, // 590
642  { 6, 7, 8, ABC_CONST(0xFFFF0000CAAACAAA), "<<ab(cd)>ef>" }, // 591
643  { 6, 9, 10, ABC_CONST(0xFFFF0000ACCAACCA), "<<ab[cd]>ef>" }, // 592
644  { 6, 7, 7, ABC_CONST(0xFFFF0000F088F088), "<<(ab)cd>ef>" }, // 593
645  { 6, 9, 8, ABC_CONST(0xFFFF0000F066F066), "<<[ab]cd>ef>" } // 594
646 };
647 
648 struct Sdm_Man_t_
649 {
650  Sdm_Dsd_t * pDsd6; // NPN class information
651  Hsh_IntMan_t * pHash; // maps DSD functions into NPN classes
652  Vec_Int_t * vConfgRes; // configurations
653  Vec_Wrd_t * vPerm6; // permutations of DSD classes
654  Vec_Int_t * vMap2Perm; // maps number into its permutation
655  char Perm6[720][6]; // permutations
656  int nCountDsd[DSD_CLASS_NUM];
657  int nNonDsd;
658  int nAllDsd;
659 };
660 
661 ////////////////////////////////////////////////////////////////////////
662 /// FUNCTION DEFINITIONS ///
663 ////////////////////////////////////////////////////////////////////////
664 
665 /**Function*************************************************************
666 
667  Synopsis []
668 
669  Description []
670 
671  SideEffects []
672 
673  SeeAlso []
674 
675 ***********************************************************************/
676 void Sdm_ManPrintDsdStats( Sdm_Man_t * p, int fVerbose )
677 {
678  int i, Absent = 0;
679  for ( i = 0; i < DSD_CLASS_NUM; i++ )
680  {
681  if ( p->nCountDsd[i] == 0 )
682  {
683  Absent++;
684  continue;
685  }
686  if ( fVerbose )
687  {
688  printf( "%5d : ", i );
689  printf( "%-20s ", p->pDsd6[i].pStr );
690  printf( "%8d ", p->nCountDsd[i] );
691  printf( "\n" );
692  }
693  }
694  printf( "Unused classes = %d (%.2f %%). ", Absent, 100.0 * Absent / DSD_CLASS_NUM );
695  printf( "Non-DSD cuts = %d (%.2f %%). ", p->nNonDsd, 100.0 * p->nNonDsd / Abc_MaxInt(1, p->nAllDsd) );
696  printf( "\n" );
697 }
698 
699 /**Function*************************************************************
700 
701  Synopsis []
702 
703  Description []
704 
705  SideEffects []
706 
707  SeeAlso []
708 
709 ***********************************************************************/
710 Hsh_IntMan_t * Sdm_ManBuildHashTable( Vec_Int_t ** pvConfgRes )
711 {
712  FILE * pFile;
713  char * pFileName = "dsdfuncs6.dat";
714  int RetValue, size = Extra_FileSize( pFileName ) / 12; // 2866420
715  Vec_Wrd_t * vTruthRes = Vec_WrdAlloc( size );
716  Vec_Int_t * vConfgRes = Vec_IntAlloc( size );
717  Hsh_IntMan_t * pHash;
718 
719  pFile = fopen( pFileName, "rb" );
720  RetValue = fread( Vec_WrdArray(vTruthRes), sizeof(word), size, pFile );
721  RetValue = fread( Vec_IntArray(vConfgRes), sizeof(int), size, pFile );
722  vTruthRes->nSize = size;
723  vConfgRes->nSize = size;
724  // create hash table
725  pHash = Hsh_WrdManHashArrayStart( vTruthRes, 1 );
726  // cleanup
727  if ( pvConfgRes )
728  *pvConfgRes = vConfgRes;
729  else
730  Vec_IntFree( vConfgRes );
731  Vec_WrdFree( vTruthRes );
732 // Hsh_IntManStop( pHash );
733  return pHash;
734 }
735 
736 /**Function*************************************************************
737 
738  Synopsis []
739 
740  Description []
741 
742  SideEffects []
743 
744  SeeAlso []
745 
746 ***********************************************************************/
747 void Sdm_ManPrecomputePerms( Sdm_Man_t * p )
748 {
749  int nVars = 6;
750  // 0(1:1) 1(2:1) 2(4:2) 3(10:6) 4(33:23) 5(131:98) 6(595:464)
751  int nClasses[7] = { 1, 2, 4, 10, 33, 131, 595 };
752  int nPerms = Extra_Factorial( nVars );
753 // int nSwaps = (1 << nVars);
754  int * pComp, * pPerm;
755  int i, k, x, One, OneCopy, Num;
756  Vec_Int_t * vVars;
757  abctime clk = Abc_Clock();
758  assert( p->pDsd6 == NULL );
759  p->pDsd6 = s_DsdClass6;
760  // precompute schedules
761  pComp = Extra_GreyCodeSchedule( nVars );
762  pPerm = Extra_PermSchedule( nVars );
763  // map numbers into perms
764  p->vMap2Perm = Vec_IntStartFull( (1<<(3*nVars)) );
765  // store permutations
766  One = 0;
767  for ( x = 0; x < nVars; x++ )
768  {
769  p->Perm6[0][x] = (char)x;
770  One |= (x << (3*x));
771  }
772 // Vec_IntWriteEntry( p->vMap2Perm, One, 0 );
773  OneCopy = One;
774  for ( k = 0; k < nPerms; k++ )
775  {
776  if ( k > 0 )
777  for ( x = 0; x < nVars; x++ )
778  p->Perm6[k][x] = p->Perm6[k-1][x];
779  ABC_SWAP( char, p->Perm6[k][pPerm[k]], p->Perm6[k][pPerm[k]+1] );
780 
781  Num = ( (One >> (3*(pPerm[k] ))) ^ (One >> (3*(pPerm[k]+1))) ) & 7;
782  One ^= (Num << (3*(pPerm[k] )));
783  One ^= (Num << (3*(pPerm[k]+1)));
784 
785  Vec_IntWriteEntry( p->vMap2Perm, One, k );
786 
787 // Sdm_ManPrintPerm( One );
788 // for ( x = 0; x < nVars; x++ )
789 // printf( "%d ", p->Perm6[k][x] );
790 // printf( "\n" );
791  }
792  assert( OneCopy == One );
793  // fill in the gaps
794  vVars = Vec_IntAlloc( 6 );
795  Vec_IntForEachEntry( p->vMap2Perm, Num, i )
796  {
797  // mark used variables
798  int Count = 0;
799  One = i;
800  Vec_IntFill( vVars, 6, 0 );
801  for ( k = 0; k < nVars; k++ )
802  {
803  int iVar = ((One >> (3*k)) & 7);
804  if ( iVar >= nVars && iVar < 7 )
805  break;
806  if ( iVar != 7 )
807  {
808  if ( Vec_IntEntry( vVars, iVar ) == 1 )
809  break;
810  Vec_IntWriteEntry( vVars, iVar, 1 );
811  Count++;
812  }
813  }
814  // skip ones with dups and complete
815  if ( k < nVars || Count == nVars )
816  continue;
817  // find unused variables
818  for ( x = k = 0; k < 6; k++ )
819  if ( Vec_IntEntry(vVars, k) == 0 )
820  Vec_IntWriteEntry( vVars, x++, k );
821  Vec_IntShrink( vVars, x );
822  // fill in used variables
823  x = 0;
824  for ( k = 0; k < nVars; k++ )
825  {
826  int iVar = ((One >> (3*k)) & 7);
827  if ( iVar == 7 )
828  One ^= ((Vec_IntEntry(vVars, x++) ^ 7) << (3*k));
829  }
830  assert( x == Vec_IntSize(vVars) );
831  // save this one
832  assert( Vec_IntEntry( p->vMap2Perm, One ) != -1 );
833  Vec_IntWriteEntry( p->vMap2Perm, i, Vec_IntEntry(p->vMap2Perm, One) );
834 /*
835  // mapping
836  Sdm_ManPrintPerm( i );
837  printf( "-> " );
838  Sdm_ManPrintPerm( One );
839  printf( "\n" );
840 */
841  }
842  Vec_IntFree( vVars );
843 
844  // store permuted truth tables
845  assert( p->vPerm6 == NULL );
846  p->vPerm6 = Vec_WrdAlloc( nPerms * DSD_CLASS_NUM );
847  for ( i = 0; i < nClasses[nVars]; i++ )
848  {
849  word uTruth = s_DsdClass6[i].uTruth;
850  for ( k = 0; k < nPerms; k++ )
851  {
852  uTruth = Abc_Tt6SwapAdjacent( uTruth, pPerm[k] );
853  Vec_WrdPush( p->vPerm6, uTruth );
854  }
855  assert( uTruth == s_DsdClass6[i].uTruth );
856  }
857  ABC_FREE( pPerm );
858  ABC_FREE( pComp );
859  // build hash table
860  p->pHash = Sdm_ManBuildHashTable( &p->vConfgRes );
861  Abc_PrintTime( 1, "Setting up DSD information", Abc_Clock() - clk );
862 }
863 
864 
865 /**Function*************************************************************
866 
867  Synopsis []
868 
869  Description []
870 
871  SideEffects []
872 
873  SeeAlso []
874 
875 ***********************************************************************/
876 void Sdm_ManPrintPerm( unsigned s )
877 {
878  int i;
879  for ( i = 0; i < 6; i++ )
880  printf( "%d ", (s >> (3*i)) & 7 );
881  printf( " " );
882 }
883 
884 /**Function*************************************************************
885 
886  Synopsis [Checks hash table for DSD class.]
887 
888  Description []
889 
890  SideEffects []
891 
892  SeeAlso []
893 
894 ***********************************************************************/
895 int Sdm_ManCheckDsd6( Sdm_Man_t * p, word t )
896 {
897  int fCompl, Entry, Config;
898  if ( (fCompl = (t & 1)) )
899  t = ~t;
900  Entry = *Hsh_IntManLookup( p->pHash, (unsigned *)&t );
901  if ( Entry == -1 )
902  return -1;
903  Config = Vec_IntEntry( p->vConfgRes, Entry );
904  if ( fCompl )
905  Config ^= (1 << 16);
906  return Config;
907 }
908 
909 /**Function*************************************************************
910 
911  Synopsis []
912 
913  Description []
914 
915  SideEffects []
916 
917  SeeAlso []
918 
919 ***********************************************************************/
920 int Sdm_ManComputeFunc( Sdm_Man_t * p, int iDsdLit0, int iDsdLit1, int * pCut, int uMask, int fXor )
921 {
922 // int fVerbose = 0;
923  int i, Config, iClass, fCompl, Res;
924  int PermMask = uMask & 0x3FFFF;
925  int ComplMask = uMask >> 18;
926  word Truth0, Truth1p, t0, t1, t;
927  p->nAllDsd++;
928 
929  assert( uMask > 1 );
930  assert( iDsdLit0 < DSD_CLASS_NUM * 2 );
931  assert( iDsdLit1 < DSD_CLASS_NUM * 2 );
932  Truth0 = p->pDsd6[Abc_Lit2Var(iDsdLit0)].uTruth;
933  Truth1p = Vec_WrdEntry( p->vPerm6, Abc_Lit2Var(iDsdLit1) * 720 + Vec_IntEntry(p->vMap2Perm, PermMask ) );
934  if ( ComplMask )
935  for ( i = 0; i < 6; i++ )
936  if ( (ComplMask >> i) & 1 )
937  Truth1p = Abc_Tt6Flip( Truth1p, i );
938  t0 = Abc_LitIsCompl(iDsdLit0) ? ~Truth0 : Truth0;
939  t1 = Abc_LitIsCompl(iDsdLit1) ? ~Truth1p : Truth1p;
940  t = fXor ? t0 ^ t1 : t0 & t1;
941 /*
942 if ( fVerbose )
943 {
944 Sdm_ManPrintPerm( PermMask ); printf( "\n" );
945 Extra_PrintBinary( stdout, &ComplMask, 6 ); printf( "\n" );
946 Kit_DsdPrintFromTruth( (unsigned *)&Truth0, 6 ); printf( "\n" );
947 Kit_DsdPrintFromTruth( (unsigned *)&Truth1p, 6 ); printf( "\n" );
948 Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ); printf( "\n" );
949 }
950 */
951  // find configuration
952  Config = Sdm_ManCheckDsd6( p, t );
953  if ( Config == -1 )
954  {
955  p->nNonDsd++;
956  return -1;
957  }
958 
959  // get the class
960  iClass = Config >> 17;
961  fCompl = (Config >> 16) & 1;
962  Config &= 0xFFFF;
963 
964  // set the function
965  Res = Abc_Var2Lit( iClass, fCompl );
966 
967  // update cut
968  assert( (Config >> 6) < 720 );
969  if ( pCut )
970  {
971  int pLeavesNew[6] = { -1, -1, -1, -1, -1, -1 };
972  assert( pCut[0] <= 6 );
973  for ( i = 0; i < pCut[0]; i++ )
974  pLeavesNew[(int)(p->Perm6[Config >> 6][i])] = Abc_LitNotCond( pCut[i+1], (Config >> i) & 1 );
975  pCut[0] = p->pDsd6[iClass].nVars;
976  for ( i = 0; i < pCut[0]; i++ )
977  assert( pLeavesNew[i] != -1 );
978  for ( i = 0; i < pCut[0]; i++ )
979  pCut[i+1] = pLeavesNew[i];
980  }
981  assert( iClass < DSD_CLASS_NUM );
982  p->nCountDsd[iClass]++;
983  return Res;
984 }
985 
986 /**Function*************************************************************
987 
988  Synopsis []
989 
990  Description []
991 
992  SideEffects []
993 
994  SeeAlso []
995 
996 ***********************************************************************/
997 int Sdm_ManReadDsdVarNum( Sdm_Man_t * p, int iDsd )
998 {
999  return p->pDsd6[iDsd].nVars;
1000 }
1001 int Sdm_ManReadDsdAndNum( Sdm_Man_t * p, int iDsd )
1002 {
1003  return p->pDsd6[iDsd].nAnds;
1004 }
1005 int Sdm_ManReadDsdClauseNum( Sdm_Man_t * p, int iDsd )
1006 {
1007  return p->pDsd6[iDsd].nClauses;
1008 }
1009 word Sdm_ManReadDsdTruth( Sdm_Man_t * p, int iDsd )
1010 {
1011  return p->pDsd6[iDsd].uTruth;
1012 }
1013 char * Sdm_ManReadDsdStr( Sdm_Man_t * p, int iDsd )
1014 {
1015  return p->pDsd6[iDsd].pStr;
1016 }
1017 void Sdm_ManReadCnfCosts( Sdm_Man_t * p, int * pCosts, int nCosts )
1018 {
1019  int i;
1020  assert( nCosts == DSD_CLASS_NUM );
1021  pCosts[0] = pCosts[1] = 0;
1022  for ( i = 2; i < DSD_CLASS_NUM; i++ )
1023  pCosts[i] = Sdm_ManReadDsdClauseNum( p, i );
1024 }
1025 
1026 
1027 /**Function*************************************************************
1028 
1029  Synopsis [Manager manipulation.]
1030 
1031  Description []
1032 
1033  SideEffects []
1034 
1035  SeeAlso []
1036 
1037 ***********************************************************************/
1038 Sdm_Man_t * Sdm_ManAlloc()
1039 {
1040  Sdm_Man_t * p;
1041  p = ABC_CALLOC( Sdm_Man_t, 1 );
1042  Sdm_ManPrecomputePerms( p );
1043  return p;
1044 }
1045 void Sdm_ManFree( Sdm_Man_t * p )
1046 {
1047  Vec_WrdFree( p->vPerm6 );
1048  Vec_IntFree( p->vMap2Perm );
1049  Vec_IntFree( p->vConfgRes );
1050  Vec_IntFree( p->pHash->vData );
1051  Hsh_IntManStop( p->pHash );
1052  ABC_FREE( p );
1053 }
1054 
1055 /**Function*************************************************************
1056 
1057  Synopsis []
1058 
1059  Description []
1060 
1061  SideEffects []
1062 
1063  SeeAlso []
1064 
1065 ***********************************************************************/
1066 static Sdm_Man_t * s_SdmMan = NULL;
1067 Sdm_Man_t * Sdm_ManRead()
1068 {
1069  if ( s_SdmMan == NULL )
1070  s_SdmMan = Sdm_ManAlloc();
1071  memset( s_SdmMan->nCountDsd, 0, sizeof(int) * DSD_CLASS_NUM );
1072  return s_SdmMan;
1073 }
1074 void Sdm_ManQuit()
1075 {
1076  if ( s_SdmMan != NULL )
1077  Sdm_ManFree( s_SdmMan );
1078  s_SdmMan = NULL;
1079 }
1080 int Sdm_ManCanRead()
1081 {
1082  char * pFileName = "dsdfuncs6.dat";
1083  FILE * pFile = fopen( pFileName, "rb" );
1084  if ( pFile == NULL )
1085  return 0;
1086  fclose( pFile );
1087  return 1;
1088 }
1089 
1090 /**Function*************************************************************
1091 
1092  Synopsis []
1093 
1094  Description []
1095 
1096  SideEffects []
1097 
1098  SeeAlso []
1099 
1100 ***********************************************************************/
1101 void Sdm_ManTest()
1102 {
1103  Sdm_Man_t * p;
1104  int iDsd0 = 4;
1105  int iDsd1 = 6;
1106  int iDsd;
1107  int uMask = 0x3FFFF ^ ((7 ^ 0) << 6) ^ ((7 ^ 1) << 9);
1108  int pCut[7] = { 4, 10, 20, 30, 40 };
1109 // Sdm_ManPrintPerm( uMask );
1110  p = Sdm_ManAlloc();
1111  iDsd = Sdm_ManComputeFunc( p, iDsd0, iDsd1, pCut, uMask, 0 );
1112  Sdm_ManFree( p );
1113 }
1114 
1115 /**Function*************************************************************
1116 
1117  Synopsis []
1118 
1119  Description []
1120 
1121  SideEffects []
1122 
1123  SeeAlso []
1124 
1125 ***********************************************************************/
1126 /*
1127 void Sdm_ManCompareCnfSizes()
1128 {
1129  Vec_Int_t * vMemory;
1130  word uTruth;
1131  int i, nSop0, nSop1, nVars, nCla, RetValue;
1132  vMemory = Vec_IntAlloc( 1 << 16 );
1133  for ( i = 1; i < DSD_CLASS_NUM; i++ )
1134  {
1135  uTruth = Sdm_ManReadDsdTruth( s_SdmMan, i );
1136  nVars = Sdm_ManReadDsdVarNum( s_SdmMan, i );
1137  nCla = Sdm_ManReadDsdClauseNum( s_SdmMan, i );
1138 
1139  RetValue = Kit_TruthIsop( &uTruth, nVars, vMemory, 0 );
1140  nSop0 = Vec_IntSize(vMemory);
1141 
1142  uTruth = ~uTruth;
1143  RetValue = Kit_TruthIsop( &uTruth, nVars, vMemory, 0 );
1144  nSop1 = Vec_IntSize(vMemory);
1145 
1146  if ( nSop0 + nSop1 != nCla )
1147  printf( "Class %4d : %d + %d != %d\n", i, nSop0, nSop1, nCla );
1148  else
1149  printf( "Class %4d : %d + %d == %d\n", i, nSop0, nSop1, nCla );
1150  }
1151  Vec_IntFree( vMemory );
1152 }
1153 */
1154 
1155 
1156 /**Function*************************************************************
1157 
1158  Synopsis [Collect DSD divisors of the function.]
1159 
1160  Description []
1161 
1162  SideEffects []
1163 
1164  SeeAlso []
1165 
1166 ***********************************************************************/
1167 void Sdm_ManDivCollect_rec( word t, Vec_Wrd_t ** pvDivs )
1168 {
1169  int i, Config, Counter = 0;
1170  // check if function is decomposable
1171  Config = Sdm_ManCheckDsd6( s_SdmMan, t );
1172  if ( Config != -1 && (Config >> 17) < 2 )
1173  return;
1174  for ( i = 0; i < 6; i++ )
1175  {
1176  if ( !Abc_Tt6HasVar( t, i ) )
1177  continue;
1178  Sdm_ManDivCollect_rec( Abc_Tt6Cofactor0(t, i), pvDivs );
1179  Sdm_ManDivCollect_rec( Abc_Tt6Cofactor1(t, i), pvDivs );
1180  Counter++;
1181  }
1182  if ( Config != -1 && Counter >= 2 && Counter <= 4 )
1183  {
1184  Vec_WrdPush( pvDivs[Counter], (t & 1) ? ~t : t );
1185 // Kit_DsdPrintFromTruth( (unsigned *)&t, 6 ); printf( "\n" );
1186  }
1187 }
1188 void Sdm_ManDivTest()
1189 {
1190 // word u, t0, t1, t = ABC_CONST(0xB0F0BBFFB0F0BAFE);
1191 // word u, t0, t1, t = ABC_CONST(0x3F1F3F13FFDFFFD3);
1192  word u, t0, t1, t = ABC_CONST(0x3F3FFFFF37003700);
1193  Rsb_Man_t * pManRsb = Rsb_ManAlloc( 6, 200, 3, 1 );
1194  Vec_Wrd_t * pvDivs[7] = { NULL };
1195  Vec_Wrd_t * vDivs = Vec_WrdAlloc( 100 );
1196  int i, RetValue;
1197 
1198  // collect divisors
1199  for ( i = 2; i <= 4; i++ )
1200  pvDivs[i] = Vec_WrdAlloc( 100 );
1201  Sdm_ManDivCollect_rec( t, pvDivs );
1202  for ( i = 2; i <= 4; i++ )
1203  Vec_WrdUniqify( pvDivs[i] );
1204 
1205  // prepare the set
1206  vDivs = Vec_WrdAlloc( 100 );
1207  for ( i = 0; i < 6; i++ )
1208  Vec_WrdPush( vDivs, s_Truths6[i] );
1209  for ( i = 2; i <= 4; i++ )
1210  Vec_WrdAppend( vDivs, pvDivs[i] );
1211  for ( i = 2; i <= 4; i++ )
1212  Vec_WrdFree( pvDivs[i] );
1213 
1214  Vec_WrdForEachEntry( vDivs, u, i )
1215  {
1216  printf( "%2d : ", i );
1217 // Kit_DsdPrintFromTruth( (unsigned *)&u, 6 );
1218  printf( "\n" );
1219  }
1220 
1221  RetValue = Rsb_ManPerformResub6( pManRsb, 6, t, vDivs, &t0, &t1, 1 );
1222  if ( RetValue )
1223  {
1224 // Kit_DsdPrintFromTruth( (unsigned *)&t0, 6 ); printf( "\n" );
1225 // Kit_DsdPrintFromTruth( (unsigned *)&t1, 6 ); printf( "\n" );
1226  printf( "Decomposition exits.\n" );
1227  }
1228 
1229 
1230  Vec_WrdFree( vDivs );
1231  Rsb_ManFree( pManRsb );
1232 }
1233 
1234 
1235 /**Function*************************************************************
1236 
1237  Synopsis [Generation of node test.]
1238 
1239  Description []
1240 
1241  SideEffects []
1242 
1243  SeeAlso []
1244 
1245 ***********************************************************************/
1246 /*
1247 #include "bool/kit/kit.h"
1248 void Sdm_ManNodeGenTest()
1249 {
1250  extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
1251  Sdm_Man_t * p = s_SdmMan;
1252  Vec_Int_t * vCover;
1253  Kit_Graph_t * pGraph;
1254  int i;
1255  vCover = Vec_IntAlloc( 1 << 16 );
1256  for ( i = 2; i < DSD_CLASS_NUM; i++ )
1257  {
1258  pGraph = Kit_TruthToGraph( (unsigned *)&p->pDsd6[i].uTruth, p->pDsd6[i].nVars, vCover );
1259  printf( "%d %s %d %d ", i, p->pDsd6[i].pStr, Kit_GraphNodeNum(pGraph), p->pDsd6[i].nAnds );
1260  }
1261  printf( "\n" );
1262 }
1263 */
1264 
1265 ////////////////////////////////////////////////////////////////////////
1266 /// END OF FILE ///
1267 ////////////////////////////////////////////////////////////////////////
1268 
1269 
1270 ABC_NAMESPACE_IMPL_END
1271 
memset
char * memset()
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Sdm_Dsd_t
typedefABC_NAMESPACE_IMPL_START struct Sdm_Dsd_t_ Sdm_Dsd_t
DECLARATIONS ///.
Definition: extraUtilDsd.c:38
Sdm_Man_t_::vConfgRes
Vec_Int_t * vConfgRes
Definition: extraUtilDsd.c:652
Extra_GreyCodeSchedule
int * Extra_GreyCodeSchedule(int n)
Definition: extraUtilMisc.c:2169
Extra_PermSchedule
int * Extra_PermSchedule(int n)
Definition: extraUtilMisc.c:2205
Sdm_Dsd_t_::nVars
int nVars
Definition: extraUtilDsd.c:41
Sdm_Dsd_t_::nClauses
int nClauses
Definition: extraUtilDsd.c:43
Sdm_ManRead
Sdm_Man_t * Sdm_ManRead()
Definition: extraUtilDsd.c:1067
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Sdm_Man_t_::nNonDsd
int nNonDsd
Definition: extraUtilDsd.c:657
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Abc_Tt6HasVar
static int Abc_Tt6HasVar(word t, int iVar)
Definition: utilTruth.h:949
Sdm_ManReadCnfCosts
void Sdm_ManReadCnfCosts(Sdm_Man_t *p, int *pCosts, int nCosts)
Definition: extraUtilDsd.c:1017
Sdm_ManAlloc
Sdm_Man_t * Sdm_ManAlloc()
Definition: extraUtilDsd.c:1038
Sdm_ManPrecomputePerms
void Sdm_ManPrecomputePerms(Sdm_Man_t *p)
Definition: extraUtilDsd.c:747
Sdm_Dsd_t_::uTruth
word uTruth
Definition: extraUtilDsd.c:44
Vec_WrdPush
static void Vec_WrdPush(Vec_Wrd_t *p, word Entry)
Definition: vecWrd.h:618
Sdm_Dsd_t_
Definition: extraUtilDsd.c:39
Sdm_Man_t_::vMap2Perm
Vec_Int_t * vMap2Perm
Definition: extraUtilDsd.c:654
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Sdm_Man_t_::pDsd6
Sdm_Dsd_t * pDsd6
Definition: extraUtilDsd.c:650
Sdm_ManFree
void Sdm_ManFree(Sdm_Man_t *p)
Definition: extraUtilDsd.c:1045
Sdm_Man_t_
Definition: extraUtilDsd.c:648
Rsb_Man_t
typedefABC_NAMESPACE_HEADER_START struct Rsb_Man_t_ Rsb_Man_t
INCLUDES ///.
Definition: rsb.h:39
Sdm_Dsd_t_::nAnds
int nAnds
Definition: extraUtilDsd.c:42
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_Tt6Cofactor0
static word Abc_Tt6Cofactor0(word t, int iVar)
Definition: utilTruth.h:370
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Sdm_Dsd_t_::pStr
char * pStr
Definition: extraUtilDsd.c:45
Sdm_ManDivTest
void Sdm_ManDivTest()
Definition: extraUtilDsd.c:1188
Vec_WrdForEachEntry
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecWrd.h:54
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition: abc_global.h:218
Vec_WrdUniqify
static void Vec_WrdUniqify(Vec_Wrd_t *p)
Definition: vecWrd.h:1076
Sdm_ManComputeFunc
int Sdm_ManComputeFunc(Sdm_Man_t *p, int iDsdLit0, int iDsdLit1, int *pCut, int uMask, int fXor)
Definition: extraUtilDsd.c:920
Hsh_WrdManHashArrayStart
static Hsh_IntMan_t * Hsh_WrdManHashArrayStart(Vec_Wrd_t *vDataW, int nSize)
Definition: vecHsh.h:217
Sdm_Man_t_::vPerm6
Vec_Wrd_t * vPerm6
Definition: extraUtilDsd.c:653
Rsb_ManAlloc
Rsb_Man_t * Rsb_ManAlloc(int nLeafMax, int nDivMax, int nDecMax, int fVerbose)
MACRO DEFINITIONS ///.
Definition: rsbMan.c:45
Sdm_ManReadDsdClauseNum
int Sdm_ManReadDsdClauseNum(Sdm_Man_t *p, int iDsd)
Definition: extraUtilDsd.c:1005
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Hsh_IntMan_t_::vData
Vec_Int_t * vData
Definition: vecHsh.h:60
DSD_CLASS_NUM
#define DSD_CLASS_NUM
Definition: extraUtilDsd.c:48
Abc_Tt6SwapAdjacent
static word Abc_Tt6SwapAdjacent(word Truth, int iVar)
Definition: utilTruth.h:1186
Rsb_ManFree
void Rsb_ManFree(Rsb_Man_t *p)
Definition: rsbMan.c:63
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Abc_Tt6Cofactor1
static word Abc_Tt6Cofactor1(word t, int iVar)
Definition: utilTruth.h:375
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Sdm_ManCheckDsd6
int Sdm_ManCheckDsd6(Sdm_Man_t *p, word t)
Definition: extraUtilDsd.c:895
Hsh_IntManLookup
static int * Hsh_IntManLookup(Hsh_IntMan_t *p, unsigned *pData)
Definition: vecHsh.h:147
Sdm_Man_t_::nCountDsd
int nCountDsd[DSD_CLASS_NUM]
Definition: extraUtilDsd.c:656
Extra_FileSize
int Extra_FileSize(char *pFileName)
Definition: extraUtilFile.c:308
Sdm_Man_t_::nAllDsd
int nAllDsd
Definition: extraUtilDsd.c:658
Sdm_ManReadDsdAndNum
int Sdm_ManReadDsdAndNum(Sdm_Man_t *p, int iDsd)
Definition: extraUtilDsd.c:1001
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_WrdFree
static void Vec_WrdFree(Vec_Wrd_t *p)
Definition: vecWrd.h:260
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Sdm_ManReadDsdTruth
word Sdm_ManReadDsdTruth(Sdm_Man_t *p, int iDsd)
Definition: extraUtilDsd.c:1009
Sdm_ManReadDsdStr
char * Sdm_ManReadDsdStr(Sdm_Man_t *p, int iDsd)
Definition: extraUtilDsd.c:1013
size
static int size
Definition: cuddSign.c:86
Counter
static int Counter
Definition: extraBddMisc.c:1877
Hsh_IntManStop
static void Hsh_IntManStop(Hsh_IntMan_t *p)
Definition: vecHsh.h:119
Sdm_Man_t_::Perm6
char Perm6[720][6]
Definition: extraUtilDsd.c:655
Abc_Tt6Flip
static word Abc_Tt6Flip(word Truth, int iVar)
Definition: utilTruth.h:1126
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
Sdm_ManBuildHashTable
Hsh_IntMan_t * Sdm_ManBuildHashTable(Vec_Int_t **pvConfgRes)
Definition: extraUtilDsd.c:710
Vec_WrdAlloc
static Vec_Wrd_t * Vec_WrdAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecWrd.h:80
s_DsdClass6
static Sdm_Dsd_t s_DsdClass6[DSD_CLASS_NUM]
Definition: extraUtilDsd.c:50
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Sdm_ManQuit
void Sdm_ManQuit()
Definition: extraUtilDsd.c:1074
Sdm_ManDivCollect_rec
void Sdm_ManDivCollect_rec(word t, Vec_Wrd_t **pvDivs)
Definition: extraUtilDsd.c:1167
s_Truths6
static word s_Truths6[6]
Definition: extraUtilEnum.c:430
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Sdm_ManPrintDsdStats
void Sdm_ManPrintDsdStats(Sdm_Man_t *p, int fVerbose)
FUNCTION DEFINITIONS ///.
Definition: extraUtilDsd.c:676
Vec_WrdArray
static word * Vec_WrdArray(Vec_Wrd_t *p)
Definition: vecWrd.h:316
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Sdm_ManReadDsdVarNum
int Sdm_ManReadDsdVarNum(Sdm_Man_t *p, int iDsd)
Definition: extraUtilDsd.c:997
Sdm_Man_t_::pHash
Hsh_IntMan_t * pHash
Definition: extraUtilDsd.c:651
Vec_WrdEntry
static word Vec_WrdEntry(Vec_Wrd_t *p, int i)
Definition: vecWrd.h:384
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Extra_Factorial
int Extra_Factorial(int n)
Definition: extraUtilMisc.c:216
s_SdmMan
static Sdm_Man_t * s_SdmMan
Definition: extraUtilDsd.c:1066
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_WrdAppend
static void Vec_WrdAppend(Vec_Wrd_t *vVec1, Vec_Wrd_t *vVec2)
Definition: vecWrd.h:1161
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Rsb_ManPerformResub6
int Rsb_ManPerformResub6(Rsb_Man_t *p, int nVars, word uTruth, Vec_Wrd_t *vDivTruths, word *puTruth0, word *puTruth1, int fVerbose)
Definition: rsbDec6.c:694
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
Sdm_ManPrintPerm
void Sdm_ManPrintPerm(unsigned s)
Definition: extraUtilDsd.c:876
Sdm_ManTest
void Sdm_ManTest()
Definition: extraUtilDsd.c:1101
Sdm_ManCanRead
int Sdm_ManCanRead()
Definition: extraUtilDsd.c:1080
Hsh_IntMan_t_
Definition: vecHsh.h:57