abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
rsbDec6.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [rsbDec6.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Truth-table-based resubstitution.]
8 
9  Synopsis [Implementation of the algorithm.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: rsbDec6.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "rsbInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis []
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 static inline unsigned Rsb_DecTry0( word c )
46 {
47  return (unsigned)(c != 0);
48 }
49 static inline unsigned Rsb_DecTry1( word c, word f1 )
50 {
51  return (Rsb_DecTry0(c&f1) << 1) | Rsb_DecTry0(c&~f1);
52 }
53 static 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 }
57 static 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 }
61 static 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 }
65 static 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 
70 /**Function*************************************************************
71 
72  Synopsis []
73 
74  Description []
75 
76  SideEffects []
77 
78  SeeAlso []
79 
80 ***********************************************************************/
81 static inline int Rsb_DecTryCex( word * g, int iCexA, int iCexB )
82 {
83  return Abc_TtGetBit(g, iCexA) == Abc_TtGetBit(g, iCexB);
84 }
85 static 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 }
96 static 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 
105 /**Function*************************************************************
106 
107  Synopsis [Checks decomposability of f with divisors g.]
108 
109  Description []
110 
111  SideEffects []
112 
113  SeeAlso []
114 
115 ***********************************************************************/
116 static 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 }
124 unsigned 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 
185 /**Function*************************************************************
186 
187  Synopsis []
188 
189  Description []
190 
191  SideEffects []
192 
193  SeeAlso []
194 
195 ***********************************************************************/
196 void 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 
280 /**Function*************************************************************
281 
282  Synopsis [Init ]
283 
284  Description [Returns the numbers of the decomposition functions and
285  the truth table of a function up to 4 variables.]
286 
287  SideEffects []
288 
289  SeeAlso []
290 
291 ***********************************************************************/
292 int 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 
325 /**Function*************************************************************
326 
327  Synopsis [Finds a setset of gs to decompose f.]
328 
329  Description [Returns the numbers of the decomposition functions and
330  the truth table of a function up to 4 variables.]
331 
332  SideEffects []
333 
334  SeeAlso []
335 
336 ***********************************************************************/
337 unsigned 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 
505 /**Function*************************************************************
506 
507  Synopsis [Verifies 4-input decomposition.]
508 
509  Description []
510 
511  SideEffects []
512 
513  SeeAlso []
514 
515 ***********************************************************************/
516 void 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 
549 /**Function*************************************************************
550 
551  Synopsis [Verifies 4-input decomposition.]
552 
553  Description []
554 
555  SideEffects []
556 
557  SeeAlso []
558 
559 ***********************************************************************/
560 int 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 
600 /**Function*************************************************************
601 
602  Synopsis [Finds a setset of gs to decompose f.]
603 
604  Description [Returns the numbers of the decomposition functions and
605  the truth table of a function up to 4 variables.]
606 
607  SideEffects []
608 
609  SeeAlso []
610 
611 ***********************************************************************/
612 unsigned 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
651 if ( fVerbose )
652 vTries = 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 
676 if ( fVerbose )
677 Rsb_DecPrintTable( pCexes, nGs, nGsAll, vTries );
678 if ( fVerbose )
679 Vec_IntFree( vTries );
680  return uTruth;
681 }
682 
683 /**Function*************************************************************
684 
685  Synopsis []
686 
687  Description []
688 
689  SideEffects []
690 
691  SeeAlso []
692 
693 ***********************************************************************/
694 int 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 
717 /**Function*************************************************************
718 
719  Synopsis []
720 
721  Description []
722 
723  SideEffects []
724 
725  SeeAlso []
726 
727 ***********************************************************************/
728 void 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 
764 ////////////////////////////////////////////////////////////////////////
765 /// END OF FILE ///
766 ////////////////////////////////////////////////////////////////////////
767 
768 
769 ABC_NAMESPACE_IMPL_END
770 
memset
char * memset()
Abc_TtSharp
static void Abc_TtSharp(word *pOut, word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:241
Rsb_Man_t_::vTries
Vec_Int_t * vTries
Definition: rsbInt.h:62
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_TtFindLastZero
static int Abc_TtFindLastZero(word *pIn, int nVars)
Definition: utilTruth.h:1540
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_WrdPush
static void Vec_WrdPush(Vec_Wrd_t *p, word Entry)
Definition: vecWrd.h:618
Abc_TtClear
static void Abc_TtClear(word *pOut, int nWords)
Definition: utilTruth.h:197
Abc_TtFindFirstBit
static int Abc_TtFindFirstBit(word *pIn, int nVars)
Definition: utilTruth.h:1516
Abc_TtFindFirstZero
static int Abc_TtFindFirstZero(word *pIn, int nVars)
Definition: utilTruth.h:1524
Abc_Tt6FirstBit
static int Abc_Tt6FirstBit(word t)
Definition: utilTruth.h:1492
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
Abc_TtOr
static void Abc_TtOr(word *pOut, word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:247
Abc_TtSetBit
static void Abc_TtSetBit(word *p, int i)
Definition: utilTruth.h:150
Rsb_Man_t
typedefABC_NAMESPACE_HEADER_START struct Rsb_Man_t_ Rsb_Man_t
INCLUDES ///.
Definition: rsb.h:39
Kit_DsdPrintFromTruth
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition: kitDsd.c:490
Abc_TtCountOnes
static int Abc_TtCountOnes(word x)
Definition: utilTruth.h:1470
Abc_TtGetBit
static int Abc_TtGetBit(word *p, int i)
MACRO DEFINITIONS ///.
Definition: utilTruth.h:149
Vec_WrdSize
static int Vec_WrdSize(Vec_Wrd_t *p)
Definition: vecWrd.h:336
nWords
int nWords
Definition: abcNpn.c:127
Rsb_DecTry4
static unsigned Rsb_DecTry4(word c, word f1, word f2, word f3, word f4)
Definition: rsbDec6.c:61
Rsb_DecVerifyCex
static void Rsb_DecVerifyCex(word *f, word **g, int nGs, int iCexA, int iCexB)
Definition: rsbDec6.c:85
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
Abc_TtFill
static void Abc_TtFill(word *pOut, int nWords)
Definition: utilTruth.h:203
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Rsb_DecCofactor
static word Rsb_DecCofactor(word **g, int nGs, int w, int iMint)
Definition: rsbDec6.c:116
Abc_TtPrintBinary
static void Abc_TtPrintBinary(word *pTruth, int nVars)
Definition: utilTruth.h:907
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Rsb_DecRecordCex
static void Rsb_DecRecordCex(word **g, int nGs, int iCexA, int iCexB, word *pCexes, int nCexes)
Definition: rsbDec6.c:96
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
Rsb_DecPrintFunc
void Rsb_DecPrintFunc(Rsb_Man_t *p, unsigned Truth4, word *f, word **ppGs, int nGs, int nVarsAll)
Definition: rsbDec6.c:516
Abc_Tt6Stretch
static word Abc_Tt6Stretch(word t, int nVars)
Definition: utilTruth.h:708
Rsb_Man_t_::fVerbose
int fVerbose
Definition: rsbInt.h:56
Abc_Tt6Isop
static word Abc_Tt6Isop(word uOn, word uOnDc, int nVars, int *pnCubes)
Definition: utilTruth.h:1704
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Rsb_DecTry2
static unsigned Rsb_DecTry2(word c, word f1, word f2)
Definition: rsbDec6.c:53
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_DecTry1
static unsigned Rsb_DecTry1(word c, word f1)
Definition: rsbDec6.c:49
Rsb_DecTry3
static unsigned Rsb_DecTry3(word c, word f1, word f2, word f3)
Definition: rsbDec6.c:57
Vec_WrdAlloc
static Vec_Wrd_t * Vec_WrdAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecWrd.h:80
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Rsb_DecCheck
unsigned Rsb_DecCheck(int nVars, word *f, word **g, int nGs, unsigned *pPat, int *pCexA, int *pCexB)
Definition: rsbDec6.c:124
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
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
Vec_WrdArray
static word * Vec_WrdArray(Vec_Wrd_t *p)
Definition: vecWrd.h:316
Abc_TtWordNum
static int Abc_TtWordNum(int nVars)
Definition: utilTruth.h:169
Rsb_ManPerformResub6Test
void Rsb_ManPerformResub6Test()
Definition: rsbDec6.c:728
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
Rsb_DecTry5
static unsigned Rsb_DecTry5(word c, word f1, word f2, word f3, word f4, word f5)
Definition: rsbDec6.c:65
Abc_TtEqual
static int Abc_TtEqual(word *pIn1, word *pIn2, int nWords)
Definition: utilTruth.h:269
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_DecPrintTable
void Rsb_DecPrintTable(word *pCexes, int nGs, int nGsAll, Vec_Int_t *vTries)
Definition: rsbDec6.c:196
assert
#define assert(ex)
Definition: util_old.h:213
Abc_TtFindLastBit
static int Abc_TtFindLastBit(word *pIn, int nVars)
Definition: utilTruth.h:1532
Vec_IntPrint
static void Vec_IntPrint(Vec_Int_t *vVec)
Definition: vecInt.h:1803
Abc_TtAnd
static void Abc_TtAnd(word *pOut, word *pIn1, word *pIn2, int nWords, int fCompl)
Definition: utilTruth.h:231
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Rsb_DecTry0
static ABC_NAMESPACE_IMPL_START unsigned Rsb_DecTry0(word c)
DECLARATIONS ///.
Definition: rsbDec6.c:45
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition: vecWrd.h:42
Rsb_DecTryCex
static int Rsb_DecTryCex(word *g, int iCexA, int iCexB)
Definition: rsbDec6.c:81
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
Vec_WrdEntryP
static word * Vec_WrdEntryP(Vec_Wrd_t *p, int i)
Definition: vecWrd.h:401