1 /**CFile****************************************************************
2
3 FileName [luckySimple.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Semi-canonical form computation package.]
8
9 Synopsis [Truth table minimization procedures.]
10
11 Author [Jake]
12
13 Date [Started - August 2012]
14
15 ***********************************************************************/
16
17 #include "luckyInt.h"
18
19 ABC_NAMESPACE_IMPL_START
20
setSwapInfoPtr(int varsN)21 static swapInfo* setSwapInfoPtr(int varsN)
22 {
23 int i;
24 swapInfo* x = (swapInfo*) malloc(sizeof(swapInfo));
25 x->posArray = (varInfo*) malloc (sizeof(varInfo)*(varsN+2));
26 x->realArray = (int*) malloc (sizeof(int)*(varsN+2));
27 x->varN = varsN;
28 x->realArray[0]=varsN+100;
29 for(i=1;i<=varsN;i++)
30 {
31 x->posArray[i].position=i;
32 x->posArray[i].direction=-1;
33 x->realArray[i]=i;
34 }
35 x->realArray[varsN+1]=varsN+10;
36 return x;
37 }
38
39
freeSwapInfoPtr(swapInfo * x)40 static void freeSwapInfoPtr(swapInfo* x)
41 {
42 free(x->posArray);
43 free(x->realArray);
44 free(x);
45 }
46
nextSwap(swapInfo * x)47 int nextSwap(swapInfo* x)
48 {
49 int i,j,temp;
50 for(i=x->varN;i>1;i--)
51 {
52 if( i > x->realArray[x->posArray[i].position + x->posArray[i].direction] )
53 {
54 x->posArray[i].position = x->posArray[i].position + x->posArray[i].direction;
55 temp = x->realArray[x->posArray[i].position];
56 x->realArray[x->posArray[i].position] = i;
57 x->realArray[x->posArray[i].position - x->posArray[i].direction] = temp;
58 x->posArray[temp].position = x->posArray[i].position - x->posArray[i].direction;
59 for(j=x->varN;j>i;j--)
60 {
61 x->posArray[j].direction = x->posArray[j].direction * -1;
62 }
63 x->positionToSwap1 = x->posArray[temp].position - 1;
64 x->positionToSwap2 = x->posArray[i].position - 1;
65 return 1;
66 }
67
68 }
69 return 0;
70 }
71
fillInSwapArray(permInfo * pi)72 void fillInSwapArray(permInfo* pi)
73 {
74 int counter=pi->totalSwaps-1;
75 swapInfo* x= setSwapInfoPtr(pi->varN);
76 while(nextSwap(x)==1)
77 {
78 if(x->positionToSwap1<x->positionToSwap2)
79 pi->swapArray[counter--]=x->positionToSwap1;
80 else
81 pi->swapArray[counter--]=x->positionToSwap2;
82 }
83
84 freeSwapInfoPtr(x);
85 }
oneBitPosition(int x,int size)86 int oneBitPosition(int x, int size)
87 {
88 int i;
89 for(i=0;i<size;i++)
90 if((x>>i)&1)
91 return i;
92 return -1;
93 }
fillInFlipArray(permInfo * pi)94 void fillInFlipArray(permInfo* pi)
95 {
96 int i, temp=0, grayNumber;
97 for(i=1;i<=pi->totalFlips;i++)
98 {
99 grayNumber = i^(i>>1);
100 pi->flipArray[pi->totalFlips-i]=oneBitPosition(temp^grayNumber, pi->varN);
101 temp = grayNumber;
102 }
103
104
105 }
factorial(int n)106 static inline int factorial(int n)
107 {
108 return (n == 1 || n == 0) ? 1 : factorial(n - 1) * n;
109 }
setPermInfoPtr(int var)110 permInfo* setPermInfoPtr(int var)
111 {
112 permInfo* x;
113 x = (permInfo*) malloc(sizeof(permInfo));
114 x->flipCtr=0;
115 x->varN = var;
116 x->totalFlips=(1<<var)-1;
117 x->swapCtr=0;
118 x->totalSwaps=factorial(var)-1;
119 x->flipArray = (int*) malloc(sizeof(int)*x->totalFlips);
120 x->swapArray = (int*) malloc(sizeof(int)*x->totalSwaps);
121 fillInSwapArray(x);
122 fillInFlipArray(x);
123 return x;
124 }
125
freePermInfoPtr(permInfo * x)126 void freePermInfoPtr(permInfo* x)
127 {
128 free(x->flipArray);
129 free(x->swapArray);
130 free(x);
131 }
minWord(word * a,word * b,word * minimal,int nVars)132 static inline void minWord(word* a, word* b, word* minimal, int nVars)
133 {
134 if(memCompare(a, b, nVars) == -1)
135 Kit_TruthCopy_64bit( minimal, a, nVars );
136 else
137 Kit_TruthCopy_64bit( minimal, b, nVars );
138 }
minWord3(word * a,word * b,word * minimal,int nVars)139 static inline void minWord3(word* a, word* b, word* minimal, int nVars)
140 {
141 if (memCompare(a, b, nVars) <= 0)
142 {
143 if (memCompare(a, minimal, nVars) < 0)
144 Kit_TruthCopy_64bit( minimal, a, nVars );
145 else
146 return ;
147 }
148 if (memCompare(b, minimal, nVars) <= 0)
149 Kit_TruthCopy_64bit( minimal, b, nVars );
150 }
minWord1(word * a,word * minimal,int nVars)151 static inline void minWord1(word* a, word* minimal, int nVars)
152 {
153 if (memCompare(a, minimal, nVars) <= 0)
154 Kit_TruthCopy_64bit( minimal, a, nVars );
155 }
simpleMinimal(word * x,word * pAux,word * minimal,permInfo * pi,int nVars)156 void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars)
157 {
158 int i,j=0;
159 Kit_TruthCopy_64bit( pAux, x, nVars );
160 Kit_TruthNot_64bit( x, nVars );
161
162 minWord(x, pAux, minimal, nVars);
163
164 for(i=pi->totalSwaps-1;i>=0;i--)
165 {
166 Kit_TruthSwapAdjacentVars_64bit(x, nVars, pi->swapArray[i]);
167 Kit_TruthSwapAdjacentVars_64bit(pAux, nVars, pi->swapArray[i]);
168 minWord3(x, pAux, minimal, nVars);
169 }
170 for(j=pi->totalFlips-1;j>=0;j--)
171 {
172 Kit_TruthSwapAdjacentVars_64bit(x, nVars, 0);
173 Kit_TruthSwapAdjacentVars_64bit(pAux, nVars, 0);
174 Kit_TruthChangePhase_64bit(x, nVars, pi->flipArray[j]);
175 Kit_TruthChangePhase_64bit(pAux, nVars, pi->flipArray[j]);
176 minWord3(x, pAux, minimal, nVars);
177 for(i=pi->totalSwaps-1;i>=0;i--)
178 {
179 Kit_TruthSwapAdjacentVars_64bit(x, nVars, pi->swapArray[i]);
180 Kit_TruthSwapAdjacentVars_64bit(pAux, nVars, pi->swapArray[i]);
181 minWord3(x, pAux, minimal, nVars);
182 }
183 }
184 Kit_TruthCopy_64bit( x, minimal, nVars );
185 }
186
187 /**
188 * pGroups: we assume that the variables are merged into adjacent groups,
189 * the size of each group is stored in pGroups
190 * nGroups: the number of groups
191 *
192 * pis: we compute all permInfos from 0 to nVars (incl.)
193 */
simpleMinimalGroups(word * x,word * pAux,word * minimal,int * pGroups,int nGroups,permInfo ** pis,int nVars,int fFlipOutput,int fFlipInput)194 void simpleMinimalGroups(word* x, word* pAux, word* minimal, int* pGroups, int nGroups, permInfo** pis, int nVars, int fFlipOutput, int fFlipInput)
195 {
196 /* variables */
197 int i, j, o, nn;
198 permInfo* pi;
199 int * a, * c, * m;
200
201 /* reorder groups and calculate group offsets */
202 int * offset = ABC_ALLOC( int, nGroups );
203 o = 0;
204 j = 0;
205
206 for ( i = 0; i < nGroups; ++i )
207 {
208 offset[j] = o;
209 o += pGroups[j];
210 ++j;
211 }
212
213 if ( fFlipOutput )
214 {
215 /* keep regular and inverted version of x */
216 Kit_TruthCopy_64bit( pAux, x, nVars );
217 Kit_TruthNot_64bit( x, nVars );
218
219 minWord(x, pAux, minimal, nVars);
220 }
221 else
222 {
223 Kit_TruthCopy_64bit( minimal, x, nVars );
224 }
225
226 /* iterate through all combinations of pGroups using mixed radix enumeration */
227 nn = ( nGroups << 1 ) + 1;
228 a = ABC_ALLOC( int, nn );
229 c = ABC_ALLOC( int, nn );
230 m = ABC_ALLOC( int, nn );
231
232 /* fill a and m arrays */
233 m[0] = 2;
234 for ( i = 1; i <= nGroups; ++i ) { m[i] = pis[pGroups[i - 1]]->totalFlips + 1; }
235 for ( i = 1; i <= nGroups; ++i ) { m[nGroups + i] = pis[pGroups[i - 1]]->totalSwaps + 1; }
236 for ( i = 0; i < nn; ++i ) { a[i] = c[i] = 0; }
237
238 while ( 1 )
239 {
240 /* consider all flips */
241 for ( i = 1; i <= nGroups; ++i )
242 {
243 if ( !c[i] ) { continue; }
244 if ( !fFlipInput && pGroups[i - 1] == 1 ) { continue; }
245
246 pi = pis[pGroups[i - 1]];
247 j = a[i] == 0 ? 0 : pi->totalFlips - a[i];
248
249 Kit_TruthChangePhase_64bit(x, nVars, offset[i - 1] + pi->flipArray[j]);
250 if ( fFlipOutput )
251 {
252 Kit_TruthChangePhase_64bit(pAux, nVars, offset[i - 1] + pi->flipArray[j]);
253 minWord3(x, pAux, minimal, nVars);
254 }
255 else
256 {
257 minWord1(x, minimal, nVars);
258 }
259 }
260
261 /* consider all swaps */
262 for ( i = 1; i <= nGroups; ++i )
263 {
264 if ( !c[nGroups + i] ) { continue; }
265 if ( pGroups[i - 1] == 1 ) { continue; }
266
267 pi = pis[pGroups[i - 1]];
268 if ( a[nGroups + i] == pi->totalSwaps )
269 {
270 j = 0;
271 }
272 else
273 {
274 j = pi->swapArray[pi->totalSwaps - a[nGroups + i] - 1];
275 }
276 Kit_TruthSwapAdjacentVars_64bit(x, nVars, offset[i - 1] + j);
277 if ( fFlipOutput )
278 {
279 Kit_TruthSwapAdjacentVars_64bit(pAux, nVars, offset[i - 1] + j);
280 minWord3(x, pAux, minimal, nVars);
281 }
282 else
283 {
284 minWord1(x, minimal, nVars);
285 }
286 }
287
288 /* update a's */
289 memset(c, 0, sizeof(int) * nn);
290 j = nn - 1;
291 while ( a[j] == m[j] - 1 ) { c[j] = 1; a[j--] = 0; }
292
293 /* done? */
294 if ( j == 0 ) { break; }
295
296 c[j] = 1;
297 a[j]++;
298 }
299 ABC_FREE( offset );
300 ABC_FREE( a );
301 ABC_FREE( c );
302 ABC_FREE( m );
303
304 Kit_TruthCopy_64bit( x, minimal, nVars );
305 }
306
307 ABC_NAMESPACE_IMPL_END
308