abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
giaHash.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [giaHash.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Scalable AIG package.]
8 
9  Synopsis [Structural hashing.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: giaHash.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "gia.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 [Returns the place where this node is stored (or should be stored).]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 static inline int Gia_ManHashOne( int iLit0, int iLit1, int iLitC, int TableSize )
46 {
47  unsigned Key = iLitC * 2011;
48  Key += Abc_Lit2Var(iLit0) * 7937;
49  Key += Abc_Lit2Var(iLit1) * 2971;
50  Key += Abc_LitIsCompl(iLit0) * 911;
51  Key += Abc_LitIsCompl(iLit1) * 353;
52  return (int)(Key % TableSize);
53 }
54 static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1, int iLitC )
55 {
56  Gia_Obj_t * pThis;
57  int * pPlace = p->pHTable + Gia_ManHashOne( iLit0, iLit1, iLitC, p->nHTable );
58  assert( p->pMuxes || iLit0 < iLit1 );
59  assert( iLit0 < iLit1 || (!Abc_LitIsCompl(iLit0) && !Abc_LitIsCompl(iLit1)) );
60  assert( iLitC == -1 || !Abc_LitIsCompl(iLit1) );
61  for ( pThis = (*pPlace)? Gia_ManObj(p, Abc_Lit2Var(*pPlace)) : NULL; pThis;
62  pPlace = (int *)&pThis->Value, pThis = (*pPlace)? Gia_ManObj(p, Abc_Lit2Var(*pPlace)) : NULL )
63  if ( Gia_ObjFaninLit0p(p, pThis) == iLit0 && Gia_ObjFaninLit1p(p, pThis) == iLit1 && (p->pMuxes == NULL || Gia_ObjFaninLit2p(p, pThis) == iLitC) )
64  break;
65  return pPlace;
66 }
67 
68 /**Function*************************************************************
69 
70  Synopsis []
71 
72  Description []
73 
74  SideEffects []
75 
76  SeeAlso []
77 
78 ***********************************************************************/
79 int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 )
80 {
81  int iLit0 = Gia_ObjToLit( p, p0 );
82  int iLit1 = Gia_ObjToLit( p, p1 );
83  if ( iLit0 > iLit1 )
84  iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
85  return *Gia_ManHashFind( p, iLit0, iLit1, -1 );
86 }
87 
88 /**Function*************************************************************
89 
90  Synopsis [Starts the hash table.]
91 
92  Description []
93 
94  SideEffects []
95 
96  SeeAlso []
97 
98 ***********************************************************************/
99 void Gia_ManHashAlloc( Gia_Man_t * p )
100 {
101  assert( p->pHTable == NULL );
102  p->nHTable = Abc_PrimeCudd( Gia_ManAndNum(p) ? Gia_ManAndNum(p) + 1000 : p->nObjsAlloc );
103  p->pHTable = ABC_CALLOC( int, p->nHTable );
104 }
105 
106 /**Function*************************************************************
107 
108  Synopsis [Starts the hash table.]
109 
110  Description []
111 
112  SideEffects []
113 
114  SeeAlso []
115 
116 ***********************************************************************/
117 void Gia_ManHashStart( Gia_Man_t * p )
118 {
119  Gia_Obj_t * pObj;
120  int * pPlace, i;
121  Gia_ManHashAlloc( p );
122  Gia_ManCleanValue( p );
123  Gia_ManForEachAnd( p, pObj, i )
124  {
125  pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i), Gia_ObjFaninLit2(p, i) );
126  assert( *pPlace == 0 );
127  *pPlace = Abc_Var2Lit( i, 0 );
128  }
129 }
130 
131 /**Function*************************************************************
132 
133  Synopsis [Stops the hash table.]
134 
135  Description []
136 
137  SideEffects []
138 
139  SeeAlso []
140 
141 ***********************************************************************/
142 void Gia_ManHashStop( Gia_Man_t * p )
143 {
144  ABC_FREE( p->pHTable );
145  p->nHTable = 0;
146 }
147 
148 /**Function*************************************************************
149 
150  Synopsis [Resizes the hash table.]
151 
152  Description []
153 
154  SideEffects []
155 
156  SeeAlso []
157 
158 ***********************************************************************/
159 void Gia_ManHashResize( Gia_Man_t * p )
160 {
161  Gia_Obj_t * pThis;
162  int * pHTableOld, * pPlace;
163  int nHTableOld, iNext, Counter, Counter2, i;
164  assert( p->pHTable != NULL );
165  // replace the table
166  pHTableOld = p->pHTable;
167  nHTableOld = p->nHTable;
168  p->nHTable = Abc_PrimeCudd( 2 * Gia_ManAndNum(p) );
169  p->pHTable = ABC_CALLOC( int, p->nHTable );
170  // rehash the entries from the old table
171  Counter = 0;
172  for ( i = 0; i < nHTableOld; i++ )
173  for ( pThis = (pHTableOld[i]? Gia_ManObj(p, Abc_Lit2Var(pHTableOld[i])) : NULL),
174  iNext = (pThis? pThis->Value : 0);
175  pThis; pThis = (iNext? Gia_ManObj(p, Abc_Lit2Var(iNext)) : NULL),
176  iNext = (pThis? pThis->Value : 0) )
177  {
178  pThis->Value = 0;
179  pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0p(p, pThis), Gia_ObjFaninLit1p(p, pThis), Gia_ObjFaninLit2p(p, pThis) );
180  assert( *pPlace == 0 ); // should not be there
181  *pPlace = Abc_Var2Lit( Gia_ObjId(p, pThis), 0 );
182  assert( *pPlace != 0 );
183  Counter++;
184  }
185  Counter2 = Gia_ManAndNum(p) - Gia_ManBufNum(p);
186  assert( Counter == Counter2 );
187  ABC_FREE( pHTableOld );
188 // if ( p->fVerbose )
189 // printf( "Resizing GIA hash table: %d -> %d.\n", nHTableOld, p->nHTable );
190 }
191 
192 /**Function********************************************************************
193 
194  Synopsis [Profiles the hash table.]
195 
196  Description []
197 
198  SideEffects []
199 
200  SeeAlso []
201 
202 ******************************************************************************/
203 void Gia_ManHashProfile( Gia_Man_t * p )
204 {
205  Gia_Obj_t * pEntry;
206  int i, Counter, Limit;
207  printf( "Table size = %d. Entries = %d. ", p->nHTable, Gia_ManAndNum(p) );
208  printf( "Hits = %d. Misses = %d.\n", (int)p->nHashHit, (int)p->nHashMiss );
209  Limit = Abc_MinInt( 1000, p->nHTable );
210  for ( i = 0; i < Limit; i++ )
211  {
212  Counter = 0;
213  for ( pEntry = (p->pHTable[i]? Gia_ManObj(p, Abc_Lit2Var(p->pHTable[i])) : NULL);
214  pEntry;
215  pEntry = (pEntry->Value? Gia_ManObj(p, Abc_Lit2Var(pEntry->Value)) : NULL) )
216  Counter++;
217  if ( Counter )
218  printf( "%d ", Counter );
219  }
220  printf( "\n" );
221 }
222 
223 /**Function*************************************************************
224 
225  Synopsis [Recognizes what nodes are control and data inputs of a MUX.]
226 
227  Description [If the node is a MUX, returns the control variable C.
228  Assigns nodes T and E to be the then and else variables of the MUX.
229  Node C is never complemented. Nodes T and E can be complemented.
230  This function also recognizes EXOR/NEXOR gates as MUXes.]
231 
232  SideEffects []
233 
234  SeeAlso []
235 
236 ***********************************************************************/
237 static inline Gia_Obj_t * Gia_ObjRecognizeMuxTwo( Gia_Obj_t * pNode0, Gia_Obj_t * pNode1, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE )
238 {
239  assert( !Gia_IsComplement(pNode0) );
240  assert( !Gia_IsComplement(pNode1) );
241  // find the control variable
242  if ( Gia_ObjFanin1(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC1(pNode1)) )
243  {
244 // if ( FrGia_IsComplement(pNode1->p2) )
245  if ( Gia_ObjFaninC1(pNode0) )
246  { // pNode2->p2 is positive phase of C
247  *ppNodeT = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
248  *ppNodeE = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
249  return Gia_ObjChild1(pNode1);//pNode2->p2;
250  }
251  else
252  { // pNode1->p2 is positive phase of C
253  *ppNodeT = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
254  *ppNodeE = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
255  return Gia_ObjChild1(pNode0);//pNode1->p2;
256  }
257  }
258  else if ( Gia_ObjFanin0(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC0(pNode1)) )
259  {
260 // if ( FrGia_IsComplement(pNode1->p1) )
261  if ( Gia_ObjFaninC0(pNode0) )
262  { // pNode2->p1 is positive phase of C
263  *ppNodeT = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
264  *ppNodeE = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
265  return Gia_ObjChild0(pNode1);//pNode2->p1;
266  }
267  else
268  { // pNode1->p1 is positive phase of C
269  *ppNodeT = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
270  *ppNodeE = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
271  return Gia_ObjChild0(pNode0);//pNode1->p1;
272  }
273  }
274  else if ( Gia_ObjFanin0(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC1(pNode1)) )
275  {
276 // if ( FrGia_IsComplement(pNode1->p1) )
277  if ( Gia_ObjFaninC0(pNode0) )
278  { // pNode2->p2 is positive phase of C
279  *ppNodeT = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
280  *ppNodeE = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
281  return Gia_ObjChild1(pNode1);//pNode2->p2;
282  }
283  else
284  { // pNode1->p1 is positive phase of C
285  *ppNodeT = Gia_Not(Gia_ObjChild1(pNode0));//pNode1->p2);
286  *ppNodeE = Gia_Not(Gia_ObjChild0(pNode1));//pNode2->p1);
287  return Gia_ObjChild0(pNode0);//pNode1->p1;
288  }
289  }
290  else if ( Gia_ObjFanin1(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC0(pNode1)) )
291  {
292 // if ( FrGia_IsComplement(pNode1->p2) )
293  if ( Gia_ObjFaninC1(pNode0) )
294  { // pNode2->p1 is positive phase of C
295  *ppNodeT = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
296  *ppNodeE = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
297  return Gia_ObjChild0(pNode1);//pNode2->p1;
298  }
299  else
300  { // pNode1->p2 is positive phase of C
301  *ppNodeT = Gia_Not(Gia_ObjChild0(pNode0));//pNode1->p1);
302  *ppNodeE = Gia_Not(Gia_ObjChild1(pNode1));//pNode2->p2);
303  return Gia_ObjChild1(pNode0);//pNode1->p2;
304  }
305  }
306  assert( 0 ); // this is not MUX
307  return NULL;
308 }
309 
310 
311 /**Function*************************************************************
312 
313  Synopsis [Rehashes AIG with mapping.]
314 
315  Description []
316 
317  SideEffects []
318 
319  SeeAlso []
320 
321 ***********************************************************************/
322 static inline Gia_Obj_t * Gia_ManHashAndP( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 )
323 {
324  return Gia_ObjFromLit( p, Gia_ManHashAnd( p, Gia_ObjToLit(p, p0), Gia_ObjToLit(p, p1) ) );
325 }
326 
327 /**Function*************************************************************
328 
329  Synopsis [Rehashes AIG with mapping.]
330 
331  Description [http://fmv.jku.at/papers/BrummayerBiere-MEMICS06.pdf]
332 
333  SideEffects []
334 
335  SeeAlso []
336 
337 ***********************************************************************/
338 static inline Gia_Obj_t * Gia_ManAddStrash( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 )
339 {
340  Gia_Obj_t * pNode0, * pNode1, * pFanA, * pFanB, * pFanC, * pFanD;
341  assert( p->fAddStrash );
342  pNode0 = Gia_Regular(p0);
343  pNode1 = Gia_Regular(p1);
344  if ( !Gia_ObjIsAnd(pNode0) && !Gia_ObjIsAnd(pNode1) )
345  return NULL;
346  pFanA = Gia_ObjIsAnd(pNode0) ? Gia_ObjChild0(pNode0) : NULL;
347  pFanB = Gia_ObjIsAnd(pNode0) ? Gia_ObjChild1(pNode0) : NULL;
348  pFanC = Gia_ObjIsAnd(pNode1) ? Gia_ObjChild0(pNode1) : NULL;
349  pFanD = Gia_ObjIsAnd(pNode1) ? Gia_ObjChild1(pNode1) : NULL;
350  if ( Gia_IsComplement(p0) )
351  {
352  if ( pFanA == Gia_Not(p1) || pFanB == Gia_Not(p1) )
353  return p1;
354  if ( pFanB == p1 )
355  return Gia_ManHashAndP( p, Gia_Not(pFanA), pFanB );
356  if ( pFanA == p1 )
357  return Gia_ManHashAndP( p, Gia_Not(pFanB), pFanA );
358  }
359  else
360  {
361  if ( pFanA == Gia_Not(p1) || pFanB == Gia_Not(p1) )
362  return Gia_ManConst0(p);
363  if ( pFanA == p1 || pFanB == p1 )
364  return p0;
365  }
366  if ( Gia_IsComplement(p1) )
367  {
368  if ( pFanC == Gia_Not(p0) || pFanD == Gia_Not(p0) )
369  return p0;
370  if ( pFanD == p0 )
371  return Gia_ManHashAndP( p, Gia_Not(pFanC), pFanD );
372  if ( pFanC == p0 )
373  return Gia_ManHashAndP( p, Gia_Not(pFanD), pFanC );
374  }
375  else
376  {
377  if ( pFanC == Gia_Not(p0) || pFanD == Gia_Not(p0) )
378  return Gia_ManConst0(p);
379  if ( pFanC == p0 || pFanD == p0 )
380  return p1;
381  }
382  if ( !Gia_IsComplement(p0) && !Gia_IsComplement(p1) )
383  {
384  if ( pFanA == Gia_Not(pFanC) || pFanA == Gia_Not(pFanD) || pFanB == Gia_Not(pFanC) || pFanB == Gia_Not(pFanD) )
385  return Gia_ManConst0(p);
386  if ( pFanA == pFanC || pFanB == pFanC )
387  return Gia_ManHashAndP( p, p0, pFanD );
388  if ( pFanB == pFanC || pFanB == pFanD )
389  return Gia_ManHashAndP( p, pFanA, p1 );
390  if ( pFanA == pFanD || pFanB == pFanD )
391  return Gia_ManHashAndP( p, p0, pFanC );
392  if ( pFanA == pFanC || pFanA == pFanD )
393  return Gia_ManHashAndP( p, pFanB, p1 );
394  }
395  else if ( Gia_IsComplement(p0) && !Gia_IsComplement(p1) )
396  {
397  if ( pFanA == Gia_Not(pFanC) || pFanA == Gia_Not(pFanD) || pFanB == Gia_Not(pFanC) || pFanB == Gia_Not(pFanD) )
398  return p1;
399  if ( pFanB == pFanC || pFanB == pFanD )
400  return Gia_ManHashAndP( p, Gia_Not(pFanA), p1 );
401  if ( pFanA == pFanC || pFanA == pFanD )
402  return Gia_ManHashAndP( p, Gia_Not(pFanB), p1 );
403  }
404  else if ( !Gia_IsComplement(p0) && Gia_IsComplement(p1) )
405  {
406  if ( pFanC == Gia_Not(pFanA) || pFanC == Gia_Not(pFanB) || pFanD == Gia_Not(pFanA) || pFanD == Gia_Not(pFanB) )
407  return p0;
408  if ( pFanD == pFanA || pFanD == pFanB )
409  return Gia_ManHashAndP( p, Gia_Not(pFanC), p0 );
410  if ( pFanC == pFanA || pFanC == pFanB )
411  return Gia_ManHashAndP( p, Gia_Not(pFanD), p0 );
412  }
413  else // if ( Gia_IsComplement(p0) && Gia_IsComplement(p1) )
414  {
415  if ( pFanA == pFanD && pFanB == Gia_Not(pFanC) )
416  return Gia_Not(pFanA);
417  if ( pFanB == pFanC && pFanA == Gia_Not(pFanD) )
418  return Gia_Not(pFanB);
419  if ( pFanA == pFanC && pFanB == Gia_Not(pFanD) )
420  return Gia_Not(pFanA);
421  if ( pFanB == pFanD && pFanA == Gia_Not(pFanC) )
422  return Gia_Not(pFanB);
423  }
424 /*
425  if ( !Gia_IsComplement(p0) || !Gia_IsComplement(p1) )
426  return NULL;
427  if ( !Gia_ObjIsAnd(pNode0) || !Gia_ObjIsAnd(pNode1) )
428  return NULL;
429  if ( (Gia_ObjFanin0(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC0(pNode1))) ||
430  (Gia_ObjFanin0(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC0(pNode0) ^ Gia_ObjFaninC1(pNode1))) ||
431  (Gia_ObjFanin1(pNode0) == Gia_ObjFanin0(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC0(pNode1))) ||
432  (Gia_ObjFanin1(pNode0) == Gia_ObjFanin1(pNode1) && (Gia_ObjFaninC1(pNode0) ^ Gia_ObjFaninC1(pNode1))) )
433  {
434  Gia_Obj_t * pNodeC, * pNodeT, * pNodeE;
435  int fCompl;
436  pNodeC = Gia_ObjRecognizeMuxTwo( pNode0, pNode1, &pNodeT, &pNodeE );
437  // using non-standard canonical rule for MUX (d0 is not compl; d1 may be compl)
438  if ( (fCompl = Gia_IsComplement(pNodeE)) )
439  {
440  pNodeE = Gia_Not(pNodeE);
441  pNodeT = Gia_Not(pNodeT);
442  }
443  pNode0 = Gia_ManHashAndP( p, Gia_Not(pNodeC), pNodeE );
444  pNode1 = Gia_ManHashAndP( p, pNodeC, pNodeT );
445  p->fAddStrash = 0;
446  pNodeC = Gia_NotCond( Gia_ManHashAndP( p, Gia_Not(pNode0), Gia_Not(pNode1) ), !fCompl );
447  p->fAddStrash = 1;
448  return pNodeC;
449  }
450 */
451  return NULL;
452 }
453 
454 /**Function*************************************************************
455 
456  Synopsis [Hashes XOR gate.]
457 
458  Description []
459 
460  SideEffects []
461 
462  SeeAlso []
463 
464 ***********************************************************************/
465 int Gia_ManHashXorReal( Gia_Man_t * p, int iLit0, int iLit1 )
466 {
467  int fCompl = 0;
468  assert( p->fAddStrash == 0 );
469  if ( iLit0 < 2 )
470  return iLit0 ? Abc_LitNot(iLit1) : iLit1;
471  if ( iLit1 < 2 )
472  return iLit1 ? Abc_LitNot(iLit0) : iLit0;
473  if ( iLit0 == iLit1 )
474  return 0;
475  if ( iLit0 == Abc_LitNot(iLit1) )
476  return 1;
477  if ( (p->nObjs & 0xFF) == 0 && 2 * p->nHTable < Gia_ManAndNum(p) )
478  Gia_ManHashResize( p );
479  if ( iLit0 < iLit1 )
480  iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
481  if ( Abc_LitIsCompl(iLit0) )
482  iLit0 = Abc_LitNot(iLit0), fCompl ^= 1;
483  if ( Abc_LitIsCompl(iLit1) )
484  iLit1 = Abc_LitNot(iLit1), fCompl ^= 1;
485  {
486  int *pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
487  if ( *pPlace )
488  {
489  p->nHashHit++;
490  return Abc_LitNotCond( *pPlace, fCompl );
491  }
492  p->nHashMiss++;
493  if ( p->nObjs < p->nObjsAlloc )
494  *pPlace = Gia_ManAppendXorReal( p, iLit0, iLit1 );
495  else
496  {
497  int iNode = Gia_ManAppendXorReal( p, iLit0, iLit1 );
498  pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
499  assert( *pPlace == 0 );
500  *pPlace = iNode;
501  }
502  return Abc_LitNotCond( *pPlace, fCompl );
503  }
504 }
505 
506 /**Function*************************************************************
507 
508  Synopsis [Hashes MUX gate.]
509 
510  Description []
511 
512  SideEffects []
513 
514  SeeAlso []
515 
516 ***********************************************************************/
517 int Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 )
518 {
519  int fCompl = 0;
520  assert( p->fAddStrash == 0 );
521  if ( iLitC < 2 )
522  return iLitC ? iLit1 : iLit0;
523  if ( iLit0 < 2 )
524  return iLit0 ? Gia_ManHashOr(p, Abc_LitNot(iLitC), iLit1) : Gia_ManHashAnd(p, iLitC, iLit1);
525  if ( iLit1 < 2 )
526  return iLit1 ? Gia_ManHashOr(p, iLitC, iLit0) : Gia_ManHashAnd(p, Abc_LitNot(iLitC), iLit0);
527  assert( iLit0 > 1 && iLit1 > 1 && iLitC > 1 );
528  if ( iLit0 == iLit1 )
529  return iLit0;
530  if ( iLitC == iLit0 || iLitC == Abc_LitNot(iLit1) )
531  return Gia_ManHashAnd(p, iLit0, iLit1);
532  if ( iLitC == iLit1 || iLitC == Abc_LitNot(iLit0) )
533  return Gia_ManHashOr(p, iLit0, iLit1);
534  if ( Abc_Lit2Var(iLit0) == Abc_Lit2Var(iLit1) )
535  return Gia_ManHashXorReal( p, iLitC, iLit0 );
536  if ( iLit0 > iLit1 )
537  iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1, iLitC = Abc_LitNot(iLitC);
538  if ( Abc_LitIsCompl(iLit1) )
539  iLit0 = Abc_LitNot(iLit0), iLit1 = Abc_LitNot(iLit1), fCompl = 1;
540  {
541  int *pPlace = Gia_ManHashFind( p, iLit0, iLit1, iLitC );
542  if ( *pPlace )
543  {
544  p->nHashHit++;
545  return Abc_LitNotCond( *pPlace, fCompl );
546  }
547  p->nHashMiss++;
548  if ( p->nObjs < p->nObjsAlloc )
549  *pPlace = Gia_ManAppendMuxReal( p, iLitC, iLit1, iLit0 );
550  else
551  {
552  int iNode = Gia_ManAppendMuxReal( p, iLitC, iLit1, iLit0 );
553  pPlace = Gia_ManHashFind( p, iLit0, iLit1, iLitC );
554  assert( *pPlace == 0 );
555  *pPlace = iNode;
556  }
557  return Abc_LitNotCond( *pPlace, fCompl );
558  }
559 }
560 
561 /**Function*************************************************************
562 
563  Synopsis [Hashes AND gate.]
564 
565  Description []
566 
567  SideEffects []
568 
569  SeeAlso []
570 
571 ***********************************************************************/
572 int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )
573 {
574  if ( iLit0 < 2 )
575  return iLit0 ? iLit1 : 0;
576  if ( iLit1 < 2 )
577  return iLit1 ? iLit0 : 0;
578  if ( iLit0 == iLit1 )
579  return iLit1;
580  if ( iLit0 == Abc_LitNot(iLit1) )
581  return 0;
582  if ( (p->nObjs & 0xFF) == 0 && 2 * p->nHTable < Gia_ManAndNum(p) )
583  Gia_ManHashResize( p );
584  if ( p->fAddStrash )
585  {
586  Gia_Obj_t * pObj = Gia_ManAddStrash( p, Gia_ObjFromLit(p, iLit0), Gia_ObjFromLit(p, iLit1) );
587  if ( pObj != NULL )
588  return Gia_ObjToLit( p, pObj );
589  }
590  if ( iLit0 > iLit1 )
591  iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
592  {
593  int * pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
594  if ( *pPlace )
595  {
596  p->nHashHit++;
597  return *pPlace;
598  }
599  p->nHashMiss++;
600  if ( p->nObjs < p->nObjsAlloc )
601  return *pPlace = Gia_ManAppendAnd( p, iLit0, iLit1 );
602  else
603  {
604  int iNode = Gia_ManAppendAnd( p, iLit0, iLit1 );
605  pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
606  assert( *pPlace == 0 );
607  return *pPlace = iNode;
608  }
609  }
610 }
611 int Gia_ManHashOr( Gia_Man_t * p, int iLit0, int iLit1 )
612 {
613  return Abc_LitNot(Gia_ManHashAnd( p, Abc_LitNot(iLit0), Abc_LitNot(iLit1) ));
614 }
615 
616 /**Function*************************************************************
617 
618  Synopsis []
619 
620  Description []
621 
622  SideEffects []
623 
624  SeeAlso []
625 
626 ***********************************************************************/
627 int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 )
628 {
629  if ( iLit0 < 2 )
630  return iLit0 ? iLit1 : 0;
631  if ( iLit1 < 2 )
632  return iLit1 ? iLit0 : 0;
633  if ( iLit0 == iLit1 )
634  return iLit1;
635  if ( iLit0 == Abc_LitNot(iLit1) )
636  return 0;
637  if ( iLit0 > iLit1 )
638  iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
639  {
640  int * pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
641  if ( *pPlace )
642  return *pPlace;
643  return -1;
644  }
645 }
646 
647 /**Function*************************************************************
648 
649  Synopsis []
650 
651  Description []
652 
653  SideEffects []
654 
655  SeeAlso []
656 
657 ***********************************************************************/
658 int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 )
659 {
660  int fCompl = Abc_LitIsCompl(iLit0) ^ Abc_LitIsCompl(iLit1);
661  int iTemp0 = Gia_ManHashAnd( p, Abc_LitRegular(iLit0), Abc_LitNot(Abc_LitRegular(iLit1)) );
662  int iTemp1 = Gia_ManHashAnd( p, Abc_LitRegular(iLit1), Abc_LitNot(Abc_LitRegular(iLit0)) );
663  return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
664 }
665 
666 /**Function*************************************************************
667 
668  Synopsis []
669 
670  Description []
671 
672  SideEffects []
673 
674  SeeAlso []
675 
676 ***********************************************************************/
677 int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 )
678 {
679  int iTemp0, iTemp1, fCompl = 0;
680  if ( iData0 > iData1 )
681  iData0 ^= iData1, iData1 ^= iData0, iData0 ^= iData1, iCtrl = Abc_LitNot(iCtrl);
682  if ( Abc_LitIsCompl(iData1) )
683  iData0 = Abc_LitNot(iData0), iData1 = Abc_LitNot(iData1), fCompl = 1;
684  iTemp0 = Gia_ManHashAnd( p, Abc_LitNot(iCtrl), iData0 );
685  iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 );
686  return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl );
687 }
688 
689 /**Function*************************************************************
690 
691  Synopsis []
692 
693  Description []
694 
695  SideEffects []
696 
697  SeeAlso []
698 
699 ***********************************************************************/
700 int Gia_ManHashMaj( Gia_Man_t * p, int iData0, int iData1, int iData2 )
701 {
702  int iTemp0 = Gia_ManHashOr( p, iData1, iData2 );
703  int iTemp1 = Gia_ManHashAnd( p, iData0, iTemp0 );
704  int iTemp2 = Gia_ManHashAnd( p, iData1, iData2 );
705  return Gia_ManHashOr( p, iTemp1, iTemp2 );
706 }
707 
708 /**Function*************************************************************
709 
710  Synopsis [Rehashes AIG.]
711 
712  Description []
713 
714  SideEffects []
715 
716  SeeAlso []
717 
718 ***********************************************************************/
719 Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash )
720 {
721  Gia_Man_t * pNew, * pTemp;
722  Gia_Obj_t * pObj;
723  int i;
724  pNew = Gia_ManStart( Gia_ManObjNum(p) );
725  pNew->pName = Abc_UtilStrsav( p->pName );
726  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
727  pNew->fAddStrash = fAddStrash;
728  Gia_ManHashAlloc( pNew );
729  Gia_ManConst0(p)->Value = 0;
730  Gia_ManForEachObj( p, pObj, i )
731  {
732  //if ( Gia_ObjIsBuf(pObj) )
733  // pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
734  //else
735  if ( Gia_ObjIsAnd(pObj) )
736  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
737  else if ( Gia_ObjIsCi(pObj) )
738  pObj->Value = Gia_ManAppendCi( pNew );
739  else if ( Gia_ObjIsCo(pObj) )
740  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
741  }
742  Gia_ManHashStop( pNew );
743  pNew->fAddStrash = 0;
744  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
745 // printf( "Top gate is %s\n", Gia_ObjFaninC0(Gia_ManCo(pNew, 0))? "OR" : "AND" );
746  pNew = Gia_ManCleanup( pTemp = pNew );
747  Gia_ManStop( pTemp );
748  return pNew;
749 }
750 
751 
752 /**Function*************************************************************
753 
754  Synopsis [Creates well-balanced AND gate.]
755 
756  Description []
757 
758  SideEffects []
759 
760  SeeAlso []
761 
762 ***********************************************************************/
763 int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits )
764 {
765  if ( Vec_IntSize(vLits) == 0 )
766  return 0;
767  while ( Vec_IntSize(vLits) > 1 )
768  {
769  int i, k = 0, Lit1, Lit2, LitRes;
770  Vec_IntForEachEntryDouble( vLits, Lit1, Lit2, i )
771  {
772  LitRes = Gia_ManHashAnd( p, Lit1, Lit2 );
773  Vec_IntWriteEntry( vLits, k++, LitRes );
774  }
775  if ( Vec_IntSize(vLits) & 1 )
776  Vec_IntWriteEntry( vLits, k++, Vec_IntEntryLast(vLits) );
777  Vec_IntShrink( vLits, k );
778  }
779  assert( Vec_IntSize(vLits) == 1 );
780  return Vec_IntEntry(vLits, 0);
781 }
782 
783 ////////////////////////////////////////////////////////////////////////
784 /// END OF FILE ///
785 ////////////////////////////////////////////////////////////////////////
786 
787 
788 ABC_NAMESPACE_IMPL_END
789 
Gia_Man_t_::nObjsAlloc
int nObjsAlloc
Definition: gia.h:102
Gia_ObjToLit
static int Gia_ObjToLit(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:497
Gia_ManHashMaj
int Gia_ManHashMaj(Gia_Man_t *p, int iData0, int iData1, int iData2)
Definition: giaHash.c:700
Gia_ManAppendAnd
static int Gia_ManAppendAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:592
Gia_ObjChild0
static Gia_Obj_t * Gia_ObjChild0(Gia_Obj_t *pObj)
Definition: gia.h:457
Gia_Man_t_::nHashMiss
word nHashMiss
Definition: gia.h:168
Gia_ObjFaninLit0
static int Gia_ObjFaninLit0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:466
Gia_ObjFaninLit2
static int Gia_ObjFaninLit2(Gia_Man_t *p, int ObjId)
Definition: gia.h:468
Abc_PrimeCudd
static int Abc_PrimeCudd(unsigned int p)
Definition: abc_global.h:383
Gia_ManAppendMuxReal
static int Gia_ManAppendMuxReal(Gia_Man_t *p, int iLitC, int iLit1, int iLit0)
Definition: gia.h:664
Gia_ManAddStrash
static Gia_Obj_t * Gia_ManAddStrash(Gia_Man_t *p, Gia_Obj_t *p0, Gia_Obj_t *p1)
Definition: giaHash.c:338
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_Man_t_::pHTable
int * pHTable
Definition: gia.h:110
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Gia_Regular
static Gia_Obj_t * Gia_Regular(Gia_Obj_t *p)
Definition: gia.h:377
Gia_ObjFaninLit2p
static int Gia_ObjFaninLit2p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:471
Gia_ObjFromLit
static Gia_Obj_t * Gia_ObjFromLit(Gia_Man_t *p, int iLit)
Definition: gia.h:496
Gia_ObjFaninLit0p
static int Gia_ObjFaninLit0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:469
Gia_ManHashMux
int Gia_ManHashMux(Gia_Man_t *p, int iCtrl, int iData1, int iData0)
Definition: giaHash.c:677
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Gia_ManCleanValue
void Gia_ManCleanValue(Gia_Man_t *p)
Definition: giaUtil.c:310
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Gia_ObjRecognizeMuxTwo
static Gia_Obj_t * Gia_ObjRecognizeMuxTwo(Gia_Obj_t *pNode0, Gia_Obj_t *pNode1, Gia_Obj_t **ppNodeT, Gia_Obj_t **ppNodeE)
Definition: giaHash.c:237
Gia_Man_t_::pMuxes
unsigned * pMuxes
Definition: gia.h:104
Gia_ManSetRegNum
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
Gia_ManHashAndMulti
int Gia_ManHashAndMulti(Gia_Man_t *p, Vec_Int_t *vLits)
Definition: giaHash.c:763
Gia_Man_t_::nObjs
int nObjs
Definition: gia.h:101
Gia_ManHashXor
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:658
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Gia_Obj_t_
Definition: gia.h:75
Gia_ObjChild1
static Gia_Obj_t * Gia_ObjChild1(Gia_Obj_t *pObj)
Definition: gia.h:458
Gia_Not
static Gia_Obj_t * Gia_Not(Gia_Obj_t *p)
Definition: gia.h:378
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Gia_ManHashMuxReal
int Gia_ManHashMuxReal(Gia_Man_t *p, int iLitC, int iLit1, int iLit0)
Definition: giaHash.c:517
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Gia_ManHashFind
static int * Gia_ManHashFind(Gia_Man_t *p, int iLit0, int iLit1, int iLitC)
Definition: giaHash.c:54
Gia_ManHashAndP
static Gia_Obj_t * Gia_ManHashAndP(Gia_Man_t *p, Gia_Obj_t *p0, Gia_Obj_t *p1)
Definition: giaHash.c:322
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
Gia_ObjFaninLit1
static int Gia_ObjFaninLit1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:467
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Gia_ManHashXorReal
int Gia_ManHashXorReal(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:465
Gia_ObjFanin1Copy
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Gia_Man_t_::pSpec
char * pSpec
Definition: gia.h:98
Gia_Man_t_::nHashHit
word nHashHit
Definition: gia.h:167
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Gia_ManHashProfile
void Gia_ManHashProfile(Gia_Man_t *p)
Definition: giaHash.c:203
Gia_ManHashOne
static ABC_NAMESPACE_IMPL_START int Gia_ManHashOne(int iLit0, int iLit1, int iLitC, int TableSize)
DECLARATIONS ///.
Definition: giaHash.c:45
Vec_IntForEachEntryDouble
#define Vec_IntForEachEntryDouble(vVec, Entry1, Entry2, i)
Definition: vecInt.h:66
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Gia_Man_t_::nHTable
int nHTable
Definition: gia.h:111
Vec_IntEntryLast
static int Vec_IntEntryLast(Vec_Int_t *p)
Definition: bblif.c:319
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Gia_ManHashResize
void Gia_ManHashResize(Gia_Man_t *p)
Definition: giaHash.c:159
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Gia_IsComplement
static int Gia_IsComplement(Gia_Obj_t *p)
Definition: gia.h:380
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
Gia_ManHashLookup
int Gia_ManHashLookup(Gia_Man_t *p, Gia_Obj_t *p0, Gia_Obj_t *p1)
Definition: giaHash.c:79
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_ManHashAndTry
int Gia_ManHashAndTry(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:627
Gia_Man_t_
Definition: gia.h:95
Gia_ManBufNum
static int Gia_ManBufNum(Gia_Man_t *p)
Definition: gia.h:392
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Gia_ManHashOr
int Gia_ManHashOr(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:611
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Abc_LitRegular
static int Abc_LitRegular(int Lit)
Definition: abc_global.h:268
assert
#define assert(ex)
Definition: util_old.h:213
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Gia_Man_t_::fAddStrash
int fAddStrash
Definition: gia.h:112
Gia_ObjFaninLit1p
static int Gia_ObjFaninLit1p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:470
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Gia_ManHashStart
void Gia_ManHashStart(Gia_Man_t *p)
Definition: giaHash.c:117
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Gia_ManAppendXorReal
static int Gia_ManAppendXorReal(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:639
Gia_ManRehash
Gia_Man_t * Gia_ManRehash(Gia_Man_t *p, int fAddStrash)
Definition: giaHash.c:719
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387