ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
lucky.h File Reference
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  permInfo
 

Functions

unsigned Kit_TruthSemiCanonicize_new (unsigned *pInOut, unsigned *pAux, int nVars, char *pCanonPerm)
 
unsigned luckyCanonicizer_final_fast (word *pInOut, int nVars, char *pCanonPerm)
 
unsigned luckyCanonicizer_final_fast1 (word *pInOut, int nVars, char *pCanonPerm)
 
void resetPCanonPermArray (char *x, int nVars)
 
permInfosetPermInfoPtr (int var)
 
void freePermInfoPtr (permInfo *x)
 
void simpleMinimal (word *x, word *pAux, word *minimal, permInfo *pi, int nVars)
 

Function Documentation

◆ freePermInfoPtr()

void freePermInfoPtr ( permInfo * x)
extern

Definition at line 126 of file luckySimple.c.

127{
128 free(x->flipArray);
129 free(x->swapArray);
130 free(x);
131}
int * swapArray
Definition lucky.h:26
int * flipArray
Definition lucky.h:29
VOID_HACK free()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Kit_TruthSemiCanonicize_new()

unsigned Kit_TruthSemiCanonicize_new ( unsigned * pInOut,
unsigned * pAux,
int nVars,
char * pCanonPerm )
extern

Definition at line 611 of file lucky.c.

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}
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
unsigned Kit_TruthSemiCanonicize_new_internal(word *pInOut, int nVars, char *pCanonPerm)
Definition lucky.c:599
Here is the call graph for this function:

◆ luckyCanonicizer_final_fast()

unsigned luckyCanonicizer_final_fast ( word * pInOut,
int nVars,
char * pCanonPerm )
extern

Definition at line 818 of file luckyFast16.c.

819{
820 int nWords;
821 int pStore[16];
822 unsigned uCanonPhase = 0;
823#ifdef LUCKY_VERIFY
824 word temp[1024] = {0};
825 word duplicate[1024] = {0};
826 Kit_TruthCopy_64bit( duplicate, pInOut, nVars );
827#endif
828 if ( nVars <= 6 )
829 pInOut[0] = luckyCanonicizer_final_fast_6Vars( pInOut[0], pStore, pCanonPerm, &uCanonPhase);
830 else if ( nVars <= 16 )
831 {
832 nWords = (nVars <= 6) ? 1 : (1 << (nVars - 6));
833 luckyCanonicizer_final_fast_16Vars( pInOut, nVars, nWords, pStore, pCanonPerm, &uCanonPhase );
834 }
835 else assert( 0 );
836#ifdef LUCKY_VERIFY
837 Kit_TruthCopy_64bit( temp, pInOut, nVars );
838 assert( ! luckyCheck(temp, duplicate, nVars, pCanonPerm, uCanonPhase) );
839#endif
840 return uCanonPhase;
841}
int nWords
Definition abcNpn.c:127
int luckyCheck(word *pAfter, word *pBefore, int nVars, char *pCanonPerm, unsigned uCanonPhase)
Definition luckyFast16.c:49
void luckyCanonicizer_final_fast_16Vars(word *pInOut, int nVars, int nWords, int *pStore, char *pCanonPerm, unsigned *pCanonPhase)
word luckyCanonicizer_final_fast_6Vars(word InOut, int *pStore, char *pCanonPerm, unsigned *pCanonPhase)
Definition luckyFast6.c:265
void Kit_TruthCopy_64bit(word *pOut, word *pIn, int nVars)
Definition luckySwap.c:136
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ luckyCanonicizer_final_fast1()

unsigned luckyCanonicizer_final_fast1 ( word * pInOut,
int nVars,
char * pCanonPerm )
extern

Definition at line 843 of file luckyFast16.c.

844{
845 int nWords;
846 int pStore[16];
847 unsigned uCanonPhase = 0;
848#ifdef LUCKY_VERIFY
849 word temp[1024] = {0};
850 word duplicate[1024] = {0};
851 Kit_TruthCopy_64bit( duplicate, pInOut, nVars );
852#endif
853 if ( nVars <= 6 )
854 pInOut[0] = luckyCanonicizer_final_fast_6Vars1( pInOut[0], pStore, pCanonPerm, &uCanonPhase);
855 else if ( nVars <= 16 )
856 {
857 nWords = 1 << (nVars - 6);
858 luckyCanonicizer_final_fast_16Vars1( pInOut, nVars, nWords, pStore, pCanonPerm, &uCanonPhase );
859 }
860 else assert( 0 );
861#ifdef LUCKY_VERIFY
862 Kit_TruthCopy_64bit( temp, pInOut, nVars );
863 assert( ! luckyCheck(temp, duplicate, nVars, pCanonPerm, uCanonPhase) );
864#endif
865 return uCanonPhase;
866}
void luckyCanonicizer_final_fast_16Vars1(word *pInOut, int nVars, int nWords, int *pStore, char *pCanonPerm, unsigned *pCanonPhase)
word luckyCanonicizer_final_fast_6Vars1(word InOut, int *pStore, char *pCanonPerm, unsigned *pCanonPhase)
Definition luckyFast6.c:270
Here is the call graph for this function:
Here is the caller graph for this function:

◆ resetPCanonPermArray()

void resetPCanonPermArray ( char * x,
int nVars )
extern

Definition at line 30 of file luckyFast6.c.

31{
32 int i;
33 for(i=0;i<nVars;i++)
34 x[i] = 'a'+i;
35}
Here is the caller graph for this function:

◆ setPermInfoPtr()

permInfo * setPermInfoPtr ( int var)
extern

Definition at line 110 of file luckySimple.c.

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}
void fillInFlipArray(permInfo *pi)
Definition luckySimple.c:94
void fillInSwapArray(permInfo *pi)
Definition luckySimple.c:72
unsigned short var
Definition giaNewBdd.h:35
int totalFlips
Definition lucky.h:31
int swapCtr
Definition lucky.h:27
int flipCtr
Definition lucky.h:30
int totalSwaps
Definition lucky.h:28
int varN
Definition lucky.h:25
char * malloc()
Here is the call graph for this function:
Here is the caller graph for this function:

◆ simpleMinimal()

void simpleMinimal ( word * x,
word * pAux,
word * minimal,
permInfo * pi,
int nVars )
extern

Definition at line 156 of file luckySimple.c.

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}
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
Here is the call graph for this function:
Here is the caller graph for this function: