ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
rsbDec6.c
Go to the documentation of this file.
1
20
21#include "rsbInt.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
33
45static inline unsigned Rsb_DecTry0( word c )
46{
47 return (unsigned)(c != 0);
48}
49static inline unsigned Rsb_DecTry1( word c, word f1 )
50{
51 return (Rsb_DecTry0(c&f1) << 1) | Rsb_DecTry0(c&~f1);
52}
53static inline unsigned Rsb_DecTry2( word c, word f1, word f2 )
54{
55 return (Rsb_DecTry1(c&f2, f1) << 2) | Rsb_DecTry1(c&~f2, f1);
56}
57static inline unsigned Rsb_DecTry3( word c, word f1, word f2, word f3 )
58{
59 return (Rsb_DecTry2(c&f3, f1, f2) << 4) | Rsb_DecTry2(c&~f3, f1, f2);
60}
61static inline unsigned Rsb_DecTry4( word c, word f1, word f2, word f3, word f4 )
62{
63 return (Rsb_DecTry3(c&f4, f1, f2, f3) << 8) | Rsb_DecTry3(c&~f4, f1, f2, f3);
64}
65static inline unsigned Rsb_DecTry5( word c, word f1, word f2, word f3, word f4, word f5 )
66{
67 return (Rsb_DecTry4(c&f5, f1, f2, f3, f4) << 16) | Rsb_DecTry4(c&~f5, f1, f2, f3, f4);
68}
69
81static inline int Rsb_DecTryCex( word * g, int iCexA, int iCexB )
82{
83 return Abc_TtGetBit(g, iCexA) == Abc_TtGetBit(g, iCexB);
84}
85static inline void Rsb_DecVerifyCex( word * f, word ** g, int nGs, int iCexA, int iCexB )
86{
87 int i;
88 // f distinquished it
89 if ( Rsb_DecTryCex( f, iCexA, iCexB ) )
90 printf( "Verification of CEX has failed: f(A) == f(B)!!!\n" );
91 // g do not distinguish it
92 for ( i = 0; i < nGs; i++ )
93 if ( !Rsb_DecTryCex( g[i], iCexA, iCexB ) )
94 printf( "Verification of CEX has failed: g[%d](A) != g[%d](B)!!!\n", i, i );
95}
96static inline void Rsb_DecRecordCex( word ** g, int nGs, int iCexA, int iCexB, word * pCexes, int nCexes )
97{
98 int i;
99 assert( nCexes < 64 );
100 for ( i = 0; i < nGs; i++ )
101 if ( Rsb_DecTryCex(g[i], iCexA, iCexB) )
102 Abc_TtSetBit( pCexes + i, nCexes );
103}
104
116static inline word Rsb_DecCofactor( word ** g, int nGs, int w, int iMint )
117{
118 int i;
119 word Cof = ~(word)0;
120 for ( i = 0; i < nGs; i++ )
121 Cof &= ((iMint >> i) & 1) ? g[i][w] : ~g[i][w];
122 return Cof;
123}
124unsigned Rsb_DecCheck( int nVars, word * f, word ** g, int nGs, unsigned * pPat, int * pCexA, int * pCexB )
125{
126 word CofA, CofB;
127 int nWords = Abc_TtWordNum( nVars );
128 int w, k, iMint, iShift = ( 1 << nGs );
129 unsigned uMask = (~(unsigned)0) >> (32-iShift);
130 unsigned uTotal = 0;
131 assert( nGs > 0 && nGs < 5 );
132 for ( w = 0; w < nWords; w++ )
133 {
134 // generate decomposition pattern
135 if ( nGs == 1 )
136 pPat[w] = Rsb_DecTry2( ~(word)0, g[0][w], f[w] );
137 else if ( nGs == 2 )
138 pPat[w] = Rsb_DecTry3( ~(word)0, g[0][w], g[1][w], f[w] );
139 else if ( nGs == 3 )
140 pPat[w] = Rsb_DecTry4( ~(word)0, g[0][w], g[1][w], g[2][w], f[w] );
141 else if ( nGs == 4 )
142 pPat[w] = Rsb_DecTry5( ~(word)0, g[0][w], g[1][w], g[2][w], g[3][w], f[w] );
143 // check if it is consistent
144 iMint = Abc_Tt6FirstBit( (pPat[w] >> iShift) & pPat[w] & uMask );
145 if ( iMint >= 0 )
146 { // generate a cex
147 CofA = Rsb_DecCofactor( g, nGs, w, iMint );
148 assert( (~f[w] & CofA) && (f[w] & CofA) );
149 *pCexA = w * 64 + Abc_Tt6FirstBit( ~f[w] & CofA );
150 *pCexB = w * 64 + Abc_Tt6FirstBit( f[w] & CofA );
151 return 0;
152 }
153 uTotal |= pPat[w];
154 if ( w == 0 )
155 continue;
156 // check if it is consistent with other patterns seen so far
157 iMint = Abc_Tt6FirstBit( (uTotal >> iShift) & uTotal & uMask );
158 if ( iMint == -1 )
159 continue;
160 // find an overlap and generate a cex
161 for ( k = 0; k < w; k++ )
162 {
163 iMint = Abc_Tt6FirstBit( ((pPat[k] | pPat[w]) >> iShift) & (pPat[k] | pPat[w]) & uMask );
164 if ( iMint == -1 )
165 continue;
166 CofA = Rsb_DecCofactor( g, nGs, k, iMint );
167 CofB = Rsb_DecCofactor( g, nGs, w, iMint );
168 if ( (~f[k] & CofA) && (f[w] & CofB) )
169 {
170 *pCexA = k * 64 + Abc_Tt6FirstBit( ~f[k] & CofA );
171 *pCexB = w * 64 + Abc_Tt6FirstBit( f[w] & CofB );
172 }
173 else
174 {
175 assert( (f[k] & CofA) && (~f[w] & CofB) );
176 *pCexA = k * 64 + Abc_Tt6FirstBit( f[k] & CofA );
177 *pCexB = w * 64 + Abc_Tt6FirstBit( ~f[w] & CofB );
178 }
179 return 0;
180 }
181 }
182 return uTotal;
183}
184
196void Rsb_DecPrintTable( word * pCexes, int nGs, int nGsAll, Vec_Int_t * vTries )
197{
198 int pCands[16], nCands;
199 int i, c, Cand, iStart = 0;
200 if ( Vec_IntSize(vTries) == 0 )
201 return;
202
203// printf( "\n" );
204 for ( i = 0; i < 4; i++ )
205 printf( " " );
206 printf( " " );
207 for ( i = 0; i < nGs; i++ )
208 printf( "%d", (i % 100) / 10 );
209 printf( "|" );
210 for ( ; i < nGsAll; i++ )
211 printf( "%d", (i % 100) / 10 );
212 printf( "\n" );
213
214 for ( i = 0; i < 4; i++ )
215 printf( " " );
216 printf( " " );
217 for ( i = 0; i < nGs; i++ )
218 printf( "%d", i % 10 );
219 printf( "|" );
220 for ( ; i < nGsAll; i++ )
221 printf( "%d", i % 10 );
222 printf( "\n" );
223 printf( "\n" );
224
225 for ( c = 0; iStart < Vec_IntSize(vTries); c++ )
226 {
227 // collect candidates
228 for ( i = 0; i < 4; i++ )
229 pCands[i] = -1;
230 nCands = 0;
231 Vec_IntForEachEntryStart( vTries, Cand, i, iStart )
232 if ( Cand == -1 )
233 {
234 iStart = i + 1;
235 break;
236 }
237 else
238 pCands[nCands++] = Cand;
239 assert( nCands <= 4 );
240 // print them
241 for ( i = 0; i < 4; i++ )
242 if ( pCands[i] >= 0 )
243 printf( "%4d", pCands[i] );
244 else
245 printf( " " );
246 // print the bit-string
247 printf( " " );
248 for ( i = 0; i < nGs; i++ )
249 printf( "%c", Abc_TtGetBit( pCexes + i, c ) ? '.' : '+' );
250 printf( "|" );
251 for ( ; i < nGsAll; i++ )
252 printf( "%c", Abc_TtGetBit( pCexes + i, c ) ? '.' : '+' );
253 printf( " %3d\n", c );
254 }
255 printf( "\n" );
256
257 // write the number of ones
258 for ( i = 0; i < 4; i++ )
259 printf( " " );
260 printf( " " );
261 for ( i = 0; i < nGs; i++ )
262 printf( "%d", Abc_TtCountOnes(pCexes[i]) / 10 );
263 printf( "|" );
264 for ( ; i < nGsAll; i++ )
265 printf( "%d", Abc_TtCountOnes(pCexes[i]) / 10 );
266 printf( "\n" );
267
268 for ( i = 0; i < 4; i++ )
269 printf( " " );
270 printf( " " );
271 for ( i = 0; i < nGs; i++ )
272 printf( "%d", Abc_TtCountOnes(pCexes[i]) % 10 );
273 printf( "|" );
274 for ( ; i < nGsAll; i++ )
275 printf( "%d", Abc_TtCountOnes(pCexes[i]) % 10 );
276 printf( "\n" );
277 printf( "\n" );
278}
279
292int Rsb_DecInitCexes( int nVars, word * f, word ** g, int nGs, int nGsAll, word * pCexes, Vec_Int_t * vTries )
293{
294 int nWords = Abc_TtWordNum( nVars );
295 int ValueB = Abc_TtGetBit( f, 0 );
296 int ValueE = Abc_TtGetBit( f, 64*nWords-1 );
297 int iCexT0, iCexT1, iCexF0, iCexF1;
298
299 iCexT0 = ValueB ? 0 : Abc_TtFindFirstBit( f, nVars );
300 iCexT1 = ValueE ? 64*nWords-1 : Abc_TtFindLastBit( f, nVars );
301
302 iCexF0 = !ValueB ? 0 : Abc_TtFindFirstZero( f, nVars );
303 iCexF1 = !ValueE ? 64*nWords-1 : Abc_TtFindLastZero( f, nVars );
304
305 assert( !Rsb_DecTryCex( f, iCexT0, iCexF0 ) );
306 assert( !Rsb_DecTryCex( f, iCexT0, iCexF1 ) );
307 assert( !Rsb_DecTryCex( f, iCexT1, iCexF0 ) );
308 assert( !Rsb_DecTryCex( f, iCexT1, iCexF1 ) );
309
310 Rsb_DecRecordCex( g, nGsAll, iCexT0, iCexF0, pCexes, 0 );
311 Rsb_DecRecordCex( g, nGsAll, iCexT0, iCexF1, pCexes, 1 );
312 Rsb_DecRecordCex( g, nGsAll, iCexT1, iCexF0, pCexes, 2 );
313 Rsb_DecRecordCex( g, nGsAll, iCexT1, iCexF1, pCexes, 3 );
314
315 if ( vTries )
316 {
317 Vec_IntPush( vTries, -1 );
318 Vec_IntPush( vTries, -1 );
319 Vec_IntPush( vTries, -1 );
320 Vec_IntPush( vTries, -1 );
321 }
322 return 4;
323}
324
337unsigned Rsb_DecPerformInt( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, int nGsAll, int fFindAll )
338{
339 word * pCexes = Vec_WrdArray(p->vCexes);
340 unsigned * pPat = (unsigned *)Vec_IntArray(p->vDecPats);
341 /*
342 The following filtering hueristic can be used:
343 after the first round (if there is more than 5 cexes,
344 remove all the divisors, except fanins of the node
345 This should lead to a speadup without sacrifying quality.
346
347 Another idea is to precompute several counter-examples
348 like the first and last 0 and 1 mints of the function
349 which yields 4 cexes.
350 */
351
352 word * pDivs[16];
353 unsigned uTruth = 0;
354 int i, k, j, n, iCexA, iCexB, nCexes = 0;
355 memset( pCexes, 0, sizeof(word) * nGsAll );
356 Vec_IntClear( p->vTries );
357 // populate the counter-examples with the three most obvious
358// nCexes = Rsb_DecInitCexes( nVars, f, g, nGs, nGsAll, pCexes, vTries );
359 // start by checking each function
360 p->vFanins->nSize = 1;
361 for ( i = 0; i < nGs; i++ )
362 {
363 if ( pCexes[i] )
364 continue;
365 pDivs[0] = g[i]; p->vFanins->pArray[0] = i;
366 uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
367 if ( uTruth )
368 {
369 if ( fFindAll )
370 {
371 uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 1 );
372 Kit_DsdPrintFromTruth( &uTruth, 1 ); printf( " " );
373 Vec_IntPrint(p->vFanins);
374 continue;
375 }
376 else
377 return uTruth;
378 }
379 if ( nCexes == 64 )
380 return 0;
381 Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
382 Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ );
383 if ( !p->fVerbose )
384 continue;
385 Vec_IntPush( p->vTries, i );
386 Vec_IntPush( p->vTries, -1 );
387 }
388 if ( p->nDecMax == 1 )
389 return 0;
390 // continue by checking pairs
391 p->vFanins->nSize = 2;
392 for ( i = 1; i < nGs; i++ )
393 for ( k = 0; k < i; k++ )
394 {
395 if ( pCexes[i] & pCexes[k] )
396 continue;
397 pDivs[0] = g[i]; p->vFanins->pArray[0] = i;
398 pDivs[1] = g[k]; p->vFanins->pArray[1] = k;
399 uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
400 if ( uTruth )
401 {
402 if ( fFindAll )
403 {
404 uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 2 );
405 Kit_DsdPrintFromTruth( &uTruth, 2 ); printf( " " );
406 Vec_IntPrint(p->vFanins);
407 continue;
408 }
409 else
410 return uTruth;
411 }
412 if ( nCexes == 64 )
413 return 0;
414 Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
415 Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ );
416 if ( !p->fVerbose )
417 continue;
418 Vec_IntPush( p->vTries, i );
419 Vec_IntPush( p->vTries, k );
420 Vec_IntPush( p->vTries, -1 );
421 }
422 if ( p->nDecMax == 2 )
423 return 0;
424 // continue by checking triples
425 p->vFanins->nSize = 3;
426 for ( i = 2; i < nGs; i++ )
427 for ( k = 1; k < i; k++ )
428 for ( j = 0; j < k; j++ )
429 {
430 if ( pCexes[i] & pCexes[k] & pCexes[j] )
431 continue;
432 pDivs[0] = g[i]; p->vFanins->pArray[0] = i;
433 pDivs[1] = g[k]; p->vFanins->pArray[1] = k;
434 pDivs[2] = g[j]; p->vFanins->pArray[2] = j;
435 uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
436 if ( uTruth )
437 {
438 if ( fFindAll )
439 {
440 uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 3 );
441 Kit_DsdPrintFromTruth( &uTruth, 3 ); printf( " " );
442 Vec_IntPrint(p->vFanins);
443 continue;
444 }
445 else
446 return uTruth;
447 }
448 if ( nCexes == 64 )
449 return 0;
450 Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
451 Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ );
452 if ( !p->fVerbose )
453 continue;
454 Vec_IntPush( p->vTries, i );
455 Vec_IntPush( p->vTries, k );
456 Vec_IntPush( p->vTries, j );
457 Vec_IntPush( p->vTries, -1 );
458 }
459 if ( p->nDecMax == 3 )
460 return 0;
461 // continue by checking quadras
462 p->vFanins->nSize = 4;
463 for ( i = 3; i < nGs; i++ )
464 for ( k = 2; k < i; k++ )
465 for ( j = 1; j < k; j++ )
466 for ( n = 0; n < j; n++ )
467 {
468 if ( pCexes[i] & pCexes[k] & pCexes[j] & pCexes[n] )
469 continue;
470 pDivs[0] = g[i]; p->vFanins->pArray[0] = i;
471 pDivs[1] = g[k]; p->vFanins->pArray[1] = k;
472 pDivs[2] = g[j]; p->vFanins->pArray[2] = j;
473 pDivs[3] = g[n]; p->vFanins->pArray[3] = n;
474 uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFanins), pPat, &iCexA, &iCexB );
475 if ( uTruth )
476 {
477 if ( fFindAll )
478 {
479 uTruth = (unsigned)Abc_Tt6Stretch( (word)uTruth, 4 );
480 Kit_DsdPrintFromTruth( &uTruth, 4 ); printf( " " );
481 Vec_IntPrint(p->vFanins);
482 continue;
483 }
484 else
485 return uTruth;
486 }
487 if ( nCexes == 64 )
488 return 0;
489 Rsb_DecVerifyCex( f, pDivs, Vec_IntSize(p->vFanins), iCexA, iCexB );
490 Rsb_DecRecordCex( g, nGsAll, iCexA, iCexB, pCexes, nCexes++ );
491 if ( !p->fVerbose )
492 continue;
493 Vec_IntPush( p->vTries, i );
494 Vec_IntPush( p->vTries, k );
495 Vec_IntPush( p->vTries, j );
496 Vec_IntPush( p->vTries, n );
497 Vec_IntPush( p->vTries, -1 );
498 }
499// printf( "%d ", nCexes );
500 if ( p->nDecMax == 4 )
501 return 0;
502 return 0;
503}
504
516void Rsb_DecPrintFunc( Rsb_Man_t * p, unsigned Truth4, word * f, word ** ppGs, int nGs, int nVarsAll )
517{
518 int nVars = Vec_IntSize(p->vFanins);
519 word Copy = Truth4;
520 word wOn = Abc_Tt6Stretch( Copy >> (1 << nVars), nVars );
521 word wOnDc = ~Abc_Tt6Stretch( Copy, nVars );
522 word wIsop = Abc_Tt6Isop( wOn, wOnDc, nVars, NULL );
523 int i;
524
525 printf( "Offset : " );
526 Abc_TtPrintBinary( &Copy, nVars ); //printf( "\n" );
527 Copy >>= ((word)1 << nVars);
528 printf( "Onset : " );
529 Abc_TtPrintBinary( &Copy, nVars ); //printf( "\n" );
530 printf( "Result : " );
531 Abc_TtPrintBinary( &wIsop, nVars ); //printf( "\n" );
532 Kit_DsdPrintFromTruth( (unsigned *)&wIsop, nVars ); printf( "\n" );
533
534 // print functions
535 printf( "Func : " );
536 Abc_TtPrintBinary( f, nVarsAll ); //printf( "\n" );
537 Kit_DsdPrintFromTruth( (unsigned *)f, nVarsAll ); printf( "\n" );
538 for ( i = 0; i < nGs; i++ )
539 {
540 printf( "Div%3d : ", i );
541 Kit_DsdPrintFromTruth( (unsigned *)ppGs[i], nVarsAll ); printf( "\n" );
542 }
543 printf( "Solution : " );
544 for ( i = 0; i < Vec_IntSize(p->vFanins); i++ )
545 printf( "%d ", Vec_IntEntry(p->vFanins, i) );
546 printf( "\n" );
547}
548
560int Rsb_DecVerify( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, unsigned Truth4, word * pTemp1, word * pTemp2 )
561{
562 word * pFanins[16];
563 int b, m, Num, nSuppSize;
564 int nWords = Abc_TtWordNum(nVars);
565 Truth4 >>= (1 << Vec_IntSize(p->vFanins));
566 Truth4 = (unsigned)Abc_Tt6Stretch( (word)Truth4, Vec_IntSize(p->vFanins) );
567//Kit_DsdPrintFromTruth( (unsigned *)&Truth4, Vec_IntSize(p->vFanins) );
568//printf( "\n" );
569// nSuppSize = Rsb_Word6SupportSize( Truth4 );
570// assert( nSuppSize == Vec_IntSize(p->vFanins) );
571 nSuppSize = Vec_IntSize(p->vFanins);
572 // collect the fanins
573 Vec_IntForEachEntry( p->vFanins, Num, b )
574 {
575 assert( Num < nGs );
576 pFanins[b] = g[Num];
577 }
578 // create the or of ands
579 Abc_TtClear( pTemp1, nWords );
580 for ( m = 0; m < (1<<nSuppSize); m++ )
581 {
582 if ( ((Truth4 >> m) & 1) == 0 )
583 continue;
584 Abc_TtFill( pTemp2, nWords );
585 for ( b = 0; b < nSuppSize; b++ )
586 if ( (m >> b) & 1 )
587 Abc_TtAnd( pTemp2, pTemp2, pFanins[b], nWords, 0 );
588 else
589 Abc_TtSharp( pTemp2, pTemp2, pFanins[b], nWords );
590 Abc_TtOr( pTemp1, pTemp1, pTemp2, nWords );
591 }
592 // check the function
593 if ( !Abc_TtEqual( pTemp1, f, nWords ) )
594 printf( "Verification failed.\n" );
595// else
596// printf( "Verification passed.\n" );
597 return 1;
598}
599
612unsigned Rsb_ManPerform( Rsb_Man_t * p, int nVars, word * f, word ** g, int nGs, int nGsAll, int fVerbose0 )
613{
614 word * pCexes = Vec_WrdArray(p->vCexes);
615 unsigned * pPat = (unsigned *)Vec_IntArray(p->vDecPats);
616 int fVerbose = 0;//(nGs > 40);
617 Vec_Int_t * vTries = NULL;
618 unsigned uTruth;
619
620 // verify original decomposition
621 if ( Vec_IntSize(p->vFaninsOld) && Vec_IntSize(p->vFaninsOld) <= 4 )
622 {
623 word * pDivs[8];
624 int i, Entry, iCexA, iCexB;
625 Vec_IntForEachEntry( p->vFaninsOld, Entry, i )
626 pDivs[i] = g[Entry];
627 uTruth = Rsb_DecCheck( nVars, f, pDivs, Vec_IntSize(p->vFaninsOld), pPat, &iCexA, &iCexB );
628// assert( uTruth != 0 );
629 if ( fVerbose )
630 {
631 printf( "Verified orig decomp with %d vars {", Vec_IntSize(p->vFaninsOld) );
632 Vec_IntForEachEntry( p->vFaninsOld, Entry, i )
633 printf( " %d", Entry );
634 printf( " }\n" );
635 }
636 if ( uTruth )
637 {
638// if ( fVerbose )
639// Rsb_DecPrintFunc( p, uTruth );
640 }
641 else
642 {
643 printf( "Verified orig decomp with %d vars {", Vec_IntSize(p->vFaninsOld) );
644 Vec_IntForEachEntry( p->vFaninsOld, Entry, i )
645 printf( " %d", Entry );
646 printf( " }\n" );
647 printf( "Verification FAILED.\n" );
648 }
649 }
650 // start tries
651if ( fVerbose )
652vTries = Vec_IntAlloc( 100 );
653 assert( nGs < nGsAll );
654 uTruth = Rsb_DecPerformInt( p, nVars, f, g, nGs, nGsAll, 0 );
655
656 if ( uTruth )
657 {
658 if ( fVerbose )
659 {
660 int i, Entry;
661 printf( "Found decomp with %d vars {", Vec_IntSize(p->vFanins) );
662 Vec_IntForEachEntry( p->vFanins, Entry, i )
663 printf( " %d", Entry );
664 printf( " }\n" );
665// Rsb_DecPrintFunc( p, uTruth );
666// Rsb_DecVerify( nVars, f, g, nGs, p->vFanins, uTruth, g[nGsAll], g[nGsAll+1] );
667 }
668 }
669 else
670 {
671 Vec_IntShrink( p->vFanins, 0 );
672 if ( fVerbose )
673 printf( "Did not find decomposition with 4 variables.\n" );
674 }
675
676if ( fVerbose )
677Rsb_DecPrintTable( pCexes, nGs, nGsAll, vTries );
678if ( fVerbose )
679Vec_IntFree( vTries );
680 return uTruth;
681}
682
694int Rsb_ManPerformResub6( Rsb_Man_t * p, int nVarsAll, word uTruth, Vec_Wrd_t * vDivTruths, word * puTruth0, word * puTruth1, int fVerbose )
695{
696 word * pGs[200];
697 unsigned uTruthRes;
698 int i, nVars, nGs = Vec_WrdSize(vDivTruths);
699 assert( nGs < 200 );
700 for ( i = 0; i < nGs; i++ )
701 pGs[i] = Vec_WrdEntryP(vDivTruths,i);
702 uTruthRes = Rsb_DecPerformInt( p, nVarsAll, &uTruth, pGs, nGs, nGs, 0 );
703 if ( uTruthRes == 0 )
704 return 0;
705
706 if ( fVerbose )
707 Rsb_DecPrintFunc( p, uTruthRes, &uTruth, pGs, nGs, nVarsAll );
708 if ( fVerbose )
709 Rsb_DecPrintTable( Vec_WrdArray(p->vCexes), nGs, nGs, p->vTries );
710
711 nVars = Vec_IntSize(p->vFanins);
712 *puTruth0 = Abc_Tt6Stretch( uTruthRes, nVars );
713 *puTruth1 = Abc_Tt6Stretch( uTruthRes >> (1 << nVars), nVars );
714 return 1;
715}
716
728void Rsb_ManPerformResub6Test()
729{
730 Rsb_Man_t * p;
731 Vec_Wrd_t * vDivTruths;
732 int RetValue;
733 word a = s_Truths6[0];
734 word b = s_Truths6[1];
735 word c = s_Truths6[2];
736 word d = s_Truths6[3];
737 word e = s_Truths6[4];
738 word f = s_Truths6[5];
739 word ab = a & b;
740 word cd = c & d;
741 word ef = e & f;
742 word F = ab | cd | ef;
743 word uTruth0, uTruth1;
744
745 vDivTruths = Vec_WrdAlloc( 100 );
746 Vec_WrdPush( vDivTruths, a );
747 Vec_WrdPush( vDivTruths, b );
748 Vec_WrdPush( vDivTruths, c );
749 Vec_WrdPush( vDivTruths, d );
750 Vec_WrdPush( vDivTruths, e );
751 Vec_WrdPush( vDivTruths, f );
752 Vec_WrdPush( vDivTruths, ab );
753 Vec_WrdPush( vDivTruths, cd );
754 Vec_WrdPush( vDivTruths, ef );
755
756 p = Rsb_ManAlloc( 6, 64, 4, 1 );
757
758 RetValue = Rsb_ManPerformResub6( p, 6, F, vDivTruths, &uTruth0, &uTruth1, 1 );
759
760 Rsb_ManFree( p );
761 Vec_WrdFree( vDivTruths );
762}
763
767
768
769ABC_NAMESPACE_IMPL_END
770
nWords
int nWords
Definition abcNpn.c:127
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
p
Cube * p
Definition exorList.c:222
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Kit_DsdPrintFromTruth
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition kitDsd.c:491
Rsb_DecInitCexes
int Rsb_DecInitCexes(int nVars, word *f, word **g, int nGs, int nGsAll, word *pCexes, Vec_Int_t *vTries)
Definition rsbDec6.c:292
Rsb_DecCheck
unsigned Rsb_DecCheck(int nVars, word *f, word **g, int nGs, unsigned *pPat, int *pCexA, int *pCexB)
Definition rsbDec6.c:124
Rsb_DecPrintTable
void Rsb_DecPrintTable(word *pCexes, int nGs, int nGsAll, Vec_Int_t *vTries)
Definition rsbDec6.c:196
Rsb_ManPerformResub6
int Rsb_ManPerformResub6(Rsb_Man_t *p, int nVarsAll, word uTruth, Vec_Wrd_t *vDivTruths, word *puTruth0, word *puTruth1, int fVerbose)
Definition rsbDec6.c:694
Rsb_ManPerformResub6Test
void Rsb_ManPerformResub6Test()
Definition rsbDec6.c:728
Rsb_ManPerform
unsigned Rsb_ManPerform(Rsb_Man_t *p, int nVars, word *f, word **g, int nGs, int nGsAll, int fVerbose0)
Definition rsbDec6.c:612
Rsb_DecPerformInt
unsigned Rsb_DecPerformInt(Rsb_Man_t *p, int nVars, word *f, word **g, int nGs, int nGsAll, int fFindAll)
Definition rsbDec6.c:337
Rsb_DecPrintFunc
void Rsb_DecPrintFunc(Rsb_Man_t *p, unsigned Truth4, word *f, word **ppGs, int nGs, int nVarsAll)
Definition rsbDec6.c:516
Rsb_DecVerify
int Rsb_DecVerify(Rsb_Man_t *p, int nVars, word *f, word **g, int nGs, unsigned Truth4, word *pTemp1, word *pTemp2)
Definition rsbDec6.c:560
Rsb_ManAlloc
Rsb_Man_t * Rsb_ManAlloc(int nLeafMax, int nDivMax, int nDecMax, int fVerbose)
MACRO DEFINITIONS ///.
Definition rsbMan.c:45
Rsb_ManFree
void Rsb_ManFree(Rsb_Man_t *p)
Definition rsbMan.c:63
Rsb_Man_t
typedefABC_NAMESPACE_HEADER_START struct Rsb_Man_t_ Rsb_Man_t
INCLUDES ///.
Definition rsb.h:39
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42