ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
rsbDec6.c File Reference
#include "rsbInt.h"
Include dependency graph for rsbDec6.c:

Go to the source code of this file.

Functions

unsigned Rsb_DecCheck (int nVars, word *f, word **g, int nGs, unsigned *pPat, int *pCexA, int *pCexB)
 
void Rsb_DecPrintTable (word *pCexes, int nGs, int nGsAll, Vec_Int_t *vTries)
 
int Rsb_DecInitCexes (int nVars, word *f, word **g, int nGs, int nGsAll, word *pCexes, Vec_Int_t *vTries)
 
unsigned Rsb_DecPerformInt (Rsb_Man_t *p, int nVars, word *f, word **g, int nGs, int nGsAll, int fFindAll)
 
void Rsb_DecPrintFunc (Rsb_Man_t *p, unsigned Truth4, word *f, word **ppGs, int nGs, int nVarsAll)
 
int Rsb_DecVerify (Rsb_Man_t *p, int nVars, word *f, word **g, int nGs, unsigned Truth4, word *pTemp1, word *pTemp2)
 
unsigned Rsb_ManPerform (Rsb_Man_t *p, int nVars, word *f, word **g, int nGs, int nGsAll, int fVerbose0)
 
int Rsb_ManPerformResub6 (Rsb_Man_t *p, int nVarsAll, word uTruth, Vec_Wrd_t *vDivTruths, word *puTruth0, word *puTruth1, int fVerbose)
 
void Rsb_ManPerformResub6Test ()
 

Function Documentation

◆ Rsb_DecCheck()

unsigned Rsb_DecCheck ( int nVars,
word * f,
word ** g,
int nGs,
unsigned * pPat,
int * pCexA,
int * pCexB )

Definition at line 124 of file rsbDec6.c.

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}
nWords
int nWords
Definition abcNpn.c:127
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
assert
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Rsb_DecInitCexes()

int Rsb_DecInitCexes ( int nVars,
word * f,
word ** g,
int nGs,
int nGsAll,
word * pCexes,
Vec_Int_t * vTries )

Function*************************************************************

Synopsis [Init ]

Description [Returns the numbers of the decomposition functions and the truth table of a function up to 4 variables.]

SideEffects []

SeeAlso []

Definition at line 292 of file rsbDec6.c.

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}

◆ Rsb_DecPerformInt()

unsigned Rsb_DecPerformInt ( Rsb_Man_t * p,
int nVars,
word * f,
word ** g,
int nGs,
int nGsAll,
int fFindAll )

Function*************************************************************

Synopsis [Finds a setset of gs to decompose f.]

Description [Returns the numbers of the decomposition functions and the truth table of a function up to 4 variables.]

SideEffects []

SeeAlso []

Definition at line 337 of file rsbDec6.c.

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}
p
Cube * p
Definition exorList.c:222
Kit_DsdPrintFromTruth
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition kitDsd.c:491
Rsb_DecCheck
unsigned Rsb_DecCheck(int nVars, word *f, word **g, int nGs, unsigned *pPat, int *pCexA, int *pCexB)
Definition rsbDec6.c:124
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Rsb_DecPrintFunc()

void Rsb_DecPrintFunc ( Rsb_Man_t * p,
unsigned Truth4,
word * f,
word ** ppGs,
int nGs,
int nVarsAll )

Function*************************************************************

Synopsis [Verifies 4-input decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 516 of file rsbDec6.c.

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}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Rsb_DecPrintTable()

void Rsb_DecPrintTable ( word * pCexes,
int nGs,
int nGsAll,
Vec_Int_t * vTries )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 196 of file rsbDec6.c.

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}
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Here is the caller graph for this function:

◆ Rsb_DecVerify()

int Rsb_DecVerify ( Rsb_Man_t * p,
int nVars,
word * f,
word ** g,
int nGs,
unsigned Truth4,
word * pTemp1,
word * pTemp2 )

Function*************************************************************

Synopsis [Verifies 4-input decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 560 of file rsbDec6.c.

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}
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54

◆ Rsb_ManPerform()

unsigned Rsb_ManPerform ( Rsb_Man_t * p,
int nVars,
word * f,
word ** g,
int nGs,
int nGsAll,
int fVerbose0 )

Function*************************************************************

Synopsis [Finds a setset of gs to decompose f.]

Description [Returns the numbers of the decomposition functions and the truth table of a function up to 4 variables.]

SideEffects []

SeeAlso []

Definition at line 612 of file rsbDec6.c.

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}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Rsb_DecPrintTable
void Rsb_DecPrintTable(word *pCexes, int nGs, int nGsAll, Vec_Int_t *vTries)
Definition rsbDec6.c:196
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
Here is the call graph for this function:

◆ Rsb_ManPerformResub6()

int Rsb_ManPerformResub6 ( Rsb_Man_t * p,
int nVarsAll,
word uTruth,
Vec_Wrd_t * vDivTruths,
word * puTruth0,
word * puTruth1,
int fVerbose )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 694 of file rsbDec6.c.

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}
Rsb_DecPrintFunc
void Rsb_DecPrintFunc(Rsb_Man_t *p, unsigned Truth4, word *f, word **ppGs, int nGs, int nVarsAll)
Definition rsbDec6.c:516
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Rsb_ManPerformResub6Test()

void Rsb_ManPerformResub6Test ( )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 728 of file rsbDec6.c.

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}
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_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
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42
Here is the call graph for this function: