summaryrefslogtreecommitdiffstats
path: root/src/bool/lucky/luckyInt.h
blob: 2e476f8684bfe2f62abd7de3d65baa9a3c78c149 (plain)
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
/**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"
#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)))
#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;

typedef struct
{
    int varN;
    int* swapArray;
    int swapCtr;
    int totalSwaps;
    int* flipArray;
    int flipCtr;
    int totalFlips; 
}permInfo;


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 void luckyCanonicizer_final_fast_16Vars(word* pInOut, int  nVars, int nWords, int * pStore, char * pCanonPerm, unsigned* pCanonPhase);
extern  inline void resetPCanonPermArray_6Vars(char* x);
extern  void swap_ij( word* f,int totalVars, int varI, int varJ);
extern  inline unsigned adjustInfoAfterSwap(char* pCanonPerm, unsigned uCanonPhase, int iVar, unsigned info);
extern  inline void resetPCanonPermArray(char* x, int nVars);


ABC_NAMESPACE_HEADER_END

#endif /* LUCKY_H_ */