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