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
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
|
/**CFile****************************************************************
FileName [fraig.h]
PackageName [FRAIG: Functionally reduced AND-INV graphs.]
Synopsis [External declarations of the FRAIG package.]
Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
Affiliation [UC Berkeley]
Date [Ver. 2.0. Started - October 1, 2004]
Revision [$Id: fraig.h,v 1.18 2005/07/08 01:01:30 alanmi Exp $]
***********************************************************************/
#ifndef __FRAIG_H__
#define __FRAIG_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Fraig_ManStruct_t_ Fraig_Man_t;
typedef struct Fraig_NodeStruct_t_ Fraig_Node_t;
typedef struct Fraig_NodeVecStruct_t_ Fraig_NodeVec_t;
typedef struct Fraig_HashTableStruct_t_ Fraig_HashTable_t;
typedef struct Fraig_ParamsStruct_t_ Fraig_Params_t;
typedef struct Fraig_PatternsStruct_t_ Fraig_Patterns_t;
struct Fraig_ParamsStruct_t_
{
int nPatsRand; // the number of words of random simulation info
int nPatsDyna; // the number of words of dynamic simulation info
int nBTLimit; // the max number of backtracks to perform
int nSeconds; // the timeout for the final proof
int fFuncRed; // performs only one level hashing
int fFeedBack; // enables solver feedback
int fDist1Pats; // enables distance-1 patterns
int fDoSparse; // performs equiv tests for sparse functions
int fChoicing; // enables recording structural choices
int fTryProve; // tries to solve the final miter
int fVerbose; // the verbosiness flag
int fVerboseP; // the verbosiness flag (for proof reporting)
int fInternal; // is set to 1 for internal fraig calls
};
////////////////////////////////////////////////////////////////////////
/// GLOBAL VARIABLES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
// macros working with complemented attributes of the nodes
#define Fraig_IsComplement(p) (((int)((long) (p) & 01)))
#define Fraig_Regular(p) ((Fraig_Node_t *)((unsigned)(p) & ~01))
#define Fraig_Not(p) ((Fraig_Node_t *)((long)(p) ^ 01))
#define Fraig_NotCond(p,c) ((Fraig_Node_t *)((long)(p) ^ (c)))
// these are currently not used
#define Fraig_Ref(p)
#define Fraig_Deref(p)
#define Fraig_RecursiveDeref(p,c)
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/*=== fraigApi.c =============================================================*/
extern Fraig_NodeVec_t * Fraig_ManReadVecInputs( Fraig_Man_t * p );
extern Fraig_NodeVec_t * Fraig_ManReadVecOutputs( Fraig_Man_t * p );
extern Fraig_NodeVec_t * Fraig_ManReadVecNodes( Fraig_Man_t * p );
extern Fraig_Node_t ** Fraig_ManReadInputs ( Fraig_Man_t * p );
extern Fraig_Node_t ** Fraig_ManReadOutputs( Fraig_Man_t * p );
extern Fraig_Node_t ** Fraig_ManReadNodes( Fraig_Man_t * p );
extern int Fraig_ManReadInputNum ( Fraig_Man_t * p );
extern int Fraig_ManReadOutputNum( Fraig_Man_t * p );
extern int Fraig_ManReadNodeNum( Fraig_Man_t * p );
extern Fraig_Node_t * Fraig_ManReadConst1 ( Fraig_Man_t * p );
extern Fraig_Node_t * Fraig_ManReadIthVar( Fraig_Man_t * p, int i );
extern Fraig_Node_t * Fraig_ManReadIthNode( Fraig_Man_t * p, int i );
extern char ** Fraig_ManReadInputNames( Fraig_Man_t * p );
extern char ** Fraig_ManReadOutputNames( Fraig_Man_t * p );
extern char * Fraig_ManReadVarsInt( Fraig_Man_t * p );
extern char * Fraig_ManReadSat( Fraig_Man_t * p );
extern int Fraig_ManReadFuncRed( Fraig_Man_t * p );
extern int Fraig_ManReadFeedBack( Fraig_Man_t * p );
extern int Fraig_ManReadDoSparse( Fraig_Man_t * p );
extern int Fraig_ManReadChoicing( Fraig_Man_t * p );
extern int Fraig_ManReadVerbose( Fraig_Man_t * p );
extern int * Fraig_ManReadModel( Fraig_Man_t * p );
extern int Fraig_ManReadPatternNumRandom( Fraig_Man_t * p );
extern int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p );
extern int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p );
extern void Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed );
extern void Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack );
extern void Fraig_ManSetDoSparse( Fraig_Man_t * p, int fDoSparse );
extern void Fraig_ManSetChoicing( Fraig_Man_t * p, int fChoicing );
extern void Fraig_ManSetTryProve( Fraig_Man_t * p, int fTryProve );
extern void Fraig_ManSetVerbose( Fraig_Man_t * p, int fVerbose );
extern void Fraig_ManSetTimeToGraph( Fraig_Man_t * p, int Time );
extern void Fraig_ManSetTimeToNet( Fraig_Man_t * p, int Time );
extern void Fraig_ManSetTimeTotal( Fraig_Man_t * p, int Time );
extern void Fraig_ManSetOutputNames( Fraig_Man_t * p, char ** ppNames );
extern void Fraig_ManSetInputNames( Fraig_Man_t * p, char ** ppNames );
extern void Fraig_ManSetPo( Fraig_Man_t * p, Fraig_Node_t * pNode );
extern Fraig_Node_t * Fraig_NodeReadData0( Fraig_Node_t * p );
extern Fraig_Node_t * Fraig_NodeReadData1( Fraig_Node_t * p );
extern int Fraig_NodeReadNum( Fraig_Node_t * p );
extern Fraig_Node_t * Fraig_NodeReadOne( Fraig_Node_t * p );
extern Fraig_Node_t * Fraig_NodeReadTwo( Fraig_Node_t * p );
extern Fraig_Node_t * Fraig_NodeReadNextE( Fraig_Node_t * p );
extern Fraig_Node_t * Fraig_NodeReadRepr( Fraig_Node_t * p );
extern int Fraig_NodeReadNumRefs( Fraig_Node_t * p );
extern int Fraig_NodeReadNumFanouts( Fraig_Node_t * p );
extern int Fraig_NodeReadSimInv( Fraig_Node_t * p );
extern int Fraig_NodeReadNumOnes( Fraig_Node_t * p );
extern unsigned * Fraig_NodeReadPatternsRandom( Fraig_Node_t * p );
extern unsigned * Fraig_NodeReadPatternsDynamic( Fraig_Node_t * p );
extern void Fraig_NodeSetData0( Fraig_Node_t * p, Fraig_Node_t * pData );
extern void Fraig_NodeSetData1( Fraig_Node_t * p, Fraig_Node_t * pData );
extern int Fraig_NodeIsConst( Fraig_Node_t * p );
extern int Fraig_NodeIsVar( Fraig_Node_t * p );
extern int Fraig_NodeIsAnd( Fraig_Node_t * p );
extern int Fraig_NodeComparePhase( Fraig_Node_t * p1, Fraig_Node_t * p2 );
extern Fraig_Node_t * Fraig_NodeOr( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
extern Fraig_Node_t * Fraig_NodeAnd( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
extern Fraig_Node_t * Fraig_NodeOr( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
extern Fraig_Node_t * Fraig_NodeExor( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
extern Fraig_Node_t * Fraig_NodeMux( Fraig_Man_t * p, Fraig_Node_t * pNode, Fraig_Node_t * pNodeT, Fraig_Node_t * pNodeE );
extern void Fraig_NodeSetChoice( Fraig_Man_t * pMan, Fraig_Node_t * pNodeOld, Fraig_Node_t * pNodeNew );
/*=== fraigMan.c =============================================================*/
extern void Fraig_ParamsSetDefault( Fraig_Params_t * pParams );
extern void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams );
extern Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams );
extern void Fraig_ManFree( Fraig_Man_t * pMan );
extern void Fraig_ManPrintStats( Fraig_Man_t * p );
extern Fraig_NodeVec_t * Fraig_ManGetSimInfo( Fraig_Man_t * p );
extern int Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 );
extern void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes );
/*=== fraigDfs.c =============================================================*/
extern Fraig_NodeVec_t * Fraig_Dfs( Fraig_Man_t * pMan, int fEquiv );
extern Fraig_NodeVec_t * Fraig_DfsOne( Fraig_Man_t * pMan, Fraig_Node_t * pNode, int fEquiv );
extern Fraig_NodeVec_t * Fraig_DfsNodes( Fraig_Man_t * pMan, Fraig_Node_t ** ppNodes, int nNodes, int fEquiv );
extern Fraig_NodeVec_t * Fraig_DfsReverse( Fraig_Man_t * pMan );
extern int Fraig_CountNodes( Fraig_Man_t * pMan, int fEquiv );
extern int Fraig_CheckTfi( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
extern int Fraig_CountLevels( Fraig_Man_t * pMan );
/*=== fraigSat.c =============================================================*/
extern int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit );
extern int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit );
extern void Fraig_ManProveMiter( Fraig_Man_t * p );
extern int Fraig_ManCheckMiter( Fraig_Man_t * p );
extern int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit );
/*=== fraigVec.c ===============================================================*/
extern Fraig_NodeVec_t * Fraig_NodeVecAlloc( int nCap );
extern void Fraig_NodeVecFree( Fraig_NodeVec_t * p );
extern Fraig_NodeVec_t * Fraig_NodeVecDup( Fraig_NodeVec_t * p );
extern Fraig_Node_t ** Fraig_NodeVecReadArray( Fraig_NodeVec_t * p );
extern int Fraig_NodeVecReadSize( Fraig_NodeVec_t * p );
extern void Fraig_NodeVecGrow( Fraig_NodeVec_t * p, int nCapMin );
extern void Fraig_NodeVecShrink( Fraig_NodeVec_t * p, int nSizeNew );
extern void Fraig_NodeVecClear( Fraig_NodeVec_t * p );
extern void Fraig_NodeVecPush( Fraig_NodeVec_t * p, Fraig_Node_t * Entry );
extern int Fraig_NodeVecPushUnique( Fraig_NodeVec_t * p, Fraig_Node_t * Entry );
extern void Fraig_NodeVecPushOrder( Fraig_NodeVec_t * p, Fraig_Node_t * pNode );
extern int Fraig_NodeVecPushUniqueOrder( Fraig_NodeVec_t * p, Fraig_Node_t * pNode );
extern void Fraig_NodeVecPushOrderByLevel( Fraig_NodeVec_t * p, Fraig_Node_t * pNode );
extern int Fraig_NodeVecPushUniqueOrderByLevel( Fraig_NodeVec_t * p, Fraig_Node_t * pNode );
extern Fraig_Node_t * Fraig_NodeVecPop( Fraig_NodeVec_t * p );
extern void Fraig_NodeVecRemove( Fraig_NodeVec_t * p, Fraig_Node_t * Entry );
extern void Fraig_NodeVecWriteEntry( Fraig_NodeVec_t * p, int i, Fraig_Node_t * Entry );
extern Fraig_Node_t * Fraig_NodeVecReadEntry( Fraig_NodeVec_t * p, int i );
extern void Fraig_NodeVecSortByLevel( Fraig_NodeVec_t * p, int fIncreasing );
extern void Fraig_NodeVecSortByNumber( Fraig_NodeVec_t * p );
/*=== fraigUtil.c ===============================================================*/
extern void Fraig_ManMarkRealFanouts( Fraig_Man_t * p );
extern int Fraig_ManCheckConsistency( Fraig_Man_t * p );
extern int Fraig_GetMaxLevel( Fraig_Man_t * pMan );
extern void Fraig_ManReportChoices( Fraig_Man_t * pMan );
extern void Fraig_MappingSetChoiceLevels( Fraig_Man_t * pMan, int fMaximum );
extern Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
#endif
|
