1 /**CFile****************************************************************
2
3 FileName [int2Util.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Interpolation engine.]
8
9 Synopsis [Various utilities.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - Dec 1, 2013.]
16
17 Revision [$Id: int2Util.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "int2Int.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 ***********************************************************************/
Int2_ManComputeCoPres(Vec_Int_t * vSop,int nRegs)45 Vec_Int_t * Int2_ManComputeCoPres( Vec_Int_t * vSop, int nRegs )
46 {
47 Vec_Int_t * vCoPres, * vMap;
48 vCoPres = Vec_IntAlloc( 100 );
49 if ( vSop == NULL )
50 Vec_IntPush( vCoPres, 0 );
51 else
52 {
53 int i, k, Limit;
54 vMap = Vec_IntStart( nRegs );
55 Vec_IntForEachEntryStart( vSop, Limit, i, 1 )
56 {
57 for ( k = 0; k < Limit; k++ )
58 {
59 i++;
60 assert( Vec_IntEntry(vSop, i + k) < 2 * nRegs );
61 Vec_IntWriteEntry( vMap, Abc_Lit2Var(Vec_IntEntry(vSop, i + k)), 1 );
62 }
63 }
64 Vec_IntForEachEntry( vMap, Limit, i )
65 if ( Limit )
66 Vec_IntPush( vCoPres, i+1 );
67 Vec_IntFree( vMap );
68 }
69 return vCoPres;
70 }
71
Int2_ManCollectInternal_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vNodes)72 void Int2_ManCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
73 {
74 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
75 return;
76 Gia_ObjSetTravIdCurrent(p, pObj);
77 if ( Gia_ObjIsCi(pObj) )
78 return;
79 assert( Gia_ObjIsAnd(pObj) );
80 Int2_ManCollectInternal_rec( p, Gia_ObjFanin0(pObj), vNodes );
81 Int2_ManCollectInternal_rec( p, Gia_ObjFanin1(pObj), vNodes );
82 Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
83 }
Int2_ManCollectInternal(Gia_Man_t * p,Vec_Int_t * vCoPres)84 Vec_Int_t * Int2_ManCollectInternal( Gia_Man_t * p, Vec_Int_t * vCoPres )
85 {
86 Vec_Int_t * vNodes;
87 Gia_Obj_t * pObj;
88 int i, Entry;
89 Gia_ManIncrementTravId( p );
90 Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
91 Gia_ManForEachCi( p, pObj, i )
92 Gia_ObjSetTravIdCurrent(p, pObj);
93 vNodes = Vec_IntAlloc( 1000 );
94 Vec_IntForEachEntry( vCoPres, Entry, i )
95 Int2_ManCollectInternal_rec( p, Gia_ObjFanin0(Gia_ManCo(p, Entry)), vNodes );
96 return vNodes;
97 }
Int2_ManProbToGia(Gia_Man_t * p,Vec_Int_t * vSop)98 Gia_Man_t * Int2_ManProbToGia( Gia_Man_t * p, Vec_Int_t * vSop )
99 {
100 Vec_Int_t * vCoPres, * vNodes;
101 Gia_Man_t * pNew, * pTemp;
102 Gia_Obj_t * pObj;
103 int i, k, Entry, Limit;
104 int Lit, Cube, Sop;
105 assert( Gia_ManPoNum(p) == 1 );
106 // collect COs and ANDs
107 vCoPres = Int2_ManComputeCoPres( vSop, Gia_ManRegNum(p) );
108 vNodes = Int2_ManCollectInternal( p, vCoPres );
109 // create new manager
110 pNew = Gia_ManStart( Gia_ManObjNum(p) );
111 pNew->pName = Abc_UtilStrsav( p->pName );
112 pNew->pSpec = Abc_UtilStrsav( p->pSpec );
113 Gia_ManConst0(p)->Value = 0;
114 Gia_ManForEachCi( p, pObj, i )
115 pObj->Value = Gia_ManAppendCi(pNew);
116 Gia_ManHashAlloc( pNew );
117 Gia_ManForEachObjVec( vNodes, p, pObj, i )
118 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
119 Vec_IntForEachEntry( vCoPres, Entry, i )
120 {
121 pObj = Gia_ManCo(p, Entry);
122 pObj->Value = Gia_ObjFanin0Copy( pObj );
123 }
124 // create additional cubes
125 Sop = 0;
126 Vec_IntForEachEntryStart( vSop, Limit, i, 1 )
127 {
128 Cube = 1;
129 for ( k = 0; k < Limit; k++ )
130 {
131 i++;
132 Lit = Vec_IntEntry( vSop, i + k );
133 pObj = Gia_ManRi( p, Abc_Lit2Var(Lit) );
134 Cube = Gia_ManHashAnd( pNew, Cube, Abc_LitNotCond(pObj->Value, Abc_LitIsCompl(Lit)) );
135 }
136 Sop = Gia_ManHashOr( pNew, Sop, Cube );
137 }
138 Gia_ManAppendCo( pNew, Sop );
139 Gia_ManHashStop( pNew );
140 // cleanup
141 pNew = Gia_ManCleanup( pTemp = pNew );
142 Gia_ManStop( pTemp );
143 return pNew;
144 }
145
146 ////////////////////////////////////////////////////////////////////////
147 /// END OF FILE ///
148 ////////////////////////////////////////////////////////////////////////
149
150
151 ABC_NAMESPACE_IMPL_END
152
153