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