1 /**CFile****************************************************************
2 
3   FileName    [llb1Man.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [BDD based reachability.]
8 
9   Synopsis    [Reachability 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: llb1Man.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "llbInt.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 ***********************************************************************/
Llb_ManPrepareVarMap(Llb_Man_t * p)45 void Llb_ManPrepareVarMap( Llb_Man_t * p )
46 {
47     Aig_Obj_t * pObjLi, * pObjLo;
48     int i, iVarLi, iVarLo;
49     assert( p->vNs2Glo == NULL );
50     assert( p->vCs2Glo == NULL );
51     assert( p->vGlo2Cs == NULL );
52     assert( p->vGlo2Ns == NULL );
53     p->vNs2Glo = Vec_IntStartFull( Vec_IntSize(p->vVar2Obj) );
54     p->vCs2Glo = Vec_IntStartFull( Vec_IntSize(p->vVar2Obj) );
55     p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
56     p->vGlo2Ns = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
57     Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
58     {
59         iVarLi = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLi));
60         iVarLo = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLo));
61         assert( iVarLi >= 0 && iVarLi < Vec_IntSize(p->vVar2Obj) );
62         assert( iVarLo >= 0 && iVarLo < Vec_IntSize(p->vVar2Obj) );
63         Vec_IntWriteEntry( p->vNs2Glo, iVarLi, i );
64         Vec_IntWriteEntry( p->vCs2Glo, iVarLo, i );
65         Vec_IntWriteEntry( p->vGlo2Cs, i, iVarLo );
66         Vec_IntWriteEntry( p->vGlo2Ns, i, iVarLi );
67     }
68     // add mapping of the PIs
69     Saig_ManForEachPi( p->pAig, pObjLo, i )
70     {
71         iVarLo = Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObjLo));
72         Vec_IntWriteEntry( p->vCs2Glo, iVarLo, Aig_ManRegNum(p->pAig)+i );
73         Vec_IntWriteEntry( p->vNs2Glo, iVarLo, Aig_ManRegNum(p->pAig)+i );
74     }
75 }
76 
77 /**Function*************************************************************
78 
79   Synopsis    []
80 
81   Description []
82 
83   SideEffects []
84 
85   SeeAlso     []
86 
87 ***********************************************************************/
Llb_ManPrepareVarLimits(Llb_Man_t * p)88 void Llb_ManPrepareVarLimits( Llb_Man_t * p )
89 {
90     Llb_Grp_t * pGroup;
91     Aig_Obj_t * pVar;
92     int i, k;
93     assert( p->vVarBegs == NULL );
94     assert( p->vVarEnds == NULL );
95     p->vVarEnds = Vec_IntStart( Aig_ManObjNumMax(p->pAig) );
96     p->vVarBegs = Vec_IntStart( Aig_ManObjNumMax(p->pAig) );
97     Vec_IntFill( p->vVarBegs, Aig_ManObjNumMax(p->pAig), p->pMatrix->nCols );
98 
99     for ( i = 0; i < p->pMatrix->nCols; i++ )
100     {
101         pGroup = p->pMatrix->pColGrps[i];
102 
103         Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
104             if ( Vec_IntEntry(p->vVarBegs, pVar->Id) > i )
105                 Vec_IntWriteEntry( p->vVarBegs, pVar->Id, i );
106         Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
107             if ( Vec_IntEntry(p->vVarBegs, pVar->Id) > i )
108                 Vec_IntWriteEntry( p->vVarBegs, pVar->Id, i );
109 
110         Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pVar, k )
111             if ( Vec_IntEntry(p->vVarEnds, pVar->Id) < i )
112                 Vec_IntWriteEntry( p->vVarEnds, pVar->Id, i );
113         Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pVar, k )
114             if ( Vec_IntEntry(p->vVarEnds, pVar->Id) < i )
115                 Vec_IntWriteEntry( p->vVarEnds, pVar->Id, i );
116     }
117 }
118 
119 /**Function*************************************************************
120 
121   Synopsis    []
122 
123   Description []
124 
125   SideEffects []
126 
127   SeeAlso     []
128 
129 ***********************************************************************/
Llb_ManStop(Llb_Man_t * p)130 void Llb_ManStop( Llb_Man_t * p )
131 {
132     Llb_Grp_t * pGrp;
133     DdNode * bTemp;
134     int i;
135 
136 //    Vec_IntFreeP( &p->vMem );
137 //    Vec_PtrFreeP( &p->vTops );
138 //    Vec_PtrFreeP( &p->vBots );
139 //    Vec_VecFreeP( (Vec_Vec_t **)&p->vCuts );
140 
141     if ( p->pMatrix )
142         Llb_MtrFree( p->pMatrix );
143     Vec_PtrForEachEntry( Llb_Grp_t *, p->vGroups, pGrp, i )
144         Llb_ManGroupStop( pGrp );
145     if ( p->dd )
146     {
147 //        printf( "Manager dd\n" );
148         Extra_StopManager( p->dd );
149     }
150     if ( p->ddG )
151     {
152 //        printf( "Manager ddG\n" );
153         if ( p->ddG->bFunc )
154             Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc );
155         Extra_StopManager( p->ddG );
156     }
157     if ( p->ddR )
158     {
159 //        printf( "Manager ddR\n" );
160         if ( p->ddR->bFunc )
161             Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
162         Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
163             Cudd_RecursiveDeref( p->ddR, bTemp );
164         Extra_StopManager( p->ddR );
165     }
166     Aig_ManStop( p->pAig );
167     Vec_PtrFreeP( &p->vGroups );
168     Vec_IntFreeP( &p->vVar2Obj );
169     Vec_IntFreeP( &p->vObj2Var );
170     Vec_IntFreeP( &p->vVarBegs );
171     Vec_IntFreeP( &p->vVarEnds );
172     Vec_PtrFreeP( &p->vRings  );
173     Vec_IntFreeP( &p->vNs2Glo );
174     Vec_IntFreeP( &p->vCs2Glo );
175     Vec_IntFreeP( &p->vGlo2Cs );
176     Vec_IntFreeP( &p->vGlo2Ns );
177 //    Vec_IntFreeP( &p->vHints );
178     ABC_FREE( p );
179 }
180 
181 
182 /**Function*************************************************************
183 
184   Synopsis    []
185 
186   Description []
187 
188   SideEffects []
189 
190   SeeAlso     []
191 
192 ***********************************************************************/
Llb_ManStart(Aig_Man_t * pAigGlo,Aig_Man_t * pAig,Gia_ParLlb_t * pPars)193 Llb_Man_t * Llb_ManStart( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
194 {
195     Llb_Man_t * p;
196     Aig_ManCleanMarkA( pAig );
197     p = ABC_CALLOC( Llb_Man_t, 1 );
198     p->pAigGlo  = pAigGlo;
199     p->pPars    = pPars;
200     p->pAig     = pAig;
201     p->vVar2Obj = Llb_ManMarkPivotNodes( p->pAig, pPars->fUsePivots );
202     p->vObj2Var = Vec_IntInvert( p->vVar2Obj, -1 );
203     p->vRings   = Vec_PtrAlloc( 100 );
204     Llb_ManPrepareVarMap( p );
205     Llb_ManPrepareGroups( p );
206     Aig_ManCleanMarkA( pAig );
207     p->pMatrix = Llb_MtrCreate( p );
208     p->pMatrix->pMan = p;
209     return p;
210 }
211 
212 ////////////////////////////////////////////////////////////////////////
213 ///                       END OF FILE                                ///
214 ////////////////////////////////////////////////////////////////////////
215 
216 
217 ABC_NAMESPACE_IMPL_END
218 
219