1 /**CFile****************************************************************
2
3 FileName [mfsMan.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [The good old minimization with complete don't-cares.]
8
9 Synopsis [Procedures working with the manager.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: mfsMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "mfsInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis []
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Mfs_ManAlloc(Mfs_Par_t * pPars)45 Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars )
46 {
47 Mfs_Man_t * p;
48 // start the manager
49 p = ABC_ALLOC( Mfs_Man_t, 1 );
50 memset( p, 0, sizeof(Mfs_Man_t) );
51 p->pPars = pPars;
52 p->vProjVarsCnf = Vec_IntAlloc( 100 );
53 p->vProjVarsSat = Vec_IntAlloc( 100 );
54 p->vDivLits = Vec_IntAlloc( 100 );
55 p->nDivWords = Abc_BitWordNum(p->pPars->nWinMax + MFS_FANIN_MAX);
56 p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nWinMax + MFS_FANIN_MAX + 1, p->nDivWords );
57 p->pMan = Int_ManAlloc();
58 p->vMem = Vec_IntAlloc( 0 );
59 p->vLevels = Vec_VecStart( 32 );
60 p->vMfsFanins= Vec_PtrAlloc( 32 );
61 return p;
62 }
63
64 /**Function*************************************************************
65
66 Synopsis []
67
68 Description []
69
70 SideEffects []
71
72 SeeAlso []
73
74 ***********************************************************************/
Mfs_ManClean(Mfs_Man_t * p)75 void Mfs_ManClean( Mfs_Man_t * p )
76 {
77 if ( p->pAigWin )
78 Aig_ManStop( p->pAigWin );
79 if ( p->pCnf )
80 Cnf_DataFree( p->pCnf );
81 if ( p->pSat )
82 sat_solver_delete( p->pSat );
83 if ( p->vRoots )
84 Vec_PtrFree( p->vRoots );
85 if ( p->vSupp )
86 Vec_PtrFree( p->vSupp );
87 if ( p->vNodes )
88 Vec_PtrFree( p->vNodes );
89 if ( p->vDivs )
90 Vec_PtrFree( p->vDivs );
91 p->pAigWin = NULL;
92 p->pCnf = NULL;
93 p->pSat = NULL;
94 p->vRoots = NULL;
95 p->vSupp = NULL;
96 p->vNodes = NULL;
97 p->vDivs = NULL;
98 }
99
100 /**Function*************************************************************
101
102 Synopsis []
103
104 Description []
105
106 SideEffects []
107
108 SeeAlso []
109
110 ***********************************************************************/
Mfs_ManPrint(Mfs_Man_t * p)111 void Mfs_ManPrint( Mfs_Man_t * p )
112 {
113 if ( p->pPars->fResub )
114 {
115 printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d. MaxDivs = %d.\n",
116 p->nTotalNodesBeg, p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts, p->nMaxDivs );
117
118 printf( "Attempts : " );
119 printf( "Remove %6d out of %6d (%6.2f %%) ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
120 printf( "Resub %6d out of %6d (%6.2f %%) ", p->nResubs, p->nTryResubs, 100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs) );
121 printf( "\n" );
122
123 printf( "Reduction: " );
124 printf( "Nodes %6d out of %6d (%6.2f %%) ", p->nTotalNodesBeg-p->nTotalNodesEnd, p->nTotalNodesBeg, 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/Abc_MaxInt(1, p->nTotalNodesBeg) );
125 printf( "Edges %6d out of %6d (%6.2f %%) ", p->nTotalEdgesBeg-p->nTotalEdgesEnd, p->nTotalEdgesBeg, 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/Abc_MaxInt(1, p->nTotalEdgesBeg) );
126 printf( "\n" );
127
128 if (p->pPars->fPower)
129 printf( "Power( %5.2f, %4.2f%%) \n",
130 p->TotalSwitchingBeg - p->TotalSwitchingEnd,
131 100.0*(p->TotalSwitchingBeg-p->TotalSwitchingEnd)/p->TotalSwitchingBeg );
132 if ( p->pPars->fSwapEdge )
133 printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n",
134 p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) );
135 // printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) );
136 }
137 else
138 {
139 printf( "Nodes = %d. Try = %d. Total mints = %d. Local DC mints = %d. Ratio = %5.2f.\n",
140 p->nTotalNodesBeg, p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare,
141 1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal );
142 // printf( "Average ratio of sequential DCs in the global space = %5.2f.\n",
143 // 1.0-(p->dTotalRatios/p->nNodesTried) );
144 printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d. Timeouts = %d.\n",
145 p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained, p->nTimeOuts );
146 }
147
148 ABC_PRTP( "Win", p->timeWin , p->timeTotal );
149 ABC_PRTP( "Div", p->timeDiv , p->timeTotal );
150 ABC_PRTP( "Aig", p->timeAig , p->timeTotal );
151 ABC_PRTP( "Gia", p->timeGia , p->timeTotal );
152 ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal );
153 ABC_PRTP( "Sat", p->timeSat-p->timeInt , p->timeTotal );
154 ABC_PRTP( "Int", p->timeInt , p->timeTotal );
155 ABC_PRTP( "ALL", p->timeTotal , p->timeTotal );
156
157 }
158
159 /**Function*************************************************************
160
161 Synopsis []
162
163 Description []
164
165 SideEffects []
166
167 SeeAlso []
168
169 ***********************************************************************/
Mfs_ManStop(Mfs_Man_t * p)170 void Mfs_ManStop( Mfs_Man_t * p )
171 {
172 if ( p->pPars->fVerbose )
173 Mfs_ManPrint( p );
174 if ( p->vTruth )
175 Vec_IntFree( p->vTruth );
176 if ( p->pManDec )
177 Bdc_ManFree( p->pManDec );
178 if ( p->pCare )
179 Aig_ManStop( p->pCare );
180 if ( p->vSuppsInv )
181 Vec_VecFree( (Vec_Vec_t *)p->vSuppsInv );
182 if ( p->vProbs )
183 Vec_IntFree( p->vProbs );
184 Mfs_ManClean( p );
185 Int_ManFree( p->pMan );
186 Vec_IntFree( p->vMem );
187 Vec_VecFree( p->vLevels );
188 Vec_PtrFree( p->vMfsFanins );
189 Vec_IntFree( p->vProjVarsCnf );
190 Vec_IntFree( p->vProjVarsSat );
191 Vec_IntFree( p->vDivLits );
192 Vec_PtrFree( p->vDivCexes );
193 ABC_FREE( p );
194 }
195
196 ////////////////////////////////////////////////////////////////////////
197 /// END OF FILE ///
198 ////////////////////////////////////////////////////////////////////////
199
200
201 ABC_NAMESPACE_IMPL_END
202
203