ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cutMerge.c
Go to the documentation of this file.
1
20
21#include "cutInt.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
33
45Cut_Cut_t * Cut_CutMergeTwo2( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
46{
47 static int M[7][3] = {{0},{0},{0},{0},{0},{0},{0}};
48 Cut_Cut_t * pRes;
49 int * pRow;
50 int nLeaves0, nLeaves1, Limit;
51 int i, k, Count, nNodes;
52
53 assert( pCut0->nLeaves >= pCut1->nLeaves );
54
55 // the case of the largest cut sizes
56 Limit = p->pParams->nVarsMax;
57 nLeaves0 = pCut0->nLeaves;
58 nLeaves1 = pCut1->nLeaves;
59 if ( nLeaves0 == Limit && nLeaves1 == Limit )
60 {
61 for ( i = 0; i < nLeaves0; i++ )
62 if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] )
63 return NULL;
64 pRes = Cut_CutAlloc( p );
65 for ( i = 0; i < nLeaves0; i++ )
66 pRes->pLeaves[i] = pCut0->pLeaves[i];
67 pRes->nLeaves = nLeaves0;
68 return pRes;
69 }
70 // the case when one of the cuts is the largest
71 if ( nLeaves0 == Limit )
72 {
73 for ( i = 0; i < nLeaves1; i++ )
74 {
75 for ( k = nLeaves0 - 1; k >= 0; k-- )
76 if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
77 break;
78 if ( k == -1 ) // did not find
79 return NULL;
80 }
81 pRes = Cut_CutAlloc( p );
82 for ( i = 0; i < nLeaves0; i++ )
83 pRes->pLeaves[i] = pCut0->pLeaves[i];
84 pRes->nLeaves = nLeaves0;
85 return pRes;
86 }
87 // other cases
88 nNodes = nLeaves0;
89 for ( i = 0; i < nLeaves1; i++ )
90 {
91 for ( k = nLeaves0 - 1; k >= 0; k-- )
92 {
93 if ( pCut0->pLeaves[k] > pCut1->pLeaves[i] )
94 continue;
95 if ( pCut0->pLeaves[k] < pCut1->pLeaves[i] )
96 {
97 pRow = M[k+1];
98 if ( pRow[0] == 0 )
99 pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
100 else if ( pRow[1] == 0 )
101 pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
102 else if ( pRow[2] == 0 )
103 pRow[2] = pCut1->pLeaves[i];
104 else
105 assert( 0 );
106 if ( ++nNodes > Limit )
107 {
108 for ( i = 0; i <= nLeaves0; i++ )
109 M[i][0] = 0;
110 return NULL;
111 }
112 }
113 break;
114 }
115 if ( k == -1 )
116 {
117 pRow = M[0];
118 if ( pRow[0] == 0 )
119 pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
120 else if ( pRow[1] == 0 )
121 pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
122 else if ( pRow[2] == 0 )
123 pRow[2] = pCut1->pLeaves[i];
124 else
125 assert( 0 );
126 if ( ++nNodes > Limit )
127 {
128 for ( i = 0; i <= nLeaves0; i++ )
129 M[i][0] = 0;
130 return NULL;
131 }
132 continue;
133 }
134 }
135
136 pRes = Cut_CutAlloc( p );
137 for ( Count = 0, i = 0; i <= nLeaves0; i++ )
138 {
139 if ( i > 0 )
140 pRes->pLeaves[Count++] = pCut0->pLeaves[i-1];
141 pRow = M[i];
142 if ( pRow[0] )
143 {
144 pRes->pLeaves[Count++] = pRow[0];
145 if ( pRow[1] )
146 {
147 pRes->pLeaves[Count++] = pRow[1];
148 if ( pRow[2] )
149 pRes->pLeaves[Count++] = pRow[2];
150 }
151 pRow[0] = 0;
152 }
153 }
154 assert( Count == nNodes );
155 pRes->nLeaves = nNodes;
156 return pRes;
157}
158
170Cut_Cut_t * Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
171{
172 Cut_Cut_t * pRes;
173 int * pLeaves;
174 int Limit, nLeaves0, nLeaves1;
175 int i, k, c;
176
177 assert( pCut0->nLeaves >= pCut1->nLeaves );
178
179 // consider two cuts
180 nLeaves0 = pCut0->nLeaves;
181 nLeaves1 = pCut1->nLeaves;
182
183 // the case of the largest cut sizes
184 Limit = p->pParams->nVarsMax;
185 if ( nLeaves0 == Limit && nLeaves1 == Limit )
186 {
187 for ( i = 0; i < nLeaves0; i++ )
188 if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] )
189 return NULL;
190 pRes = Cut_CutAlloc( p );
191 for ( i = 0; i < nLeaves0; i++ )
192 pRes->pLeaves[i] = pCut0->pLeaves[i];
193 pRes->nLeaves = pCut0->nLeaves;
194 return pRes;
195 }
196 // the case when one of the cuts is the largest
197 if ( nLeaves0 == Limit )
198 {
199 for ( i = 0; i < nLeaves1; i++ )
200 {
201 for ( k = nLeaves0 - 1; k >= 0; k-- )
202 if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
203 break;
204 if ( k == -1 ) // did not find
205 return NULL;
206 }
207 pRes = Cut_CutAlloc( p );
208 for ( i = 0; i < nLeaves0; i++ )
209 pRes->pLeaves[i] = pCut0->pLeaves[i];
210 pRes->nLeaves = pCut0->nLeaves;
211 return pRes;
212 }
213
214 // prepare the cut
215 if ( p->pReady == NULL )
216 p->pReady = Cut_CutAlloc( p );
217 pLeaves = p->pReady->pLeaves;
218
219 // compare two cuts with different numbers
220 i = k = 0;
221 for ( c = 0; c < Limit; c++ )
222 {
223 if ( k == nLeaves1 )
224 {
225 if ( i == nLeaves0 )
226 {
227 p->pReady->nLeaves = c;
228 pRes = p->pReady; p->pReady = NULL;
229 return pRes;
230 }
231 pLeaves[c] = pCut0->pLeaves[i++];
232 continue;
233 }
234 if ( i == nLeaves0 )
235 {
236 if ( k == nLeaves1 )
237 {
238 p->pReady->nLeaves = c;
239 pRes = p->pReady; p->pReady = NULL;
240 return pRes;
241 }
242 pLeaves[c] = pCut1->pLeaves[k++];
243 continue;
244 }
245 if ( pCut0->pLeaves[i] < pCut1->pLeaves[k] )
246 {
247 pLeaves[c] = pCut0->pLeaves[i++];
248 continue;
249 }
250 if ( pCut0->pLeaves[i] > pCut1->pLeaves[k] )
251 {
252 pLeaves[c] = pCut1->pLeaves[k++];
253 continue;
254 }
255 pLeaves[c] = pCut0->pLeaves[i++];
256 k++;
257 }
258 if ( i < nLeaves0 || k < nLeaves1 )
259 return NULL;
260 p->pReady->nLeaves = c;
261 pRes = p->pReady; p->pReady = NULL;
262 return pRes;
263}
264
265
277Cut_Cut_t * Cut_CutMergeTwo3( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
278{
279 Cut_Cut_t * pRes;
280 int * pLeaves;
281 int Limit, nLeaves0, nLeaves1;
282 int i, k, c;
283
284 assert( pCut0->nLeaves >= pCut1->nLeaves );
285
286 // prepare the cut
287 if ( p->pReady == NULL )
288 p->pReady = Cut_CutAlloc( p );
289 pLeaves = p->pReady->pLeaves;
290
291 // consider two cuts
292 Limit = p->pParams->nVarsMax;
293 nLeaves0 = pCut0->nLeaves;
294 nLeaves1 = pCut1->nLeaves;
295 if ( nLeaves0 == Limit )
296 { // the case when one of the cuts is the largest
297 if ( nLeaves1 == Limit )
298 { // the case when both cuts are the largest
299 for ( i = 0; i < nLeaves0; i++ )
300 {
301 pLeaves[i] = pCut0->pLeaves[i];
302 if ( pLeaves[i] != pCut1->pLeaves[i] )
303 return NULL;
304 }
305 }
306 else
307 {
308 for ( i = k = 0; i < nLeaves0; i++ )
309 {
310 pLeaves[i] = pCut0->pLeaves[i];
311 if ( k == (int)nLeaves1 )
312 continue;
313 if ( pLeaves[i] < pCut1->pLeaves[k] )
314 continue;
315 if ( pLeaves[i] == pCut1->pLeaves[k++] )
316 continue;
317 return NULL;
318 }
319 if ( k < nLeaves1 )
320 return NULL;
321 }
322 p->pReady->nLeaves = nLeaves0;
323 pRes = p->pReady; p->pReady = NULL;
324 return pRes;
325 }
326
327 // compare two cuts with different numbers
328 i = k = 0;
329 for ( c = 0; c < Limit; c++ )
330 {
331 if ( k == nLeaves1 )
332 {
333 if ( i == nLeaves0 )
334 {
335 p->pReady->nLeaves = c;
336 pRes = p->pReady; p->pReady = NULL;
337 return pRes;
338 }
339 pLeaves[c] = pCut0->pLeaves[i++];
340 continue;
341 }
342 if ( i == nLeaves0 )
343 {
344 if ( k == nLeaves1 )
345 {
346 p->pReady->nLeaves = c;
347 pRes = p->pReady; p->pReady = NULL;
348 return pRes;
349 }
350 pLeaves[c] = pCut1->pLeaves[k++];
351 continue;
352 }
353 if ( pCut0->pLeaves[i] < pCut1->pLeaves[k] )
354 {
355 pLeaves[c] = pCut0->pLeaves[i++];
356 continue;
357 }
358 if ( pCut0->pLeaves[i] > pCut1->pLeaves[k] )
359 {
360 pLeaves[c] = pCut1->pLeaves[k++];
361 continue;
362 }
363 pLeaves[c] = pCut0->pLeaves[i++];
364 k++;
365 }
366 if ( i < nLeaves0 || k < nLeaves1 )
367 return NULL;
368 p->pReady->nLeaves = c;
369 pRes = p->pReady; p->pReady = NULL;
370 return pRes;
371}
372
384Cut_Cut_t * Cut_CutMergeTwo4( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
385{
386 Cut_Cut_t * pRes;
387 int * pLeaves;
388 int i, k, min, NodeTemp, Limit, nTotal;
389
390 assert( pCut0->nLeaves >= pCut1->nLeaves );
391
392 // prepare the cut
393 if ( p->pReady == NULL )
394 p->pReady = Cut_CutAlloc( p );
395 pLeaves = p->pReady->pLeaves;
396
397 // consider two cuts
398 Limit = p->pParams->nVarsMax;
399 if ( pCut0->nLeaves == (unsigned)Limit )
400 { // the case when one of the cuts is the largest
401 if ( pCut1->nLeaves == (unsigned)Limit )
402 { // the case when both cuts are the largest
403 for ( i = 0; i < (int)pCut0->nLeaves; i++ )
404 {
405 pLeaves[i] = pCut0->pLeaves[i];
406 if ( pLeaves[i] != pCut1->pLeaves[i] )
407 return NULL;
408 }
409 }
410 else
411 {
412 for ( i = k = 0; i < (int)pCut0->nLeaves; i++ )
413 {
414 pLeaves[i] = pCut0->pLeaves[i];
415 if ( k == (int)pCut1->nLeaves )
416 continue;
417 if ( pLeaves[i] < pCut1->pLeaves[k] )
418 continue;
419 if ( pLeaves[i] == pCut1->pLeaves[k++] )
420 continue;
421 return NULL;
422 }
423 if ( k < (int)pCut1->nLeaves )
424 return NULL;
425 }
426 p->pReady->nLeaves = pCut0->nLeaves;
427 pRes = p->pReady; p->pReady = NULL;
428 return pRes;
429 }
430
431 // count the number of unique entries in pCut1
432 nTotal = pCut0->nLeaves;
433 for ( i = 0; i < (int)pCut1->nLeaves; i++ )
434 {
435 // try to find this entry among the leaves of pCut0
436 for ( k = 0; k < (int)pCut0->nLeaves; k++ )
437 if ( pCut1->pLeaves[i] == pCut0->pLeaves[k] )
438 break;
439 if ( k < (int)pCut0->nLeaves ) // found
440 continue;
441 // we found a new entry to add
442 if ( nTotal == Limit )
443 return NULL;
444 pLeaves[nTotal++] = pCut1->pLeaves[i];
445 }
446 // we know that the feasible cut exists
447
448 // add the starting entries
449 for ( k = 0; k < (int)pCut0->nLeaves; k++ )
450 pLeaves[k] = pCut0->pLeaves[k];
451
452 // selection-sort the entries
453 for ( i = 0; i < nTotal - 1; i++ )
454 {
455 min = i;
456 for ( k = i+1; k < nTotal; k++ )
457 if ( pLeaves[k] < pLeaves[min] )
458 min = k;
459 NodeTemp = pLeaves[i];
460 pLeaves[i] = pLeaves[min];
461 pLeaves[min] = NodeTemp;
462 }
463 p->pReady->nLeaves = nTotal;
464 pRes = p->pReady; p->pReady = NULL;
465 return pRes;
466}
467
479Cut_Cut_t * Cut_CutMergeTwo5( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
480{
481 static int M[7][3] = {{0},{0},{0},{0},{0},{0},{0}};
482 Cut_Cut_t * pRes;
483 int * pRow;
484 unsigned uSign0, uSign1;
485 int i, k, nNodes, Count;
486 unsigned Limit = p->pParams->nVarsMax;
487
488 assert( pCut0->nLeaves >= pCut1->nLeaves );
489
490 // the case of the largest cut sizes
491 if ( pCut0->nLeaves == Limit && pCut1->nLeaves == Limit )
492 {
493 for ( i = 0; i < (int)pCut0->nLeaves; i++ )
494 if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] )
495 return NULL;
496 pRes = Cut_CutAlloc( p );
497 for ( i = 0; i < (int)pCut0->nLeaves; i++ )
498 pRes->pLeaves[i] = pCut0->pLeaves[i];
499 pRes->nLeaves = pCut0->nLeaves;
500 return pRes;
501 }
502 // the case when one of the cuts is the largest
503 if ( pCut0->nLeaves == Limit )
504 {
505 if ( !p->pParams->fTruth )
506 {
507 for ( i = 0; i < (int)pCut1->nLeaves; i++ )
508 {
509 for ( k = pCut0->nLeaves - 1; k >= 0; k-- )
510 if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
511 break;
512 if ( k == -1 ) // did not find
513 return NULL;
514 }
515 pRes = Cut_CutAlloc( p );
516 }
517 else
518 {
519 uSign1 = 0;
520 for ( i = 0; i < (int)pCut1->nLeaves; i++ )
521 {
522 for ( k = pCut0->nLeaves - 1; k >= 0; k-- )
523 if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
524 {
525 uSign1 |= (1 << i);
526 break;
527 }
528 if ( k == -1 ) // did not find
529 return NULL;
530 }
531 pRes = Cut_CutAlloc( p );
532 pRes->Num1 = uSign1;
533 }
534 for ( i = 0; i < (int)pCut0->nLeaves; i++ )
535 pRes->pLeaves[i] = pCut0->pLeaves[i];
536 pRes->nLeaves = pCut0->nLeaves;
537 return pRes;
538 }
539 // other cases
540 nNodes = pCut0->nLeaves;
541 for ( i = 0; i < (int)pCut1->nLeaves; i++ )
542 {
543 for ( k = pCut0->nLeaves - 1; k >= 0; k-- )
544 {
545 if ( pCut0->pLeaves[k] > pCut1->pLeaves[i] )
546 continue;
547 if ( pCut0->pLeaves[k] < pCut1->pLeaves[i] )
548 {
549 pRow = M[k+1];
550 if ( pRow[0] == 0 )
551 pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
552 else if ( pRow[1] == 0 )
553 pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
554 else if ( pRow[2] == 0 )
555 pRow[2] = pCut1->pLeaves[i];
556 else
557 assert( 0 );
558 if ( ++nNodes > (int)Limit )
559 {
560 for ( i = 0; i <= (int)pCut0->nLeaves; i++ )
561 M[i][0] = 0;
562 return NULL;
563 }
564 }
565 break;
566 }
567 if ( k == -1 )
568 {
569 pRow = M[0];
570 if ( pRow[0] == 0 )
571 pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
572 else if ( pRow[1] == 0 )
573 pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
574 else if ( pRow[2] == 0 )
575 pRow[2] = pCut1->pLeaves[i];
576 else
577 assert( 0 );
578 if ( ++nNodes > (int)Limit )
579 {
580 for ( i = 0; i <= (int)pCut0->nLeaves; i++ )
581 M[i][0] = 0;
582 return NULL;
583 }
584 continue;
585 }
586 }
587
588 pRes = Cut_CutAlloc( p );
589 if ( !p->pParams->fTruth )
590 {
591 for ( Count = 0, i = 0; i <= (int)pCut0->nLeaves; i++ )
592 {
593 if ( i > 0 )
594 pRes->pLeaves[Count++] = pCut0->pLeaves[i-1];
595 pRow = M[i];
596 if ( pRow[0] )
597 {
598 pRes->pLeaves[Count++] = pRow[0];
599 if ( pRow[1] )
600 {
601 pRes->pLeaves[Count++] = pRow[1];
602 if ( pRow[2] )
603 pRes->pLeaves[Count++] = pRow[2];
604 }
605 pRow[0] = 0;
606 }
607 }
608 assert( Count == nNodes );
609 pRes->nLeaves = nNodes;
610/*
611 // make sure that the cut is correct
612 {
613 for ( i = 1; i < (int)pRes->nLeaves; i++ )
614 if ( pRes->pLeaves[i-1] >= pRes->pLeaves[i] )
615 {
616 int v = 0;
617 }
618 }
619*/
620 return pRes;
621 }
622
623 uSign0 = uSign1 = 0;
624 for ( Count = 0, i = 0; i <= (int)pCut0->nLeaves; i++ )
625 {
626 if ( i > 0 )
627 {
628 uSign0 |= (1 << Count);
629 pRes->pLeaves[Count++] = pCut1->pLeaves[i-1];
630 }
631 pRow = M[i];
632 if ( pRow[0] )
633 {
634 uSign1 |= (1 << Count);
635 pRes->pLeaves[Count++] = pRow[0];
636 if ( pRow[1] )
637 {
638 uSign1 |= (1 << Count);
639 pRes->pLeaves[Count++] = pRow[1];
640 if ( pRow[2] )
641 {
642 uSign1 |= (1 << Count);
643 pRes->pLeaves[Count++] = pRow[2];
644 }
645 }
646 pRow[0] = 0;
647 }
648 }
649 assert( Count == nNodes );
650 pRes->nLeaves = nNodes;
651 pRes->Num1 = uSign1;
652 pRes->Num0 = uSign0;
653 return pRes;
654}
655
659
660
661ABC_NAMESPACE_IMPL_END
662
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
nTotal
int nTotal
DECLARATIONS ///.
Definition cutTruth.c:37
Cut_CutAlloc
ABC_NAMESPACE_IMPL_START Cut_Cut_t * Cut_CutAlloc(Cut_Man_t *p)
DECLARATIONS ///.
Definition cutCut.c:45
Cut_CutMergeTwo
Cut_Cut_t * Cut_CutMergeTwo(Cut_Man_t *p, Cut_Cut_t *pCut0, Cut_Cut_t *pCut1)
Definition cutMerge.c:170
Cut_CutMergeTwo3
Cut_Cut_t * Cut_CutMergeTwo3(Cut_Man_t *p, Cut_Cut_t *pCut0, Cut_Cut_t *pCut1)
Definition cutMerge.c:277
Cut_CutMergeTwo5
Cut_Cut_t * Cut_CutMergeTwo5(Cut_Man_t *p, Cut_Cut_t *pCut0, Cut_Cut_t *pCut1)
Definition cutMerge.c:479
Cut_CutMergeTwo4
Cut_Cut_t * Cut_CutMergeTwo4(Cut_Man_t *p, Cut_Cut_t *pCut0, Cut_Cut_t *pCut1)
Definition cutMerge.c:384
Cut_CutMergeTwo2
ABC_NAMESPACE_IMPL_START Cut_Cut_t * Cut_CutMergeTwo2(Cut_Man_t *p, Cut_Cut_t *pCut0, Cut_Cut_t *pCut1)
DECLARATIONS ///.
Definition cutMerge.c:45
Cut_Man_t
struct Cut_ManStruct_t_ Cut_Man_t
BASIC TYPES ///.
Definition cut.h:48
Cut_Cut_t
struct Cut_CutStruct_t_ Cut_Cut_t
Definition cut.h:50
p
Cube * p
Definition exorList.c:222
M
word M(word f1, word f2, int n)
Definition kitPerm.c:240
Cut_CutStruct_t_::Num1
unsigned Num1
Definition cut.h:80
Cut_CutStruct_t_::Num0
unsigned Num0
Definition cut.h:79
Cut_CutStruct_t_::pLeaves
int pLeaves[0]
Definition cut.h:89
Cut_CutStruct_t_::nLeaves
unsigned nLeaves
Definition cut.h:84
assert
#define assert(ex)
Definition util_old.h:213