abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
extraUtilPerm.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [extraUtilPerm.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [extra]
8 
9  Synopsis [Permutation computation.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: extraUtilPerm.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include <stdio.h>
22 #include <stdlib.h>
23 #include <string.h>
24 #include <assert.h>
25 #include "misc/vec/vec.h"
26 #include "aig/gia/gia.h"
27 
28 ABC_NAMESPACE_IMPL_START
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 typedef enum
35 {
36  ABC_ZDD_OPER_NONE,
37  ABC_ZDD_OPER_DIFF,
38  ABC_ZDD_OPER_UNION,
39  ABC_ZDD_OPER_MIN_UNION,
40  ABC_ZDD_OPER_INTER,
41  ABC_ZDD_OPER_PERM,
42  ABC_ZDD_OPER_PERM_PROD,
43  ABC_ZDD_OPER_COF0,
44  ABC_ZDD_OPER_COF1,
45  ABC_ZDD_OPER_THRESH,
46  ABC_ZDD_OPER_DOT_PROD,
47  ABC_ZDD_OPER_DOT_PROD_6,
48  ABC_ZDD_OPER_INSERT,
49  ABC_ZDD_OPER_PATHS,
50  ABC_ZDD_OPER_NODES,
51  ABC_ZDD_OPER_ITE
52 } Abc_ZddOper;
53 
54 typedef struct Abc_ZddObj_ Abc_ZddObj;
55 struct Abc_ZddObj_
56 {
57  unsigned Var : 31;
58  unsigned Mark : 1;
59  unsigned True;
60  unsigned False;
61 };
62 
63 typedef struct Abc_ZddEnt_ Abc_ZddEnt;
64 struct Abc_ZddEnt_
65 {
66  int Arg0;
67  int Arg1;
68  int Arg2;
69  int Res;
70 };
71 
72 typedef struct Abc_ZddMan_ Abc_ZddMan;
73 struct Abc_ZddMan_
74 {
75  int nVars;
76  int nObjs;
77  int nObjsAlloc;
78  int nPermSize;
79  unsigned nUniqueMask;
80  unsigned nCacheMask;
81  int * pUnique;
82  int * pNexts;
83  Abc_ZddEnt * pCache;
84  Abc_ZddObj * pObjs;
85  int nCacheLookups;
86  int nCacheMisses;
87  word nMemory;
88  int * pV2TI;
89  int * pV2TJ;
90  int * pT2V;
91 };
92 
93 static inline int Abc_ZddIthVar( int i ) { return i + 2; }
94 static inline unsigned Abc_ZddHash( int Arg0, int Arg1, int Arg2 ) { return 12582917 * Arg0 + 4256249 * Arg1 + 741457 * Arg2; }
95 
96 static inline Abc_ZddObj * Abc_ZddNode( Abc_ZddMan * p, int i ) { return p->pObjs + i; }
97 static inline int Abc_ZddObjId( Abc_ZddMan * p, Abc_ZddObj * pObj ) { return pObj - p->pObjs; }
98 static inline int Abc_ZddObjVar( Abc_ZddMan * p, int i ) { return Abc_ZddNode(p, i)->Var; }
99 
100 static inline void Abc_ZddSetVarIJ( Abc_ZddMan * p, int i, int j, int v ) { assert( i < j ); p->pT2V[i * p->nPermSize + j] = v; }
101 static inline int Abc_ZddVarIJ( Abc_ZddMan * p, int i, int j ) { assert( i < j ); return p->pT2V[i * p->nPermSize + j]; }
102 static inline int Abc_ZddVarsClash( Abc_ZddMan * p, int v0, int v1 ) { return p->pV2TI[v0] == p->pV2TI[v1] || p->pV2TJ[v0] == p->pV2TJ[v1] || p->pV2TI[v0] == p->pV2TJ[v1] || p->pV2TJ[v0] == p->pV2TI[v1]; }
103 
104 ////////////////////////////////////////////////////////////////////////
105 /// FUNCTION DEFINITIONS ///
106 ////////////////////////////////////////////////////////////////////////
107 
108 /**Function*************************************************************
109 
110  Synopsis []
111 
112  Description []
113 
114  SideEffects []
115 
116  SeeAlso []
117 
118 ***********************************************************************/
119 static inline int Abc_ZddCacheLookup( Abc_ZddMan * p, int Arg0, int Arg1, int Arg2 )
120 {
121  Abc_ZddEnt * pEnt = p->pCache + (Abc_ZddHash(Arg0, Arg1, Arg2) & p->nCacheMask);
122  p->nCacheLookups++;
123  return (pEnt->Arg0 == Arg0 && pEnt->Arg1 == Arg1 && pEnt->Arg2 == Arg2) ? pEnt->Res : -1;
124 }
125 static inline int Abc_ZddCacheInsert( Abc_ZddMan * p, int Arg0, int Arg1, int Arg2, int Res )
126 {
127  Abc_ZddEnt * pEnt = p->pCache + (Abc_ZddHash(Arg0, Arg1, Arg2) & p->nCacheMask);
128  pEnt->Arg0 = Arg0; pEnt->Arg1 = Arg1; pEnt->Arg2 = Arg2; pEnt->Res = Res;
129  p->nCacheMisses++;
130  assert( Res >= 0 );
131  return Res;
132 }
133 static inline int Abc_ZddUniqueLookup( Abc_ZddMan * p, int Var, int True, int False )
134 {
135  int *q = p->pUnique + (Abc_ZddHash(Var, True, False) & p->nUniqueMask);
136  for ( ; *q; q = p->pNexts + *q )
137  if ( p->pObjs[*q].Var == (unsigned)Var && p->pObjs[*q].True == (unsigned)True && p->pObjs[*q].False == (unsigned)False )
138  return *q;
139  return 0;
140 }
141 static inline int Abc_ZddUniqueCreate( Abc_ZddMan * p, int Var, int True, int False )
142 {
143  assert( Var >= 0 && Var < p->nVars );
144  assert( Var < Abc_ZddObjVar(p, True) );
145  assert( Var < Abc_ZddObjVar(p, False) );
146  if ( True == 0 )
147  return False;
148  {
149  int *q = p->pUnique + (Abc_ZddHash(Var, True, False) & p->nUniqueMask);
150  for ( ; *q; q = p->pNexts + *q )
151  if ( p->pObjs[*q].Var == (unsigned)Var && p->pObjs[*q].True == (unsigned)True && p->pObjs[*q].False == (unsigned)False )
152  return *q;
153  if ( p->nObjs == p->nObjsAlloc )
154  printf( "Aborting because the number of nodes exceeded %d.\n", p->nObjsAlloc ), fflush(stdout);
155  assert( p->nObjs < p->nObjsAlloc );
156  *q = p->nObjs++;
157  p->pObjs[*q].Var = Var;
158  p->pObjs[*q].True = True;
159  p->pObjs[*q].False = False;
160 // printf( "Added node %3d: Var = %3d. True = %3d. False = %3d\n", *q, Var, True, False );
161  return *q;
162  }
163 }
164 int Abc_ZddBuildSet( Abc_ZddMan * p, int * pSet, int Size )
165 {
166  int i, Res = 1;
167  Vec_IntSelectSort( pSet, Size );
168  for ( i = Size - 1; i >= 0; i-- )
169  Res = Abc_ZddUniqueCreate( p, pSet[i], Res, 0 );
170  return Res;
171 }
172 
173 /**Function*************************************************************
174 
175  Synopsis []
176 
177  Description []
178 
179  SideEffects []
180 
181  SeeAlso []
182 
183 ***********************************************************************/
184 Abc_ZddMan * Abc_ZddManAlloc( int nVars, int nObjs )
185 {
186  Abc_ZddMan * p; int i;
187  p = ABC_CALLOC( Abc_ZddMan, 1 );
188  p->nVars = nVars;
189  p->nObjsAlloc = nObjs;
190  p->nUniqueMask = (1 << Abc_Base2Log(nObjs)) - 1;
191  p->nCacheMask = (1 << Abc_Base2Log(nObjs)) - 1;
192  p->pUnique = ABC_CALLOC( int, p->nUniqueMask + 1 );
193  p->pNexts = ABC_CALLOC( int, p->nObjsAlloc );
194  p->pCache = ABC_CALLOC( Abc_ZddEnt, p->nCacheMask + 1 );
195  p->pObjs = ABC_CALLOC( Abc_ZddObj, p->nObjsAlloc );
196  p->nObjs = 2;
197  memset( p->pObjs, 0xff, sizeof(Abc_ZddObj) * 2 );
198  p->pObjs[0].Var = nVars;
199  p->pObjs[1].Var = nVars;
200  for ( i = 0; i < nVars; i++ )
201  Abc_ZddUniqueCreate( p, i, 1, 0 );
202  assert( p->nObjs == nVars + 2 );
203  p->nMemory = sizeof(Abc_ZddMan)/4 +
204  p->nUniqueMask + 1 + p->nObjsAlloc +
205  (p->nCacheMask + 1) * sizeof(Abc_ZddEnt)/4 +
206  p->nObjsAlloc * sizeof(Abc_ZddObj)/4;
207  return p;
208 }
209 void Abc_ZddManCreatePerms( Abc_ZddMan * p, int nPermSize )
210 {
211  int i, j, v = 0;
212  assert( 2 * p->nVars == nPermSize * (nPermSize - 1) );
213  assert( p->nPermSize == 0 );
214  p->nPermSize = nPermSize;
215  p->pV2TI = ABC_FALLOC( int, p->nVars );
216  p->pV2TJ = ABC_FALLOC( int, p->nVars );
217  p->pT2V = ABC_FALLOC( int, p->nPermSize * p->nPermSize );
218  for ( i = 0; i < nPermSize; i++ )
219  for ( j = i + 1; j < nPermSize; j++ )
220  {
221  p->pV2TI[v] = i;
222  p->pV2TJ[v] = j;
223  Abc_ZddSetVarIJ( p, i, j, v++ );
224  }
225  assert( v == p->nVars );
226 }
227 void Abc_ZddManFree( Abc_ZddMan * p )
228 {
229  printf( "ZDD stats: Var = %d Obj = %d Alloc = %d Hit = %d Miss = %d ",
230  p->nVars, p->nObjs, p->nObjsAlloc, p->nCacheLookups-p->nCacheMisses, p->nCacheMisses );
231  printf( "Mem = %.2f MB\n", 4.0*(int)(p->nMemory/(1<<20)) );
232  ABC_FREE( p->pT2V );
233  ABC_FREE( p->pV2TI );
234  ABC_FREE( p->pV2TJ );
235  ABC_FREE( p->pUnique );
236  ABC_FREE( p->pNexts );
237  ABC_FREE( p->pCache );
238  ABC_FREE( p->pObjs );
239  ABC_FREE( p );
240 }
241 
242 /**Function*************************************************************
243 
244  Synopsis []
245 
246  Description []
247 
248  SideEffects []
249 
250  SeeAlso []
251 
252 ***********************************************************************/
253 int Abc_ZddDiff( Abc_ZddMan * p, int a, int b )
254 {
255  Abc_ZddObj * A, * B;
256  int r0, r1, r;
257  if ( a == 0 ) return 0;
258  if ( b == 0 ) return a;
259  if ( a == b ) return 0;
260  if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_DIFF)) >= 0 )
261  return r;
262  A = Abc_ZddNode( p, a );
263  B = Abc_ZddNode( p, b );
264  if ( A->Var < B->Var )
265  r0 = Abc_ZddDiff( p, A->False, b ),
266  r = Abc_ZddUniqueCreate( p, A->Var, A->True, r0 );
267  else if ( A->Var > B->Var )
268  r = Abc_ZddDiff( p, a, B->False );
269  else
270  r0 = Abc_ZddDiff( p, A->False, B->False ),
271  r1 = Abc_ZddDiff( p, A->True, B->True ),
272  r = Abc_ZddUniqueCreate( p, A->Var, A->True, r0 );
273  return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_DIFF, r );
274 }
275 int Abc_ZddUnion( Abc_ZddMan * p, int a, int b )
276 {
277  Abc_ZddObj * A, * B;
278  int r0, r1, r;
279  if ( a == 0 ) return b;
280  if ( b == 0 ) return a;
281  if ( a == b ) return a;
282  if ( a > b ) return Abc_ZddUnion( p, b, a );
283  if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_UNION)) >= 0 )
284  return r;
285  A = Abc_ZddNode( p, a );
286  B = Abc_ZddNode( p, b );
287  if ( A->Var < B->Var )
288  r0 = Abc_ZddUnion( p, A->False, b ),
289  r1 = A->True;
290  else if ( A->Var > B->Var )
291  r0 = Abc_ZddUnion( p, a, B->False ),
292  r1 = B->True;
293  else
294  r0 = Abc_ZddUnion( p, A->False, B->False ),
295  r1 = Abc_ZddUnion( p, A->True, B->True );
296  r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 );
297  return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_UNION, r );
298 }
299 int Abc_ZddMinUnion( Abc_ZddMan * p, int a, int b )
300 {
301  Abc_ZddObj * A, * B;
302  int r0, r1, r;
303  if ( a == 0 ) return b;
304  if ( b == 0 ) return a;
305  if ( a == b ) return a;
306  if ( a > b ) return Abc_ZddMinUnion( p, b, a );
307  if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_MIN_UNION)) >= 0 )
308  return r;
309  A = Abc_ZddNode( p, a );
310  B = Abc_ZddNode( p, b );
311  if ( A->Var < B->Var )
312  r0 = Abc_ZddMinUnion( p, A->False, b ),
313  r1 = A->True;
314  else if ( A->Var > B->Var )
315  r0 = Abc_ZddMinUnion( p, a, B->False ),
316  r1 = B->True;
317  else
318  r0 = Abc_ZddMinUnion( p, A->False, B->False ),
319  r1 = Abc_ZddMinUnion( p, A->True, B->True );
320  r1 = Abc_ZddDiff( p, r1, r0 ); // assume args are minimal
321  r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 );
322  return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_MIN_UNION, r );
323 }
324 int Abc_ZddIntersect( Abc_ZddMan * p, int a, int b )
325 {
326  Abc_ZddObj * A, * B;
327  int r0, r1, r;
328  if ( a == 0 ) return 0;
329  if ( b == 0 ) return 0;
330  if ( a == b ) return a;
331  if ( a > b ) return Abc_ZddIntersect( p, b, a );
332  if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_INTER)) >= 0 )
333  return r;
334  A = Abc_ZddNode( p, a );
335  B = Abc_ZddNode( p, b );
336  if ( A->Var < B->Var )
337  r0 = Abc_ZddIntersect( p, A->False, b ),
338  r1 = A->True;
339  else if ( A->Var > B->Var )
340  r0 = Abc_ZddIntersect( p, a, B->False ),
341  r1 = B->True;
342  else
343  r0 = Abc_ZddIntersect( p, A->False, B->False ),
344  r1 = Abc_ZddIntersect( p, A->True, B->True );
345  r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 );
346  return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_INTER, r );
347 }
348 int Abc_ZddCof0( Abc_ZddMan * p, int a, int Var )
349 {
350  Abc_ZddObj * A;
351  int r0, r1, r;
352  if ( a < 2 ) return a;
353  A = Abc_ZddNode( p, a );
354  if ( (int)A->Var > Var )
355  return a;
356  if ( (r = Abc_ZddCacheLookup(p, a, Var, ABC_ZDD_OPER_COF0)) >= 0 )
357  return r;
358  if ( (int)A->Var < Var )
359  r0 = Abc_ZddCof0( p, A->False, Var ),
360  r1 = Abc_ZddCof0( p, A->True, Var ),
361  r = Abc_ZddUniqueCreate( p, A->Var, r1, r0 );
362  else
363  r = Abc_ZddCof0( p, A->False, Var );
364  return Abc_ZddCacheInsert( p, a, Var, ABC_ZDD_OPER_COF0, r );
365 }
366 int Abc_ZddCof1( Abc_ZddMan * p, int a, int Var )
367 {
368  Abc_ZddObj * A;
369  int r0, r1, r;
370  if ( a < 2 ) return a;
371  A = Abc_ZddNode( p, a );
372  if ( (int)A->Var > Var )
373  return a;
374  if ( (r = Abc_ZddCacheLookup(p, a, Var, ABC_ZDD_OPER_COF1)) >= 0 )
375  return r;
376  if ( (int)A->Var < Var )
377  r0 = Abc_ZddCof1( p, A->False, Var ),
378  r1 = Abc_ZddCof1( p, A->True, Var );
379  else
380  r0 = 0,
381  r1 = Abc_ZddCof1( p, A->True, Var );
382  r = Abc_ZddUniqueCreate( p, A->Var, r1, r0 );
383  return Abc_ZddCacheInsert( p, a, Var, ABC_ZDD_OPER_COF1, r );
384 }
385 int Abc_ZddCountPaths( Abc_ZddMan * p, int a )
386 {
387  Abc_ZddObj * A;
388  int r;
389  if ( a < 2 ) return a;
390  if ( (r = Abc_ZddCacheLookup(p, a, 0, ABC_ZDD_OPER_PATHS)) >= 0 )
391  return r;
392  A = Abc_ZddNode( p, a );
393  r = Abc_ZddCountPaths( p, A->False ) + Abc_ZddCountPaths( p, A->True );
394  return Abc_ZddCacheInsert( p, a, 0, ABC_ZDD_OPER_PATHS, r );
395 }
396 /*
397 int Abc_ZddCountNodes( Abc_ZddMan * p, int a )
398 {
399  Abc_ZddObj * A;
400  int r;
401  if ( a < 2 ) return 0;
402  if ( (r = Abc_ZddCacheLookup(p, a, 0, ABC_ZDD_OPER_NODES)) >= 0 )
403  return r;
404  A = Abc_ZddNode( p, a );
405  r = 1 + Abc_ZddCountNodes( p, A->False ) + Abc_ZddCountNodes( p, A->True );
406  return Abc_ZddCacheInsert( p, a, 0, ABC_ZDD_OPER_NODES, r );
407 }
408 */
409 int Abc_ZddCount_rec( Abc_ZddMan * p, int i )
410 {
411  Abc_ZddObj * A;
412  if ( i < 2 )
413  return 0;
414  A = Abc_ZddNode( p, i );
415  if ( A->Mark )
416  return 0;
417  A->Mark = 1;
418  return 1 + Abc_ZddCount_rec(p, A->False) + Abc_ZddCount_rec(p, A->True);
419 }
420 void Abc_ZddUnmark_rec( Abc_ZddMan * p, int i )
421 {
422  Abc_ZddObj * A;
423  if ( i < 2 )
424  return;
425  A = Abc_ZddNode( p, i );
426  if ( !A->Mark )
427  return;
428  A->Mark = 0;
429  Abc_ZddUnmark_rec( p, A->False );
430  Abc_ZddUnmark_rec( p, A->True );
431 }
432 int Abc_ZddCountNodes( Abc_ZddMan * p, int i )
433 {
434  int Count = Abc_ZddCount_rec( p, i );
435  Abc_ZddUnmark_rec( p, i );
436  return Count;
437 }
438 int Abc_ZddCountNodesArray( Abc_ZddMan * p, Vec_Int_t * vNodes )
439 {
440  int i, Id, Count = 0;
441  Vec_IntForEachEntry( vNodes, Id, i )
442  Count += Abc_ZddCount_rec( p, Id );
443  Vec_IntForEachEntry( vNodes, Id, i )
444  Abc_ZddUnmark_rec( p, Id );
445  return Count;
446 }
447 
448 /**Function*************************************************************
449 
450  Synopsis []
451 
452  Description []
453 
454  SideEffects []
455 
456  SeeAlso []
457 
458 ***********************************************************************/
459 int Abc_ZddThresh( Abc_ZddMan * p, int a, int b )
460 {
461  Abc_ZddObj * A;
462  int r0, r1, r;
463  if ( a < 2 ) return a;
464  if ( b == 0 ) return 0;
465  if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_THRESH)) >= 0 )
466  return r;
467  A = Abc_ZddNode( p, a );
468  r0 = Abc_ZddThresh( p, A->False, b ),
469  r1 = Abc_ZddThresh( p, A->True, b-1 );
470  r = Abc_ZddUniqueCreate( p, A->Var, r1, r0 );
471  return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_THRESH, r );
472 }
473 int Abc_ZddDotProduct( Abc_ZddMan * p, int a, int b )
474 {
475  Abc_ZddObj * A, * B;
476  int r0, r1, b2, t1, t2, r;
477  if ( a == 0 ) return 0;
478  if ( b == 0 ) return 0;
479  if ( a == 1 ) return b;
480  if ( b == 1 ) return a;
481  if ( a > b ) return Abc_ZddDotProduct( p, b, a );
482  if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_DOT_PROD)) >= 0 )
483  return r;
484  A = Abc_ZddNode( p, a );
485  B = Abc_ZddNode( p, b );
486  if ( A->Var < B->Var )
487  r0 = Abc_ZddDotProduct( p, A->False, b ),
488  r1 = Abc_ZddDotProduct( p, A->True, b );
489  else if ( A->Var > B->Var )
490  r0 = Abc_ZddDotProduct( p, a, B->False ),
491  r1 = Abc_ZddDotProduct( p, a, B->True );
492  else
493  r0 = Abc_ZddDotProduct( p, A->False, B->False ),
494  b2 = Abc_ZddUnion( p, B->False, B->True ),
495  t1 = Abc_ZddDotProduct( p, A->True, b2 ),
496  t2 = Abc_ZddDotProduct( p, A->False, B->True ),
497  r1 = Abc_ZddUnion( p, t1, t2 );
498  r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 );
499  return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_DOT_PROD, r );
500 }
501 int Abc_ZddDotMinProduct6( Abc_ZddMan * p, int a, int b )
502 {
503  Abc_ZddObj * A, * B;
504  int r0, r1, b2, t1, t2, r;
505  if ( a == 0 ) return 0;
506  if ( b == 0 ) return 0;
507  if ( a == 1 ) return b;
508  if ( b == 1 ) return a;
509  if ( a > b ) return Abc_ZddDotMinProduct6( p, b, a );
510  if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_DOT_PROD_6)) >= 0 )
511  return r;
512  A = Abc_ZddNode( p, a );
513  B = Abc_ZddNode( p, b );
514  if ( A->Var < B->Var )
515  r0 = Abc_ZddDotMinProduct6( p, A->False, b ),
516  r1 = Abc_ZddDotMinProduct6( p, A->True, b );
517  else if ( A->Var > B->Var )
518  r0 = Abc_ZddDotMinProduct6( p, a, B->False ),
519  r1 = Abc_ZddDotMinProduct6( p, a, B->True );
520  else
521  r0 = Abc_ZddDotMinProduct6( p, A->False, B->False ),
522  b2 = Abc_ZddMinUnion( p, B->False, B->True ),
523  t1 = Abc_ZddDotMinProduct6( p, A->True, b2 ),
524  t2 = Abc_ZddDotMinProduct6( p, A->False, B->True ),
525  r1 = Abc_ZddMinUnion( p, t1, t2 );
526  r1 = Abc_ZddThresh( p, r1, 5 ),
527  r1 = Abc_ZddDiff( p, r1, r0 );
528  r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 );
529  return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_DOT_PROD_6, r );
530 }
531 
532 /**Function*************************************************************
533 
534  Synopsis []
535 
536  Description []
537 
538  SideEffects []
539 
540  SeeAlso []
541 
542 ***********************************************************************/
543 int Abc_ZddPerm( Abc_ZddMan * p, int a, int Var )
544 {
545  Abc_ZddObj * A;
546  int r0, r1, r;
547  assert( Var < p->nVars );
548  if ( a == 0 ) return 0;
549  if ( a == 1 ) return Abc_ZddIthVar(Var);
550  if ( (r = Abc_ZddCacheLookup(p, a, Var, ABC_ZDD_OPER_PERM)) >= 0 )
551  return r;
552  A = Abc_ZddNode( p, a );
553  if ( p->pV2TI[A->Var] > p->pV2TI[Var] ) // Ai > Bi
554  r = Abc_ZddUniqueCreate( p, Var, a, 0 );
555  else if ( (int)A->Var == Var ) // Ai == Bi && Aj == Bj
556  r0 = Abc_ZddPerm( p, A->False, Var ),
557  r = Abc_ZddUnion( p, r0, A->True );
558  else
559  {
560  int VarPerm, VarTop;
561  int Ai = p->pV2TI[A->Var];
562  int Aj = p->pV2TJ[A->Var];
563  int Bi = p->pV2TI[Var];
564  int Bj = p->pV2TJ[Var];
565  assert( Ai < Aj && Bi < Bj && Ai <= Bi );
566  if ( Aj == Bi )
567  VarPerm = Var,
568  VarTop = Abc_ZddVarIJ(p, Ai, Bj);
569  else if ( Aj == Bj )
570  VarPerm = Var,
571  VarTop = Abc_ZddVarIJ(p, Ai, Bi);
572  else if ( Ai == Bi )
573  VarPerm = Abc_ZddVarIJ(p, Abc_MinInt(Aj, Bj), Abc_MaxInt(Aj, Bj)),
574  VarTop = A->Var;
575  else // no clash
576  VarPerm = Var,
577  VarTop = A->Var;
578  assert( p->pV2TI[VarPerm] > p->pV2TI[VarTop] );
579  r0 = Abc_ZddPerm( p, A->False, Var );
580  r1 = Abc_ZddPerm( p, A->True, VarPerm );
581  assert( Abc_ZddObjVar(p, r1) > VarTop );
582  if ( Abc_ZddObjVar(p, r0) > VarTop )
583  r = Abc_ZddUniqueCreate( p, VarTop, r1, r0 );
584  else
585  r1 = Abc_ZddUniqueCreate( p, VarTop, r1, 0 ),
586  r = Abc_ZddUnion( p, r0, r1 );
587  }
588  return Abc_ZddCacheInsert( p, a, Var, ABC_ZDD_OPER_PERM, r );
589 }
590 int Abc_ZddPermProduct( Abc_ZddMan * p, int a, int b )
591 {
592  Abc_ZddObj * B;
593  int r0, r1, r;
594  if ( a == 0 ) return 0;
595  if ( a == 1 ) return b;
596  if ( b == 0 ) return 0;
597  if ( b == 1 ) return a;
598  if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_PERM_PROD)) >= 0 )
599  return r;
600  B = Abc_ZddNode( p, b );
601  r0 = Abc_ZddPermProduct( p, a, B->False );
602  r1 = Abc_ZddPermProduct( p, a, B->True );
603  r1 = Abc_ZddPerm( p, r1, B->Var );
604  r = Abc_ZddUnion( p, r0, r1 );
605  return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_PERM_PROD, r );
606 }
607 
608 /**Function*************************************************************
609 
610  Synopsis [Printing permutations and transpositions.]
611 
612  Description []
613 
614  SideEffects []
615 
616  SeeAlso []
617 
618 ***********************************************************************/
619 void Abc_ZddPermPrint( int * pPerm, int Size )
620 {
621  int i;
622  printf( "{" );
623  for ( i = 0; i < Size; i++ )
624  printf( " %2d", pPerm[i] );
625  printf( " }\n" );
626 }
627 void Abc_ZddCombPrint( int * pComb, int nTrans )
628 {
629  int i;
630  if ( nTrans == 0 )
631  printf( "Empty set" );
632  for ( i = 0; i < nTrans; i++ )
633  printf( "(%d %d)", pComb[i] >> 16, pComb[i] & 0xffff );
634  printf( "\n" );
635 }
636 int Abc_ZddPerm2Comb( int * pPerm, int Size, int * pComb )
637 {
638  int i, j, nTrans = 0;
639  for ( i = 0; i < Size; i++ )
640  if ( i != pPerm[i] )
641  {
642  for ( j = i+1; j < Size; j++ )
643  if ( i == pPerm[j] )
644  break;
645  pComb[nTrans++] = (i << 16) | j;
646  ABC_SWAP( int, pPerm[i], pPerm[j] );
647  assert( i == pPerm[i] );
648  }
649  return nTrans;
650 }
651 void Abc_ZddComb2Perm( int * pComb, int nTrans, int * pPerm, int Size )
652 {
653  int v;
654  for ( v = 0; v < Size; v++ )
655  pPerm[v] = v;
656  for ( v = nTrans-1; v >= 0; v-- )
657  ABC_SWAP( int, pPerm[pComb[v] >> 16], pPerm[pComb[v] & 0xffff] );
658 }
659 void Abc_ZddPermCombTest()
660 {
661  int Size = 10;
662  int pPerm[10] = { 6, 5, 7, 0, 3, 2, 1, 8, 9, 4 };
663  int pComb[10], nTrans;
664  Abc_ZddPermPrint( pPerm, Size );
665  nTrans = Abc_ZddPerm2Comb( pPerm, Size, pComb );
666  Abc_ZddCombPrint( pComb, nTrans );
667  Abc_ZddComb2Perm( pComb, nTrans, pPerm, Size );
668  Abc_ZddPermPrint( pPerm, Size );
669  Size = 0;
670 }
671 
672 /**Function*************************************************************
673 
674  Synopsis [Printing ZDDs.]
675 
676  Description []
677 
678  SideEffects []
679 
680  SeeAlso []
681 
682 ***********************************************************************/
683 void Abc_ZddPrint_rec( Abc_ZddMan * p, int a, int * pPath, int Size )
684 {
685  Abc_ZddObj * A;
686  if ( a == 0 ) return;
687 // if ( a == 1 ) { Abc_ZddPermPrint( pPath, Size ); return; }
688  if ( a == 1 )
689  {
690  int pPerm[24], pComb[24], i;
691  assert( p->nPermSize <= 24 );
692  for ( i = 0; i < Size; i++ )
693  pComb[i] = (p->pV2TI[pPath[i]] << 16) | p->pV2TJ[pPath[i]];
694  Abc_ZddCombPrint( pComb, Size );
695  Abc_ZddComb2Perm( pComb, Size, pPerm, p->nPermSize );
696  Abc_ZddPermPrint( pPerm, p->nPermSize );
697  return;
698  }
699  A = Abc_ZddNode( p, a );
700  Abc_ZddPrint_rec( p, A->False, pPath, Size );
701  pPath[Size] = A->Var;
702  Abc_ZddPrint_rec( p, A->True, pPath, Size + 1 );
703 }
704 void Abc_ZddPrint( Abc_ZddMan * p, int a )
705 {
706  int * pPath = ABC_CALLOC( int, p->nVars );
707  Abc_ZddPrint_rec( p, a, pPath, 0 );
708  ABC_FREE( pPath );
709 }
710 void Abc_ZddPrintTest( Abc_ZddMan * p )
711 {
712 // int nSets = 2;
713 // int Size = 2;
714 // int pSets[2][2] = { {5, 0}, {3, 11} };
715  int nSets = 3;
716  int Size = 5;
717  int pSets[3][5] = { {5, 0, 2, 10, 7}, {3, 11, 10, 7, 2}, {0, 2, 5, 10, 7} };
718  int i, Set, Union = 0;
719  for ( i = 0; i < nSets; i++ )
720  {
721  Abc_ZddPermPrint( pSets[i], Size );
722  Set = Abc_ZddBuildSet( p, pSets[i], Size );
723  Union = Abc_ZddUnion( p, Union, Set );
724  }
725  printf( "Resulting set:\n" );
726  Abc_ZddPrint( p, Union );
727  printf( "\n" );
728  printf( "Nodes = %d. Path = %d.\n", Abc_ZddCountNodes(p, Union), Abc_ZddCountPaths(p, Union) );
729  Size = 0;
730 }
731 
732 /**Function*************************************************************
733 
734  Synopsis []
735 
736  Description []
737 
738  SideEffects []
739 
740  SeeAlso []
741 
742 ***********************************************************************/
743 void Abc_ZddGiaTest( Gia_Man_t * pGia )
744 {
745  Abc_ZddMan * p;
746  Gia_Obj_t * pObj;
747  Vec_Int_t * vNodes;
748  int i, r, Paths = 0;
749  p = Abc_ZddManAlloc( Gia_ManObjNum(pGia), 1 << 24 ); // 576 MB (36 B/node)
750  Gia_ManFillValue( pGia );
751  Gia_ManForEachCi( pGia, pObj, i )
752  pObj->Value = Abc_ZddIthVar( Gia_ObjId(pGia, pObj) );
753  vNodes = Vec_IntAlloc( Gia_ManAndNum(pGia) );
754  Gia_ManForEachAnd( pGia, pObj, i )
755  {
756  r = Abc_ZddDotMinProduct6( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
757  r = Abc_ZddUnion( p, r, Abc_ZddIthVar(i) );
758  pObj->Value = r;
759  Vec_IntPush( vNodes, r );
760  // print
761 // printf( "Node %d:\n", i );
762 // Abc_ZddPrint( p, r );
763 // printf( "Node %d ZddNodes = %d\n", i, Abc_ZddCountNodes(p, r) );
764  }
765  Gia_ManForEachAnd( pGia, pObj, i )
766  Paths += Abc_ZddCountPaths(p, pObj->Value);
767  printf( "Paths = %d. Shared nodes = %d.\n", Paths, Abc_ZddCountNodesArray(p, vNodes) );
768  Vec_IntFree( vNodes );
769  Abc_ZddManFree( p );
770 }
771 /*
772  abc 01> &r pj1.aig; &ps; &test
773  pj1 : i/o = 1769/ 1063 and = 16285 lev = 156 (12.91) mem = 0.23 MB
774  Paths = 839934. Shared nodes = 770999.
775  ZDD stats: Var = 19118 Obj = 11578174 All = 16777216 Hits = 25617277 Miss = 40231476 Mem = 576.00 MB
776 */
777 
778 /**Function*************************************************************
779 
780  Synopsis []
781 
782  Description []
783 
784  SideEffects []
785 
786  SeeAlso []
787 
788 ***********************************************************************/
789 void Abc_ZddPermTestInt( Abc_ZddMan * p )
790 {
791  int nPerms = 3;
792  int Size = 5;
793  int pPerms[3][5] = { {1, 0, 2, 4, 3}, {1, 2, 4, 0, 3}, {0, 3, 2, 1, 4} };
794  int pComb[5], nTrans;
795  int i, k, Set, Union = 0, iPivot;
796  for ( i = 0; i < nPerms; i++ )
797  Abc_ZddPermPrint( pPerms[i], Size );
798  for ( i = 0; i < nPerms; i++ )
799  {
800  printf( "Perm %d:\n", i );
801  Abc_ZddPermPrint( pPerms[i], Size );
802  nTrans = Abc_ZddPerm2Comb( pPerms[i], Size, pComb );
803  Abc_ZddCombPrint( pComb, nTrans );
804  for ( k = 0; k < nTrans; k++ )
805  pComb[k] = Abc_ZddVarIJ( p, pComb[k] >> 16, pComb[k] & 0xFFFF );
806  Abc_ZddPermPrint( pComb, nTrans );
807  // add to ZDD
808  Set = Abc_ZddBuildSet( p, pComb, nTrans );
809  Union = Abc_ZddUnion( p, Union, Set );
810  }
811  printf( "\nResulting set of permutations:\n" );
812  Abc_ZddPrint( p, Union );
813  printf( "Nodes = %d. Path = %d.\n", Abc_ZddCountNodes(p, Union), Abc_ZddCountPaths(p, Union) );
814 
815  iPivot = Abc_ZddVarIJ( p, 3, 4 );
816  Union = Abc_ZddPerm( p, Union, iPivot );
817 
818  printf( "\nResulting set of permutations:\n" );
819  Abc_ZddPrint( p, Union );
820  printf( "Nodes = %d. Path = %d.\n", Abc_ZddCountNodes(p, Union), Abc_ZddCountPaths(p, Union) );
821  printf( "\n" );
822 }
823 
824 void Abc_ZddPermTest()
825 {
826  Abc_ZddMan * p;
827  p = Abc_ZddManAlloc( 10, 1 << 20 );
828  Abc_ZddManCreatePerms( p, 5 );
829  Abc_ZddPermTestInt( p );
830  Abc_ZddManFree( p );
831 }
832 
833 
834 /**Function*************************************************************
835 
836  Synopsis []
837 
838  Description []
839 
840  SideEffects []
841 
842  SeeAlso []
843 
844 ***********************************************************************/
845 void Abc_EnumerateCubeStatesZdd()
846 {
847  int pXYZ[3][9][2] = {
848  { {3, 5}, {3,17}, {3,15}, {1, 6}, {1,16}, {1,14}, {2, 4}, {2,18}, {2,13} },
849  { {2,14}, {2,24}, {2,12}, {3,13}, {3,23}, {3,10}, {1,15}, {1,22}, {1,11} },
850  { {1,10}, {1, 7}, {1, 4}, {3,12}, {3, 9}, {3, 6}, {2,11}, {2, 8}, {2, 5} } };
851 #ifdef WIN32
852  int LogObj = 24;
853 #else
854  int LogObj = 27;
855 #endif
856  Abc_ZddMan * p;
857  int i, k, pComb[9], pPerm[24], nSize;
858  int ZddTurn1, ZddTurn2, ZddTurn3, ZddTurns, ZddAll;
859  abctime clk = Abc_Clock();
860  printf( "Enumerating states of 2x2x2 cube.\n" );
861  p = Abc_ZddManAlloc( 24 * 23 / 2, 1 << LogObj ); // finished with 2^27 (4 GB)
862  Abc_ZddManCreatePerms( p, 24 );
863  // init state
864  printf( "Iter %2d -> %8d Nodes = %7d Used = %10d ", 0, 1, 0, 2 );
865  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
866  // first 9 states
867  ZddTurns = 1;
868  for ( i = 0; i < 3; i++ )
869  {
870  for ( k = 0; k < 24; k++ )
871  pPerm[k] = k;
872  for ( k = 0; k < 9; k++ )
873  ABC_SWAP( int, pPerm[pXYZ[i][k][0]-1], pPerm[pXYZ[i][k][1]-1] );
874  nSize = Abc_ZddPerm2Comb( pPerm, 24, pComb );
875  assert( nSize == 9 );
876  for ( k = 0; k < 9; k++ )
877  pComb[k] = Abc_ZddVarIJ( p, pComb[k] >> 16, pComb[k] & 0xffff );
878  // add first turn
879  ZddTurn1 = Abc_ZddBuildSet( p, pComb, 9 );
880  ZddTurns = Abc_ZddUnion( p, ZddTurns, ZddTurn1 );
881  //Abc_ZddPrint( p, ZddTurn1 );
882  // add second turn
883  ZddTurn2 = Abc_ZddPermProduct( p, ZddTurn1, ZddTurn1 );
884  ZddTurns = Abc_ZddUnion( p, ZddTurns, ZddTurn2 );
885  //Abc_ZddPrint( p, ZddTurn2 );
886  // add third turn
887  ZddTurn3 = Abc_ZddPermProduct( p, ZddTurn2, ZddTurn1 );
888  ZddTurns = Abc_ZddUnion( p, ZddTurns, ZddTurn3 );
889  //Abc_ZddPrint( p, ZddTurn3 );
890  //printf( "\n" );
891  }
892  //Abc_ZddPrint( p, ZddTurns );
893  printf( "Iter %2d -> %8d Nodes = %7d Used = %10d ", 1, Abc_ZddCountPaths(p, ZddTurns), Abc_ZddCountNodes(p, ZddTurns), p->nObjs );
894  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
895  // other states
896  ZddAll = ZddTurns;
897  for ( i = 2; i <= 100; i++ )
898  {
899  int ZddAllPrev = ZddAll;
900  ZddAll = Abc_ZddPermProduct( p, ZddAll, ZddTurns );
901  printf( "Iter %2d -> %8d Nodes = %7d Used = %10d ", i, Abc_ZddCountPaths(p, ZddAll), Abc_ZddCountNodes(p, ZddAll), p->nObjs );
902  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
903  if ( ZddAllPrev == ZddAll )
904  break;
905  }
906  Abc_ZddManFree( p );
907 }
908 
909 /*
910 Enumerating states of 2x2x2 cube.
911 Iter 0 -> 1 Nodes = 0 Used = 2 Time = 0.00 sec
912 Iter 1 -> 10 Nodes = 63 Used = 577 Time = 0.00 sec
913 Iter 2 -> 64 Nodes = 443 Used = 4349 Time = 0.03 sec
914 Iter 3 -> 385 Nodes = 2018 Used = 26654 Time = 0.14 sec
915 Iter 4 -> 2232 Nodes = 7451 Used = 119442 Time = 0.45 sec
916 Iter 5 -> 12224 Nodes = 25178 Used = 490038 Time = 1.10 sec
917 Iter 6 -> 62360 Nodes = 83955 Used = 1919750 Time = 1.79 sec
918 Iter 7 -> 289896 Nodes = 290863 Used = 7182932 Time = 3.15 sec
919 Iter 8 -> 1159968 Nodes = 614845 Used = 25301123 Time = 8.03 sec
920 Iter 9 -> 3047716 Nodes = 585664 Used = 66228369 Time = 20.22 sec
921 Iter 10 -> 3671516 Nodes = 19430 Used = 102292452 Time = 33.41 sec
922 Iter 11 -> 3674160 Nodes = 511 Used = 103545878 Time = 33.92 sec
923 Iter 12 -> 3674160 Nodes = 511 Used = 103566266 Time = 33.93 sec
924 ZDD stats: Var = 276 Obj = 103566266 Alloc = 134217728 Hit = 63996630 Miss = 141768893 Mem = 4608.00 MB
925 */
926 
927 ////////////////////////////////////////////////////////////////////////
928 /// END OF FILE ///
929 ////////////////////////////////////////////////////////////////////////
930 
931 
932 ABC_NAMESPACE_IMPL_END
933 
memset
char * memset()
Abc_ZddMan_::pObjs
Abc_ZddObj * pObjs
Definition: extraUtilPerm.c:84
Abc_ZddObj_::Mark
unsigned Mark
Definition: extraUtilPerm.c:58
Abc_ZddUnion
int Abc_ZddUnion(Abc_ZddMan *p, int a, int b)
Definition: extraUtilPerm.c:275
Abc_ZddMan_::nObjs
int nObjs
Definition: extraUtilPerm.c:76
Abc_ZddPrintTest
void Abc_ZddPrintTest(Abc_ZddMan *p)
Definition: extraUtilPerm.c:710
Abc_ZddEnt
struct Abc_ZddEnt_ Abc_ZddEnt
Definition: extraUtilPerm.c:63
Abc_ZddEnt_::Res
int Res
Definition: extraUtilPerm.c:69
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
Abc_ZddComb2Perm
void Abc_ZddComb2Perm(int *pComb, int nTrans, int *pPerm, int Size)
Definition: extraUtilPerm.c:651
Abc_ZddDiff
int Abc_ZddDiff(Abc_ZddMan *p, int a, int b)
Definition: extraUtilPerm.c:253
Abc_ZddPermTestInt
void Abc_ZddPermTestInt(Abc_ZddMan *p)
Definition: extraUtilPerm.c:789
Abc_ZddPrint
void Abc_ZddPrint(Abc_ZddMan *p, int a)
Definition: extraUtilPerm.c:704
Abc_ZddCombPrint
void Abc_ZddCombPrint(int *pComb, int nTrans)
Definition: extraUtilPerm.c:627
Abc_ZddCount_rec
int Abc_ZddCount_rec(Abc_ZddMan *p, int i)
Definition: extraUtilPerm.c:409
Abc_ZddObj_::True
unsigned True
Definition: extraUtilPerm.c:59
Abc_ZddHash
static unsigned Abc_ZddHash(int Arg0, int Arg1, int Arg2)
Definition: extraUtilPerm.c:94
Abc_ZddMan_::pCache
Abc_ZddEnt * pCache
Definition: extraUtilPerm.c:83
Abc_ZddPermCombTest
void Abc_ZddPermCombTest()
Definition: extraUtilPerm.c:659
Abc_ZddIthVar
static int Abc_ZddIthVar(int i)
Definition: extraUtilPerm.c:93
Abc_ZddCacheInsert
static int Abc_ZddCacheInsert(Abc_ZddMan *p, int Arg0, int Arg1, int Arg2, int Res)
Definition: extraUtilPerm.c:125
Abc_ZddEnt_
Definition: extraUtilPerm.c:64
Abc_ZddObjVar
static int Abc_ZddObjVar(Abc_ZddMan *p, int i)
Definition: extraUtilPerm.c:98
Abc_ZddUniqueCreate
static int Abc_ZddUniqueCreate(Abc_ZddMan *p, int Var, int True, int False)
Definition: extraUtilPerm.c:141
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Abc_ZddDotProduct
int Abc_ZddDotProduct(Abc_ZddMan *p, int a, int b)
Definition: extraUtilPerm.c:473
Abc_EnumerateCubeStatesZdd
void Abc_EnumerateCubeStatesZdd()
Definition: extraUtilPerm.c:845
Abc_ZddMan_::nVars
int nVars
Definition: extraUtilPerm.c:75
Gia_Obj_t_
Definition: gia.h:75
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition: abc_global.h:218
Abc_ZddObj_::Var
unsigned Var
Definition: extraUtilPerm.c:57
Abc_ZddUniqueLookup
static int Abc_ZddUniqueLookup(Abc_ZddMan *p, int Var, int True, int False)
Definition: extraUtilPerm.c:133
Abc_ZddPrint_rec
void Abc_ZddPrint_rec(Abc_ZddMan *p, int a, int *pPath, int Size)
Definition: extraUtilPerm.c:683
Abc_ZddPermTest
void Abc_ZddPermTest()
Definition: extraUtilPerm.c:824
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Abc_ZddObj_
Definition: extraUtilPerm.c:55
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Vec_IntSelectSort
static void Vec_IntSelectSort(int *pArray, int nSize)
Definition: vecInt.h:1740
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Abc_ZddPermProduct
int Abc_ZddPermProduct(Abc_ZddMan *p, int a, int b)
Definition: extraUtilPerm.c:590
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Abc_ZddThresh
int Abc_ZddThresh(Abc_ZddMan *p, int a, int b)
Definition: extraUtilPerm.c:459
Abc_ZddCacheLookup
static int Abc_ZddCacheLookup(Abc_ZddMan *p, int Arg0, int Arg1, int Arg2)
FUNCTION DEFINITIONS ///.
Definition: extraUtilPerm.c:119
Abc_ZddGiaTest
void Abc_ZddGiaTest(Gia_Man_t *pGia)
Definition: extraUtilPerm.c:743
Abc_ZddIntersect
int Abc_ZddIntersect(Abc_ZddMan *p, int a, int b)
Definition: extraUtilPerm.c:324
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Abc_ZddMan_::nMemory
word nMemory
Definition: extraUtilPerm.c:87
Abc_ZddBuildSet
int Abc_ZddBuildSet(Abc_ZddMan *p, int *pSet, int Size)
Definition: extraUtilPerm.c:164
Abc_ZddCountNodesArray
int Abc_ZddCountNodesArray(Abc_ZddMan *p, Vec_Int_t *vNodes)
Definition: extraUtilPerm.c:438
Abc_ZddEnt_::Arg1
int Arg1
Definition: extraUtilPerm.c:67
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Abc_ZddObj_::False
unsigned False
Definition: extraUtilPerm.c:60
Abc_ZddMan_::nUniqueMask
unsigned nUniqueMask
Definition: extraUtilPerm.c:79
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Abc_ZddMan_::nCacheMask
unsigned nCacheMask
Definition: extraUtilPerm.c:80
Gia_ManFillValue
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
Abc_ZddDotMinProduct6
int Abc_ZddDotMinProduct6(Abc_ZddMan *p, int a, int b)
Definition: extraUtilPerm.c:501
Abc_ZddMan_::pV2TI
int * pV2TI
Definition: extraUtilPerm.c:88
Abc_ZddOper
Abc_ZddOper
DECLARATIONS ///.
Definition: extraUtilPerm.c:34
Abc_ZddMan_::pT2V
int * pT2V
Definition: extraUtilPerm.c:90
Abc_ZddPerm
int Abc_ZddPerm(Abc_ZddMan *p, int a, int Var)
Definition: extraUtilPerm.c:543
Abc_ZddNode
static Abc_ZddObj * Abc_ZddNode(Abc_ZddMan *p, int i)
Definition: extraUtilPerm.c:96
Abc_ZddObjId
static int Abc_ZddObjId(Abc_ZddMan *p, Abc_ZddObj *pObj)
Definition: extraUtilPerm.c:97
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
Abc_ZddMan_::nObjsAlloc
int nObjsAlloc
Definition: extraUtilPerm.c:77
Abc_ZddMan_::pNexts
int * pNexts
Definition: extraUtilPerm.c:82
Abc_ZddSetVarIJ
static void Abc_ZddSetVarIJ(Abc_ZddMan *p, int i, int j, int v)
Definition: extraUtilPerm.c:100
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Abc_ZddCountPaths
int Abc_ZddCountPaths(Abc_ZddMan *p, int a)
Definition: extraUtilPerm.c:385
Abc_ZddEnt_::Arg0
int Arg0
Definition: extraUtilPerm.c:66
Abc_ZddMan_::nPermSize
int nPermSize
Definition: extraUtilPerm.c:78
Abc_ZddVarsClash
static int Abc_ZddVarsClash(Abc_ZddMan *p, int v0, int v1)
Definition: extraUtilPerm.c:102
Abc_ZddPerm2Comb
int Abc_ZddPerm2Comb(int *pPerm, int Size, int *pComb)
Definition: extraUtilPerm.c:636
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
Abc_Base2Log
static int Abc_Base2Log(unsigned n)
Definition: abc_global.h:251
Abc_ZddUnmark_rec
void Abc_ZddUnmark_rec(Abc_ZddMan *p, int i)
Definition: extraUtilPerm.c:420
Abc_ZddManCreatePerms
void Abc_ZddManCreatePerms(Abc_ZddMan *p, int nPermSize)
Definition: extraUtilPerm.c:209
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Minisat::Var
int Var
Definition: SolverTypes.h:42
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Abc_ZddMinUnion
int Abc_ZddMinUnion(Abc_ZddMan *p, int a, int b)
Definition: extraUtilPerm.c:299
Abc_ZddMan_::nCacheLookups
int nCacheLookups
Definition: extraUtilPerm.c:85
Abc_ZddEnt_::Arg2
int Arg2
Definition: extraUtilPerm.c:68
Abc_ZddManFree
void Abc_ZddManFree(Abc_ZddMan *p)
Definition: extraUtilPerm.c:227
True
#define True
Definition: bzlib_private.h:51
assert
#define assert(ex)
Definition: util_old.h:213
Abc_ZddPermPrint
void Abc_ZddPermPrint(int *pPerm, int Size)
Definition: extraUtilPerm.c:619
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Abc_ZddVarIJ
static int Abc_ZddVarIJ(Abc_ZddMan *p, int i, int j)
Definition: extraUtilPerm.c:101
Abc_ZddManAlloc
Abc_ZddMan * Abc_ZddManAlloc(int nVars, int nObjs)
Definition: extraUtilPerm.c:184
False
#define False
Definition: bzlib_private.h:52
Abc_ZddMan_
Definition: extraUtilPerm.c:73
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Abc_ZddCof0
int Abc_ZddCof0(Abc_ZddMan *p, int a, int Var)
Definition: extraUtilPerm.c:348
Abc_ZddMan_::nCacheMisses
int nCacheMisses
Definition: extraUtilPerm.c:86
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Abc_ZddMan_::pUnique
int * pUnique
Definition: extraUtilPerm.c:81
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Abc_ZddCountNodes
int Abc_ZddCountNodes(Abc_ZddMan *p, int i)
Definition: extraUtilPerm.c:432
Abc_ZddMan
struct Abc_ZddMan_ Abc_ZddMan
Definition: extraUtilPerm.c:72
Abc_ZddMan_::pV2TJ
int * pV2TJ
Definition: extraUtilPerm.c:89
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
ABC_FALLOC
#define ABC_FALLOC(type, num)
Definition: abc_global.h:231
Abc_ZddCof1
int Abc_ZddCof1(Abc_ZddMan *p, int a, int Var)
Definition: extraUtilPerm.c:366