ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
mpmPre.c
Go to the documentation of this file.
1
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
32ABC_NAMESPACE_IMPL_START
33
34
38
39typedef struct Ifd_Obj_t_ Ifd_Obj_t;
40struct 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
50typedef struct Ifd_Man_t_ Ifd_Man_t;
51struct 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
68static inline int Ifd_ObjIsVar( Ifd_Obj_t * p ) { return p->Type == 0; }
69static inline int Ifd_ObjIsAnd( Ifd_Obj_t * p ) { return p->Type == 1; }
70static inline int Ifd_ObjIsXor( Ifd_Obj_t * p ) { return p->Type == 2; }
71static inline int Ifd_ObjIsMux( Ifd_Obj_t * p ) { return p->Type == 3; }
72
73static inline Ifd_Obj_t * Ifd_ManObj( Ifd_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return p->pObjs + i; }
74static inline Ifd_Obj_t * Ifd_ManObjFromLit( Ifd_Man_t * p, int iLit ) { return Ifd_ManObj( p, Abc_Lit2Var(iLit) ); }
75static 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; }
76static inline int Ifd_LitSuppSize( Ifd_Man_t * p, int iLit ) { return iLit > 0 ? Ifd_ManObjFromLit(p, iLit)->nSupp : 0; }
77static 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
86
98Ifd_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}
122void 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
154void 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}
172void 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}
181void 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}
191void 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
221word 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}
257word 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}
268void 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
293int 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}
332void 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
356int 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}
367void 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}
381int 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}
428void 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}
439int 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
510int 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
565int * 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}
583int 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
608void 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
631Vec_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
706void 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}
713Vec_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}
749int 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
775static 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}
788static 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}
802Vec_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}
835Vec_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
882void 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}
897int 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
929int 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
995int 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
1026
1027
1028ABC_NAMESPACE_IMPL_END
1029
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition abc_global.h:265
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Vec_Str_t
struct Vec_Str_t_ Vec_Str_t
Definition bblif.c:46
Pos
ush Pos
Definition deflate.h:88
p
Cube * p
Definition exorList.c:222
Cube
struct cube Cube
Extra_FileSize
int Extra_FileSize(char *pFileName)
Definition extraUtilFile.c:327
Extra_TruthSupportSize
int Extra_TruthSupportSize(unsigned *pTruth, int nVars)
Definition extraUtilTruth.c:358
Extra_PermSchedule
int * Extra_PermSchedule(int n)
Definition extraUtilMisc.c:2206
Extra_Factorial
int Extra_Factorial(int n)
Definition extraUtilMisc.c:217
Extra_GreyCodeSchedule
int * Extra_GreyCodeSchedule(int n)
Definition extraUtilMisc.c:2170
Extra_PrintHex
void Extra_PrintHex(FILE *pFile, unsigned *pTruth, int nVars)
Definition extraUtilFile.c:643
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Kit_TruthIsop
int Kit_TruthIsop(unsigned *puTruth, int nVars, Vec_Int_t *vMemory, int fTryBoth)
Definition kitIsop.c:134
Kit_DsdPrintFromTruth
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition kitDsd.c:491
Extra_Truth6SwapAdjacent
word Extra_Truth6SwapAdjacent(word t, int iVar)
Definition luckyFast6.c:73
Extra_Truth6ChangePhase
word Extra_Truth6ChangePhase(word t, int iVar)
Definition luckyFast6.c:86
Ifd_ManOperSuper_rec
void Ifd_ManOperSuper_rec(Ifd_Man_t *p, int iLit, int Type, Vec_Int_t *vObjs)
Definition mpmPre.c:428
Ifd_ObjPrint
void Ifd_ObjPrint(Ifd_Man_t *p, int iLit)
Definition mpmPre.c:172
Ifd_ManDsdTest4
int Ifd_ManDsdTest4()
Definition mpmPre.c:749
Ifd_ManComputeMatches
int * Ifd_ManComputeMatches(char *p)
Definition mpmPre.c:565
Ifd_ManHashFindOrAdd
int Ifd_ManHashFindOrAdd(Ifd_Man_t *p, int iDsd0, int iDsd1, int iDsdC, int Type)
Definition mpmPre.c:381
Ifd_ManHashLookup
int Ifd_ManHashLookup(Ifd_Man_t *p, int iDsd0, int iDsd1, int iDsdC, int Type)
Definition mpmPre.c:356
Extra_Truth6AllConfigs2
Vec_Wrd_t * Extra_Truth6AllConfigs2(word t, int *pComp, int *pPerm, int nVars)
Definition mpmPre.c:802
Ifd_ManStop
void Ifd_ManStop(Ifd_Man_t *p)
Definition mpmPre.c:122
Ifd_ManPrint
void Ifd_ManPrint(Ifd_Man_t *p)
Definition mpmPre.c:191
Ifd_ManFindDsd
int Ifd_ManFindDsd(Ifd_Man_t *pMan, char *p)
Definition mpmPre.c:583
Ifd_ManDsdTest2
void Ifd_ManDsdTest2()
Definition mpmPre.c:608
Ifd_ManHashInsert
void Ifd_ManHashInsert(Ifd_Man_t *p, int iDsd0, int iDsd1, int iDsdC, int Type, int Res)
Definition mpmPre.c:367
Ifd_ManDsdTruths
Vec_Wrd_t * Ifd_ManDsdTruths(int nVars)
Definition mpmPre.c:631
Mpm_ComputeCnfSizeOne
int Mpm_ComputeCnfSizeOne(word Truth, int nVars, Vec_Int_t *vCover, Vec_Str_t *vCnf)
Definition mpmPre.c:293
Ifd_ObjTruth
word Ifd_ObjTruth(Ifd_Man_t *p, int iLit)
Definition mpmPre.c:257
Ifd_ComputeSignature
void Ifd_ComputeSignature(word uTruth, int pCounts[6])
Definition mpmPre.c:882
Ifd_ManDsdTest
int Ifd_ManDsdTest()
Definition mpmPre.c:929
Ifd_ManStart
Ifd_Man_t * Ifd_ManStart()
FUNCTION DEFINITIONS ///.
Definition mpmPre.c:98
Ifd_Man_t
struct Ifd_Man_t_ Ifd_Man_t
Definition mpmPre.c:50
Ifd_ObjTruth_rec
word Ifd_ObjTruth_rec(Ifd_Man_t *p, int iLit, int *pCounter)
Definition mpmPre.c:221
IFM_MAX_STR
#define IFM_MAX_STR
Definition mpmPre.c:563
Ifd_ObjPrint_rec
void Ifd_ObjPrint_rec(Ifd_Man_t *p, int iLit, int *pCounter, int DiffType)
Definition mpmPre.c:154
Ifd_ManPrint2
void Ifd_ManPrint2(Ifd_Man_t *p)
Definition mpmPre.c:181
Ifd_ManFindDsd_rec
int Ifd_ManFindDsd_rec(Ifd_Man_t *pMan, char *pStr, char **p, int *pMatches)
Definition mpmPre.c:510
Extra_Truth6AllConfigs
Vec_Wrd_t * Extra_Truth6AllConfigs(word t, int *pComp, int *pPerm, int nVars)
Definition mpmPre.c:835
Ifd_ManDsdTest55
int Ifd_ManDsdTest55()
Definition mpmPre.c:995
Ifd_ManTruthAll
void Ifd_ManTruthAll(Ifd_Man_t *p)
Definition mpmPre.c:268
Ifd_ManDsdTest33
int Ifd_ManDsdTest33()
Definition mpmPre.c:897
Ifd_ManForEachNodeWithSupp
#define Ifd_ManForEachNodeWithSupp(p, nVars, pLeaf, i)
Definition mpmPre.c:79
Ifd_ManDsdPermJT
Vec_Int_t * Ifd_ManDsdPermJT(int n)
Definition mpmPre.c:713
IFM_MAX_VAR
#define IFM_MAX_VAR
Definition mpmPre.c:564
Ifd_Obj_t
typedefABC_NAMESPACE_IMPL_START struct Ifd_Obj_t_ Ifd_Obj_t
DECLARATIONS ///.
Definition mpmPre.c:39
Mpm_ComputeCnfSizeAll
void Mpm_ComputeCnfSizeAll(Ifd_Man_t *p)
Definition mpmPre.c:332
Ifd_ManOper
int Ifd_ManOper(Ifd_Man_t *p, int iDsd0, int iDsd1, int iDsdC, int Type)
Definition mpmPre.c:439
Ifd_ManDsdPermPrint
void Ifd_ManDsdPermPrint(int *perm, int size)
Definition mpmPre.c:706
Ifd_Man_t_
Definition mpmPre.c:52
Ifd_Man_t_::nObjsAlloc
int nObjsAlloc
Definition mpmPre.c:55
Ifd_Man_t_::vSuper
Vec_Int_t * vSuper
Definition mpmPre.c:64
Ifd_Man_t_::vHash
Hsh_IntMan_t * vHash
Definition mpmPre.c:59
Ifd_Man_t_::vRes
Vec_Int_t * vRes
Definition mpmPre.c:58
Ifd_Man_t_::pObjs
Ifd_Obj_t * pObjs
Definition mpmPre.c:53
Ifd_Man_t_::vMarks
Vec_Int_t * vMarks
Definition mpmPre.c:60
Ifd_Man_t_::vArgs
Vec_Int_t * vArgs
Definition mpmPre.c:57
Ifd_Man_t_::vTruths
Vec_Wrd_t * vTruths
Definition mpmPre.c:61
Ifd_Man_t_::vClauses
Vec_Int_t * vClauses
Definition mpmPre.c:62
Ifd_Man_t_::nObjs
int nObjs
Definition mpmPre.c:54
Ifd_Obj_t_
Definition mpmPre.c:41
Ifd_Obj_t_::nAnds
unsigned nAnds
Definition mpmPre.c:43
Ifd_Obj_t_::pFans
unsigned pFans[3]
Definition mpmPre.c:47
Ifd_Obj_t_::Type
unsigned Type
Definition mpmPre.c:45
Ifd_Obj_t_::nFreq
unsigned nFreq
Definition mpmPre.c:42
Ifd_Obj_t_::fWay
unsigned fWay
Definition mpmPre.c:46
Ifd_Obj_t_::nSupp
unsigned nSupp
Definition mpmPre.c:44
assert
#define assert(ex)
Definition util_old.h:213
calloc
char * calloc()
memset
char * memset()
sprintf
char * sprintf()
free
VOID_HACK free()
malloc
char * malloc()
Hsh_IntMan_t
struct Hsh_IntMan_t_ Hsh_IntMan_t
Definition vecHsh.h:66
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition vecInt.h:56
Vec_WrdForEachEntry
#define Vec_WrdForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecWrd.h:54
Vec_Wrd_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wrd_t_ Vec_Wrd_t
INCLUDES ///.
Definition vecWrd.h:42