ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
extraUtilCanon.c
Go to the documentation of this file.
1
20
21#include "extra.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
26/*---------------------------------------------------------------------------*/
27/* Constant declarations */
28/*---------------------------------------------------------------------------*/
29
30/*---------------------------------------------------------------------------*/
31/* Stucture declarations */
32/*---------------------------------------------------------------------------*/
33
34/*---------------------------------------------------------------------------*/
35/* Type declarations */
36/*---------------------------------------------------------------------------*/
37
38/*---------------------------------------------------------------------------*/
39/* Variable declarations */
40/*---------------------------------------------------------------------------*/
41
42
43static unsigned s_Truths3[256] =
44{
45 0x00000000, 0x01010101, 0x01010101, 0x03030303, 0x01010101, 0x05050505, 0x06060606, 0x07070707,
46 0x01010101, 0x06060606, 0x05050505, 0x07070707, 0x03030303, 0x07070707, 0x07070707, 0x0f0f0f0f,
47 0x01010101, 0x11111111, 0x12121212, 0x13131313, 0x14141414, 0x15151515, 0x16161616, 0x17171717,
48 0x18181818, 0x19191919, 0x1a1a1a1a, 0x1b1b1b1b, 0x1c1c1c1c, 0x1d1d1d1d, 0x1e1e1e1e, 0x1f1f1f1f,
49 0x01010101, 0x12121212, 0x11111111, 0x13131313, 0x18181818, 0x1a1a1a1a, 0x19191919, 0x1b1b1b1b,
50 0x14141414, 0x16161616, 0x15151515, 0x17171717, 0x1c1c1c1c, 0x1e1e1e1e, 0x1d1d1d1d, 0x1f1f1f1f,
51 0x03030303, 0x13131313, 0x13131313, 0x33333333, 0x1c1c1c1c, 0x35353535, 0x36363636, 0x37373737,
52 0x1c1c1c1c, 0x36363636, 0x35353535, 0x37373737, 0x3c3c3c3c, 0x3d3d3d3d, 0x3d3d3d3d, 0x3f3f3f3f,
53 0x01010101, 0x14141414, 0x18181818, 0x1c1c1c1c, 0x11111111, 0x15151515, 0x19191919, 0x1d1d1d1d,
54 0x12121212, 0x16161616, 0x1a1a1a1a, 0x1e1e1e1e, 0x13131313, 0x17171717, 0x1b1b1b1b, 0x1f1f1f1f,
55 0x05050505, 0x15151515, 0x1a1a1a1a, 0x35353535, 0x15151515, 0x55555555, 0x56565656, 0x57575757,
56 0x1a1a1a1a, 0x56565656, 0x5a5a5a5a, 0x5b5b5b5b, 0x35353535, 0x57575757, 0x5b5b5b5b, 0x5f5f5f5f,
57 0x06060606, 0x16161616, 0x19191919, 0x36363636, 0x19191919, 0x56565656, 0x66666666, 0x67676767,
58 0x16161616, 0x69696969, 0x56565656, 0x6b6b6b6b, 0x36363636, 0x6b6b6b6b, 0x67676767, 0x6f6f6f6f,
59 0x07070707, 0x17171717, 0x1b1b1b1b, 0x37373737, 0x1d1d1d1d, 0x57575757, 0x67676767, 0x77777777,
60 0x1e1e1e1e, 0x6b6b6b6b, 0x5b5b5b5b, 0x7b7b7b7b, 0x3d3d3d3d, 0x7d7d7d7d, 0x7e7e7e7e, 0x7f7f7f7f,
61 0x01010101, 0x18181818, 0x14141414, 0x1c1c1c1c, 0x12121212, 0x1a1a1a1a, 0x16161616, 0x1e1e1e1e,
62 0x11111111, 0x19191919, 0x15151515, 0x1d1d1d1d, 0x13131313, 0x1b1b1b1b, 0x17171717, 0x1f1f1f1f,
63 0x06060606, 0x19191919, 0x16161616, 0x36363636, 0x16161616, 0x56565656, 0x69696969, 0x6b6b6b6b,
64 0x19191919, 0x66666666, 0x56565656, 0x67676767, 0x36363636, 0x67676767, 0x6b6b6b6b, 0x6f6f6f6f,
65 0x05050505, 0x1a1a1a1a, 0x15151515, 0x35353535, 0x1a1a1a1a, 0x5a5a5a5a, 0x56565656, 0x5b5b5b5b,
66 0x15151515, 0x56565656, 0x55555555, 0x57575757, 0x35353535, 0x5b5b5b5b, 0x57575757, 0x5f5f5f5f,
67 0x07070707, 0x1b1b1b1b, 0x17171717, 0x37373737, 0x1e1e1e1e, 0x5b5b5b5b, 0x6b6b6b6b, 0x7b7b7b7b,
68 0x1d1d1d1d, 0x67676767, 0x57575757, 0x77777777, 0x3d3d3d3d, 0x7e7e7e7e, 0x7d7d7d7d, 0x7f7f7f7f,
69 0x03030303, 0x1c1c1c1c, 0x1c1c1c1c, 0x3c3c3c3c, 0x13131313, 0x35353535, 0x36363636, 0x3d3d3d3d,
70 0x13131313, 0x36363636, 0x35353535, 0x3d3d3d3d, 0x33333333, 0x37373737, 0x37373737, 0x3f3f3f3f,
71 0x07070707, 0x1d1d1d1d, 0x1e1e1e1e, 0x3d3d3d3d, 0x17171717, 0x57575757, 0x6b6b6b6b, 0x7d7d7d7d,
72 0x1b1b1b1b, 0x67676767, 0x5b5b5b5b, 0x7e7e7e7e, 0x37373737, 0x77777777, 0x7b7b7b7b, 0x7f7f7f7f,
73 0x07070707, 0x1e1e1e1e, 0x1d1d1d1d, 0x3d3d3d3d, 0x1b1b1b1b, 0x5b5b5b5b, 0x67676767, 0x7e7e7e7e,
74 0x17171717, 0x6b6b6b6b, 0x57575757, 0x7d7d7d7d, 0x37373737, 0x7b7b7b7b, 0x77777777, 0x7f7f7f7f,
75 0x0f0f0f0f, 0x1f1f1f1f, 0x1f1f1f1f, 0x3f3f3f3f, 0x1f1f1f1f, 0x5f5f5f5f, 0x6f6f6f6f, 0x7f7f7f7f,
76 0x1f1f1f1f, 0x6f6f6f6f, 0x5f5f5f5f, 0x7f7f7f7f, 0x3f3f3f3f, 0x7f7f7f7f, 0x7f7f7f7f, 0xffffffff
77};
78
79static char s_Phases3[256][9] =
80{
81/* 0 */ { 8, 0, 1, 2, 3, 4, 5, 6, 7 },
82/* 1 */ { 1, 0 },
83/* 2 */ { 1, 1 },
84/* 3 */ { 2, 0, 1 },
85/* 4 */ { 1, 2 },
86/* 5 */ { 2, 0, 2 },
87/* 6 */ { 2, 0, 3 },
88/* 7 */ { 1, 0 },
89/* 8 */ { 1, 3 },
90/* 9 */ { 2, 1, 2 },
91/* 10 */ { 2, 1, 3 },
92/* 11 */ { 1, 1 },
93/* 12 */ { 2, 2, 3 },
94/* 13 */ { 1, 2 },
95/* 14 */ { 1, 3 },
96/* 15 */ { 4, 0, 1, 2, 3 },
97/* 16 */ { 1, 4 },
98/* 17 */ { 2, 0, 4 },
99/* 18 */ { 2, 0, 5 },
100/* 19 */ { 1, 0 },
101/* 20 */ { 2, 0, 6 },
102/* 21 */ { 1, 0 },
103/* 22 */ { 1, 0 },
104/* 23 */ { 1, 0 },
105/* 24 */ { 2, 0, 7 },
106/* 25 */ { 1, 0 },
107/* 26 */ { 1, 0 },
108/* 27 */ { 1, 0 },
109/* 28 */ { 1, 0 },
110/* 29 */ { 1, 0 },
111/* 30 */ { 1, 0 },
112/* 31 */ { 1, 0 },
113/* 32 */ { 1, 5 },
114/* 33 */ { 2, 1, 4 },
115/* 34 */ { 2, 1, 5 },
116/* 35 */ { 1, 1 },
117/* 36 */ { 2, 1, 6 },
118/* 37 */ { 1, 1 },
119/* 38 */ { 1, 1 },
120/* 39 */ { 1, 1 },
121/* 40 */ { 2, 1, 7 },
122/* 41 */ { 1, 1 },
123/* 42 */ { 1, 1 },
124/* 43 */ { 1, 1 },
125/* 44 */ { 1, 1 },
126/* 45 */ { 1, 1 },
127/* 46 */ { 1, 1 },
128/* 47 */ { 1, 1 },
129/* 48 */ { 2, 4, 5 },
130/* 49 */ { 1, 4 },
131/* 50 */ { 1, 5 },
132/* 51 */ { 4, 0, 1, 4, 5 },
133/* 52 */ { 1, 6 },
134/* 53 */ { 1, 0 },
135/* 54 */ { 1, 0 },
136/* 55 */ { 1, 0 },
137/* 56 */ { 1, 7 },
138/* 57 */ { 1, 1 },
139/* 58 */ { 1, 1 },
140/* 59 */ { 1, 1 },
141/* 60 */ { 4, 0, 1, 6, 7 },
142/* 61 */ { 1, 0 },
143/* 62 */ { 1, 1 },
144/* 63 */ { 2, 0, 1 },
145/* 64 */ { 1, 6 },
146/* 65 */ { 2, 2, 4 },
147/* 66 */ { 2, 2, 5 },
148/* 67 */ { 1, 2 },
149/* 68 */ { 2, 2, 6 },
150/* 69 */ { 1, 2 },
151/* 70 */ { 1, 2 },
152/* 71 */ { 1, 2 },
153/* 72 */ { 2, 2, 7 },
154/* 73 */ { 1, 2 },
155/* 74 */ { 1, 2 },
156/* 75 */ { 1, 2 },
157/* 76 */ { 1, 2 },
158/* 77 */ { 1, 2 },
159/* 78 */ { 1, 2 },
160/* 79 */ { 1, 2 },
161/* 80 */ { 2, 4, 6 },
162/* 81 */ { 1, 4 },
163/* 82 */ { 1, 5 },
164/* 83 */ { 1, 4 },
165/* 84 */ { 1, 6 },
166/* 85 */ { 4, 0, 2, 4, 6 },
167/* 86 */ { 1, 0 },
168/* 87 */ { 1, 0 },
169/* 88 */ { 1, 7 },
170/* 89 */ { 1, 2 },
171/* 90 */ { 4, 0, 2, 5, 7 },
172/* 91 */ { 1, 0 },
173/* 92 */ { 1, 6 },
174/* 93 */ { 1, 2 },
175/* 94 */ { 1, 2 },
176/* 95 */ { 2, 0, 2 },
177/* 96 */ { 2, 4, 7 },
178/* 97 */ { 1, 4 },
179/* 98 */ { 1, 5 },
180/* 99 */ { 1, 4 },
181/* 100 */ { 1, 6 },
182/* 101 */ { 1, 4 },
183/* 102 */ { 4, 0, 3, 4, 7 },
184/* 103 */ { 1, 0 },
185/* 104 */ { 1, 7 },
186/* 105 */ { 4, 0, 3, 5, 6 },
187/* 106 */ { 1, 7 },
188/* 107 */ { 1, 0 },
189/* 108 */ { 1, 7 },
190/* 109 */ { 1, 3 },
191/* 110 */ { 1, 3 },
192/* 111 */ { 2, 0, 3 },
193/* 112 */ { 1, 4 },
194/* 113 */ { 1, 4 },
195/* 114 */ { 1, 5 },
196/* 115 */ { 1, 4 },
197/* 116 */ { 1, 6 },
198/* 117 */ { 1, 4 },
199/* 118 */ { 1, 4 },
200/* 119 */ { 2, 0, 4 },
201/* 120 */ { 1, 7 },
202/* 121 */ { 1, 5 },
203/* 122 */ { 1, 5 },
204/* 123 */ { 2, 0, 5 },
205/* 124 */ { 1, 6 },
206/* 125 */ { 2, 0, 6 },
207/* 126 */ { 2, 0, 7 },
208/* 127 */ { 1, 0 },
209/* 128 */ { 1, 7 },
210/* 129 */ { 2, 3, 4 },
211/* 130 */ { 2, 3, 5 },
212/* 131 */ { 1, 3 },
213/* 132 */ { 2, 3, 6 },
214/* 133 */ { 1, 3 },
215/* 134 */ { 1, 3 },
216/* 135 */ { 1, 3 },
217/* 136 */ { 2, 3, 7 },
218/* 137 */ { 1, 3 },
219/* 138 */ { 1, 3 },
220/* 139 */ { 1, 3 },
221/* 140 */ { 1, 3 },
222/* 141 */ { 1, 3 },
223/* 142 */ { 1, 3 },
224/* 143 */ { 1, 3 },
225/* 144 */ { 2, 5, 6 },
226/* 145 */ { 1, 4 },
227/* 146 */ { 1, 5 },
228/* 147 */ { 1, 5 },
229/* 148 */ { 1, 6 },
230/* 149 */ { 1, 6 },
231/* 150 */ { 4, 1, 2, 4, 7 },
232/* 151 */ { 1, 1 },
233/* 152 */ { 1, 7 },
234/* 153 */ { 4, 1, 2, 5, 6 },
235/* 154 */ { 1, 5 },
236/* 155 */ { 1, 1 },
237/* 156 */ { 1, 6 },
238/* 157 */ { 1, 2 },
239/* 158 */ { 1, 2 },
240/* 159 */ { 2, 1, 2 },
241/* 160 */ { 2, 5, 7 },
242/* 161 */ { 1, 4 },
243/* 162 */ { 1, 5 },
244/* 163 */ { 1, 5 },
245/* 164 */ { 1, 6 },
246/* 165 */ { 4, 1, 3, 4, 6 },
247/* 166 */ { 1, 3 },
248/* 167 */ { 1, 1 },
249/* 168 */ { 1, 7 },
250/* 169 */ { 1, 1 },
251/* 170 */ { 4, 1, 3, 5, 7 },
252/* 171 */ { 1, 1 },
253/* 172 */ { 1, 7 },
254/* 173 */ { 1, 3 },
255/* 174 */ { 1, 3 },
256/* 175 */ { 2, 1, 3 },
257/* 176 */ { 1, 5 },
258/* 177 */ { 1, 4 },
259/* 178 */ { 1, 5 },
260/* 179 */ { 1, 5 },
261/* 180 */ { 1, 6 },
262/* 181 */ { 1, 4 },
263/* 182 */ { 1, 4 },
264/* 183 */ { 2, 1, 4 },
265/* 184 */ { 1, 7 },
266/* 185 */ { 1, 5 },
267/* 186 */ { 1, 5 },
268/* 187 */ { 2, 1, 5 },
269/* 188 */ { 1, 7 },
270/* 189 */ { 2, 1, 6 },
271/* 190 */ { 2, 1, 7 },
272/* 191 */ { 1, 1 },
273/* 192 */ { 2, 6, 7 },
274/* 193 */ { 1, 4 },
275/* 194 */ { 1, 5 },
276/* 195 */ { 4, 2, 3, 4, 5 },
277/* 196 */ { 1, 6 },
278/* 197 */ { 1, 2 },
279/* 198 */ { 1, 3 },
280/* 199 */ { 1, 2 },
281/* 200 */ { 1, 7 },
282/* 201 */ { 1, 2 },
283/* 202 */ { 1, 3 },
284/* 203 */ { 1, 3 },
285/* 204 */ { 4, 2, 3, 6, 7 },
286/* 205 */ { 1, 2 },
287/* 206 */ { 1, 3 },
288/* 207 */ { 2, 2, 3 },
289/* 208 */ { 1, 6 },
290/* 209 */ { 1, 4 },
291/* 210 */ { 1, 5 },
292/* 211 */ { 1, 4 },
293/* 212 */ { 1, 6 },
294/* 213 */ { 1, 6 },
295/* 214 */ { 1, 7 },
296/* 215 */ { 2, 2, 4 },
297/* 216 */ { 1, 7 },
298/* 217 */ { 1, 6 },
299/* 218 */ { 1, 7 },
300/* 219 */ { 2, 2, 5 },
301/* 220 */ { 1, 6 },
302/* 221 */ { 2, 2, 6 },
303/* 222 */ { 2, 2, 7 },
304/* 223 */ { 1, 2 },
305/* 224 */ { 1, 7 },
306/* 225 */ { 1, 4 },
307/* 226 */ { 1, 5 },
308/* 227 */ { 1, 5 },
309/* 228 */ { 1, 6 },
310/* 229 */ { 1, 6 },
311/* 230 */ { 1, 7 },
312/* 231 */ { 2, 3, 4 },
313/* 232 */ { 1, 7 },
314/* 233 */ { 1, 6 },
315/* 234 */ { 1, 7 },
316/* 235 */ { 2, 3, 5 },
317/* 236 */ { 1, 7 },
318/* 237 */ { 2, 3, 6 },
319/* 238 */ { 2, 3, 7 },
320/* 239 */ { 1, 3 },
321/* 240 */ { 4, 4, 5, 6, 7 },
322/* 241 */ { 1, 4 },
323/* 242 */ { 1, 5 },
324/* 243 */ { 2, 4, 5 },
325/* 244 */ { 1, 6 },
326/* 245 */ { 2, 4, 6 },
327/* 246 */ { 2, 4, 7 },
328/* 247 */ { 1, 4 },
329/* 248 */ { 1, 7 },
330/* 249 */ { 2, 5, 6 },
331/* 250 */ { 2, 5, 7 },
332/* 251 */ { 1, 5 },
333/* 252 */ { 2, 6, 7 },
334/* 253 */ { 1, 6 },
335/* 254 */ { 1, 7 },
336/* 255 */ { 8, 0, 1, 2, 3, 4, 5, 6, 7 }
337};
338
339
340/*---------------------------------------------------------------------------*/
341/* Macro declarations */
342/*---------------------------------------------------------------------------*/
343
344
346
347/*---------------------------------------------------------------------------*/
348/* Static function prototypes */
349/*---------------------------------------------------------------------------*/
350
351static int Extra_TruthCanonN_rec( int nVars, unsigned char * pt, unsigned ** pptRes, char ** ppfRes, int Flag );
352
354
355/*---------------------------------------------------------------------------*/
356/* Definition of exported functions */
357/*---------------------------------------------------------------------------*/
358
374int Extra_TruthCanonFastN( int nVarsMax, int nVarsReal, unsigned * pt, unsigned ** pptRes, char ** ppfRes )
375{
376 static unsigned uTruthStore6[2];
377 int RetValue;
378 assert( nVarsMax <= 6 );
379 assert( nVarsReal <= nVarsMax );
380 RetValue = Extra_TruthCanonN_rec( nVarsReal <= 3? 3: nVarsReal, (unsigned char *)pt, pptRes, ppfRes, 0 );
381 if ( nVarsMax == 6 && nVarsReal < nVarsMax )
382 {
383 uTruthStore6[0] = **pptRes;
384 uTruthStore6[1] = **pptRes;
385 *pptRes = uTruthStore6;
386 }
387 return RetValue;
388}
389
390/*---------------------------------------------------------------------------*/
391/* Definition of internal functions */
392/*---------------------------------------------------------------------------*/
393
406int Extra_TruthCanonN_rec( int nVars, unsigned char * pt, unsigned ** pptRes, char ** ppfRes, int Flag )
407{
408 static unsigned uTruthStore[7][2][2];
409 static char uPhaseStore[7][2][64];
410
411 unsigned char * pt0, * pt1;
412 unsigned * ptRes0, * ptRes1, * ptRes;
413 unsigned uInit0, uInit1, uTruth0, uTruth1, uTemp;
414 char * pfRes0, * pfRes1, * pfRes;
415 int nf0, nf1, nfRes, i, nVarsN;
416
417 // table lookup for three vars
418 if ( nVars == 3 )
419 {
420 *pptRes = &s_Truths3[*pt];
421 *ppfRes = s_Phases3[*pt]+1;
422 return s_Phases3[*pt][0];
423 }
424
425 // number of vars for the next call
426 nVarsN = nVars-1;
427 // truth table for the next call
428 pt0 = pt;
429 pt1 = pt + (1 << nVarsN) / 8;
430 // 5-var truth tables for this call
431// uInit0 = *((unsigned *)pt0);
432// uInit1 = *((unsigned *)pt1);
433 if ( nVarsN == 3 )
434 {
435 uInit0 = (pt0[0] << 24) | (pt0[0] << 16) | (pt0[0] << 8) | pt0[0];
436 uInit1 = (pt1[0] << 24) | (pt1[0] << 16) | (pt1[0] << 8) | pt1[0];
437 }
438 else if ( nVarsN == 4 )
439 {
440 uInit0 = (pt0[1] << 24) | (pt0[0] << 16) | (pt0[1] << 8) | pt0[0];
441 uInit1 = (pt1[1] << 24) | (pt1[0] << 16) | (pt1[1] << 8) | pt1[0];
442 }
443 else
444 {
445 uInit0 = (pt0[3] << 24) | (pt0[2] << 16) | (pt0[1] << 8) | pt0[0];
446 uInit1 = (pt1[3] << 24) | (pt1[2] << 16) | (pt1[1] << 8) | pt1[0];
447 }
448
449 // storage for truth tables and phases
450 ptRes = uTruthStore[nVars][Flag];
451 pfRes = uPhaseStore[nVars][Flag];
452
453 // solve trivial cases
454 if ( uInit1 == 0 )
455 {
456 nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 );
457 uTruth1 = uInit1;
458 uTruth0 = *ptRes0;
459 nfRes = 0;
460 for ( i = 0; i < nf0; i++ )
461 pfRes[nfRes++] = pfRes0[i];
462 goto finish;
463 }
464 if ( uInit0 == 0 )
465 {
466 nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 );
467 uTruth1 = uInit0;
468 uTruth0 = *ptRes1;
469 nfRes = 0;
470 for ( i = 0; i < nf1; i++ )
471 pfRes[nfRes++] = pfRes1[i] | (1<<nVarsN);
472 goto finish;
473 }
474
475 if ( uInit1 == 0xFFFFFFFF )
476 {
477 nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 );
478 uTruth1 = *ptRes0;
479 uTruth0 = uInit1;
480 nfRes = 0;
481 for ( i = 0; i < nf0; i++ )
482 pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
483 goto finish;
484 }
485 if ( uInit0 == 0xFFFFFFFF )
486 {
487 nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 );
488 uTruth1 = *ptRes1;
489 uTruth0 = uInit0;
490 nfRes = 0;
491 for ( i = 0; i < nf1; i++ )
492 pfRes[nfRes++] = pfRes1[i];
493 goto finish;
494 }
495
496 // solve the problem for cofactors
497 nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 );
498 nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 );
499
500 // combine the result
501 if ( *ptRes1 < *ptRes0 )
502 {
503 uTruth0 = 0xFFFFFFFF;
504 nfRes = 0;
505 for ( i = 0; i < nf1; i++ )
506 {
507 uTemp = Extra_TruthPolarize( uInit0, pfRes1[i], nVarsN );
508 if ( uTruth0 > uTemp )
509 {
510 nfRes = 0;
511 uTruth0 = uTemp;
512 pfRes[nfRes++] = pfRes1[i];
513 }
514 else if ( uTruth0 == uTemp )
515 pfRes[nfRes++] = pfRes1[i];
516 }
517 uTruth1 = *ptRes1;
518 }
519 else if ( *ptRes1 > *ptRes0 )
520 {
521 uTruth0 = 0xFFFFFFFF;
522 nfRes = 0;
523 for ( i = 0; i < nf0; i++ )
524 {
525 uTemp = Extra_TruthPolarize( uInit1, pfRes0[i], nVarsN );
526 if ( uTruth0 > uTemp )
527 {
528 nfRes = 0;
529 uTruth0 = uTemp;
530 pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
531 }
532 else if ( uTruth0 == uTemp )
533 pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
534 }
535 uTruth1 = *ptRes0;
536 }
537 else
538 {
539 assert( nf0 == nf1 );
540 nfRes = 0;
541 for ( i = 0; i < nf1; i++ )
542 pfRes[nfRes++] = pfRes1[i];
543 for ( i = 0; i < nf0; i++ )
544 pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
545 uTruth0 = Extra_TruthPolarize( uInit0, pfRes1[0], nVarsN );
546 uTruth1 = *ptRes0;
547 }
548
549finish :
550 if ( nVarsN == 3 )
551 {
552 uTruth0 &= 0xFF;
553 uTruth1 &= 0xFF;
554 uTemp = (uTruth1 << 8) | uTruth0;
555 *ptRes = (uTemp << 16) | uTemp;
556 }
557 else if ( nVarsN == 4 )
558 {
559 uTruth0 &= 0xFFFF;
560 uTruth1 &= 0xFFFF;
561 *ptRes = (uTruth1 << 16) | uTruth0;
562 }
563 else if ( nVarsN == 5 )
564 {
565 *(ptRes+0) = uTruth0;
566 *(ptRes+1) = uTruth1;
567 }
568
569 *pptRes = ptRes;
570 *ppfRes = pfRes;
571 return nfRes;
572}
573
585void Map_Var3Print()
586{
587 extern void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounters );
588
589 unsigned * uCanons;
590 char ** uPhases;
591 char * pCounters;
592 int i, k;
593
594 Extra_Truth3VarN( &uCanons, &uPhases, &pCounters );
595
596 for ( i = 0; i < 256; i++ )
597 {
598 if ( i % 8 == 0 )
599 printf( "\n" );
600 Extra_PrintHex( stdout, uCanons + i, 5 );
601 printf( ", " );
602 }
603 printf( "\n" );
604
605 for ( i = 0; i < 256; i++ )
606 {
607 printf( "%3d */ { %2d, ", i, pCounters[i] );
608 for ( k = 0; k < pCounters[i]; k++ )
609 printf( "%s%d", k? ", ":"", uPhases[i][k] );
610 printf( " }\n" );
611 }
612 printf( "\n" );
613}
614
626void Map_Var3Test()
627{
628 extern void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounters );
629
630 unsigned * uCanons;
631 char ** uPhases;
632 char * pCounters;
633 int i;
634 unsigned * ptRes;
635 char * pfRes;
636 unsigned uTruth;
637 int Count;
638
639 Extra_Truth3VarN( &uCanons, &uPhases, &pCounters );
640
641 for ( i = 0; i < 256; i++ )
642 {
643 uTruth = i;
644 Count = Extra_TruthCanonFastN( 5, 3, &uTruth, &ptRes, &pfRes );
645 }
646}
647
659void Map_Var4Test()
660{
661 extern void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** ppCounters, int PhaseMax );
662
663 unsigned short * uCanons;
664 char ** uPhases;
665 char * pCounters;
666 int i;
667 unsigned * ptRes;
668 char * pfRes;
669 unsigned uTruth;
670 int Count;
671
672 Extra_Truth4VarN( &uCanons, &uPhases, &pCounters, 16 );
673
674 for ( i = 0; i < 256*256; i++ )
675 {
676 uTruth = i;
677 Count = Extra_TruthCanonFastN( 5, 4, &uTruth, &ptRes, &pfRes );
678 }
679}
680
681/*---------------------------------------------------------------------------*/
682/* Definition of static Functions */
683/*---------------------------------------------------------------------------*/
684
688
689
690ABC_NAMESPACE_IMPL_END
691
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
Map_Var3Print
void Map_Var3Print()
Definition extraUtilCanon.c:585
Map_Var4Test
void Map_Var4Test()
Definition extraUtilCanon.c:659
Map_Var3Test
void Map_Var3Test()
Definition extraUtilCanon.c:626
Extra_TruthCanonFastN
int Extra_TruthCanonFastN(int nVarsMax, int nVarsReal, unsigned *pt, unsigned **pptRes, char **ppfRes)
Definition extraUtilCanon.c:374
Extra_Truth3VarN
void Extra_Truth3VarN(unsigned **puCanons, char ***puPhases, char **ppCounters)
Definition extraUtilMisc.c:747
Extra_TruthPolarize
unsigned Extra_TruthPolarize(unsigned uTruth, int Polarity, int nVars)
Definition extraUtilMisc.c:401
Extra_Truth4VarN
void Extra_Truth4VarN(unsigned short **puCanons, char ***puPhases, char **ppCounters, int nPhasesMax)
Definition extraUtilMisc.c:815
Extra_PrintHex
void Extra_PrintHex(FILE *pFile, unsigned *pTruth, int nVars)
Definition extraUtilFile.c:643
assert
#define assert(ex)
Definition util_old.h:213