1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
/**CFile****************************************************************
FileName [luckyInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Semi-canonical form computation package.]
Synopsis [Internal declarations.]
Author [Jake]
Date [Started - August 2012]
***********************************************************************/
#ifndef ABC__bool__lucky__LUCKY_INT_H_
#define ABC__bool__lucky__LUCKY_INT_H_
#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#include <string.h>
#include <math.h>
#include <time.h>
// comment out this line to run Lucky Code outside of ABC
#define _RUNNING_ABC_
#ifdef _RUNNING_ABC_
#include "misc/util/abc_global.h"
#include "lucky.h"
#else
#define ABC_NAMESPACE_HEADER_START
#define ABC_NAMESPACE_HEADER_END
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedef unsigned __int64 word;
#define bool int
#define false 0
#define true 1
#define inline __inline // compatible with MS VS 6.0
#define ABC_ALLOC(type, num) ((type *) malloc(sizeof(type) * (num)))
// #define LUCKY_VERIFY
typedef struct
{
int varN;
int* swapArray;
int swapCtr;
int totalSwaps;
int* flipArray;
int flipCtr;
int totalFlips;
}permInfo;
#endif
ABC_NAMESPACE_HEADER_START
typedef struct
{
int nVars;
int nWords;
int nFuncs;
word ** pFuncs;
}Abc_TtStore_t;
typedef struct
{
int direction;
int position;
} varInfo;
typedef struct
{
varInfo* posArray;
int* realArray;
int varN;
int positionToSwap1;
int positionToSwap2;
} swapInfo;
static inline void TimePrint( char* Message )
{
static int timeBegin;
double time = 1.0*(clock() - timeBegin)/CLOCKS_PER_SEC ;
if ( Message != NULL)
printf("%s = %f sec.\n", Message, time);
timeBegin = clock();
}
static inline int CompareWords( word x, word y)
{
if( x > y )
return 1;
if( x < y )
return -1;
return 0;
}
static inline int luckyMin( int x, int y ) { return (x < y) ? x : y; }
static inline int luckyMax( int x, int y ) { return (x < y) ? y : x; }
extern inline int memCompare(word* x, word* y, int nVars);
extern inline int Kit_TruthWordNum_64bit( int nVars );
extern Abc_TtStore_t * setTtStore(char * pFileInput);
extern inline void Abc_TruthStoreFree( Abc_TtStore_t * p );
extern inline void Kit_TruthChangePhase_64bit( word * pInOut, int nVars, int iVar );
extern inline void Kit_TruthNot_64bit(word * pIn, int nVars );
extern inline void Kit_TruthCopy_64bit( word * pOut, word * pIn, int nVars );
extern inline void Kit_TruthSwapAdjacentVars_64bit( word * pInOut, int nVars, int iVar );
extern inline int Kit_TruthCountOnes_64bit( word* pIn, int nVars );
extern void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars);
extern permInfo* setPermInfoPtr(int var);
extern void freePermInfoPtr(permInfo* x);
extern inline void Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, int * pStore );
extern inline unsigned Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char * pCanonPerm);
extern inline unsigned Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore);
extern inline word luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase);
extern inline word luckyCanonicizer_final_fast_6Vars1(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase);
extern inline unsigned adjustInfoAfterSwap(char* pCanonPerm, unsigned uCanonPhase, int iVar, unsigned info);
extern void resetPCanonPermArray_6Vars(char* x);
extern void swap_ij( word* f,int totalVars, int varI, int varJ);
ABC_NAMESPACE_HEADER_END
#endif /* LUCKY_H_ */
|
