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