ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
lucky.c
Go to the documentation of this file.
1
16
17#include "luckyInt.h"
18
20
21
22int memCompare(word* x, word* y, int nVars)
23{
24 int i;
25 for(i=Kit_TruthWordNum_64bit( nVars )-1;i>=0;i--)
26 {
27 if(x[i]==y[i])
28 continue;
29 else if(x[i]>y[i])
30 return 1;
31 else
32 return -1;
33 }
34 return 0;
35}
36
37 int compareWords1 (const void * a, const void * b)
38 {
39 if( *(word*)a > *(word*)b )
40 return 1;
41 else
42 return( *(word*)a < *(word*)b ) ? -1: 0;
43
44 }
45
47 {
48 int i, count=1, WordsN = p->nFuncs;
49 word tempWord;
50 qsort(a,(size_t)WordsN,sizeof(word),compareWords1);
51 tempWord = a[0];
52 for(i=1;i<WordsN;i++)
53 if(tempWord != a[i])
54 {
55 a[count] = a[i];
56 tempWord = a[i];
57 count++;
58 }
59 p->nFuncs = count;
60}
61
62int compareWords2 (const void ** x, const void ** y)
63{
64
65 if(**(word**)x > **(word**)y)
66 return 1;
67 else if(**(word**)x < **(word**)y)
68 return -1;
69 else
70 return 0;
71
72}
73int compareWords (const void ** a, const void ** b)
74{
75 if( memcmp(*(word**)a,*(word**)b,sizeof(word)*1) > 0 )
76 return 1;
77 else
78 return ( memcmp(*(word**)a,*(word**)b,sizeof(word)*1) < 0 ) ? -1: 0;
79}
80int compareWords3 (const void ** x, const void ** y)
81{
82 return memCompare(*(word**)x, *(word**)y, 16);
83}
85{
86 int i, count=1, WordsPtrN = p->nFuncs;
87 word* tempWordPtr;
88 qsort(a,WordsPtrN,sizeof(word*),(int(*)(const void *,const void *))compareWords3);
89 tempWordPtr = a[0];
90 for(i=1;i<WordsPtrN;i++)
91 if(memcmp(a[i],tempWordPtr,sizeof(word)*(p->nWords)) != 0)
92 {
93 a[count] = a[i];
94 tempWordPtr = a[i];
95 count++;
96 }
97 p->nFuncs = count;
98}
99
100
101typedef struct
102{
106
107}cycleCtr;
109{
110 cycleCtr* x = (cycleCtr*) malloc(sizeof(cycleCtr));
111 x->totalCycles=0;
112 x->maxNCycles=0;
113 x->minNCycles=111111111;
114 return x;
115}
117{
118 free(x);
119}
121{
122 int i;
123 word** a;
124 a = (word**)malloc(sizeof(word*)*(p->nFuncs));
125 for(i=0;i<p->nFuncs;i++)
126 {
127 a[i] = (word*)malloc(sizeof(word)*(p->nWords));
128 memcpy(a[i],p->pFuncs[i],sizeof(word)*(p->nWords));
129
130 }
131 return a;
132}
134{
135 int i;
136 for(i=0;i<p->nFuncs;i++)
137 free(a[i]);
138 free(a);
139}
140
141word* makeArrayB(word** a, int nFuncs)
142{
143 int i;
144 word* b;
145 b = (word*)malloc(sizeof(word)*(nFuncs));
146 for(i=0;i<nFuncs;i++)
147 b[i] = a[i][0];
148
149 return b;
150}
152{
153 free(b);
154}
155
157
158// if highest bit in F ( all ones min term ) is one => inverse
159// if pInOnt changed(minimized) by function return 1 if not 0
160// int minimalInitialFlip_propper(word* pInOut, word* pDuplicat, int nVars)
161// {
162// word oneWord=1;
163// Kit_TruthCopy_64bit( pDuplicat, pInOut, nVars );
164// Kit_TruthNot_64bit( pDuplicat, nVars );
165// if( memCompare(pDuplicat,pInOut,nVars) == -1)
166// {
167// Kit_TruthCopy_64bit(pInOut, pDuplicat, nVars );
168// return 1;
169// }
170// return 0;
171// }
172// int minimalFlip(word* pInOut, word* pMinimal, word* PDuplicat, int nVars)
173// {
174// int i;
175// int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
176// memcpy(pMinimal, pInOut, blockSize);
177// memcpy(PDuplicat, pInOut, blockSize);
178// for(i=0;i<nVars;i++)
179// {
180// Kit_TruthChangePhase_64bit( pInOut, nVars, i );
181// if( memCompare(pMinimal,pInOut,nVars) == 1)
182// memcpy(pMinimal, pInOut, blockSize);
183// memcpy(pInOut,PDuplicat,blockSize);
184// }
185// memcpy(pInOut,pMinimal,blockSize);
186// if(memCompare(pMinimal,PDuplicat,nVars) == 0)
187// return 0;
188// else
189// return 1;
190// }
191// int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int nVars)
192// {
193// int i;
194// int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
195// memcpy(pMinimal, pInOut, blockSize);
196// memcpy(PDuplicat, pInOut, blockSize);
197// for(i=0;i<nVars-1;i++)
198// {
199// Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
200// if(memCompare(pMinimal,pInOut,nVars) == 1)
201// memcpy(pMinimal, pInOut, blockSize);
202// memcpy(pInOut,PDuplicat,blockSize);
203// }
204// memcpy(pInOut,pMinimal,blockSize);
205// if(memCompare(pMinimal,PDuplicat,nVars) == 0)
206// return 0;
207// else
208// return 1;
209// }
210//
211// void luckyCanonicizer(word* pInOut, word* pAux, word* pAux1, int nVars, cycleCtr* cCtr)
212// {
213// int counter=1, cycles=0;
214// assert( nVars <= 16 );
215// while(counter>0 ) // && cycles < 10 if we wanna limit cycles
216// {
217// counter=0;
218// counter += minimalInitialFlip(pInOut, nVars);
219// counter += minimalFlip(pInOut, pAux, pAux1, nVars);
220// counter += minimalSwap(pInOut, pAux, pAux1, nVars);
221// cCtr->totalCycles++;
222// cycles++;
223// }
224// if(cycles < cCtr->minNCycles)
225// cCtr->minNCycles = cycles;
226// else if(cycles > cCtr->maxNCycles)
227// cCtr->maxNCycles = cycles;
228// }
229// runs paralel F and ~F in luckyCanonicizer
230// void luckyCanonicizer2(word* pInOut, word* pAux, word* pAux1, word* temp, int nVars)
231// {
232// int nWords = Kit_TruthWordNum_64bit( nVars );
233// int counter=1, nOnes;
234// assert( nVars <= 16 );
235// nOnes = Kit_TruthCountOnes_64bit(pInOut, nVars);
236//
237// if ( (nOnes*2 == nWords * 32) )
238// {
239// Kit_TruthCopy_64bit( temp, pInOut, nVars );
240// Kit_TruthNot_64bit( temp, nVars );
241// luckyCanonicizer1_simple(pInOut, pAux, pAux1, nVars);
242// luckyCanonicizer1_simple(temp, pAux, pAux1, nVars);
243// if( memCompare(temp,pInOut,nVars) == -1)
244// Kit_TruthCopy_64bit(pInOut, temp, nVars );
245// return;
246// }
247// while(counter>0 ) // && cycles < 10 if we wanna limit cycles
248// {
249// counter=0;
250// counter += minimalInitialFlip_propper(pInOut, pAux, nVars);
251// counter += minimalFlip1(pInOut, pAux, pAux1, nVars);
252// counter += minimalSwap1(pInOut, pAux, pAux1, nVars);
253// }
254// }
255// same as luckyCanonicizer + cycleCtr stutistics
256// void luckyCanonicizer1(word* pInOut, word* pAux, word* pAux1, int nVars, cycleCtr* cCtr)
257// {
258// int counter=1, cycles=0;
259// assert( nVars <= 16 );
260// while(counter>0 ) // && cycles < 10 if we wanna limit cycles
261// {
262// counter=0;
263// counter += minimalInitialFlip1(pInOut, nVars);
264// counter += minimalFlip1(pInOut, pAux, pAux1, nVars);
265// counter += minimalSwap1(pInOut, pAux, pAux1, nVars);
266// cCtr->totalCycles++;
267// cycles++;
268// }
269// if(cycles < cCtr->minNCycles)
270// cCtr->minNCycles = cycles;
271// else if(cycles > cCtr->maxNCycles)
272// cCtr->maxNCycles = cycles;
273// }
274// luckyCanonicizer
275
276void printCCtrInfo(cycleCtr* cCtr, int nFuncs)
277{
278 printf("maxNCycles = %d\n",cCtr->maxNCycles);
279 printf("minNCycles = %d\n",cCtr->minNCycles);
280 printf("average NCycles = %.3f\n",cCtr->totalCycles/(double)nFuncs);
281}
282
283
284// if highest bit in F ( all ones min term ) is one => inverse
285// returns: if pInOnt changed(minimized) by function return 1 if not 0
286int minimalInitialFlip1(word* pInOut, int nVars)
287{
288 word oneWord=1;
289 if( (pInOut[Kit_TruthWordNum_64bit( nVars ) -1]>>63) & oneWord )
290 {
291 Kit_TruthNot_64bit( pInOut, nVars );
292 return 1;
293 }
294 return 0;
295}
296
297// compare F with F1 = (F with changed phase in one of the vars).
298// keeps smaller.
299// same for all vars in F.
300// returns: if pInOnt changed(minimized) by function return 1 if not 0
301int minimalFlip1(word* pInOut, word* pMinimal, word* PDuplicat, int nVars)
302{
303 int i;
304 int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
305 memcpy(pMinimal, pInOut, (size_t)blockSize);
306 memcpy(PDuplicat, pInOut, (size_t)blockSize);
307 Kit_TruthChangePhase_64bit( pInOut, nVars, 0 );
308 for(i=1;i<nVars;i++)
309 {
310 if( memCompare(pMinimal,pInOut,nVars) == 1)
311 {
312 memcpy(pMinimal, pInOut, (size_t)blockSize);
313 Kit_TruthChangePhase_64bit( pInOut, nVars, i );
314 }
315 else
316 {
317 memcpy(pInOut, pMinimal, (size_t)blockSize);
318 Kit_TruthChangePhase_64bit( pInOut, nVars, i );
319 }
320 }
321 if( memCompare(pMinimal,pInOut,nVars) == -1)
322 memcpy(pInOut, pMinimal, (size_t)blockSize);
323 if(memcmp(pInOut,PDuplicat,(size_t)blockSize) == 0)
324 return 0;
325 else
326 return 1;
327}
328// compare F with F1 = (F with swapped two adjacent vars).
329// keeps smaller.
330// same for all vars in F.
331// returns: if pInOnt changed(minimized) by function return 1 if not 0
332int minimalSwap1(word* pInOut, word* pMinimal, word* PDuplicat, int nVars)
333{
334 int i;
335 int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
336 memcpy(pMinimal, pInOut, (size_t)blockSize);
337 memcpy(PDuplicat, pInOut, (size_t)blockSize);
338 Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, 0 );
339 for(i=1;i<nVars-1;i++)
340 {
341 if( memCompare(pMinimal,pInOut,nVars) == 1)
342 {
343 memcpy(pMinimal, pInOut, (size_t)blockSize);
344 Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
345 }
346 else
347 {
348 memcpy(pInOut, pMinimal, (size_t)blockSize);
349 Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
350 }
351 }
352 if( memCompare(pMinimal,pInOut,nVars) == -1)
353 memcpy(pInOut, pMinimal, (size_t)blockSize);
354 if(memcmp(pInOut,PDuplicat,(size_t)blockSize) == 0)
355 return 0;
356 else
357 return 1;
358}
359
360// if highest bit in F ( all ones min term ) is one => inverse
361// returns: if pInOnt changed(minimized) by function return 1 if not 0
362int minimalInitialFlip(word* pInOut, int nVars, unsigned* p_uCanonPhase)
363{
364 word oneWord=1;
365 if( (pInOut[Kit_TruthWordNum_64bit( nVars ) -1]>>63) & oneWord )
366 {
367 Kit_TruthNot_64bit( pInOut, nVars );
368 *p_uCanonPhase ^= (1 << nVars);
369 return 1;
370 }
371 return 0;
372}
373
374// compare F with F1 = (F with changed phase in one of the vars).
375// keeps smaller.
376// same for all vars in F.
377// returns: if pInOnt changed(minimized) by function return 1 if not 0
378int minimalFlip(word* pInOut, word* pMinimal, word* PDuplicat, int nVars, unsigned* p_uCanonPhase)
379{
380 int i;
381 unsigned minTemp = *p_uCanonPhase;
382 int blockSize = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
383 memcpy(pMinimal, pInOut, (size_t)blockSize);
384 memcpy(PDuplicat, pInOut, (size_t)blockSize);
385 Kit_TruthChangePhase_64bit( pInOut, nVars, 0 );
386 *p_uCanonPhase ^= (unsigned)1;
387 for(i=1;i<nVars;i++)
388 {
389 if( memCompare(pMinimal,pInOut,nVars) == 1)
390 {
391 memcpy(pMinimal, pInOut, (size_t)blockSize);
392 minTemp = *p_uCanonPhase;
393 }
394 else
395 {
396 memcpy(pInOut, pMinimal, (size_t)blockSize);
397 *p_uCanonPhase = minTemp;
398 }
399 Kit_TruthChangePhase_64bit( pInOut, nVars, i );
400 *p_uCanonPhase ^= (1 << i);
401 }
402 if( memCompare(pMinimal,pInOut,nVars) == -1)
403 {
404 memcpy(pInOut, pMinimal, (size_t)blockSize);
405 *p_uCanonPhase = minTemp;
406 }
407 if(memcmp(pInOut,PDuplicat,(size_t)blockSize) == 0)
408 return 0;
409 else
410 return 1;
411}
412
413// swaps iVar and iVar+1 elements in pCanonPerm ant p_uCanonPhase
414void swapInfoAdjacentVars(int iVar, char * pCanonPerm, unsigned* p_uCanonPhase)
415{
416 char Temp = pCanonPerm[iVar];
417 pCanonPerm[iVar] = pCanonPerm[iVar+1];
418 pCanonPerm[iVar+1] = Temp;
419
420 // if the polarity of variables is different, swap them
421 if ( ((*p_uCanonPhase & (1 << iVar)) > 0) != ((*p_uCanonPhase & (1 << (iVar+1))) > 0) )
422 {
423 *p_uCanonPhase ^= (1 << iVar);
424 *p_uCanonPhase ^= (1 << (iVar+1));
425 }
426
427}
428
429
430// compare F with F1 = (F with swapped two adjacent vars).
431// keeps smaller.
432// same for all vars in F.
433// returns: if pInOnt changed(minimized) by function return 1 if not 0
434
435
436/*
437// this version is buggy and is fixed below
438int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int nVars, char * pCanonPerm, char * tempArray, unsigned* p_uCanonPhase)
439{
440 int i;
441 int blockSizeWord = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
442 int blockSizeChar = nVars *sizeof(char);
443 memcpy(pMinimal, pInOut, blockSizeWord);
444 memcpy(PDuplicat, pInOut, blockSizeWord);
445 memcpy(tempArray, pCanonPerm, blockSizeChar);
446 Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, 0 );
447 swapInfoAdjacentVars(0, pCanonPerm, p_uCanonPhase);
448 for(i=1;i<nVars-1;i++)
449 {
450 if( memCompare(pMinimal,pInOut,nVars) == 1)
451 {
452 memcpy(pMinimal, pInOut, blockSizeWord);
453 memcpy(tempArray, pCanonPerm, blockSizeChar);
454 }
455 else
456 {
457 memcpy(pInOut, pMinimal, blockSizeWord);
458 memcpy(pCanonPerm, tempArray, blockSizeChar);
459 }
460 Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
461 swapInfoAdjacentVars(i, pCanonPerm, p_uCanonPhase);
462 }
463 if( memCompare(pMinimal,pInOut,nVars) == -1)
464 {
465 memcpy(pInOut, pMinimal, blockSizeWord);
466 memcpy(pCanonPerm, tempArray, blockSizeChar);
467 }
468 if(memcmp(pInOut,PDuplicat,blockSizeWord) == 0)
469 return 0;
470 else
471 return 1;
472}
473*/
474
475int minimalSwap(word* pInOut, word* pMinimal, word* PDuplicat, int nVars, char * pCanonPerm, char * tempArray, unsigned* p_uCanonPhase)
476{
477 int i;
478 int blockSizeWord = Kit_TruthWordNum_64bit( nVars )*sizeof(word);
479 int blockSizeChar = nVars *sizeof(char);
480 unsigned TempuCanonPhase = *p_uCanonPhase;
481 memcpy(pMinimal, pInOut, (size_t)blockSizeWord);
482 memcpy(PDuplicat, pInOut, (size_t)blockSizeWord);
483 memcpy(tempArray, pCanonPerm, (size_t)blockSizeChar);
484 Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, 0 );
485 swapInfoAdjacentVars(0, pCanonPerm, p_uCanonPhase);
486 for(i=1;i<nVars-1;i++)
487 {
488 if( memCompare(pMinimal,pInOut,nVars) == 1)
489 {
490 memcpy(pMinimal, pInOut, (size_t)blockSizeWord);
491 memcpy(tempArray, pCanonPerm, (size_t)blockSizeChar);
492 TempuCanonPhase = *p_uCanonPhase;
493
494 }
495 else
496 {
497 memcpy(pInOut, pMinimal, (size_t)blockSizeWord);
498 memcpy(pCanonPerm, tempArray, (size_t)blockSizeChar);
499 *p_uCanonPhase = TempuCanonPhase;
500 }
501 Kit_TruthSwapAdjacentVars_64bit( pInOut, nVars, i );
502 swapInfoAdjacentVars(i, pCanonPerm, p_uCanonPhase);
503 }
504 if( memCompare(pMinimal,pInOut,nVars) == -1)
505 {
506 memcpy(pInOut, pMinimal, (size_t)blockSizeWord);
507 memcpy(pCanonPerm, tempArray, (size_t)blockSizeChar);
508 *p_uCanonPhase = TempuCanonPhase;
509 }
510 if(memcmp(pInOut,PDuplicat,(size_t)blockSizeWord) == 0)
511 return 0;
512 else
513 return 1;
514}
515
516
519/*
520void swapAndFlip(word* pAfter, int nVars, int iVarInPosition, int jVar, char * pCanonPerm, unsigned* pUCanonPhase)
521{
522 int Temp;
523 swap_ij(pAfter, nVars, iVarInPosition, jVar);
524
525 Temp = pCanonPerm[iVarInPosition];
526 pCanonPerm[iVarInPosition] = pCanonPerm[jVar];
527 pCanonPerm[jVar] = Temp;
528
529 if ( ((*pUCanonPhase & (1 << iVarInPosition)) > 0) != ((*pUCanonPhase & (1 << jVar)) > 0) )
530 {
531 *pUCanonPhase ^= (1 << iVarInPosition);
532 *pUCanonPhase ^= (1 << jVar);
533 }
534 if(*pUCanonPhase>>iVarInPosition & (unsigned)1 == 1)
535 Kit_TruthChangePhase_64bit( pAfter, nVars, iVarInPosition );
536
537}
538int luckyCheck(word* pAfter, word* pBefore, int nVars, char * pCanonPerm, unsigned uCanonPhase)
539{
540 int i,j;
541 char tempChar;
542 for(j=0;j<nVars;j++)
543 {
544 tempChar = 'a'+ j;
545 for(i=j;i<nVars;i++)
546 {
547 if(tempChar != pCanonPerm[i])
548 continue;
549 swapAndFlip(pAfter , nVars, j, i, pCanonPerm, &uCanonPhase);
550 break;
551 }
552 }
553 if(uCanonPhase>>nVars & (unsigned)1 == 1)
554 Kit_TruthNot_64bit(pAfter, nVars );
555 if(memcmp(pAfter, pBefore, Kit_TruthWordNum_64bit( nVars )*sizeof(word)) == 0)
556 return 0;
557 else
558 return 1;
559}
560*/
562
563
564void luckyCanonicizer(word* pInOut, word* pAux, word* pAux1, int nVars, char * pCanonPerm, char * tempArray, unsigned* p_uCanonPhase)
565{
566 int counter=1;
567 assert( nVars <= 16 );
568 while(counter>0 ) // && cycles < 10 if we wanna limit cycles
569 {
570 counter=0;
571 counter += minimalInitialFlip(pInOut, nVars, p_uCanonPhase);
572 counter += minimalFlip(pInOut, pAux, pAux1, nVars, p_uCanonPhase);
573 counter += minimalSwap(pInOut, pAux, pAux1, nVars, pCanonPerm, tempArray, p_uCanonPhase);
574 }
575}
576// tries to find minimal F till F at the beginning of the loop is the same as at the end - irreducible
577unsigned luckyCanonicizer1_simple(word* pInOut, word* pAux, word* pAux1, int nVars, char * pCanonPerm, unsigned CanonPhase)
578{
579 int counter=1;
580 assert( nVars <= 16 );
581 while(counter>0 ) // && cycles < 10 if we wanna limit cycles
582 {
583 counter=0;
584 counter += minimalInitialFlip1(pInOut, nVars);
585 counter += minimalFlip1(pInOut, pAux, pAux1, nVars);
586 counter += minimalSwap1(pInOut, pAux, pAux1, nVars);
587 }
588 return CanonPhase;
589}
590
591void luckyCanonicizer_final(word* pInOut, word* pAux, word* pAux1, int nVars)
592{
593 Kit_TruthSemiCanonicize_Yasha_simple( pInOut, nVars, NULL );
594 luckyCanonicizer1_simple(pInOut, pAux, pAux1, nVars, NULL, 0);
595}
596
597// this procedure calls internal canoniziers
598// it returns canonical phase (as return value) and canonical permutation (in pCanonPerm)
599unsigned Kit_TruthSemiCanonicize_new_internal( word * pInOut, int nVars, char * pCanonPerm )
600{
601 word pAux[1024], pAux1[1024];
602 char tempArray[16];
603 unsigned CanonPhase;
604 assert( nVars <= 16 );
605 CanonPhase = Kit_TruthSemiCanonicize_Yasha( pInOut, nVars, pCanonPerm );
606 luckyCanonicizer(pInOut, pAux, pAux1, nVars, pCanonPerm, tempArray, &CanonPhase);
607 return CanonPhase;
608}
609
610// this procedure is translates truth table from 'unsingeds' into 'words'
611unsigned Kit_TruthSemiCanonicize_new( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm )
612{
613 unsigned Result;
614 if ( nVars < 6 )
615 {
616 word Temp = ((word)pInOut[0] << 32) | (word)pInOut[0];
617 Result = Kit_TruthSemiCanonicize_new_internal( &Temp, nVars, pCanonPerm );
618 pInOut[0] = (unsigned)Temp;
619 }
620 else
621 Result = Kit_TruthSemiCanonicize_new_internal( (word *)pInOut, nVars, pCanonPerm );
622 return Result;
623}
624
625
626
627// compile main() procedure only if running outside of ABC environment
628#ifndef _RUNNING_ABC_
629
630int main ()
631{
632// char * pFileInput = "nonDSDfunc06var1M.txt";
633// char * pFileInput1 = "partDSDfunc06var1M.txt";
634// char * pFileInput2 = "fullDSDfunc06var1M.txt";
635
636// char * pFileInput = "nonDSDfunc10var100K.txt";
637// char * pFileInput1 = "partDSDfunc10var100K.txt";
638// char * pFileInput2 = "fullDSDfunc10var100K.txt";
639
640// char * pFileInput = "partDSDfunc12var100K.txt";
641// char * pFileInput = "nonDSDfunc12var100K.txt";
642// char * pFileInput1 = "partDSDfunc12var100K.txt";
643// char * pFileInput2 = "fullDSDfunc12var100K.txt";
644
645// char * pFileInput = "nonDSDfunc14var10K.txt";
646// char * pFileInput1 = "partDSDfunc14var10K.txt";
647// char * pFileInput2 = "fullDSDfunc14var10K.txt";
648
649 char * pFileInput = "nonDSDfunc16var10K.txt";
650 char * pFileInput1 = "partDSDfunc16var10K.txt";
651 char * pFileInput2 = "fullDSDfunc16var10K.txt";
652
653 int i, j, tempNF;
654 char** charArray;
655 word** a, ** b;
657 word * pAux, * pAux1;
658 int * pStore;
659// cycleCtr* cCtr;
660 charArray = (char**)malloc(sizeof(char*)*3);
661
662 charArray[0] = pFileInput;
663 charArray[1] = pFileInput1;
664 charArray[2] = pFileInput2;
665 for(j=0;j<3;j++)
666 {
667 p = setTtStore(charArray[j]);
668// p = setTtStore(pFileInput);
669 a = makeArray(p);
670 b = makeArray(p);
671// cCtr = setCycleCtrPtr();
672
673 pAux = (word*)malloc(sizeof(word)*(p->nWords));
674 pAux1 = (word*)malloc(sizeof(word)*(p->nWords));
675 pStore = (int*)malloc(sizeof(int)*(p->nVars));
676 printf("In %s Fs at start = %d\n",charArray[j],p->nFuncs);
677
678 tempNF = p->nFuncs;
679
680 TimePrint("start");
681 for(i=0;i<p->nFuncs;i++)
682 luckyCanonicizer_final(a[i], pAux, pAux1, p->nVars, pStore);
683 TimePrint("done with A");
684
685 sortAndUnique(a, p);
686 printf("F left in A final = %d\n",p->nFuncs);
687 freeArray(a,p);
688 TimePrint("Done with sort");
689
690
691// delete data-structures
692 free(pAux);
693 free(pAux1);
694 free(pStore);
695// freeCycleCtr(cCtr);
697 }
698 return 0;
699}
700
701#endif
702
703
704
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
ABC_NAMESPACE_IMPL_END int main(int argc, char *argv[])
GLOBAL VARIABLES ///.
Definition main.c:9
Cube * p
Definition exorList.c:222
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 Abc_TruthStoreFree(Abc_TtStore_t *p)
Definition luckyRead.c:115
int Kit_TruthWordNum_64bit(int nVars)
Definition luckySwap.c:36
void Kit_TruthSemiCanonicize_Yasha_simple(word *pInOut, int nVars, int *pStore)
Definition luckySwap.c:358
void Kit_TruthNot_64bit(word *pIn, int nVars)
Definition luckySwap.c:130
unsigned Kit_TruthSemiCanonicize_Yasha(word *pInOut, int nVars, char *pCanonPerm)
Definition luckySwap.c:186
Abc_TtStore_t * setTtStore(char *pFileInput)
Definition luckyRead.c:319
int compareWords2(const void **x, const void **y)
Definition lucky.c:62
void luckyCanonicizer(word *pInOut, word *pAux, word *pAux1, int nVars, char *pCanonPerm, char *tempArray, unsigned *p_uCanonPhase)
Definition lucky.c:564
unsigned Kit_TruthSemiCanonicize_new_internal(word *pInOut, int nVars, char *pCanonPerm)
Definition lucky.c:599
int minimalFlip(word *pInOut, word *pMinimal, word *PDuplicat, int nVars, unsigned *p_uCanonPhase)
Definition lucky.c:378
int minimalInitialFlip1(word *pInOut, int nVars)
Definition lucky.c:286
int minimalSwap(word *pInOut, word *pMinimal, word *PDuplicat, int nVars, char *pCanonPerm, char *tempArray, unsigned *p_uCanonPhase)
Definition lucky.c:475
unsigned luckyCanonicizer1_simple(word *pInOut, word *pAux, word *pAux1, int nVars, char *pCanonPerm, unsigned CanonPhase)
Definition lucky.c:577
ABC_NAMESPACE_IMPL_START int memCompare(word *x, word *y, int nVars)
Definition lucky.c:22
unsigned Kit_TruthSemiCanonicize_new(unsigned *pInOut, unsigned *pAux, int nVars, char *pCanonPerm)
Definition lucky.c:611
void sortAndUnique1(word *a, Abc_TtStore_t *p)
Definition lucky.c:46
int minimalInitialFlip(word *pInOut, int nVars, unsigned *p_uCanonPhase)
Definition lucky.c:362
word * makeArrayB(word **a, int nFuncs)
Definition lucky.c:141
int compareWords3(const void **x, const void **y)
Definition lucky.c:80
void luckyCanonicizer_final(word *pInOut, word *pAux, word *pAux1, int nVars)
Definition lucky.c:591
word ** makeArray(Abc_TtStore_t *p)
Definition lucky.c:120
int compareWords(const void **a, const void **b)
Definition lucky.c:73
int minimalSwap1(word *pInOut, word *pMinimal, word *PDuplicat, int nVars)
Definition lucky.c:332
void freeArrayB(word *b)
Definition lucky.c:151
int minimalFlip1(word *pInOut, word *pMinimal, word *PDuplicat, int nVars)
Definition lucky.c:301
cycleCtr * setCycleCtrPtr()
Definition lucky.c:108
void sortAndUnique(word **a, Abc_TtStore_t *p)
Definition lucky.c:84
int compareWords1(const void *a, const void *b)
Definition lucky.c:37
void swapInfoAdjacentVars(int iVar, char *pCanonPerm, unsigned *p_uCanonPhase)
Definition lucky.c:414
void freeCycleCtr(cycleCtr *x)
Definition lucky.c:116
void printCCtrInfo(cycleCtr *cCtr, int nFuncs)
Definition lucky.c:276
void freeArray(word **a, Abc_TtStore_t *p)
Definition lucky.c:133
Definition walk.c:35
int minNCycles
Definition lucky.c:105
int totalCycles
Definition lucky.c:103
int maxNCycles
Definition lucky.c:104
#define assert(ex)
Definition util_old.h:213
char * memcpy()
int memcmp()
VOID_HACK free()
char * malloc()