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
Ifd_ObjIsVar(Ifd_Obj_t * p)68 static inline int Ifd_ObjIsVar( Ifd_Obj_t * p ) { return p->Type == 0; }
Ifd_ObjIsAnd(Ifd_Obj_t * p)69 static inline int Ifd_ObjIsAnd( Ifd_Obj_t * p ) { return p->Type == 1; }
Ifd_ObjIsXor(Ifd_Obj_t * p)70 static inline int Ifd_ObjIsXor( Ifd_Obj_t * p ) { return p->Type == 2; }
Ifd_ObjIsMux(Ifd_Obj_t * p)71 static inline int Ifd_ObjIsMux( Ifd_Obj_t * p ) { return p->Type == 3; }
72
Ifd_ManObj(Ifd_Man_t * p,int i)73 static inline Ifd_Obj_t * Ifd_ManObj( Ifd_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return p->pObjs + i; }
Ifd_ManObjFromLit(Ifd_Man_t * p,int iLit)74 static inline Ifd_Obj_t * Ifd_ManObjFromLit( Ifd_Man_t * p, int iLit ) { return Ifd_ManObj( p, Abc_Lit2Var(iLit) ); }
Ifd_ObjId(Ifd_Man_t * p,Ifd_Obj_t * pObj)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; }
Ifd_LitSuppSize(Ifd_Man_t * p,int iLit)76 static inline int Ifd_LitSuppSize( Ifd_Man_t * p, int iLit ) { return iLit > 0 ? Ifd_ManObjFromLit(p, iLit)->nSupp : 0; }
Ifd_LitNumAnds(Ifd_Man_t * p,int iLit)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 ***********************************************************************/
Ifd_ManStart()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 }
Ifd_ManStop(Ifd_Man_t * p)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 ***********************************************************************/
Ifd_ObjPrint_rec(Ifd_Man_t * p,int iLit,int * pCounter,int DiffType)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 }
Ifd_ObjPrint(Ifd_Man_t * p,int iLit)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 }
Ifd_ManPrint2(Ifd_Man_t * p)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 }
Ifd_ManPrint(Ifd_Man_t * p)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 ***********************************************************************/
Ifd_ObjTruth_rec(Ifd_Man_t * p,int iLit,int * pCounter)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 }
Ifd_ObjTruth(Ifd_Man_t * p,int iLit)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 }
Ifd_ManTruthAll(Ifd_Man_t * p)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 ***********************************************************************/
Mpm_ComputeCnfSizeOne(word Truth,int nVars,Vec_Int_t * vCover,Vec_Str_t * vCnf)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 }
Mpm_ComputeCnfSizeAll(Ifd_Man_t * p)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 ***********************************************************************/
Ifd_ManHashLookup(Ifd_Man_t * p,int iDsd0,int iDsd1,int iDsdC,int Type)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 }
Ifd_ManHashInsert(Ifd_Man_t * p,int iDsd0,int iDsd1,int iDsdC,int Type,int Res)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 }
Ifd_ManHashFindOrAdd(Ifd_Man_t * p,int iDsd0,int iDsd1,int iDsdC,int Type)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 }
Ifd_ManOperSuper_rec(Ifd_Man_t * p,int iLit,int Type,Vec_Int_t * vObjs)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 }
Ifd_ManOper(Ifd_Man_t * p,int iDsd0,int iDsd1,int iDsdC,int Type)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 ***********************************************************************/
Ifd_ManFindDsd_rec(Ifd_Man_t * pMan,char * pStr,char ** p,int * pMatches)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
Ifd_ManComputeMatches(char * p)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 }
Ifd_ManFindDsd(Ifd_Man_t * pMan,char * p)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 ***********************************************************************/
Ifd_ManDsdTest2()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 ***********************************************************************/
Ifd_ManDsdTruths(int nVars)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 ***********************************************************************/
Ifd_ManDsdPermPrint(int * perm,int size)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 }
Ifd_ManDsdPermJT(int n)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 }
Ifd_ManDsdTest4()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 ***********************************************************************/
Extra_Truth6SwapAdjacent(word t,int iVar)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 }
Extra_Truth6ChangePhase(word t,int iVar)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 }
Extra_Truth6AllConfigs2(word t,int * pComp,int * pPerm,int nVars)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 }
Extra_Truth6AllConfigs(word t,int * pComp,int * pPerm,int nVars)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 ***********************************************************************/
Ifd_ComputeSignature(word uTruth,int pCounts[6])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 }
Ifd_ManDsdTest33()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 ***********************************************************************/
Ifd_ManDsdTest()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
Ifd_ManDsdTest55()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
1030