1 /**CFile****************************************************************
2
3 FileName [ Fxch.h ]
4
5 PackageName [ Fast eXtract with Cube Hashing (FXCH) ]
6
7 Synopsis [ External declarations of fast extract with cube hashing. ]
8
9 Author [ Bruno Schmitt - boschmitt at inf.ufrgs.br ]
10
11 Affiliation [ UFRGS ]
12
13 Date [ Ver. 1.0. Started - March 6, 2016. ]
14
15 Revision []
16
17 ***********************************************************************/
18
19 #ifndef ABC__opt__fxch__fxch_h
20 #define ABC__opt__fxch__fxch_h
21
22 #include "base/abc/abc.h"
23
24 #include "misc/vec/vecHsh.h"
25 #include "misc/vec/vecQue.h"
26 #include "misc/vec/vecVec.h"
27 #include "misc/vec/vecWec.h"
28
29 ABC_NAMESPACE_HEADER_START
30
31 typedef unsigned char uint8_t;
32 typedef unsigned int uint32_t;
33
34 ////////////////////////////////////////////////////////////////////////
35 /// TYPEDEF DECLARATIONS ///
36 ////////////////////////////////////////////////////////////////////////
37 typedef struct Fxch_Man_t_ Fxch_Man_t;
38 typedef struct Fxch_SubCube_t_ Fxch_SubCube_t;
39 typedef struct Fxch_SCHashTable_t_ Fxch_SCHashTable_t;
40 typedef struct Fxch_SCHashTable_Entry_t_ Fxch_SCHashTable_Entry_t;
41 ////////////////////////////////////////////////////////////////////////
42 /// STRUCTURES DEFINITIONS ///
43 ////////////////////////////////////////////////////////////////////////
44 /* Sub-Cube Structure
45 *
46 * In the context of this program, a sub-cube is a cube derived from
47 * another cube by removing one or two literals. Since a cube is represented
48 * as a vector of literals, one might think that a sub-cube would also be
49 * represented in the same way. However, in order to same memory, we only
50 * store a sub-cube identifier and the data necessary to generate the sub-cube:
51 * - The index number of the orignal cube in the cover. (iCube)
52 * - Identifiers of which literal(s) was(were) removed. (iLit0, iLit1)
53 *
54 * The sub-cube identifier is generated by adding the unique identifiers of
55 * its literals.
56 *
57 */
58
59 struct Fxch_SubCube_t_
60 {
61 uint32_t Id,
62 iCube;
63 uint32_t iLit0 : 16,
64 iLit1 : 16;
65 };
66
67 /* Sub-cube Hash Table
68 */
69 struct Fxch_SCHashTable_Entry_t_
70 {
71 Fxch_SubCube_t* vSCData;
72 uint32_t Size : 16,
73 Cap : 16;
74 };
75
76 struct Fxch_SCHashTable_t_
77 {
78 Fxch_Man_t* pFxchMan;
79 /* Internal data */
80 Fxch_SCHashTable_Entry_t* pBins;
81 unsigned int nEntries,
82 SizeMask;
83
84 /* Temporary data */
85 Vec_Int_t vSubCube0;
86 Vec_Int_t vSubCube1;
87 };
88
89 struct Fxch_Man_t_
90 {
91 /* user's data */
92 Vec_Wec_t* vCubes;
93 int nCubesInit;
94 int LitCountMax;
95
96 /* internal data */
97 Fxch_SCHashTable_t* pSCHashTable;
98
99 Vec_Wec_t* vLits; /* lit -> cube */
100 Vec_Int_t* vLitCount; /* literal counts (currently not used) */
101 Vec_Int_t* vLitHashKeys; /* Literal hash keys used to generate subcube hash */
102
103 Hsh_VecMan_t* pDivHash;
104 Vec_Flt_t* vDivWeights; /* divisor weights */
105 Vec_Que_t* vDivPrio; /* priority queue for divisors by weight */
106 Vec_Wec_t* vDivCubePairs; /* cube pairs for each div */
107
108 Vec_Int_t* vLevels; /* variable levels */
109
110 // Cube Grouping
111 Vec_Int_t* vTranslation;
112 Vec_Int_t* vOutputID;
113 int* pTempOutputID;
114 int nSizeOutputID;
115
116 // temporary data to update the data-structure when a divisor is extracted
117 Vec_Int_t* vCubesS; /* cubes for the given single cube divisor */
118 Vec_Int_t* vPairs; /* cube pairs for the given double cube divisor */
119 Vec_Int_t* vCubeFree; // cube-free divisor
120 Vec_Int_t* vDiv; // selected divisor
121
122 Vec_Int_t* vCubesToRemove;
123 Vec_Int_t* vCubesToUpdate;
124 Vec_Int_t* vSCC;
125
126 /* Statistics */
127 abctime timeInit; /* Initialization time */
128 abctime timeExt; /* Extraction time */
129 int nVars; // original problem variables
130 int nLits; // the number of SOP literals
131 int nPairsS; // number of lit pairs
132 int nPairsD; // number of cube pairs
133 int nExtDivs; /* Number of extracted divisor */
134 };
135
136 ////////////////////////////////////////////////////////////////////////
137 /// FUNCTION DEFINITIONS ///
138 ////////////////////////////////////////////////////////////////////////
139 /* The following functions are from abcFx.c
140 * They are use in order to retrive SOP information for fast_extract
141 * Since I want an implementation that change only the core part of
142 * the algorithm I'm using this */
143 extern Vec_Wec_t* Abc_NtkFxRetrieve( Abc_Ntk_t* pNtk );
144 extern void Abc_NtkFxInsert( Abc_Ntk_t* pNtk, Vec_Wec_t* vCubes );
145 extern int Abc_NtkFxCheck( Abc_Ntk_t* pNtk );
146
Fxch_CountOnes(unsigned num)147 static inline int Fxch_CountOnes( unsigned num )
148 {
149 num = ( num & 0x55555555 ) + ( ( num >> 1) & 0x55555555 );
150 num = ( num & 0x33333333 ) + ( ( num >> 2) & 0x33333333 );
151 num = ( num & 0x0F0F0F0F ) + ( ( num >> 4) & 0x0F0F0F0F );
152 num = ( num & 0x00FF00FF ) + ( ( num >> 8) & 0x00FF00FF );
153 return ( num & 0x0000FFFF ) + ( num >> 16 );
154 }
155
156 /*===== Fxch.c =======================================================*/
157 int Abc_NtkFxchPerform( Abc_Ntk_t* pNtk, int nMaxDivExt, int fVerbose, int fVeryVerbose );
158 int Fxch_FastExtract( Vec_Wec_t* vCubes, int ObjIdMax, int nMaxDivExt, int fVerbose, int fVeryVerbose );
159
160 /*===== FxchDiv.c ====================================================================================================*/
161 int Fxch_DivCreate( Fxch_Man_t* pFxchMan, Fxch_SubCube_t* pSubCube0, Fxch_SubCube_t* pSubCube1 );
162 int Fxch_DivAdd( Fxch_Man_t* pFxchMan, int fUpdate, int fSingleCube, int fBase );
163 int Fxch_DivRemove( Fxch_Man_t* pFxchMan, int fUpdate, int fSingleCube, int fBase );
164 void Fxch_DivSepareteCubes( Vec_Int_t* vDiv, Vec_Int_t* vCube0, Vec_Int_t* vCube1 );
165 int Fxch_DivRemoveLits( Vec_Int_t* vCube0, Vec_Int_t* vCube1, Vec_Int_t* vDiv, int *fCompl );
166 void Fxch_DivPrint( Fxch_Man_t* pFxchMan, int iDiv );
167 int Fxch_DivIsNotConstant1( Vec_Int_t* vDiv );
168
169 /*===== FxchMan.c ====================================================================================================*/
170 Fxch_Man_t* Fxch_ManAlloc( Vec_Wec_t* vCubes );
171 void Fxch_ManFree( Fxch_Man_t* pFxchMan );
172 void Fxch_ManMapLiteralsIntoCubes( Fxch_Man_t* pFxchMan, int nVars );
173 void Fxch_ManGenerateLitHashKeys( Fxch_Man_t* pFxchMan );
174 void Fxch_ManSCHashTablesInit( Fxch_Man_t* pFxchMan );
175 void Fxch_ManSCHashTablesFree( Fxch_Man_t* pFxchMan );
176 void Fxch_ManDivCreate( Fxch_Man_t* pFxchMan );
177 int Fxch_ManComputeLevelDiv( Fxch_Man_t* pFxchMan, Vec_Int_t* vCubeFree );
178 int Fxch_ManComputeLevelCube( Fxch_Man_t* pFxchMan, Vec_Int_t* vCube );
179 void Fxch_ManComputeLevel( Fxch_Man_t* pFxchMan );
180 void Fxch_ManUpdate( Fxch_Man_t* pFxchMan, int iDiv );
181 void Fxch_ManPrintDivs( Fxch_Man_t* pFxchMan );
182 void Fxch_ManPrintStats( Fxch_Man_t* pFxchMan );
183
Fxch_ManGetCube(Fxch_Man_t * pFxchMan,int iCube)184 static inline Vec_Int_t* Fxch_ManGetCube( Fxch_Man_t* pFxchMan,
185 int iCube )
186 {
187 return Vec_WecEntry( pFxchMan->vCubes, iCube );
188 }
189
Fxch_ManGetLit(Fxch_Man_t * pFxchMan,int iCube,int iLit)190 static inline int Fxch_ManGetLit( Fxch_Man_t* pFxchMan,
191 int iCube,
192 int iLit )
193 {
194 return Vec_IntEntry( Vec_WecEntry(pFxchMan->vCubes, iCube), iLit );
195 }
196
197 /*===== FxchSCHashTable.c ============================================*/
198 Fxch_SCHashTable_t* Fxch_SCHashTableCreate( Fxch_Man_t* pFxchMan, int nEntries );
199
200 void Fxch_SCHashTableDelete( Fxch_SCHashTable_t* );
201
202 int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable,
203 Vec_Wec_t* vCubes,
204 uint32_t SubCubeID,
205 uint32_t iCube,
206 uint32_t iLit0,
207 uint32_t iLit1,
208 char fUpdate );
209
210
211 int Fxch_SCHashTableRemove( Fxch_SCHashTable_t* pSCHashTable,
212 Vec_Wec_t* vCubes,
213 uint32_t SubCubeID,
214 uint32_t iCube,
215 uint32_t iLit0,
216 uint32_t iLit1,
217 char fUpdate );
218
219 unsigned int Fxch_SCHashTableMemory( Fxch_SCHashTable_t* );
220 void Fxch_SCHashTablePrint( Fxch_SCHashTable_t* );
221
222 ABC_NAMESPACE_HEADER_END
223
224 #endif
225
226 ////////////////////////////////////////////////////////////////////////
227 /// END OF FILE ///
228 ////////////////////////////////////////////////////////////////////////
229
230