abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraigUtil.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [fraigUtil.c]
4 
5  PackageName [FRAIG: Functionally reduced AND-INV graphs.]
6 
7  Synopsis [Various utilities.]
8 
9  Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
10 
11  Affiliation [UC Berkeley]
12 
13  Date [Ver. 2.0. Started - October 1, 2004]
14 
15  Revision [$Id: fraigUtil.c,v 1.15 2005/07/08 01:01:34 alanmi Exp $]
16 
17 ***********************************************************************/
18 
19 #include "fraigInt.h"
20 #include <limits.h>
21 
22 ABC_NAMESPACE_IMPL_START
23 
24 
25 ////////////////////////////////////////////////////////////////////////
26 /// DECLARATIONS ///
27 ////////////////////////////////////////////////////////////////////////
28 
29 static int bit_count[256] = {
30  0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
31  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
32  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
33  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
34  1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
35  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
36  2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
37  3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
38 };
39 
40 static void Fraig_Dfs_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeVec_t * vNodes, int fEquiv );
41 static int Fraig_CheckTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_Node_t * pOld );
42 
43 ////////////////////////////////////////////////////////////////////////
44 /// FUNCTION DEFINITIONS ///
45 ////////////////////////////////////////////////////////////////////////
46 
47 /**Function*************************************************************
48 
49  Synopsis [Computes the DFS ordering of the nodes.]
50 
51  Description []
52 
53  SideEffects []
54 
55  SeeAlso []
56 
57 ***********************************************************************/
58 Fraig_NodeVec_t * Fraig_Dfs( Fraig_Man_t * pMan, int fEquiv )
59 {
60  Fraig_NodeVec_t * vNodes;
61  int i;
62  pMan->nTravIds++;
63  vNodes = Fraig_NodeVecAlloc( 100 );
64  for ( i = 0; i < pMan->vOutputs->nSize; i++ )
65  Fraig_Dfs_rec( pMan, Fraig_Regular(pMan->vOutputs->pArray[i]), vNodes, fEquiv );
66  return vNodes;
67 }
68 
69 /**Function*************************************************************
70 
71  Synopsis [Computes the DFS ordering of the nodes.]
72 
73  Description []
74 
75  SideEffects []
76 
77  SeeAlso []
78 
79 ***********************************************************************/
80 Fraig_NodeVec_t * Fraig_DfsOne( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int fEquiv )
81 {
82  Fraig_NodeVec_t * vNodes;
83  pMan->nTravIds++;
84  vNodes = Fraig_NodeVecAlloc( 100 );
85  Fraig_Dfs_rec( pMan, Fraig_Regular(pNode), vNodes, fEquiv );
86  return vNodes;
87 }
88 
89 /**Function*************************************************************
90 
91  Synopsis [Computes the DFS ordering of the nodes.]
92 
93  Description []
94 
95  SideEffects []
96 
97  SeeAlso []
98 
99 ***********************************************************************/
100 Fraig_NodeVec_t * Fraig_DfsNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppNodes, int nNodes, int fEquiv )
101 {
102  Fraig_NodeVec_t * vNodes;
103  int i;
104  pMan->nTravIds++;
105  vNodes = Fraig_NodeVecAlloc( 100 );
106  for ( i = 0; i < nNodes; i++ )
107  Fraig_Dfs_rec( pMan, Fraig_Regular(ppNodes[i]), vNodes, fEquiv );
108  return vNodes;
109 }
110 
111 /**Function*************************************************************
112 
113  Synopsis [Recursively computes the DFS ordering of the nodes.]
114 
115  Description []
116 
117  SideEffects []
118 
119  SeeAlso []
120 
121 ***********************************************************************/
122 void Fraig_Dfs_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_NodeVec_t * vNodes, int fEquiv )
123 {
124  assert( !Fraig_IsComplement(pNode) );
125  // skip the visited node
126  if ( pNode->TravId == pMan->nTravIds )
127  return;
128  pNode->TravId = pMan->nTravIds;
129  // visit the transitive fanin
130  if ( Fraig_NodeIsAnd(pNode) )
131  {
132  Fraig_Dfs_rec( pMan, Fraig_Regular(pNode->p1), vNodes, fEquiv );
133  Fraig_Dfs_rec( pMan, Fraig_Regular(pNode->p2), vNodes, fEquiv );
134  }
135  if ( fEquiv && pNode->pNextE )
136  Fraig_Dfs_rec( pMan, pNode->pNextE, vNodes, fEquiv );
137  // save the node
138  Fraig_NodeVecPush( vNodes, pNode );
139 }
140 
141 /**Function*************************************************************
142 
143  Synopsis [Computes the DFS ordering of the nodes.]
144 
145  Description []
146 
147  SideEffects []
148 
149  SeeAlso []
150 
151 ***********************************************************************/
152 int Fraig_CountNodes( Fraig_Man_t * pMan, int fEquiv )
153 {
154  Fraig_NodeVec_t * vNodes;
155  int RetValue;
156  vNodes = Fraig_Dfs( pMan, fEquiv );
157  RetValue = vNodes->nSize;
158  Fraig_NodeVecFree( vNodes );
159  return RetValue;
160 }
161 
162 /**Function*************************************************************
163 
164  Synopsis [Returns 1 if pOld is in the TFI of pNew.]
165 
166  Description []
167 
168  SideEffects []
169 
170  SeeAlso []
171 
172 ***********************************************************************/
173 int Fraig_CheckTfi( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
174 {
175  assert( !Fraig_IsComplement(pOld) );
176  assert( !Fraig_IsComplement(pNew) );
177  pMan->nTravIds++;
178  return Fraig_CheckTfi_rec( pMan, pNew, pOld );
179 }
180 
181 /**Function*************************************************************
182 
183  Synopsis [Returns 1 if pOld is in the TFI of pNew.]
184 
185  Description []
186 
187  SideEffects []
188 
189  SeeAlso []
190 
191 ***********************************************************************/
192 int Fraig_CheckTfi_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, Fraig_Node_t * pOld )
193 {
194  // check the trivial cases
195  if ( pNode == NULL )
196  return 0;
197  if ( pNode->Num < pOld->Num && !pMan->fChoicing )
198  return 0;
199  if ( pNode == pOld )
200  return 1;
201  // skip the visited node
202  if ( pNode->TravId == pMan->nTravIds )
203  return 0;
204  pNode->TravId = pMan->nTravIds;
205  // check the children
206  if ( Fraig_CheckTfi_rec( pMan, Fraig_Regular(pNode->p1), pOld ) )
207  return 1;
208  if ( Fraig_CheckTfi_rec( pMan, Fraig_Regular(pNode->p2), pOld ) )
209  return 1;
210  // check equivalent nodes
211  return Fraig_CheckTfi_rec( pMan, pNode->pNextE, pOld );
212 }
213 
214 
215 /**Function*************************************************************
216 
217  Synopsis [Returns 1 if pOld is in the TFI of pNew.]
218 
219  Description []
220 
221  SideEffects []
222 
223  SeeAlso []
224 
225 ***********************************************************************/
226 int Fraig_CheckTfi2( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
227 {
228  Fraig_NodeVec_t * vNodes;
229  int RetValue;
230  vNodes = Fraig_DfsOne( pMan, pNew, 1 );
231  RetValue = (pOld->TravId == pMan->nTravIds);
232  Fraig_NodeVecFree( vNodes );
233  return RetValue;
234 }
235 
236 /**Function*************************************************************
237 
238  Synopsis [Sets the number of fanouts (none, one, or many).]
239 
240  Description [This procedure collects the nodes reachable from
241  the POs of the AIG and sets the type of fanout counter (none, one,
242  or many) for each node. This procedure is useful to determine
243  fanout-free cones of AND-nodes, which is helpful for rebalancing
244  the AIG (see procedure Fraig_ManRebalance, or something like that).]
245 
246  SideEffects []
247 
248  SeeAlso []
249 
250 ***********************************************************************/
251 void Fraig_ManMarkRealFanouts( Fraig_Man_t * p )
252 {
253  Fraig_NodeVec_t * vNodes;
254  Fraig_Node_t * pNodeR;
255  int i;
256  // collect the nodes reachable
257  vNodes = Fraig_Dfs( p, 0 );
258  // clean the fanouts field
259  for ( i = 0; i < vNodes->nSize; i++ )
260  {
261  vNodes->pArray[i]->nFanouts = 0;
262  vNodes->pArray[i]->pData0 = NULL;
263  }
264  // mark reachable nodes by setting the two-bit counter pNode->nFans
265  for ( i = 0; i < vNodes->nSize; i++ )
266  {
267  pNodeR = Fraig_Regular(vNodes->pArray[i]->p1);
268  if ( pNodeR && ++pNodeR->nFanouts == 3 )
269  pNodeR->nFanouts = 2;
270  pNodeR = Fraig_Regular(vNodes->pArray[i]->p2);
271  if ( pNodeR && ++pNodeR->nFanouts == 3 )
272  pNodeR->nFanouts = 2;
273  }
274  Fraig_NodeVecFree( vNodes );
275 }
276 
277 /**Function*************************************************************
278 
279  Synopsis [Creates the constant 1 node.]
280 
281  Description []
282 
283  SideEffects []
284 
285  SeeAlso []
286 
287 ***********************************************************************/
288 int Fraig_BitStringCountOnes( unsigned * pString, int nWords )
289 {
290  unsigned char * pSuppBytes = (unsigned char *)pString;
291  int i, nOnes, nBytes = sizeof(unsigned) * nWords;
292  // count the number of ones in the simulation vector
293  for ( i = nOnes = 0; i < nBytes; i++ )
294  nOnes += bit_count[pSuppBytes[i]];
295  return nOnes;
296 }
297 
298 /**Function*************************************************************
299 
300  Synopsis [Verify one useful property.]
301 
302  Description [This procedure verifies one useful property. After
303  the FRAIG construction with choice nodes is over, each primary node
304  should have fanins that are primary nodes. The primary nodes is the
305  one that does not have pNode->pRepr set to point to another node.]
306 
307  SideEffects []
308 
309  SeeAlso []
310 
311 ***********************************************************************/
312 int Fraig_ManCheckConsistency( Fraig_Man_t * p )
313 {
314  Fraig_Node_t * pNode;
315  Fraig_NodeVec_t * pVec;
316  int i;
317  pVec = Fraig_Dfs( p, 0 );
318  for ( i = 0; i < pVec->nSize; i++ )
319  {
320  pNode = pVec->pArray[i];
321  if ( Fraig_NodeIsVar(pNode) )
322  {
323  if ( pNode->pRepr )
324  printf( "Primary input %d is a secondary node.\n", pNode->Num );
325  }
326  else if ( Fraig_NodeIsConst(pNode) )
327  {
328  if ( pNode->pRepr )
329  printf( "Constant 1 %d is a secondary node.\n", pNode->Num );
330  }
331  else
332  {
333  if ( pNode->pRepr )
334  printf( "Internal node %d is a secondary node.\n", pNode->Num );
335  if ( Fraig_Regular(pNode->p1)->pRepr )
336  printf( "Internal node %d has first fanin %d that is a secondary node.\n",
337  pNode->Num, Fraig_Regular(pNode->p1)->Num );
338  if ( Fraig_Regular(pNode->p2)->pRepr )
339  printf( "Internal node %d has second fanin %d that is a secondary node.\n",
340  pNode->Num, Fraig_Regular(pNode->p2)->Num );
341  }
342  }
343  Fraig_NodeVecFree( pVec );
344  return 1;
345 }
346 
347 /**Function*************************************************************
348 
349  Synopsis [Prints the node.]
350 
351  Description []
352 
353  SideEffects []
354 
355  SeeAlso []
356 
357 ***********************************************************************/
358 void Fraig_PrintNode( Fraig_Man_t * p, Fraig_Node_t * pNode )
359 {
360  Fraig_NodeVec_t * vNodes;
361  Fraig_Node_t * pTemp;
362  int fCompl1, fCompl2, i;
363 
364  vNodes = Fraig_DfsOne( p, pNode, 0 );
365  for ( i = 0; i < vNodes->nSize; i++ )
366  {
367  pTemp = vNodes->pArray[i];
368  if ( Fraig_NodeIsVar(pTemp) )
369  {
370  printf( "%3d : PI ", pTemp->Num );
371  Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimR, 20 );
372  printf( " " );
373  Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimD, 20 );
374  printf( " %d\n", pTemp->fInv );
375  continue;
376  }
377 
378  fCompl1 = Fraig_IsComplement(pTemp->p1);
379  fCompl2 = Fraig_IsComplement(pTemp->p2);
380  printf( "%3d : %c%3d %c%3d ", pTemp->Num,
381  (fCompl1? '-':'+'), Fraig_Regular(pTemp->p1)->Num,
382  (fCompl2? '-':'+'), Fraig_Regular(pTemp->p2)->Num );
383  Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimR, 20 );
384  printf( " " );
385  Fraig_PrintBinary( stdout, (unsigned *)&pTemp->puSimD, 20 );
386  printf( " %d\n", pTemp->fInv );
387  }
388  Fraig_NodeVecFree( vNodes );
389 }
390 
391 /**Function*************************************************************
392 
393  Synopsis [Prints the bit string.]
394 
395  Description []
396 
397  SideEffects []
398 
399  SeeAlso []
400 
401 ***********************************************************************/
402 void Fraig_PrintBinary( FILE * pFile, unsigned * pSign, int nBits )
403 {
404  int Remainder, nWords;
405  int w, i;
406 
407  Remainder = (nBits%(sizeof(unsigned)*8));
408  nWords = (nBits/(sizeof(unsigned)*8)) + (Remainder>0);
409 
410  for ( w = nWords-1; w >= 0; w-- )
411  for ( i = ((w == nWords-1 && Remainder)? Remainder-1: 31); i >= 0; i-- )
412  fprintf( pFile, "%c", '0' + (int)((pSign[w] & (1<<i)) > 0) );
413 
414 // fprintf( pFile, "\n" );
415 }
416 
417 /**Function*************************************************************
418 
419  Synopsis [Sets up the mask.]
420 
421  Description []
422 
423  SideEffects []
424 
425  SeeAlso []
426 
427 ***********************************************************************/
428 int Fraig_GetMaxLevel( Fraig_Man_t * pMan )
429 {
430  int nLevelMax, i;
431  nLevelMax = 0;
432  for ( i = 0; i < pMan->vOutputs->nSize; i++ )
433  nLevelMax = nLevelMax > Fraig_Regular(pMan->vOutputs->pArray[i])->Level?
434  nLevelMax : Fraig_Regular(pMan->vOutputs->pArray[i])->Level;
435  return nLevelMax;
436 }
437 
438 /**Function*************************************************************
439 
440  Synopsis [Analyses choice nodes.]
441 
442  Description []
443 
444  SideEffects []
445 
446  SeeAlso []
447 
448 ***********************************************************************/
449 int Fraig_MappingUpdateLevel_rec( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int fMaximum )
450 {
451  Fraig_Node_t * pTemp;
452  int Level1, Level2, LevelE;
453  assert( !Fraig_IsComplement(pNode) );
454  if ( !Fraig_NodeIsAnd(pNode) )
455  return pNode->Level;
456  // skip the visited node
457  if ( pNode->TravId == pMan->nTravIds )
458  return pNode->Level;
459  pNode->TravId = pMan->nTravIds;
460  // compute levels of the children nodes
461  Level1 = Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pNode->p1), fMaximum );
462  Level2 = Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pNode->p2), fMaximum );
463  pNode->Level = 1 + Abc_MaxInt( Level1, Level2 );
464  if ( pNode->pNextE )
465  {
466  LevelE = Fraig_MappingUpdateLevel_rec( pMan, pNode->pNextE, fMaximum );
467  if ( fMaximum )
468  {
469  if ( pNode->Level < LevelE )
470  pNode->Level = LevelE;
471  }
472  else
473  {
474  if ( pNode->Level > LevelE )
475  pNode->Level = LevelE;
476  }
477  // set the level of all equivalent nodes to be the same minimum
478  if ( pNode->pRepr == NULL ) // the primary node
479  for ( pTemp = pNode->pNextE; pTemp; pTemp = pTemp->pNextE )
480  pTemp->Level = pNode->Level;
481  }
482  return pNode->Level;
483 }
484 
485 /**Function*************************************************************
486 
487  Synopsis [Resets the levels of the nodes in the choice graph.]
488 
489  Description [Makes the level of the choice nodes to be equal to the
490  maximum of the level of the nodes in the equivalence class. This way
491  sorting by level leads to the reverse topological order, which is
492  needed for the required time computation.]
493 
494  SideEffects []
495 
496  SeeAlso []
497 
498 ***********************************************************************/
499 void Fraig_MappingSetChoiceLevels( Fraig_Man_t * pMan, int fMaximum )
500 {
501  int i;
502  pMan->nTravIds++;
503  for ( i = 0; i < pMan->vOutputs->nSize; i++ )
504  Fraig_MappingUpdateLevel_rec( pMan, Fraig_Regular(pMan->vOutputs->pArray[i]), fMaximum );
505 }
506 
507 /**Function*************************************************************
508 
509  Synopsis [Reports statistics on choice nodes.]
510 
511  Description [The number of choice nodes is the number of primary nodes,
512  which has pNextE set to a pointer. The number of choices is the number
513  of entries in the equivalent-node lists of the primary nodes.]
514 
515  SideEffects []
516 
517  SeeAlso []
518 
519 ***********************************************************************/
520 void Fraig_ManReportChoices( Fraig_Man_t * pMan )
521 {
522  Fraig_Node_t * pNode, * pTemp;
523  int nChoiceNodes, nChoices;
524  int i, LevelMax1, LevelMax2;
525 
526  // report the number of levels
527  LevelMax1 = Fraig_GetMaxLevel( pMan );
528  Fraig_MappingSetChoiceLevels( pMan, 0 );
529  LevelMax2 = Fraig_GetMaxLevel( pMan );
530 
531  // report statistics about choices
532  nChoiceNodes = nChoices = 0;
533  for ( i = 0; i < pMan->vNodes->nSize; i++ )
534  {
535  pNode = pMan->vNodes->pArray[i];
536  if ( pNode->pRepr == NULL && pNode->pNextE != NULL )
537  { // this is a choice node = the primary node that has equivalent nodes
538  nChoiceNodes++;
539  for ( pTemp = pNode; pTemp; pTemp = pTemp->pNextE )
540  nChoices++;
541  }
542  }
543  printf( "Maximum level: Original = %d. Reduced due to choices = %d.\n", LevelMax1, LevelMax2 );
544  printf( "Choice stats: Choice nodes = %d. Total choices = %d.\n", nChoiceNodes, nChoices );
545 }
546 
547 /**Function*************************************************************
548 
549  Synopsis [Returns 1 if the node is the root of EXOR/NEXOR gate.]
550 
551  Description [The node can be complemented.]
552 
553  SideEffects []
554 
555  SeeAlso []
556 
557 ***********************************************************************/
558 int Fraig_NodeIsExorType( Fraig_Node_t * pNode )
559 {
560  Fraig_Node_t * pNode1, * pNode2;
561  // make the node regular (it does not matter for EXOR/NEXOR)
562  pNode = Fraig_Regular(pNode);
563  // if the node or its children are not ANDs or not compl, this cannot be EXOR type
564  if ( !Fraig_NodeIsAnd(pNode) )
565  return 0;
566  if ( !Fraig_NodeIsAnd(pNode->p1) || !Fraig_IsComplement(pNode->p1) )
567  return 0;
568  if ( !Fraig_NodeIsAnd(pNode->p2) || !Fraig_IsComplement(pNode->p2) )
569  return 0;
570 
571  // get children
572  pNode1 = Fraig_Regular(pNode->p1);
573  pNode2 = Fraig_Regular(pNode->p2);
574  assert( pNode1->Num < pNode2->Num );
575 
576  // compare grandchildren
577  return pNode1->p1 == Fraig_Not(pNode2->p1) && pNode1->p2 == Fraig_Not(pNode2->p2);
578 }
579 
580 /**Function*************************************************************
581 
582  Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
583 
584  Description [The node can be complemented.]
585 
586  SideEffects []
587 
588  SeeAlso []
589 
590 ***********************************************************************/
591 int Fraig_NodeIsMuxType( Fraig_Node_t * pNode )
592 {
593  Fraig_Node_t * pNode1, * pNode2;
594 
595  // make the node regular (it does not matter for EXOR/NEXOR)
596  pNode = Fraig_Regular(pNode);
597  // if the node or its children are not ANDs or not compl, this cannot be EXOR type
598  if ( !Fraig_NodeIsAnd(pNode) )
599  return 0;
600  if ( !Fraig_NodeIsAnd(pNode->p1) || !Fraig_IsComplement(pNode->p1) )
601  return 0;
602  if ( !Fraig_NodeIsAnd(pNode->p2) || !Fraig_IsComplement(pNode->p2) )
603  return 0;
604 
605  // get children
606  pNode1 = Fraig_Regular(pNode->p1);
607  pNode2 = Fraig_Regular(pNode->p2);
608  assert( pNode1->Num < pNode2->Num );
609 
610  // compare grandchildren
611  // node is an EXOR/NEXOR
612  if ( pNode1->p1 == Fraig_Not(pNode2->p1) && pNode1->p2 == Fraig_Not(pNode2->p2) )
613  return 1;
614 
615  // otherwise the node is MUX iff it has a pair of equal grandchildren
616  return pNode1->p1 == Fraig_Not(pNode2->p1) ||
617  pNode1->p1 == Fraig_Not(pNode2->p2) ||
618  pNode1->p2 == Fraig_Not(pNode2->p1) ||
619  pNode1->p2 == Fraig_Not(pNode2->p2);
620 }
621 
622 /**Function*************************************************************
623 
624  Synopsis [Returns 1 if the node is EXOR, 0 if it is NEXOR.]
625 
626  Description [The node should be EXOR type and not complemented.]
627 
628  SideEffects []
629 
630  SeeAlso []
631 
632 ***********************************************************************/
633 int Fraig_NodeIsExor( Fraig_Node_t * pNode )
634 {
635  Fraig_Node_t * pNode1;
636  assert( !Fraig_IsComplement(pNode) );
637  assert( Fraig_NodeIsExorType(pNode) );
638  assert( Fraig_IsComplement(pNode->p1) );
639  // get children
640  pNode1 = Fraig_Regular(pNode->p1);
641  return Fraig_IsComplement(pNode1->p1) == Fraig_IsComplement(pNode1->p2);
642 }
643 
644 /**Function*************************************************************
645 
646  Synopsis [Recognizes what nodes are control and data inputs of a MUX.]
647 
648  Description [If the node is a MUX, returns the control variable C.
649  Assigns nodes T and E to be the then and else variables of the MUX.
650  Node C is never complemented. Nodes T and E can be complemented.
651  This function also recognizes EXOR/NEXOR gates as MUXes.]
652 
653  SideEffects []
654 
655  SeeAlso []
656 
657 ***********************************************************************/
658 Fraig_Node_t * Fraig_NodeRecognizeMux( Fraig_Node_t * pNode, Fraig_Node_t ** ppNodeT, Fraig_Node_t ** ppNodeE )
659 {
660  Fraig_Node_t * pNode1, * pNode2;
661  assert( !Fraig_IsComplement(pNode) );
662  assert( Fraig_NodeIsMuxType(pNode) );
663  // get children
664  pNode1 = Fraig_Regular(pNode->p1);
665  pNode2 = Fraig_Regular(pNode->p2);
666  // find the control variable
667  if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
668  {
669  if ( Fraig_IsComplement(pNode1->p1) )
670  { // pNode2->p1 is positive phase of C
671  *ppNodeT = Fraig_Not(pNode2->p2);
672  *ppNodeE = Fraig_Not(pNode1->p2);
673  return pNode2->p1;
674  }
675  else
676  { // pNode1->p1 is positive phase of C
677  *ppNodeT = Fraig_Not(pNode1->p2);
678  *ppNodeE = Fraig_Not(pNode2->p2);
679  return pNode1->p1;
680  }
681  }
682  else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
683  {
684  if ( Fraig_IsComplement(pNode1->p1) )
685  { // pNode2->p2 is positive phase of C
686  *ppNodeT = Fraig_Not(pNode2->p1);
687  *ppNodeE = Fraig_Not(pNode1->p2);
688  return pNode2->p2;
689  }
690  else
691  { // pNode1->p1 is positive phase of C
692  *ppNodeT = Fraig_Not(pNode1->p2);
693  *ppNodeE = Fraig_Not(pNode2->p1);
694  return pNode1->p1;
695  }
696  }
697  else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
698  {
699  if ( Fraig_IsComplement(pNode1->p2) )
700  { // pNode2->p1 is positive phase of C
701  *ppNodeT = Fraig_Not(pNode2->p2);
702  *ppNodeE = Fraig_Not(pNode1->p1);
703  return pNode2->p1;
704  }
705  else
706  { // pNode1->p2 is positive phase of C
707  *ppNodeT = Fraig_Not(pNode1->p1);
708  *ppNodeE = Fraig_Not(pNode2->p2);
709  return pNode1->p2;
710  }
711  }
712  else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
713  {
714  if ( Fraig_IsComplement(pNode1->p2) )
715  { // pNode2->p2 is positive phase of C
716  *ppNodeT = Fraig_Not(pNode2->p1);
717  *ppNodeE = Fraig_Not(pNode1->p1);
718  return pNode2->p2;
719  }
720  else
721  { // pNode1->p2 is positive phase of C
722  *ppNodeT = Fraig_Not(pNode1->p1);
723  *ppNodeE = Fraig_Not(pNode2->p1);
724  return pNode1->p2;
725  }
726  }
727  assert( 0 ); // this is not MUX
728  return NULL;
729 }
730 
731 /**Function*************************************************************
732 
733  Synopsis [Counts the number of EXOR type nodes.]
734 
735  Description []
736 
737  SideEffects []
738 
739  SeeAlso []
740 
741 ***********************************************************************/
742 int Fraig_ManCountExors( Fraig_Man_t * pMan )
743 {
744  int i, nExors;
745  nExors = 0;
746  for ( i = 0; i < pMan->vNodes->nSize; i++ )
747  nExors += Fraig_NodeIsExorType( pMan->vNodes->pArray[i] );
748  return nExors;
749 
750 }
751 
752 /**Function*************************************************************
753 
754  Synopsis [Counts the number of EXOR type nodes.]
755 
756  Description []
757 
758  SideEffects []
759 
760  SeeAlso []
761 
762 ***********************************************************************/
763 int Fraig_ManCountMuxes( Fraig_Man_t * pMan )
764 {
765  int i, nMuxes;
766  nMuxes = 0;
767  for ( i = 0; i < pMan->vNodes->nSize; i++ )
768  nMuxes += Fraig_NodeIsMuxType( pMan->vNodes->pArray[i] );
769  return nMuxes;
770 
771 }
772 
773 /**Function*************************************************************
774 
775  Synopsis [Returns 1 if siminfo of Node1 is contained in siminfo of Node2.]
776 
777  Description []
778 
779  SideEffects []
780 
781  SeeAlso []
782 
783 ***********************************************************************/
784 int Fraig_NodeSimsContained( Fraig_Man_t * pMan, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 )
785 {
786  unsigned * pUnsigned1, * pUnsigned2;
787  int i;
788 
789  // compare random siminfo
790  pUnsigned1 = pNode1->puSimR;
791  pUnsigned2 = pNode2->puSimR;
792  for ( i = 0; i < pMan->nWordsRand; i++ )
793  if ( pUnsigned1[i] & ~pUnsigned2[i] )
794  return 0;
795 
796  // compare systematic siminfo
797  pUnsigned1 = pNode1->puSimD;
798  pUnsigned2 = pNode2->puSimD;
799  for ( i = 0; i < pMan->iWordStart; i++ )
800  if ( pUnsigned1[i] & ~pUnsigned2[i] )
801  return 0;
802 
803  return 1;
804 }
805 
806 /**Function*************************************************************
807 
808  Synopsis [Count the number of PI variables.]
809 
810  Description []
811 
812  SideEffects []
813 
814  SeeAlso []
815 
816 ***********************************************************************/
817 int Fraig_CountPis( Fraig_Man_t * p, Msat_IntVec_t * vVarNums )
818 {
819  int * pVars, nVars, i, Counter;
820 
821  nVars = Msat_IntVecReadSize(vVarNums);
822  pVars = Msat_IntVecReadArray(vVarNums);
823  Counter = 0;
824  for ( i = 0; i < nVars; i++ )
825  Counter += Fraig_NodeIsVar( p->vNodes->pArray[pVars[i]] );
826  return Counter;
827 }
828 
829 
830 
831 /**Function*************************************************************
832 
833  Synopsis [Counts the number of EXOR type nodes.]
834 
835  Description []
836 
837  SideEffects []
838 
839  SeeAlso []
840 
841 ***********************************************************************/
842 int Fraig_ManPrintRefs( Fraig_Man_t * pMan )
843 {
844  Fraig_NodeVec_t * vPivots;
845  Fraig_Node_t * pNode, * pNode2;
846  int i, k, Counter, nProved;
847  abctime clk;
848 
849  vPivots = Fraig_NodeVecAlloc( 1000 );
850  for ( i = 0; i < pMan->vNodes->nSize; i++ )
851  {
852  pNode = pMan->vNodes->pArray[i];
853 
854  if ( pNode->nOnes == 0 || pNode->nOnes == (unsigned)pMan->nWordsRand * 32 )
855  continue;
856 
857  if ( pNode->nRefs > 5 )
858  {
859  Fraig_NodeVecPush( vPivots, pNode );
860 // printf( "Node %6d : nRefs = %2d Level = %3d.\n", pNode->Num, pNode->nRefs, pNode->Level );
861  }
862  }
863  printf( "Total nodes = %d. Referenced nodes = %d.\n", pMan->vNodes->nSize, vPivots->nSize );
864 
865 clk = Abc_Clock();
866  // count implications
867  Counter = nProved = 0;
868  for ( i = 0; i < vPivots->nSize; i++ )
869  for ( k = i+1; k < vPivots->nSize; k++ )
870  {
871  pNode = vPivots->pArray[i];
872  pNode2 = vPivots->pArray[k];
873  if ( Fraig_NodeSimsContained( pMan, pNode, pNode2 ) )
874  {
875  if ( Fraig_NodeIsImplication( pMan, pNode, pNode2, -1 ) )
876  nProved++;
877  Counter++;
878  }
879  else if ( Fraig_NodeSimsContained( pMan, pNode2, pNode ) )
880  {
881  if ( Fraig_NodeIsImplication( pMan, pNode2, pNode, -1 ) )
882  nProved++;
883  Counter++;
884  }
885  }
886  printf( "Number of candidate pairs = %d. Proved = %d.\n", Counter, nProved );
887 //ABC_PRT( "Time", Abc_Clock() - clk );
888  return 0;
889 }
890 
891 
892 /**Function*************************************************************
893 
894  Synopsis [Checks if pNew exists among the implication fanins of pOld.]
895 
896  Description [If pNew is an implication fanin of pOld, returns 1.
897  If Fraig_Not(pNew) is an implication fanin of pOld, return -1.
898  Otherwise returns 0.]
899 
900  SideEffects []
901 
902  SeeAlso []
903 
904 ***********************************************************************/
905 int Fraig_NodeIsInSupergate( Fraig_Node_t * pOld, Fraig_Node_t * pNew )
906 {
907  int RetValue1, RetValue2;
908  if ( Fraig_Regular(pOld) == Fraig_Regular(pNew) )
909  return (pOld == pNew)? 1 : -1;
910  if ( Fraig_IsComplement(pOld) || Fraig_NodeIsVar(pOld) )
911  return 0;
912  RetValue1 = Fraig_NodeIsInSupergate( pOld->p1, pNew );
913  RetValue2 = Fraig_NodeIsInSupergate( pOld->p2, pNew );
914  if ( RetValue1 == -1 || RetValue2 == -1 )
915  return -1;
916  if ( RetValue1 == 1 || RetValue2 == 1 )
917  return 1;
918  return 0;
919 }
920 
921 
922 /**Function*************************************************************
923 
924  Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]
925 
926  Description []
927 
928  SideEffects []
929 
930  SeeAlso []
931 
932 ***********************************************************************/
933 void Fraig_CollectSupergate_rec( Fraig_Node_t * pNode, Fraig_NodeVec_t * vSuper, int fFirst, int fStopAtMux )
934 {
935  // if the new node is complemented or a PI, another gate begins
936 // if ( Fraig_IsComplement(pNode) || Fraig_NodeIsVar(pNode) || Fraig_NodeIsMuxType(pNode) )
937  if ( (!fFirst && Fraig_Regular(pNode)->nRefs > 1) ||
938  Fraig_IsComplement(pNode) || Fraig_NodeIsVar(pNode) ||
939  (fStopAtMux && Fraig_NodeIsMuxType(pNode)) )
940  {
941  Fraig_NodeVecPushUnique( vSuper, pNode );
942  return;
943  }
944  // go through the branches
945  Fraig_CollectSupergate_rec( pNode->p1, vSuper, 0, fStopAtMux );
946  Fraig_CollectSupergate_rec( pNode->p2, vSuper, 0, fStopAtMux );
947 }
948 
949 /**Function*************************************************************
950 
951  Synopsis [Returns the array of nodes to be combined into one multi-input AND-gate.]
952 
953  Description []
954 
955  SideEffects []
956 
957  SeeAlso []
958 
959 ***********************************************************************/
960 Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux )
961 {
962  Fraig_NodeVec_t * vSuper;
963  vSuper = Fraig_NodeVecAlloc( 8 );
964  Fraig_CollectSupergate_rec( pNode, vSuper, 1, fStopAtMux );
965  return vSuper;
966 }
967 
968 
969 /**Function*************************************************************
970 
971  Synopsis []
972 
973  Description []
974 
975  SideEffects []
976 
977  SeeAlso []
978 
979 ***********************************************************************/
980 void Fraig_ManIncrementTravId( Fraig_Man_t * pMan )
981 {
982  pMan->nTravIds2++;
983 }
984 
985 /**Function*************************************************************
986 
987  Synopsis []
988 
989  Description []
990 
991  SideEffects []
992 
993  SeeAlso []
994 
995 ***********************************************************************/
996 void Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
997 {
998  pNode->TravId2 = pMan->nTravIds2;
999 }
1000 
1001 /**Function*************************************************************
1002 
1003  Synopsis []
1004 
1005  Description []
1006 
1007  SideEffects []
1008 
1009  SeeAlso []
1010 
1011 ***********************************************************************/
1012 int Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
1013 {
1014  return pNode->TravId2 == pMan->nTravIds2;
1015 }
1016 
1017 /**Function*************************************************************
1018 
1019  Synopsis []
1020 
1021  Description []
1022 
1023  SideEffects []
1024 
1025  SeeAlso []
1026 
1027 ***********************************************************************/
1028 int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
1029 {
1030  return pNode->TravId2 == pMan->nTravIds2 - 1;
1031 }
1032 
1033 ////////////////////////////////////////////////////////////////////////
1034 /// END OF FILE ///
1035 ////////////////////////////////////////////////////////////////////////
1036 
1037 
1038 ABC_NAMESPACE_IMPL_END
1039 
Fraig_ManReportChoices
void Fraig_ManReportChoices(Fraig_Man_t *pMan)
Definition: fraigUtil.c:520
Fraig_CollectSupergate_rec
void Fraig_CollectSupergate_rec(Fraig_Node_t *pNode, Fraig_NodeVec_t *vSuper, int fFirst, int fStopAtMux)
Definition: fraigUtil.c:933
Fraig_NodeVecPush
void Fraig_NodeVecPush(Fraig_NodeVec_t *p, Fraig_Node_t *Entry)
Definition: fraigVec.c:189
Fraig_DfsOne
Fraig_NodeVec_t * Fraig_DfsOne(Fraig_Man_t *pMan, Fraig_Node_t *pNode, int fEquiv)
Definition: fraigUtil.c:80
Fraig_NodeStruct_t_::TravId
int TravId
Definition: fraigInt.h:214
Fraig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Fraig_ManStruct_t_ Fraig_Man_t
INCLUDES ///.
Definition: fraig.h:40
Fraig_ManCountMuxes
int Fraig_ManCountMuxes(Fraig_Man_t *pMan)
Definition: fraigUtil.c:763
Fraig_NodeIsExor
int Fraig_NodeIsExor(Fraig_Node_t *pNode)
Definition: fraigUtil.c:633
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fraig_CheckTfi_rec
static int Fraig_CheckTfi_rec(Fraig_Man_t *pMan, Fraig_Node_t *pNode, Fraig_Node_t *pOld)
Definition: fraigUtil.c:192
Fraig_NodeIsExorType
int Fraig_NodeIsExorType(Fraig_Node_t *pNode)
Definition: fraigUtil.c:558
Msat_IntVec_t_
Definition: msatInt.h:162
Fraig_PrintNode
void Fraig_PrintNode(Fraig_Man_t *p, Fraig_Node_t *pNode)
Definition: fraigUtil.c:358
Fraig_NodeVecPushUnique
int Fraig_NodeVecPushUnique(Fraig_NodeVec_t *p, Fraig_Node_t *Entry)
Definition: fraigVec.c:212
Fraig_NodeStruct_t_::puSimD
unsigned * puSimD
Definition: fraigInt.h:248
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Fraig_CheckTfi
int Fraig_CheckTfi(Fraig_Man_t *pMan, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
Definition: fraigUtil.c:173
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Fraig_NodeStruct_t_::p2
Fraig_Node_t * p2
Definition: fraigInt.h:233
nWords
int nWords
Definition: abcNpn.c:127
Fraig_NodeStruct_t_::nRefs
int nRefs
Definition: fraigInt.h:213
Fraig_BitStringCountOnes
int Fraig_BitStringCountOnes(unsigned *pString, int nWords)
Definition: fraigUtil.c:288
Fraig_GetMaxLevel
int Fraig_GetMaxLevel(Fraig_Man_t *pMan)
Definition: fraigUtil.c:428
Fraig_Not
#define Fraig_Not(p)
Definition: fraig.h:109
Fraig_NodeRecognizeMux
Fraig_Node_t * Fraig_NodeRecognizeMux(Fraig_Node_t *pNode, Fraig_Node_t **ppNodeT, Fraig_Node_t **ppNodeE)
Definition: fraigUtil.c:658
Fraig_CheckTfi2
int Fraig_CheckTfi2(Fraig_Man_t *pMan, Fraig_Node_t *pOld, Fraig_Node_t *pNew)
Definition: fraigUtil.c:226
Msat_IntVecReadSize
int Msat_IntVecReadSize(Msat_IntVec_t *p)
Definition: msatVec.c:233
Fraig_NodeSetTravIdCurrent
void Fraig_NodeSetTravIdCurrent(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition: fraigUtil.c:996
Fraig_NodeIsTravIdPrevious
int Fraig_NodeIsTravIdPrevious(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition: fraigUtil.c:1028
Fraig_NodeStruct_t_::puSimR
unsigned * puSimR
Definition: fraigInt.h:247
Fraig_NodeStruct_t_::pNextE
Fraig_Node_t * pNextE
Definition: fraigInt.h:241
Fraig_NodeVecFree
void Fraig_NodeVecFree(Fraig_NodeVec_t *p)
Definition: fraigVec.c:66
Fraig_NodeVecAlloc
Fraig_NodeVec_t * Fraig_NodeVecAlloc(int nCap)
DECLARATIONS ///.
Definition: fraigVec.c:43
nMuxes
static int nMuxes
Definition: abcSat.c:36
Fraig_NodeStruct_t_
Definition: fraigInt.h:207
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Fraig_NodeIsMuxType
int Fraig_NodeIsMuxType(Fraig_Node_t *pNode)
Definition: fraigUtil.c:591
Fraig_NodeStruct_t_::p1
Fraig_Node_t * p1
Definition: fraigInt.h:232
Fraig_ManMarkRealFanouts
void Fraig_ManMarkRealFanouts(Fraig_Man_t *p)
Definition: fraigUtil.c:251
Fraig_NodeSimsContained
int Fraig_NodeSimsContained(Fraig_Man_t *pMan, Fraig_Node_t *pNode1, Fraig_Node_t *pNode2)
Definition: fraigUtil.c:784
Fraig_NodeIsAnd
int Fraig_NodeIsAnd(Fraig_Node_t *p)
Definition: fraigApi.c:153
Fraig_NodeIsImplication
int Fraig_NodeIsImplication(Fraig_Man_t *p, Fraig_Node_t *pOld, Fraig_Node_t *pNew, int nBTLimit)
Definition: fraigSat.c:551
Fraig_Dfs
Fraig_NodeVec_t * Fraig_Dfs(Fraig_Man_t *pMan, int fEquiv)
FUNCTION DEFINITIONS ///.
Definition: fraigUtil.c:58
Counter
static int Counter
Definition: extraBddMisc.c:1877
Fraig_PrintBinary
void Fraig_PrintBinary(FILE *pFile, unsigned *pSign, int nBits)
Definition: fraigUtil.c:402
Fraig_CollectSupergate
Fraig_NodeVec_t * Fraig_CollectSupergate(Fraig_Node_t *pNode, int fStopAtMux)
Definition: fraigUtil.c:960
bit_count
static ABC_NAMESPACE_IMPL_START int bit_count[256]
DECLARATIONS ///.
Definition: fraigUtil.c:29
Fraig_IsComplement
#define Fraig_IsComplement(p)
GLOBAL VARIABLES ///.
Definition: fraig.h:107
Fraig_ManPrintRefs
int Fraig_ManPrintRefs(Fraig_Man_t *pMan)
Definition: fraigUtil.c:842
Fraig_CountNodes
int Fraig_CountNodes(Fraig_Man_t *pMan, int fEquiv)
Definition: fraigUtil.c:152
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Fraig_DfsNodes
Fraig_NodeVec_t * Fraig_DfsNodes(Fraig_Man_t *pMan, Fraig_Node_t **ppNodes, int nNodes, int fEquiv)
Definition: fraigUtil.c:100
Fraig_NodeStruct_t_::pRepr
Fraig_Node_t * pRepr
Definition: fraigInt.h:242
Fraig_NodeIsConst
int Fraig_NodeIsConst(Fraig_Node_t *p)
Definition: fraigApi.c:151
Fraig_NodeStruct_t_::Num
int Num
Definition: fraigInt.h:210
Fraig_NodeStruct_t_::TravId2
int TravId2
Definition: fraigInt.h:215
Fraig_NodeIsInSupergate
int Fraig_NodeIsInSupergate(Fraig_Node_t *pOld, Fraig_Node_t *pNew)
Definition: fraigUtil.c:905
Fraig_NodeVecStruct_t_::pArray
Fraig_Node_t ** pArray
Definition: fraigInt.h:267
Fraig_Regular
#define Fraig_Regular(p)
Definition: fraig.h:108
Fraig_NodeStruct_t_::Level
int Level
Definition: fraigInt.h:212
Fraig_MappingSetChoiceLevels
void Fraig_MappingSetChoiceLevels(Fraig_Man_t *pMan, int fMaximum)
Definition: fraigUtil.c:499
Msat_IntVecReadArray
int * Msat_IntVecReadArray(Msat_IntVec_t *p)
Definition: msatVec.c:217
Fraig_NodeStruct_t_::nOnes
unsigned nOnes
Definition: fraigInt.h:229
Fraig_ManCountExors
int Fraig_ManCountExors(Fraig_Man_t *pMan)
Definition: fraigUtil.c:742
Fraig_NodeIsVar
int Fraig_NodeIsVar(Fraig_Node_t *p)
Definition: fraigApi.c:152
assert
#define assert(ex)
Definition: util_old.h:213
Fraig_ManIncrementTravId
void Fraig_ManIncrementTravId(Fraig_Man_t *pMan)
Definition: fraigUtil.c:980
Fraig_Dfs_rec
static void Fraig_Dfs_rec(Fraig_Man_t *pMan, Fraig_Node_t *pNode, Fraig_NodeVec_t *vNodes, int fEquiv)
Definition: fraigUtil.c:122
Fraig_NodeVecStruct_t_::nSize
int nSize
Definition: fraigInt.h:266
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Fraig_NodeStruct_t_::nFanouts
unsigned nFanouts
Definition: fraigInt.h:228
Fraig_CountPis
int Fraig_CountPis(Fraig_Man_t *p, Msat_IntVec_t *vVarNums)
Definition: fraigUtil.c:817
Fraig_NodeStruct_t_::fInv
unsigned fInv
Definition: fraigInt.h:218
Fraig_ManCheckConsistency
int Fraig_ManCheckConsistency(Fraig_Man_t *p)
Definition: fraigUtil.c:312
Fraig_MappingUpdateLevel_rec
int Fraig_MappingUpdateLevel_rec(Fraig_Man_t *pMan, Fraig_Node_t *pNode, int fMaximum)
Definition: fraigUtil.c:449
Fraig_NodeVecStruct_t_
Definition: fraigInt.h:263
Fraig_NodeIsTravIdCurrent
int Fraig_NodeIsTravIdCurrent(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition: fraigUtil.c:1012
Fraig_NodeStruct_t_::pData0
Fraig_Node_t * pData0
Definition: fraigInt.h:251