ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
luckySimple.c
Go to the documentation of this file.
1
16
17#include "luckyInt.h"
18
20
21static 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
40static void freeSwapInfoPtr(swapInfo* x)
41{
42 free(x->posArray);
43 free(x->realArray);
44 free(x);
45}
46
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 {
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
73{
74 int counter=pi->totalSwaps-1;
75 swapInfo* x= setSwapInfoPtr(pi->varN);
76 while(nextSwap(x)==1)
77 {
80 else
82 }
83
84 freeSwapInfoPtr(x);
85}
86int 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}
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}
106static inline int factorial(int n)
107{
108 return (n == 1 || n == 0) ? 1 : factorial(n - 1) * n;
109}
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);
123 return x;
124}
125
127{
128 free(x->flipArray);
129 free(x->swapArray);
130 free(x);
131}
132static 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}
139static 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}
151static 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}
156void 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 {
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 {
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 {
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
194void 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
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
void Kit_TruthChangePhase_64bit(word *pInOut, int nVars, int iVar)
Definition luckySwap.c:100
void Kit_TruthSwapAdjacentVars_64bit(word *pInOut, int nVars, int iVar)
Definition luckySwap.c:141
void Kit_TruthNot_64bit(word *pIn, int nVars)
Definition luckySwap.c:130
void Kit_TruthCopy_64bit(word *pOut, word *pIn, int nVars)
Definition luckySwap.c:136
void freePermInfoPtr(permInfo *x)
int oneBitPosition(int x, int size)
Definition luckySimple.c:86
void simpleMinimal(word *x, word *pAux, word *minimal, permInfo *pi, int nVars)
permInfo * setPermInfoPtr(int var)
void simpleMinimalGroups(word *x, word *pAux, word *minimal, int *pGroups, int nGroups, permInfo **pis, int nVars, int fFlipOutput, int fFlipInput)
void fillInFlipArray(permInfo *pi)
Definition luckySimple.c:94
void fillInSwapArray(permInfo *pi)
Definition luckySimple.c:72
int nextSwap(swapInfo *x)
Definition luckySimple.c:47
ABC_NAMESPACE_IMPL_START int memCompare(word *x, word *y, int nVars)
Definition lucky.c:22
Definition walk.c:35
int * swapArray
Definition lucky.h:26
int totalFlips
Definition lucky.h:31
int * flipArray
Definition lucky.h:29
int swapCtr
Definition lucky.h:27
int flipCtr
Definition lucky.h:30
int totalSwaps
Definition lucky.h:28
int varN
Definition lucky.h:25
int positionToSwap2
Definition luckyInt.h:86
int * realArray
Definition luckyInt.h:83
varInfo * posArray
Definition luckyInt.h:82
int positionToSwap1
Definition luckyInt.h:85
int varN
Definition luckyInt.h:84
int position
Definition luckyInt.h:76
int direction
Definition luckyInt.h:75
char * memset()
VOID_HACK free()
char * malloc()