summaryrefslogtreecommitdiffstats
path: root/src/bool/lucky/luckyInt.h
blob: 58a7235cdf1d885d36d5e9361f0db501559cfc6c (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
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  int             memCompare(word* x, word*  y, int nVars);
extern  int             Kit_TruthWordNum_64bit( int nVars );
extern  Abc_TtStore_t * setTtStore(char * pFileInput);
extern  void            Abc_TruthStoreFree( Abc_TtStore_t * p );
extern  void            Kit_TruthChangePhase_64bit( word * pInOut, int nVars, int iVar );
extern  void            Kit_TruthNot_64bit(word * pIn, int nVars );
extern  void            Kit_TruthCopy_64bit( word * pOut, word * pIn, int nVars );
extern  void            Kit_TruthSwapAdjacentVars_64bit( word * pInOut, int nVars, int iVar );
extern  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  void            Kit_TruthSemiCanonicize_Yasha_simple( word* pInOut, int nVars, int * pStore );
extern  unsigned        Kit_TruthSemiCanonicize_Yasha( word* pInOut, int nVars, char * pCanonPerm);
extern  unsigned        Kit_TruthSemiCanonicize_Yasha1( word* pInOut, int nVars, char * pCanonPerm, int * pStore);
extern  word            luckyCanonicizer_final_fast_6Vars(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase);
extern  word            luckyCanonicizer_final_fast_6Vars1(word InOut, int* pStore, char* pCanonPerm, unsigned* pCanonPhase);
extern  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_ */