abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
mpmPre.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [mpmPre.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Configurable technology mapper.]
8 
9  Synopsis [DSD-related precomputations.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 1, 2013.]
16 
17  Revision [$Id: mpmPre.c,v 1.00 2013/06/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 
26 #include "misc/vec/vec.h"
27 #include "misc/vec/vecHsh.h"
28 #include "misc/extra/extra.h"
29 #include "bool/kit/kit.h"
30 #include "misc/util/utilTruth.h"
31 
32 ABC_NAMESPACE_IMPL_START
33 
34 
35 ////////////////////////////////////////////////////////////////////////
36 /// DECLARATIONS ///
37 ////////////////////////////////////////////////////////////////////////
38 
39 typedef struct Ifd_Obj_t_ Ifd_Obj_t;
40 struct Ifd_Obj_t_
41 {
42  unsigned nFreq : 18; // frequency
43  unsigned nAnds : 6; // number of AND gates
44  unsigned nSupp : 5; // support size
45  unsigned Type : 2; // type
46  unsigned fWay : 1; // transparent edge
47  unsigned pFans[3]; // fanins
48 };
49 
50 typedef struct Ifd_Man_t_ Ifd_Man_t;
51 struct Ifd_Man_t_
52 {
53  Ifd_Obj_t * pObjs;
54  int nObjs;
55  int nObjsAlloc;
56  // hashing operations
57  Vec_Int_t * vArgs; // iDsd1 op iDsdC
58  Vec_Int_t * vRes; // result of operation
59  Hsh_IntMan_t * vHash; // hash table
60  Vec_Int_t * vMarks; // marks where given N begins
61  Vec_Wrd_t * vTruths; // truth tables
62  Vec_Int_t * vClauses; // truth tables
63  // other data
64  Vec_Int_t * vSuper;
65 
66 };
67 
68 static inline int Ifd_ObjIsVar( Ifd_Obj_t * p ) { return p->Type == 0; }
69 static inline int Ifd_ObjIsAnd( Ifd_Obj_t * p ) { return p->Type == 1; }
70 static inline int Ifd_ObjIsXor( Ifd_Obj_t * p ) { return p->Type == 2; }
71 static inline int Ifd_ObjIsMux( Ifd_Obj_t * p ) { return p->Type == 3; }
72 
73 static inline Ifd_Obj_t * Ifd_ManObj( Ifd_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return p->pObjs + i; }
74 static inline Ifd_Obj_t * Ifd_ManObjFromLit( Ifd_Man_t * p, int iLit ) { return Ifd_ManObj( p, Abc_Lit2Var(iLit) ); }
75 static inline int Ifd_ObjId( Ifd_Man_t * p, Ifd_Obj_t * pObj ) { assert( pObj - p->pObjs >= 0 && pObj - p->pObjs < p->nObjs ); return pObj - p->pObjs; }
76 static inline int Ifd_LitSuppSize( Ifd_Man_t * p, int iLit ) { return iLit > 0 ? Ifd_ManObjFromLit(p, iLit)->nSupp : 0; }
77 static inline int Ifd_LitNumAnds( Ifd_Man_t * p, int iLit ) { return iLit > 0 ? Ifd_ManObjFromLit(p, iLit)->nAnds : 0; }
78 
79 #define Ifd_ManForEachNodeWithSupp( p, nVars, pLeaf, i ) \
80  for ( i = Vec_IntEntry(p->vMarks, nVars); (i < Vec_IntEntry(p->vMarks, nVars+1)) && (pLeaf = Ifd_ManObj(p, i)); i++ )
81 
82 
83 ////////////////////////////////////////////////////////////////////////
84 /// FUNCTION DEFINITIONS ///
85 ////////////////////////////////////////////////////////////////////////
86 
87 /**Function*************************************************************
88 
89  Synopsis []
90 
91  Description []
92 
93  SideEffects []
94 
95  SeeAlso []
96 
97 ***********************************************************************/
98 Ifd_Man_t * Ifd_ManStart()
99 {
100  Ifd_Man_t * p;
101  p = ABC_CALLOC( Ifd_Man_t, 1 );
102  p->nObjsAlloc = Abc_PrimeCudd( 50000000 );
103  p->nObjs = 2;
104  p->pObjs = ABC_CALLOC( Ifd_Obj_t, p->nObjsAlloc );
105  memset( p->pObjs, 0xFF, sizeof(Ifd_Obj_t) ); // const node
106  (p->pObjs + 1)->nSupp = 1; // variable
107  (p->pObjs + 1)->fWay = 1; // variable
108  // hashing operations
109  p->vArgs = Vec_IntAlloc( 4000 );
110  p->vRes = Vec_IntAlloc( 1000 );
111  p->vHash = Hsh_IntManStart( p->vArgs, 4, 1000 );
112  p->vMarks = Vec_IntAlloc( 100 );
113  Vec_IntPush( p->vMarks, 0 );
114  Vec_IntPush( p->vMarks, 1 );
115  Vec_IntPush( p->vMarks, p->nObjs );
116  // other data
117  p->vSuper = Vec_IntAlloc( 1000 );
118  p->vTruths = Vec_WrdAlloc( 1000 );
119  p->vClauses = Vec_IntAlloc( 1000 );
120  return p;
121 }
122 void Ifd_ManStop( Ifd_Man_t * p )
123 {
124  int i, This, Prev = 0;
125  Vec_IntForEachEntryStart( p->vMarks, This, i, 1 )
126  {
127  printf( "%d(%d:%d) ", i-1, This, This - Prev );
128  Prev = This;
129  }
130  printf( "\n" );
131 
132  Vec_IntFreeP( &p->vArgs );
133  Vec_IntFreeP( &p->vRes );
134  Vec_WrdFreeP( &p->vTruths );
135  Vec_IntFreeP( &p->vClauses );
136  Vec_IntFreeP( &p->vMarks );
137  Hsh_IntManStop( p->vHash );
138  Vec_IntFreeP( &p->vSuper );
139  ABC_FREE( p->pObjs );
140  ABC_FREE( p );
141 }
142 
143 /**Function*************************************************************
144 
145  Synopsis [Printing structures.]
146 
147  Description []
148 
149  SideEffects []
150 
151  SeeAlso []
152 
153 ***********************************************************************/
154 void Ifd_ObjPrint_rec( Ifd_Man_t * p, int iLit, int * pCounter, int DiffType )
155 {
156  char Symb[2][4] = { {'?','(','[','<'}, {'?',')',']','>'} };
157  Ifd_Obj_t * pDsd;
158  if ( Abc_LitIsCompl(iLit) )
159  printf( "!" ), iLit = Abc_LitNot(iLit);
160  if ( iLit == 2 )
161  { printf( "%c", 'a' + (*pCounter)++ ); return; }
162  pDsd = Ifd_ManObjFromLit( p, iLit );
163  if ( DiffType )
164  printf( "%c", Symb[0][pDsd->Type] );
165  Ifd_ObjPrint_rec( p, pDsd->pFans[0], pCounter, pDsd->Type == 3 || Abc_LitIsCompl(pDsd->pFans[0]) || pDsd->Type != Ifd_ManObjFromLit(p, pDsd->pFans[0])->Type );
166  Ifd_ObjPrint_rec( p, pDsd->pFans[1], pCounter, pDsd->Type == 3 || Abc_LitIsCompl(pDsd->pFans[1]) || pDsd->Type != Ifd_ManObjFromLit(p, pDsd->pFans[1])->Type );
167  if ( pDsd->pFans[2] != -1 )
168  Ifd_ObjPrint_rec( p, pDsd->pFans[2], pCounter, pDsd->Type == 3 || Abc_LitIsCompl(pDsd->pFans[2]) || pDsd->Type != Ifd_ManObjFromLit(p, pDsd->pFans[2])->Type );
169  if ( DiffType )
170  printf( "%c", Symb[1][pDsd->Type] );
171 }
172 void Ifd_ObjPrint( Ifd_Man_t * p, int iLit )
173 {
174  int Counter = 0;
175  if ( iLit == 0 )
176  { printf( "0" ); return; }
177  if ( iLit == 1 )
178  { printf( "1" ); return; }
179  Ifd_ObjPrint_rec( p, iLit, &Counter, 1 );
180 }
181 void Ifd_ManPrint2( Ifd_Man_t * p )
182 {
183  int i;
184  for ( i = 0; i < p->nObjs; i++ )
185  {
186  printf( "%4d : ", i );
187  Ifd_ObjPrint( p, Abc_Var2Lit( i, 0 ) );
188  printf( "\n" );
189  }
190 }
191 void Ifd_ManPrint( Ifd_Man_t * p )
192 {
193  int i;
194  for ( i = 0; i < p->nObjs; i++ )
195  {
196  word Fun = Vec_WrdEntry( p->vTruths, i );
197  printf( " { " );
198  printf( "%d, ", Extra_TruthSupportSize((unsigned *)&Fun, 6) );
199  printf( "%2d, ", Ifd_LitNumAnds(p, Abc_Var2Lit(i, 0)) );
200  printf( "%2d, ", Vec_IntEntry(p->vClauses, i) );
201  printf( "ABC_CONST(" );
202  Extra_PrintHex( stdout, (unsigned *)&Fun, 6 );
203  printf( "), \"" );
204  Ifd_ObjPrint( p, Abc_Var2Lit( i, 0 ) );
205  printf( "\" }, // %4d \n", i );
206  }
207 }
208 
209 
210 /**Function*************************************************************
211 
212  Synopsis [Computing truth tables.]
213 
214  Description []
215 
216  SideEffects []
217 
218  SeeAlso []
219 
220 ***********************************************************************/
221 word Ifd_ObjTruth_rec( Ifd_Man_t * p, int iLit, int * pCounter )
222 {
223  static word s_Truths6[6] = {
224  ABC_CONST(0xAAAAAAAAAAAAAAAA),
225  ABC_CONST(0xCCCCCCCCCCCCCCCC),
226  ABC_CONST(0xF0F0F0F0F0F0F0F0),
227  ABC_CONST(0xFF00FF00FF00FF00),
228  ABC_CONST(0xFFFF0000FFFF0000),
229  ABC_CONST(0xFFFFFFFF00000000)
230  };
231  Ifd_Obj_t * pDsd;
232  word Fun0, Fun1, Fun2 = 0;
233  assert( !Abc_LitIsCompl(iLit) );
234  if ( iLit == 2 )
235  return s_Truths6[(*pCounter)++];
236  pDsd = Ifd_ManObjFromLit( p, iLit );
237 
238  Fun0 = Ifd_ObjTruth_rec( p, Abc_LitRegular(pDsd->pFans[0]), pCounter );
239  Fun1 = Ifd_ObjTruth_rec( p, Abc_LitRegular(pDsd->pFans[1]), pCounter );
240  if ( pDsd->pFans[2] != -1 )
241  Fun2 = Ifd_ObjTruth_rec( p, Abc_LitRegular(pDsd->pFans[2]), pCounter );
242 
243  Fun0 = Abc_LitIsCompl(pDsd->pFans[0]) ? ~Fun0 : Fun0;
244  Fun1 = Abc_LitIsCompl(pDsd->pFans[1]) ? ~Fun1 : Fun1;
245  if ( pDsd->pFans[2] != -1 )
246  Fun2 = Abc_LitIsCompl(pDsd->pFans[2]) ? ~Fun2 : Fun2;
247 
248  if ( pDsd->Type == 1 )
249  return Fun0 & Fun1;
250  if ( pDsd->Type == 2 )
251  return Fun0 ^ Fun1;
252  if ( pDsd->Type == 3 )
253  return (Fun2 & Fun1) | (~Fun2 & Fun0);
254  assert( 0 );
255  return -1;
256 }
257 word Ifd_ObjTruth( Ifd_Man_t * p, int iLit )
258 {
259  word Fun;
260  int Counter = 0;
261  if ( iLit == 0 )
262  return 0;
263  if ( iLit == 1 )
264  return ~(word)0;
265  Fun = Ifd_ObjTruth_rec( p, Abc_LitRegular(iLit), &Counter );
266  return Abc_LitIsCompl(iLit) ? ~Fun : Fun;
267 }
268 void Ifd_ManTruthAll( Ifd_Man_t * p )
269 {
270  word Fun;
271  int i;
272  assert( Vec_WrdSize(p->vTruths) == 0 );
273  for ( i = 0; i < p->nObjs; i++ )
274  {
275  Fun = Ifd_ObjTruth( p, Abc_Var2Lit( i, 0 ) );
276  Vec_WrdPush( p->vTruths, Fun );
277 // Extra_PrintHex( stdout, (unsigned *)&Fun, 6 ); printf( " " );
278 // Kit_DsdPrintFromTruth( (unsigned *)&Fun, 6 ); printf( "\n" );
279  }
280 }
281 
282 /**Function*************************************************************
283 
284  Synopsis []
285 
286  Description []
287 
288  SideEffects []
289 
290  SeeAlso []
291 
292 ***********************************************************************/
293 int Mpm_ComputeCnfSizeOne( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
294 {
295  Vec_StrClear( vCnf );
296  if ( Truth == 0 || ~Truth == 0 )
297  {
298 // assert( nVars == 0 );
299  Vec_StrPush( vCnf, (char)(Truth == 0) );
300  Vec_StrPush( vCnf, (char)-1 );
301  return 1;
302  }
303  else
304  {
305  int i, k, c, RetValue, Literal, Cube, nCubes = 0;
306  assert( nVars > 0 );
307  for ( c = 0; c < 2; c ++ )
308  {
309  Truth = c ? ~Truth : Truth;
310  RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
311  assert( RetValue == 0 );
312  nCubes += Vec_IntSize( vCover );
313  Vec_IntForEachEntry( vCover, Cube, i )
314  {
315  for ( k = 0; k < nVars; k++ )
316  {
317  Literal = 3 & (Cube >> (k << 1));
318  if ( Literal == 1 ) // '0' -> pos lit
319  Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) );
320  else if ( Literal == 2 ) // '1' -> neg lit
321  Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) );
322  else if ( Literal != 0 )
323  assert( 0 );
324  }
325  Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
326  Vec_StrPush( vCnf, (char)-1 );
327  }
328  }
329  return nCubes;
330  }
331 }
332 void Mpm_ComputeCnfSizeAll( Ifd_Man_t * p )
333 {
334  Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 );
335  Vec_Str_t * vCnf = Vec_StrAlloc( 1000 );
336  word Truth;
337  int i;
338  assert( Vec_IntSize(p->vClauses) == 0 );
339  Vec_WrdForEachEntry( p->vTruths, Truth, i )
340  Vec_IntPush( p->vClauses, Mpm_ComputeCnfSizeOne(Truth, 6, vCover, vCnf) );
341  Vec_IntFree( vCover );
342  Vec_StrFree( vCnf );
343 }
344 
345 /**Function*************************************************************
346 
347  Synopsis [Canonicizing DSD structures.]
348 
349  Description []
350 
351  SideEffects []
352 
353  SeeAlso []
354 
355 ***********************************************************************/
356 int Ifd_ManHashLookup( Ifd_Man_t * p, int iDsd0, int iDsd1, int iDsdC, int Type )
357 {
358  int pData[4];
359  assert( iDsdC != -1 || iDsd0 >= iDsd1 );
360  assert( iDsdC == -1 || !Abc_LitIsCompl(iDsd1) );
361  pData[0] = iDsd0;
362  pData[1] = iDsd1;
363  pData[2] = iDsdC;
364  pData[3] = Type;
365  return *Hsh_IntManLookup( p->vHash, (unsigned *)pData );
366 }
367 void Ifd_ManHashInsert( Ifd_Man_t * p, int iDsd0, int iDsd1, int iDsdC, int Type, int Res )
368 {
369  int iObj;
370  assert( iDsdC != -1 || iDsd0 >= iDsd1 );
371  assert( iDsdC == -1 || !Abc_LitIsCompl(iDsd1) );
372  Vec_IntPush( p->vArgs, iDsd0 );
373  Vec_IntPush( p->vArgs, iDsd1 );
374  Vec_IntPush( p->vArgs, iDsdC );
375  Vec_IntPush( p->vArgs, Type );
376  iObj = Hsh_IntManAdd( p->vHash, Vec_IntSize(p->vRes) );
377  assert( iObj == Vec_IntSize(p->vRes) );
378  Vec_IntPush( p->vRes, Res );
379  assert( 4 * Vec_IntSize(p->vRes) == Vec_IntSize(p->vArgs) );
380 }
381 int Ifd_ManHashFindOrAdd( Ifd_Man_t * p, int iDsd0, int iDsd1, int iDsdC, int Type )
382 {
383  Ifd_Obj_t * pObj;
384  int iObj, Value;
385  assert( iDsdC != -1 || iDsd0 >= iDsd1 );
386  assert( iDsdC == -1 || !Abc_LitIsCompl(iDsd1) );
387  Vec_IntPush( p->vArgs, iDsd0 );
388  Vec_IntPush( p->vArgs, iDsd1 );
389  Vec_IntPush( p->vArgs, iDsdC );
390  Vec_IntPush( p->vArgs, Type );
391  Value = Hsh_IntManAdd( p->vHash, Vec_IntSize(p->vRes) );
392  if ( Value < Vec_IntSize(p->vRes) )
393  {
394  iObj = Vec_IntEntry(p->vRes, Value);
395  Vec_IntShrink( p->vArgs, Vec_IntSize(p->vArgs) - 4 );
396  pObj = Ifd_ManObj( p, iObj );
397 // pObj->nFreq++;
398  assert( (int)pObj->Type == Type );
399  assert( (int)pObj->nSupp == Ifd_LitSuppSize(p, iDsd0) + Ifd_LitSuppSize(p, iDsd1) + Ifd_LitSuppSize(p, iDsdC) );
400  }
401  else
402  {
403  if ( p->nObjs == p->nObjsAlloc )
404  printf( "The number of nodes is more than %d\n", p->nObjs );
405  assert( p->nObjs < p->nObjsAlloc );
406  iObj = p->nObjs;
407  pObj = Ifd_ManObj( p, p->nObjs++ );
408 // pObj->nFreq = 1;
409  pObj->nSupp = Ifd_LitSuppSize(p, iDsd0) + Ifd_LitSuppSize(p, iDsd1) + Ifd_LitSuppSize(p, iDsdC);
410  pObj->nAnds = Ifd_LitNumAnds(p, iDsd0) + Ifd_LitNumAnds(p, iDsd1) + Ifd_LitNumAnds(p, iDsdC) + ((Type == 1) ? 1 : 3);
411  pObj->Type = Type;
412  if ( Type == 1 )
413  pObj->fWay = 0;
414  else if ( Type == 2 )
415  pObj->fWay = Ifd_ManObjFromLit(p, iDsd0)->fWay || Ifd_ManObjFromLit(p, iDsd1)->fWay;
416  else if ( Type == 3 )
417 // pObj->fWay = (Ifd_ManObjFromLit(p, iDsd0)->fWay && Ifd_ManObjFromLit(p, iDsd1)->fWay) || (Abc_Lit2Var(iDsd0) == Abc_Lit2Var(iDsd1) && Ifd_ManObjFromLit(p, iDsdC)->fWay);
418  pObj->fWay = (Ifd_ManObjFromLit(p, iDsd0)->fWay && Ifd_ManObjFromLit(p, iDsd1)->fWay) || (iDsd0 == Abc_LitNot(iDsd1) && Ifd_ManObjFromLit(p, iDsdC)->fWay);
419  else assert( 0 );
420  pObj->pFans[0] = iDsd0;
421  pObj->pFans[1] = iDsd1;
422  pObj->pFans[2] = iDsdC;
423  Vec_IntPush( p->vRes, iObj );
424  }
425  assert( 4 * Vec_IntSize(p->vRes) == Vec_IntSize(p->vArgs) );
426  return iObj;
427 }
428 void Ifd_ManOperSuper_rec( Ifd_Man_t * p, int iLit, int Type, Vec_Int_t * vObjs )
429 {
430  Ifd_Obj_t * pDsd = Ifd_ManObjFromLit( p, iLit );
431  if ( Abc_LitIsCompl(iLit) || (int)pDsd->Type != Type )
432  Vec_IntPush( vObjs, iLit );
433  else
434  {
435  Ifd_ManOperSuper_rec( p, pDsd->pFans[0], Type, vObjs );
436  Ifd_ManOperSuper_rec( p, pDsd->pFans[1], Type, vObjs );
437  }
438 }
439 int Ifd_ManOper( Ifd_Man_t * p, int iDsd0, int iDsd1, int iDsdC, int Type )
440 {
441  int i, iLit0, iLit1, iThis, fCompl = 0;
442  if ( Type == 1 ) // AND
443  {
444  if ( iDsd0 == 0 || iDsd1 == 0 )
445  return 0;
446  if ( iDsd0 == 1 || iDsd1 == 1 )
447  return (iDsd0 == 1) ? iDsd1 : iDsd0;
448  }
449  else if ( Type == 2 ) // XOR
450  {
451  if ( iDsd0 < 2 )
452  return Abc_LitNotCond( iDsd1, iDsd0 );
453  if ( iDsd1 < 2 )
454  return Abc_LitNotCond( iDsd0, iDsd1 );
455  if ( Abc_LitIsCompl(iDsd0) )
456  fCompl ^= 1, iDsd0 = Abc_LitNot(iDsd0);
457  if ( Abc_LitIsCompl(iDsd1) )
458  fCompl ^= 1, iDsd1 = Abc_LitNot(iDsd1);
459  }
460  else if ( Type == 3 )
461  {
462  if ( Abc_LitIsCompl(iDsdC) )
463  {
464  ABC_SWAP( int, iDsd0, iDsd1 );
465  iDsdC = Abc_LitNot(iDsdC);
466  }
467  if ( Abc_LitIsCompl(iDsd1) )
468  fCompl ^= 1, iDsd0 = Abc_LitNot(iDsd0), iDsd1 = Abc_LitNot(iDsd1);
469  }
470  assert( iDsd0 > 1 && iDsd1 > 1 && Type >= 1 && Type <= 3 );
471 /*
472  // check cache
473  iThis = Ifd_ManHashLookup( p, iDsd0, iDsd1, iDsdC, Type );
474  if ( iThis != -1 )
475  return Abc_Var2Lit( iThis, fCompl );
476 */
477  // create new entry
478  if ( Type == 3 )
479  {
480  iThis = Ifd_ManHashFindOrAdd( p, iDsd0, iDsd1, iDsdC, Type );
481  return Abc_Var2Lit( iThis, fCompl );
482  }
483  assert( iDsdC == -1 );
484  Vec_IntClear( p->vSuper );
485  Ifd_ManOperSuper_rec( p, iDsd0, Type, p->vSuper );
486  Ifd_ManOperSuper_rec( p, iDsd1, Type, p->vSuper );
487  Vec_IntSort( p->vSuper, 1 );
488  iLit0 = Vec_IntEntry( p->vSuper, 0 );
489  Vec_IntForEachEntryStart( p->vSuper, iLit1, i, 1 )
490  iLit0 = Abc_Var2Lit( Ifd_ManHashFindOrAdd(p, iLit0, iLit1, -1, Type), 0 );
491  assert( !Abc_LitIsCompl(iLit0) );
492  // insert into cache
493 // if ( Vec_IntSize(p->vSuper) > 2 )
494 // Ifd_ManHashInsert( p, iDsd0, iDsd1, iDsdC, Type, iLit0 );
495  return Abc_LitNotCond( iLit0, fCompl );
496 }
497 
498 
499 /**Function*************************************************************
500 
501  Synopsis []
502 
503  Description []
504 
505  SideEffects []
506 
507  SeeAlso []
508 
509 ***********************************************************************/
510 int Ifd_ManFindDsd_rec( Ifd_Man_t * pMan, char * pStr, char ** p, int * pMatches )
511 {
512  int fCompl = 0;
513  if ( **p == '!' )
514  (*p)++, fCompl = 1;
515  if ( **p >= 'a' && **p <= 'f' ) // var
516  {
517  assert( **p - 'a' >= 0 && **p - 'a' < 6 );
518  return Abc_Var2Lit( 1, fCompl );
519  }
520  if ( **p == '(' ) // and/or
521  {
522  char * q = pStr + pMatches[ *p - pStr ];
523  int Lit, Res = 1;
524  assert( **p == '(' && *q == ')' );
525  for ( (*p)++; *p < q; (*p)++ )
526  {
527  Lit = Ifd_ManFindDsd_rec( pMan, pStr, p, pMatches );
528  Res = Ifd_ManOper( pMan, Res, Lit, 0, 1 );
529  }
530  assert( *p == q );
531  return Abc_LitNotCond( Res, fCompl );
532  }
533  if ( **p == '[' ) // xor
534  {
535  char * q = pStr + pMatches[ *p - pStr ];
536  int Lit, Res = 0;
537  assert( **p == '[' && *q == ']' );
538  for ( (*p)++; *p < q; (*p)++ )
539  {
540  Lit = Ifd_ManFindDsd_rec( pMan, pStr, p, pMatches );
541  Res = Ifd_ManOper( pMan, Res, Lit, 0, 2 );
542  }
543  assert( *p == q );
544  return Abc_LitNotCond( Res, fCompl );
545  }
546  if ( **p == '<' ) // mux
547  {
548  int Temp[3], * pTemp = Temp, Res;
549  char * q = pStr + pMatches[ *p - pStr ];
550  assert( **p == '<' && *q == '>' );
551  // derive MAX components
552  for ( (*p)++; *p < q; (*p)++ )
553  *pTemp++ = Ifd_ManFindDsd_rec( pMan, pStr, p, pMatches );
554  assert( pTemp == Temp + 3 );
555  assert( *p == q );
556 // Res = (Temp[0] & Temp[1]) | (~Temp[0] & Temp[2]);
557  Res = Ifd_ManOper( pMan, Temp[2], Temp[1], Temp[0], 3 );
558  return Abc_LitNotCond( Res, fCompl );
559  }
560  assert( 0 );
561  return 0;
562 }
563 #define IFM_MAX_STR 100
564 #define IFM_MAX_VAR 16
565 int * Ifd_ManComputeMatches( char * p )
566 {
567  static int pMatches[IFM_MAX_STR];
568  int pNested[IFM_MAX_VAR];
569  int v, nNested = 0;
570  for ( v = 0; p[v]; v++ )
571  {
572  assert( v < IFM_MAX_STR );
573  pMatches[v] = 0;
574  if ( p[v] == '(' || p[v] == '[' || p[v] == '<' || p[v] == '{' )
575  pNested[nNested++] = v;
576  else if ( p[v] == ')' || p[v] == ']' || p[v] == '>' || p[v] == '}' )
577  pMatches[pNested[--nNested]] = v;
578  assert( nNested < IFM_MAX_VAR );
579  }
580  assert( nNested == 0 );
581  return pMatches;
582 }
583 int Ifd_ManFindDsd( Ifd_Man_t * pMan, char * p )
584 {
585  int Res;
586  if ( *p == '0' && *(p+1) == 0 )
587  Res = 0;
588  else if ( *p == '1' && *(p+1) == 0 )
589  Res = 1;
590  else
591  Res = Ifd_ManFindDsd_rec( pMan, p, &p, Ifd_ManComputeMatches(p) );
592  assert( *++p == 0 );
593  return Res;
594 }
595 
596 
597 /**Function*************************************************************
598 
599  Synopsis []
600 
601  Description []
602 
603  SideEffects []
604 
605  SeeAlso []
606 
607 ***********************************************************************/
608 void Ifd_ManDsdTest2()
609 {
610  char * p = "(abc)";
611 // char * q = "(a[bc])";
612 // char * r = "[<abc>(def)]";
613  Ifd_Man_t * pMan = Ifd_ManStart();
614  int iLit = Ifd_ManFindDsd( pMan, p );
615  Ifd_ObjPrint( pMan, iLit );
616  Ifd_ManStop( pMan );
617  printf( "\n" );
618 }
619 
620 /**Function*************************************************************
621 
622  Synopsis []
623 
624  Description []
625 
626  SideEffects []
627 
628  SeeAlso []
629 
630 ***********************************************************************/
631 Vec_Wrd_t * Ifd_ManDsdTruths( int nVars )
632 {
633  int fUseMux = 1;
634  Vec_Wrd_t * vTruths;
635  Ifd_Man_t * pMan = Ifd_ManStart();
636  Ifd_Obj_t * pLeaf0, * pLeaf1, * pLeaf2;
637  int v, i, j, k, c0, c1, c2;
638  for ( v = 2; v <= nVars; v++ )
639  {
640  // create ANDs/XORs
641  for ( i = 1; i < v; i++ )
642  for ( j = 1; j < v; j++ )
643  if ( i + j == v )
644  {
645  Ifd_ManForEachNodeWithSupp( pMan, i, pLeaf0, c0 )
646  Ifd_ManForEachNodeWithSupp( pMan, j, pLeaf1, c1 )
647  {
648  assert( (int)pLeaf0->nSupp == i );
649  assert( (int)pLeaf1->nSupp == j );
650  Ifd_ManOper( pMan, Abc_Var2Lit(c0, 0), Abc_Var2Lit(c1, 0), -1, 1 );
651  if ( !pLeaf1->fWay )
652  Ifd_ManOper( pMan, Abc_Var2Lit(c0, 0), Abc_Var2Lit(c1, 1), -1, 1 );
653  if ( !pLeaf0->fWay )
654  Ifd_ManOper( pMan, Abc_Var2Lit(c0, 1), Abc_Var2Lit(c1, 0), -1, 1 );
655  if ( !pLeaf0->fWay && !pLeaf1->fWay )
656  Ifd_ManOper( pMan, Abc_Var2Lit(c0, 1), Abc_Var2Lit(c1, 1), -1, 1 );
657  Ifd_ManOper( pMan, Abc_Var2Lit(c0, 0), Abc_Var2Lit(c1, 0), -1, 2 );
658  }
659  }
660  // create MUX
661  if ( fUseMux )
662  for ( i = 1; i < v-1; i++ )
663  for ( j = 1; j < v-1; j++ )
664  for ( k = 1; k < v-1; k++ )
665  if ( i + j + k == v )
666  {
667  Ifd_ManForEachNodeWithSupp( pMan, i, pLeaf0, c0 )
668  Ifd_ManForEachNodeWithSupp( pMan, j, pLeaf1, c1 )
669  Ifd_ManForEachNodeWithSupp( pMan, k, pLeaf2, c2 )
670  {
671  assert( (int)pLeaf0->nSupp == i );
672  assert( (int)pLeaf1->nSupp == j );
673  assert( (int)pLeaf2->nSupp == k );
674 //printf( "%d %d %d ", i, j, k );
675 //printf( "%d %d %d\n", Ifd_ObjId(pMan, pLeaf0), Ifd_ObjId(pMan, pLeaf1), Ifd_ObjId(pMan, pLeaf2) );
676  if ( pLeaf2->fWay && c0 < c1 )
677  continue;
678  Ifd_ManOper( pMan, Abc_Var2Lit(c0, 0), Abc_Var2Lit(c1, 0), Abc_Var2Lit(c2, 0), 3 );
679  if ( !pLeaf0->fWay && !pLeaf1->fWay )
680  Ifd_ManOper( pMan, Abc_Var2Lit(c0, 1), Abc_Var2Lit(c1, 0), Abc_Var2Lit(c2, 0), 3 );
681  }
682  }
683  // bookmark
684  Vec_IntPush( pMan->vMarks, pMan->nObjs );
685  }
686  Ifd_ManTruthAll( pMan );
687  Mpm_ComputeCnfSizeAll( pMan );
688 // Ifd_ManPrint( pMan );
689  vTruths = pMan->vTruths; pMan->vTruths = NULL;
690  Ifd_ManStop( pMan );
691  return vTruths;
692 }
693 
694 
695 /**Function*************************************************************
696 
697  Synopsis [Generating the guided array for minimal permutations.]
698 
699  Description [http://icodesnip.com/search/johnson%20trotter/]
700 
701  SideEffects []
702 
703  SeeAlso []
704 
705 ***********************************************************************/
706 void Ifd_ManDsdPermPrint( int * perm, int size )
707 {
708  int i;
709  for ( i = 0; i < size; i++ )
710  printf( "%d", perm[i] );
711  printf( "\n" );
712 }
713 Vec_Int_t * Ifd_ManDsdPermJT( int n )
714 {
715  Vec_Int_t * vGuide = Vec_IntAlloc( 100 );
716  int *array, *dir, tmp, tmp2, i, max;
717  array = (int*)malloc(sizeof(int) * n);
718  dir = (int*)calloc(n, sizeof(int));
719  for (i = 0; i < n; i++)
720  array[i] = i;
721  max = n - 1;
722  if (n != 1)
723  do
724  {
725 // Ifd_ManDsdPermPrint(array, n);
726  tmp = array[max];
727  tmp2 = dir[max];
728  i = !dir[max] ? max - 1 : max + 1;
729  array[max] = array[i];
730  array[i] = tmp;
731  Vec_IntPush( vGuide, Abc_MinInt(max, i) );
732  dir[max] = dir[i];
733  dir[i] = tmp2;
734  for (i = 0; i < n; i++)
735  if (array[i] > tmp)
736  dir[i] = !dir[i];
737  max = n;
738  for (i = 0; i < n; i++)
739  if (((!dir[i] && i != 0 && array[i] > array[i-1]) || (dir[i] && i != n-1 && array[i] > array[i+1])) && (array[i] > array[max] || max == n))
740  max = i;
741  }
742  while (max < n);
743 // Ifd_ManDsdPermPrint(array,n);
744  Vec_IntPush( vGuide, 0 );
745  free(dir);
746  free(array);
747  return vGuide;
748 }
749 int Ifd_ManDsdTest4()
750 {
751  int pPerm[6] = { 0, 1, 2, 3, 4, 5 };
752  Vec_Int_t * vGuide = Ifd_ManDsdPermJT( 6 );
753  int i, Entry;
754  Vec_IntForEachEntry( vGuide, Entry, i )
755  {
756  ABC_SWAP( int, pPerm[Entry], pPerm[Entry+1] );
757  Ifd_ManDsdPermPrint( pPerm, 6 );
758  }
759  Vec_IntFree( vGuide );
760  return 1;
761 }
762 
763 
764 /**Function*************************************************************
765 
766  Synopsis []
767 
768  Description []
769 
770  SideEffects []
771 
772  SeeAlso []
773 
774 ***********************************************************************/
775 static inline word Extra_Truth6SwapAdjacent( word t, int iVar )
776 {
777  // variable swapping code
778  static word PMasks[5][3] = {
779  { ABC_CONST(0x9999999999999999), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444) },
780  { ABC_CONST(0xC3C3C3C3C3C3C3C3), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030) },
781  { ABC_CONST(0xF00FF00FF00FF00F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00) },
782  { ABC_CONST(0xFF0000FFFF0000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000) },
783  { ABC_CONST(0xFFFF00000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000) }
784  };
785  assert( iVar < 5 );
786  return (t & PMasks[iVar][0]) | ((t & PMasks[iVar][1]) << (1 << iVar)) | ((t & PMasks[iVar][2]) >> (1 << iVar));
787 }
788 static inline word Extra_Truth6ChangePhase( word t, int iVar)
789 {
790  // elementary truth tables
791  static word Truth6[6] = {
792  ABC_CONST(0xAAAAAAAAAAAAAAAA),
793  ABC_CONST(0xCCCCCCCCCCCCCCCC),
794  ABC_CONST(0xF0F0F0F0F0F0F0F0),
795  ABC_CONST(0xFF00FF00FF00FF00),
796  ABC_CONST(0xFFFF0000FFFF0000),
797  ABC_CONST(0xFFFFFFFF00000000)
798  };
799  assert( iVar < 6 );
800  return ((t & ~Truth6[iVar]) << (1 << iVar)) | ((t & Truth6[iVar]) >> (1 << iVar));
801 }
802 Vec_Wrd_t * Extra_Truth6AllConfigs2( word t, int * pComp, int * pPerm, int nVars )
803 {
804  int nPerms = Extra_Factorial( nVars );
805  int nSwaps = (1 << nVars);
806  Vec_Wrd_t * vTruths = Vec_WrdStart( nPerms * (1 << (nVars+1)) );
807  word tCur, tTemp1, tTemp2;
808  int i, p, c;
809  for ( i = 0; i < 2; i++ )
810  {
811  tCur = i ? t : ~t;
812  tTemp1 = tCur;
813  for ( p = 0; p < nPerms; p++ )
814  {
815  tTemp2 = tCur;
816  for ( c = 0; c < nSwaps; c++ )
817  {
818  Vec_WrdWriteEntry( vTruths, (p << (nVars+1))|(i << nVars)|c, tCur );
819  tCur = Extra_Truth6ChangePhase( tCur, pComp[c] );
820  }
821  assert( tTemp2 == tCur );
822  tCur = Extra_Truth6SwapAdjacent( tCur, pPerm[p] );
823  }
824  assert( tTemp1 == tCur );
825  }
826  if ( t )
827  {
828  int i;
829  word Truth;
830  Vec_WrdForEachEntry( vTruths, Truth, i )
831  assert( Truth );
832  }
833  return vTruths;
834 }
835 Vec_Wrd_t * Extra_Truth6AllConfigs( word t, int * pComp, int * pPerm, int nVars )
836 {
837  int nPerms = Extra_Factorial( nVars );
838  int nSwaps = (1 << nVars);
839  Vec_Wrd_t * vTruths = Vec_WrdStart( nPerms * nSwaps );
840  word tCur = t, tTemp1, tTemp2;
841  int p, c, Config;
842 
843  tTemp1 = tCur;
844  for ( p = 0; p < nPerms; p++ )
845  {
846  tCur = Extra_Truth6SwapAdjacent( tCur, pPerm[p] );
847  Config = 0;
848  tTemp2 = tCur;
849  for ( c = 0; c < nSwaps; c++ )
850  {
851  Vec_WrdWriteEntry( vTruths, (p << nVars)|Config, tCur );
852  tCur = Extra_Truth6ChangePhase( tCur, pComp[c] );
853  Config ^= (1 << pComp[c]);
854  }
855  assert( Config == 0 );
856  assert( tTemp2 == tCur );
857  }
858  assert( tTemp1 == tCur );
859 
860  if ( t )
861  {
862  int i;
863  word Truth;
864  Vec_WrdForEachEntry( vTruths, Truth, i )
865  assert( Truth );
866  }
867  return vTruths;
868 }
869 
870 
871 /**Function*************************************************************
872 
873  Synopsis []
874 
875  Description []
876 
877  SideEffects []
878 
879  SeeAlso []
880 
881 ***********************************************************************/
882 void Ifd_ComputeSignature( word uTruth, int pCounts[6] )
883 {
884  int v, Pos, Neg, Xor;
885  for ( v = 0; v < 6; v++ )
886  {
887  Neg = Abc_TtCountOnes( Abc_Tt6Cofactor0(uTruth, v) ) / 2;
888  Pos = Abc_TtCountOnes( Abc_Tt6Cofactor1(uTruth, v) ) / 2;
889  Xor = Abc_TtCountOnes( Abc_Tt6Cofactor0(uTruth, v) ^ Abc_Tt6Cofactor1(uTruth, v) ) / 2;
890  if ( Pos <= Neg )
891  pCounts[v] = (Pos << 20) | (Neg << 10) | Xor;
892  else
893  pCounts[v] = (Neg << 20) | (Pos << 10) | Xor;
894  }
895  Vec_IntSelectSort( pCounts, 6 );
896 }
897 int Ifd_ManDsdTest33()
898 {
899  int nVars = 6;
900  Vec_Wrd_t * vTruths = Ifd_ManDsdTruths( nVars );
901  int i, v, pCounts[6];
902  word uTruth;
903  Vec_WrdForEachEntry( vTruths, uTruth, i )
904  {
905  Ifd_ComputeSignature( uTruth, pCounts );
906  // print
907  printf( "%5d : ", i );
908  for ( v = 0; v < 6; v++ )
909  printf( "%2d %2d %2d ", (pCounts[v] >> 20) & 0xFF, (pCounts[v] >> 10) & 0xFF, (pCounts[v] >> 0) & 0xFF );
910  printf( " " );
911  Kit_DsdPrintFromTruth( (unsigned *)&uTruth, nVars );
912  printf( "\n" );
913  }
914  Vec_WrdFree( vTruths );
915  return 1;
916 }
917 
918 /**Function*************************************************************
919 
920  Synopsis []
921 
922  Description []
923 
924  SideEffects []
925 
926  SeeAlso []
927 
928 ***********************************************************************/
929 int Ifd_ManDsdTest()
930 {
931  int nVars = 6;
932  FILE * pFile;
933  char pFileName[32];
934  Vec_Wrd_t * vTruths = Ifd_ManDsdTruths( nVars );
935  Vec_Wrd_t * vVariants;
936  Vec_Int_t * vUniques;
937  Vec_Int_t * vCompls;
938  Vec_Wrd_t * vTruthRes = Vec_WrdAlloc( 4000000 );
939  Vec_Int_t * vConfgRes = Vec_IntAlloc( 4000000 );
940  int * pComp, * pPerm;
941  word Truth, Variant;
942  int i, k, Uniq, Runner, Counter = 0;
943  assert( nVars >= 3 && nVars <= 6 );
944  assert( Vec_WrdSize(vTruths) < (1<<10) );
945  vCompls = Vec_IntAlloc( 720 * 64 );
946  pComp = Extra_GreyCodeSchedule( nVars );
947  pPerm = Extra_PermSchedule( nVars );
948  Vec_WrdForEachEntry( vTruths, Truth, i )
949  {
950  vVariants = Extra_Truth6AllConfigs( Truth, pComp, pPerm, nVars );
951  // save compl bits
952  Vec_IntClear( vCompls );
953  Vec_WrdForEachEntry( vVariants, Variant, k )
954  {
955  Vec_IntPush( vCompls, (int)(Variant & 1) );
956  Vec_WrdWriteEntry( vVariants, k, Variant & 1 ? ~Variant : Variant );
957  }
958  // uniqify
959  vUniques = Hsh_WrdManHashArray( vVariants, 1 );
960  Runner = 0;
961  Vec_IntForEachEntry( vUniques, Uniq, k )
962  if ( Runner == Uniq )
963  {
964  Variant = Vec_WrdEntry(vVariants, k);
965  assert( (Variant & 1) == 0 );
966  Vec_WrdPush( vTruthRes, Variant );
967  Vec_IntPush( vConfgRes, (i << 17)|(Vec_IntEntry(vCompls, k) << 16)|k );
968  Runner++;
969  }
970  Vec_IntUniqify( vUniques );
971  assert( Runner == Vec_IntSize(vUniques) );
972  Counter += Vec_IntSize(vUniques);
973 //printf( "%5d : ", i ); Kit_DsdPrintFromTruth( &Truth, nVars ), printf( " " ), Vec_IntPrint( vUniques ), printf( "\n" );
974  Vec_IntFree( vUniques );
975  Vec_WrdFree( vVariants );
976  }
977  Vec_IntFree( vCompls );
978  Vec_WrdFree( vTruths );
979  ABC_FREE( pPerm );
980  ABC_FREE( pComp );
981  printf( "Total = %d.\n", Counter );
982  assert( Vec_WrdSize(vTruthRes) == Counter );
983  // write the data into a file
984  sprintf( pFileName, "dsdfuncs%d.dat", nVars );
985  pFile = fopen( pFileName, "wb" );
986  fwrite( Vec_WrdArray(vTruthRes), sizeof(word), Vec_WrdSize(vTruthRes), pFile );
987  fwrite( Vec_IntArray(vConfgRes), sizeof(int), Vec_IntSize(vConfgRes), pFile );
988  fclose( pFile );
989  printf( "File \"%s\" with %d 6-input functions has been written out.\n", pFileName, Vec_IntSize(vConfgRes) );
990  Vec_WrdFree( vTruthRes );
991  Vec_IntFree( vConfgRes );
992  return 1;
993 }
994 
995 int Ifd_ManDsdTest55()
996 {
997  abctime clk = Abc_Clock();
998  FILE * pFile;
999  char * pFileName = "dsdfuncs6.dat";
1000  int RetValue, size = Extra_FileSize( pFileName ) / 12; // 2866420
1001  Vec_Wrd_t * vTruthRes = Vec_WrdAlloc( size + 1 );
1002  Vec_Int_t * vConfgRes = Vec_IntAlloc( size );
1003  Hsh_IntMan_t * pHash;
1004 
1005  pFile = fopen( pFileName, "rb" );
1006  RetValue = fread( Vec_WrdArray(vTruthRes), sizeof(word), size, pFile );
1007  RetValue = fread( Vec_IntArray(vConfgRes), sizeof(int), size, pFile );
1008  vTruthRes->nSize = size;
1009  vConfgRes->nSize = size;
1010  // create hash table
1011  pHash = Hsh_WrdManHashArrayStart( vTruthRes, 1 );
1012  // experiment with functions
1013 
1014  // cleanup
1015  Hsh_IntManStop( pHash );
1016  Vec_WrdFree( vTruthRes );
1017  Vec_IntFree( vConfgRes );
1018  Abc_PrintTime( 1, "Reading file", Abc_Clock() - clk );
1019  return 1;
1020 }
1021 
1022 
1023 ////////////////////////////////////////////////////////////////////////
1024 /// END OF FILE ///
1025 ////////////////////////////////////////////////////////////////////////
1026 
1027 
1028 ABC_NAMESPACE_IMPL_END
1029 
memset
char * memset()
Ifd_ManDsdPermPrint
void Ifd_ManDsdPermPrint(int *perm, int size)
Definition: mpmPre.c:706
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Ifd_ObjIsAnd
static int Ifd_ObjIsAnd(Ifd_Obj_t *p)
Definition: mpmPre.c:69
IFM_MAX_STR
#define IFM_MAX_STR
Definition: mpmPre.c:563
malloc
char * malloc()
Ifd_ManFindDsd
int Ifd_ManFindDsd(Ifd_Man_t *pMan, char *p)
Definition: mpmPre.c:583
Ifd_Man_t_::vMarks
Vec_Int_t * vMarks
Definition: mpmPre.c:60
Ifd_ManTruthAll
void Ifd_ManTruthAll(Ifd_Man_t *p)
Definition: mpmPre.c:268
Ifd_ObjIsXor
static int Ifd_ObjIsXor(Ifd_Obj_t *p)
Definition: mpmPre.c:70
Ifd_ManDsdTruths
Vec_Wrd_t * Ifd_ManDsdTruths(int nVars)
Definition: mpmPre.c:631
Ifd_LitNumAnds
static int Ifd_LitNumAnds(Ifd_Man_t *p, int iLit)
Definition: mpmPre.c:77
Abc_PrimeCudd
static int Abc_PrimeCudd(unsigned int p)
Definition: abc_global.h:383
Ifd_ManDsdTest4
int Ifd_ManDsdTest4()
Definition: mpmPre.c:749
free
VOID_HACK free()
Ifd_ObjPrint_rec
void Ifd_ObjPrint_rec(Ifd_Man_t *p, int iLit, int *pCounter, int DiffType)
Definition: mpmPre.c:154
Ifd_ManOperSuper_rec
void Ifd_ManOperSuper_rec(Ifd_Man_t *p, int iLit, int Type, Vec_Int_t *vObjs)
Definition: mpmPre.c:428
Ifd_Obj_t
typedefABC_NAMESPACE_IMPL_START struct Ifd_Obj_t_ Ifd_Obj_t
DECLARATIONS ///.
Definition: mpmPre.c:39
Extra_GreyCodeSchedule
int * Extra_GreyCodeSchedule(int n)
Definition: extraUtilMisc.c:2169
Extra_PermSchedule
int * Extra_PermSchedule(int n)
Definition: extraUtilMisc.c:2205
Ifd_Obj_t_::nFreq
unsigned nFreq
Definition: mpmPre.c:42
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ifd_ManForEachNodeWithSupp
#define Ifd_ManForEachNodeWithSupp(p, nVars, pLeaf, i)
Definition: mpmPre.c:79
Ifd_Man_t_::vClauses
Vec_Int_t * vClauses
Definition: mpmPre.c:62
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Pos
ush Pos
Definition: deflate.h:88
Vec_WrdPush
static void Vec_WrdPush(Vec_Wrd_t *p, word Entry)
Definition: vecWrd.h:618
Ifd_LitSuppSize
static int Ifd_LitSuppSize(Ifd_Man_t *p, int iLit)
Definition: mpmPre.c:76
Ifd_ObjIsMux
static int Ifd_ObjIsMux(Ifd_Obj_t *p)
Definition: mpmPre.c:71
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Vec_StrClear
static void Vec_StrClear(Vec_Str_t *p)
Definition: vecStr.h:519
Ifd_ManHashInsert
void Ifd_ManHashInsert(Ifd_Man_t *p, int iDsd0, int iDsd1, int iDsdC, int Type, int Res)
Definition: mpmPre.c:367
Ifd_ManPrint
void Ifd_ManPrint(Ifd_Man_t *p)
Definition: mpmPre.c:191
Ifd_ObjPrint
void Ifd_ObjPrint(Ifd_Man_t *p, int iLit)
Definition: mpmPre.c:172
Ifd_Obj_t_
Definition: mpmPre.c:40
Ifd_ObjTruth
word Ifd_ObjTruth(Ifd_Man_t *p, int iLit)
Definition: mpmPre.c:257
Ifd_ManDsdTest2
void Ifd_ManDsdTest2()
Definition: mpmPre.c:608
Vec_StrAlloc
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
Kit_DsdPrintFromTruth
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition: kitDsd.c:490
Abc_TtCountOnes
static int Abc_TtCountOnes(word x)
Definition: utilTruth.h:1470
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Ifd_ManObjFromLit
static Ifd_Obj_t * Ifd_ManObjFromLit(Ifd_Man_t *p, int iLit)
Definition: mpmPre.c:74
Abc_Tt6Cofactor0
static word Abc_Tt6Cofactor0(word t, int iVar)
Definition: utilTruth.h:370
Vec_StrPush
static void Vec_StrPush(Vec_Str_t *p, char Entry)
Definition: vecStr.h:535
Vec_WrdSize
static int Vec_WrdSize(Vec_Wrd_t *p)
Definition: vecWrd.h:336
Vec_WrdFreeP
static void Vec_WrdFreeP(Vec_Wrd_t **p)
Definition: vecWrd.h:277
Vec_WrdForEachEntry
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecWrd.h:54
Vec_IntSort
static void Vec_IntSort(Vec_Int_t *p, int fReverse)
Definition: vecInt.h:1293
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Hsh_WrdManHashArray
static Vec_Int_t * Hsh_WrdManHashArray(Vec_Wrd_t *vDataW, int nSize)
Definition: vecHsh.h:203
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition: abc_global.h:218
Ifd_ManStop
void Ifd_ManStop(Ifd_Man_t *p)
Definition: mpmPre.c:122
Hsh_WrdManHashArrayStart
static Hsh_IntMan_t * Hsh_WrdManHashArrayStart(Vec_Wrd_t *vDataW, int nSize)
Definition: vecHsh.h:217
Ifd_Man_t_::vSuper
Vec_Int_t * vSuper
Definition: mpmPre.c:64
Extra_Truth6AllConfigs2
Vec_Wrd_t * Extra_Truth6AllConfigs2(word t, int *pComp, int *pPerm, int nVars)
Definition: mpmPre.c:802
Ifd_ManDsdTest
int Ifd_ManDsdTest()
Definition: mpmPre.c:929
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Ifd_Man_t_::vRes
Vec_Int_t * vRes
Definition: mpmPre.c:58
Ifd_ManOper
int Ifd_ManOper(Ifd_Man_t *p, int iDsd0, int iDsd1, int iDsdC, int Type)
Definition: mpmPre.c:439
Extra_PrintHex
void Extra_PrintHex(FILE *pFile, unsigned *pTruth, int nVars)
Definition: extraUtilFile.c:620
Ifd_ObjId
static int Ifd_ObjId(Ifd_Man_t *p, Ifd_Obj_t *pObj)
Definition: mpmPre.c:75
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_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Abc_Tt6Cofactor1
static word Abc_Tt6Cofactor1(word t, int iVar)
Definition: utilTruth.h:375
Ifd_ManHashLookup
int Ifd_ManHashLookup(Ifd_Man_t *p, int iDsd0, int iDsd1, int iDsdC, int Type)
Definition: mpmPre.c:356
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Ifd_Man_t_::vTruths
Vec_Wrd_t * vTruths
Definition: mpmPre.c:61
Hsh_IntManLookup
static int * Hsh_IntManLookup(Hsh_IntMan_t *p, unsigned *pData)
Definition: vecHsh.h:147
Extra_FileSize
int Extra_FileSize(char *pFileName)
Definition: extraUtilFile.c:308
Ifd_ManPrint2
void Ifd_ManPrint2(Ifd_Man_t *p)
Definition: mpmPre.c:181
Kit_TruthIsop
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
FUNCTION DEFINITIONS ///.
Definition: kitIsop.c:55
Mpm_ComputeCnfSizeOne
int Mpm_ComputeCnfSizeOne(word Truth, int nVars, Vec_Int_t *vCover, Vec_Str_t *vCnf)
Definition: mpmPre.c:293
Vec_StrFree
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
Extra_Truth6SwapAdjacent
static word Extra_Truth6SwapAdjacent(word t, int iVar)
Definition: mpmPre.c:775
Vec_WrdWriteEntry
static void Vec_WrdWriteEntry(Vec_Wrd_t *p, int i, word Entry)
Definition: vecWrd.h:418
Ifd_Man_t_::pObjs
Ifd_Obj_t * pObjs
Definition: mpmPre.c:53
Truth6
static word Truth6[6]
Definition: ifDec07.c:52
IFM_MAX_VAR
#define IFM_MAX_VAR
Definition: mpmPre.c:564
Ifd_ManHashFindOrAdd
int Ifd_ManHashFindOrAdd(Ifd_Man_t *p, int iDsd0, int iDsd1, int iDsdC, int Type)
Definition: mpmPre.c:381
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Extra_TruthSupportSize
int Extra_TruthSupportSize(unsigned *pTruth, int nVars)
Definition: extraUtilTruth.c:358
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Ifd_Obj_t_::pFans
unsigned pFans[3]
Definition: mpmPre.c:47
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_WrdFree
static void Vec_WrdFree(Vec_Wrd_t *p)
Definition: vecWrd.h:260
Mpm_ComputeCnfSizeAll
void Mpm_ComputeCnfSizeAll(Ifd_Man_t *p)
Definition: mpmPre.c:332
Ifd_Man_t_::vArgs
Vec_Int_t * vArgs
Definition: mpmPre.c:57
max
static double max
Definition: cuddSubsetHB.c:134
Ifd_ManStart
Ifd_Man_t * Ifd_ManStart()
FUNCTION DEFINITIONS ///.
Definition: mpmPre.c:98
Vec_IntUniqify
static int Vec_IntUniqify(Vec_Int_t *p)
Definition: vecInt.h:1314
Ifd_ObjIsVar
static int Ifd_ObjIsVar(Ifd_Obj_t *p)
Definition: mpmPre.c:68
size
static int size
Definition: cuddSign.c:86
Ifd_ManDsdTest33
int Ifd_ManDsdTest33()
Definition: mpmPre.c:897
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
sprintf
char * sprintf()
Counter
static int Counter
Definition: extraBddMisc.c:1877
Ifd_ManFindDsd_rec
int Ifd_ManFindDsd_rec(Ifd_Man_t *pMan, char *pStr, char **p, int *pMatches)
Definition: mpmPre.c:510
Ifd_Obj_t_::fWay
unsigned fWay
Definition: mpmPre.c:46
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Hsh_IntManStop
static void Hsh_IntManStop(Hsh_IntMan_t *p)
Definition: vecHsh.h:119
Ifd_Man_t_::vHash
Hsh_IntMan_t * vHash
Definition: mpmPre.c:59
Extra_Truth6ChangePhase
static word Extra_Truth6ChangePhase(word t, int iVar)
Definition: mpmPre.c:788
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
PMasks
static word PMasks[5][3]
Definition: ifDec07.c:44
Ifd_ManObj
static Ifd_Obj_t * Ifd_ManObj(Ifd_Man_t *p, int i)
Definition: mpmPre.c:73
Vec_WrdAlloc
static Vec_Wrd_t * Vec_WrdAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecWrd.h:80
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Hsh_IntManAdd
static int Hsh_IntManAdd(Hsh_IntMan_t *p, int iData)
Definition: vecHsh.h:157
Vec_WrdStart
static Vec_Wrd_t * Vec_WrdStart(int nSize)
Definition: vecWrd.h:103
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Truth
static ABC_NAMESPACE_IMPL_START word Truth[8]
DECLARATIONS ///.
Definition: giaShrink6.c:32
s_Truths6
static word s_Truths6[6]
Definition: extraUtilEnum.c:430
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Ifd_ComputeSignature
void Ifd_ComputeSignature(word uTruth, int pCounts[6])
Definition: mpmPre.c:882
Vec_WrdArray
static word * Vec_WrdArray(Vec_Wrd_t *p)
Definition: vecWrd.h:316
Vec_Str_t_
Definition: bblif.c:47
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition: abc_global.h:206
calloc
char * calloc()
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Extra_Truth6AllConfigs
Vec_Wrd_t * Extra_Truth6AllConfigs(word t, int *pComp, int *pPerm, int nVars)
Definition: mpmPre.c:835
Vec_WrdEntry
static word Vec_WrdEntry(Vec_Wrd_t *p, int i)
Definition: vecWrd.h:384
Ifd_ManComputeMatches
int * Ifd_ManComputeMatches(char *p)
Definition: mpmPre.c:565
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
Extra_Factorial
int Extra_Factorial(int n)
Definition: extraUtilMisc.c:216
Ifd_Man_t_
Definition: mpmPre.c:51
Abc_LitRegular
static int Abc_LitRegular(int Lit)
Definition: abc_global.h:268
assert
#define assert(ex)
Definition: util_old.h:213
Ifd_ManDsdPermJT
Vec_Int_t * Ifd_ManDsdPermJT(int n)
Definition: mpmPre.c:713
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Hsh_IntManStart
static Hsh_IntMan_t * Hsh_IntManStart(Vec_Int_t *vData, int nSize, int nEntries)
FUNCTION DEFINITIONS ///.
Definition: vecHsh.h:109
Ifd_ObjTruth_rec
word Ifd_ObjTruth_rec(Ifd_Man_t *p, int iLit, int *pCounter)
Definition: mpmPre.c:221
Ifd_Obj_t_::Type
unsigned Type
Definition: mpmPre.c:45
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Ifd_ManDsdTest55
int Ifd_ManDsdTest55()
Definition: mpmPre.c:995
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition: vecWrd.h:42
Ifd_Obj_t_::nAnds
unsigned nAnds
Definition: mpmPre.c:43
Ifd_Man_t_::nObjs
int nObjs
Definition: mpmPre.c:54
Ifd_Man_t_::nObjsAlloc
int nObjsAlloc
Definition: mpmPre.c:55
Ifd_Obj_t_::nSupp
unsigned nSupp
Definition: mpmPre.c:44
Hsh_IntMan_t_
Definition: vecHsh.h:57