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
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
|
/**CFile****************************************************************
FileName [fraigInt.h]
PackageName [FRAIG: Functionally reduced AND-INV graphs.]
Synopsis [Internal 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: fraigInt.h,v 1.15 2005/07/08 01:01:31 alanmi Exp $]
***********************************************************************/
#ifndef __FRAIG_INT_H__
#define __FRAIG_INT_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
//#include "leaks.h"
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>
#include "fraig.h"
#include "msat.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
/*
The AIG node policy:
- Each node has its main number (pNode->Num)
This is the number of this node in the array of all nodes and its SAT variable number
- The PI nodes are stored along with other nodes
Additionally, PI nodes have a PI number, by which they are stored in the PI node array
- The constant node is has number 0 and is also stored in the array
*/
////////////////////////////////////////////////////////////////////////
/// MACRO DEFITIONS ///
////////////////////////////////////////////////////////////////////////
// enable this macro to support the fanouts
#define FRAIG_ENABLE_FANOUTS
#define FRAIG_PATTERNS_RANDOM 2048 // should not be less than 128 and more than 32768 (2^15)
#define FRAIG_PATTERNS_DYNAMIC 2048 // should not be less than 256 and more than 32768 (2^15)
#define FRAIG_MAX_PRIMES 1024 // the maximum number of primes used for hashing
// this parameter determines when simulation info is extended
// it will be extended when the free storage in the dynamic simulation
// info is less or equal to this number of words (FRAIG_WORDS_STORE)
// this is done because if the free storage for dynamic simulation info
// is not sufficient, computation becomes inefficient
#define FRAIG_WORDS_STORE 5
// the bit masks
#define FRAIG_MASK(n) ((~((unsigned)0)) >> (32-(n)))
#define FRAIG_FULL (~((unsigned)0))
#define FRAIG_NUM_WORDS(n) ((n)/32 + (((n)%32) > 0))
// maximum/minimum operators
#define FRAIG_MIN(a,b) (((a) < (b))? (a) : (b))
#define FRAIG_MAX(a,b) (((a) > (b))? (a) : (b))
// generating random unsigned (#define RAND_MAX 0x7fff)
#define FRAIG_RANDOM_UNSIGNED ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
// macros to get hold of the bits in a bit string
#define Fraig_BitStringSetBit(p,i) ((p)[(i)>>5] |= (1<<((i) & 31)))
#define Fraig_BitStringXorBit(p,i) ((p)[(i)>>5] ^= (1<<((i) & 31)))
#define Fraig_BitStringHasBit(p,i) (((p)[(i)>>5] & (1<<((i) & 31))) > 0)
// macros to get hold of the bits in the support info
//#define Fraig_NodeSetVarStr(p,i) (Fraig_Regular(p)->pSuppStr[((i)%FRAIG_SUPP_SIGN)>>5] |= (1<<(((i)%FRAIG_SUPP_SIGN) & 31)))
//#define Fraig_NodeHasVarStr(p,i) ((Fraig_Regular(p)->pSuppStr[((i)%FRAIG_SUPP_SIGN)>>5] & (1<<(((i)%FRAIG_SUPP_SIGN) & 31))) > 0)
#define Fraig_NodeSetVarStr(p,i) Fraig_BitStringSetBit(Fraig_Regular(p)->pSuppStr,i)
#define Fraig_NodeHasVarStr(p,i) Fraig_BitStringHasBit(Fraig_Regular(p)->pSuppStr,i)
// copied from "util.h" for standaloneness
#ifndef ALLOC
# define ALLOC(type, num) \
((type *) malloc(sizeof(type) * (num)))
#endif
#ifndef REALLOC
# define REALLOC(type, obj, num) \
(obj) ? ((type *) realloc((char *) obj, sizeof(type) * (num))) : \
((type *) malloc(sizeof(type) * (num)))
#endif
#ifndef FREE
# define FREE(obj) \
((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
#endif
// copied from "extra.h" for stand-aloneness
#define Fraig_PrintTime(a,t) printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
#define Fraig_HashKey2(a,b,TSIZE) (((unsigned)(a) + (unsigned)(b) * 12582917) % TSIZE)
//#define Fraig_HashKey2(a,b,TSIZE) (( ((unsigned)(a)->Num * 19) ^ ((unsigned)(b)->Num * 1999) ) % TSIZE)
//#define Fraig_HashKey2(a,b,TSIZE) ( ((unsigned)((a)->Num + (b)->Num) * ((a)->Num + (b)->Num + 1) / 2) % TSIZE)
// the other two hash functions give bad distribution of hash chain lengths (not clear why)
#ifndef PRT
#define PRT(a,t) printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )
#endif
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Fraig_MemFixed_t_ Fraig_MemFixed_t;
// the mapping manager
struct Fraig_ManStruct_t_
{
// the AIG nodes
Fraig_NodeVec_t * vInputs; // the array of primary inputs
Fraig_NodeVec_t * vNodes; // the array of all nodes, including primary inputs
Fraig_NodeVec_t * vOutputs; // the array of primary outputs (some internal nodes)
Fraig_Node_t * pConst1; // the pointer to the constant node (vNodes->pArray[0])
// info about the original circuit
char ** ppInputNames; // the primary input names
char ** ppOutputNames; // the primary output names
// various hash-tables
Fraig_HashTable_t * pTableS; // hashing by structure
Fraig_HashTable_t * pTableF; // hashing by simulation info
Fraig_HashTable_t * pTableF0; // hashing by simulation info (sparse functions)
// parameters
int nWordsRand; // the number of words of random simulation info
int nWordsDyna; // the number of words of dynamic simulation info
int nBTLimit; // the max number of backtracks to perform
int nSeconds; // the runtime limit for the miter proof
int fFuncRed; // performs only one level hashing
int fFeedBack; // enables solver feedback
int fDist1Pats; // enables solver feedback
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
int nTravIds; // the traversal counter
int nTravIds2; // the traversal counter
// info related to the solver feedback
int iWordStart; // the first word to use for simulation
int iWordPerm; // the number of words stored permanently
int iPatsPerm; // the number of patterns stored permanently
Fraig_NodeVec_t * vCones; // the temporary array of internal variables
Msat_IntVec_t * vPatsReal; // the array of real pattern numbers
unsigned * pSimsReal; // used for simulation patterns
unsigned * pSimsDiff; // used for simulation patterns
unsigned * pSimsTemp; // used for simulation patterns
// the support information
int nSuppWords;
unsigned ** pSuppS;
unsigned ** pSuppF;
// the memory managers
Fraig_MemFixed_t * mmNodes; // the memory manager for nodes
Fraig_MemFixed_t * mmSims; // the memory manager for simulation info
// solving the SAT problem
Msat_Solver_t * pSat; // the SAT solver
Msat_IntVec_t * vProj; // the temporary array of projection vars
int nSatNums; // the counter of SAT variables
int * pModel; // the assignment, which satisfies the miter
// these arrays belong to the solver
Msat_IntVec_t * vVarsInt; // the temporary array of variables
Msat_ClauseVec_t * vAdjacents; // the temporary storage for connectivity
Msat_IntVec_t * vVarsUsed; // the array marking vars appearing in the cone
// various statistic variables
int nSatCalls; // the number of times equivalence checking was called
int nSatProof; // the number of times a proof was found
int nSatCounter; // the number of times a counter example was found
int nSatFails; // the number of times the SAT solver failed to complete
int nSatCallsImp; // the number of times equivalence checking was called
int nSatProofImp; // the number of times a proof was found
int nSatCounterImp;// the number of times a counter example was found
int nSatFailsImp; // the number of times the SAT solver failed to complete
int nSatZeros; // the number of times the simulation vector is zero
int nSatSupps; // the number of times the support info was useful
int nRefErrors; // the number of ref counting errors
int nImplies; // the number of implication cases
int nSatImpls; // the number of implication SAT calls
int nVarsClauses; // the number of variables with clauses
int nSimplifies0;
int nSimplifies1;
int nImplies0;
int nImplies1;
// runtime statistics
int timeToAig; // time to transfer to the mapping structure
int timeSims; // time to compute k-feasible cuts
int timeTrav; // time to traverse the network
int timeFeed; // time for solver feedback (recording and resimulating)
int timeImply; // time to analyze implications
int timeSat; // time to compute the truth table for each cut
int timeToNet; // time to transfer back to the network
int timeTotal; // the total mapping time
int time1; // time to perform one task
int time2; // time to perform another task
int time3; // time to perform another task
int time4; // time to perform another task
};
// the mapping node
struct Fraig_NodeStruct_t_
{
// various numbers associated with the node
int Num; // the unique number (SAT var number) of this node
int NumPi; // if the node is a PI, this is its variable number
int Level; // the level of the node
int nRefs; // the number of references of the node
int TravId; // the traversal ID (use to avoid cleaning marks)
int TravId2; // the traversal ID (use to avoid cleaning marks)
// general information about the node
unsigned fInv : 1; // the mark to show that simulation info is complemented
unsigned fNodePo : 1; // the mark used for primary outputs
unsigned fClauses : 1; // the clauses for this node are loaded
unsigned fMark0 : 1; // the mark used for traversals
unsigned fMark1 : 1; // the mark used for traversals
unsigned fMark2 : 1; // the mark used for traversals
unsigned fMark3 : 1; // the mark used for traversals
unsigned fFeedUse : 1; // the presence of the variable in the feedback
unsigned fFeedVal : 1; // the value of the variable in the feedback
unsigned nFanouts : 2; // the indicator of fanouts (none, one, or many)
unsigned nOnes : 21; // the number of 1's in the random sim info
// the children of the node
Fraig_Node_t * p1; // the first child
Fraig_Node_t * p2; // the second child
Fraig_NodeVec_t * vFanins; // the fanins of the supergate rooted at this node
// Fraig_NodeVec_t * vFanouts; // the fanouts of the supergate rooted at this node
// various linked lists
Fraig_Node_t * pNextS; // the next node in the structural hash table
Fraig_Node_t * pNextF; // the next node in the functional (simulation) hash table
Fraig_Node_t * pNextD; // the next node in the list of nodes based on dynamic simulation
Fraig_Node_t * pNextE; // the next structural choice (functionally-equivalent node)
Fraig_Node_t * pRepr; // the canonical functional representative of the node
// simulation data
unsigned uHashR; // the hash value for random information
unsigned uHashD; // the hash value for dynamic information
unsigned * puSimR; // the simulation information (random)
unsigned * puSimD; // the simulation information (dynamic)
// misc information
Fraig_Node_t * pData0; // temporary storage for the corresponding network node
Fraig_Node_t * pData1; // temporary storage for the corresponding network node
#ifdef FRAIG_ENABLE_FANOUTS
// representation of node's fanouts
Fraig_Node_t * pFanPivot; // the first fanout of this node
Fraig_Node_t * pFanFanin1; // the next fanout of p1
Fraig_Node_t * pFanFanin2; // the next fanout of p2
#endif
};
// the vector of nodes
struct Fraig_NodeVecStruct_t_
{
int nCap; // the number of allocated entries
int nSize; // the number of entries in the array
Fraig_Node_t ** pArray; // the array of nodes
};
// the hash table
struct Fraig_HashTableStruct_t_
{
Fraig_Node_t ** pBins; // the table bins
int nBins; // the size of the table
int nEntries; // the total number of entries in the table
};
// getting hold of the next fanout of the node
#define Fraig_NodeReadNextFanout( pNode, pFanout ) \
( ( pFanout == NULL )? NULL : \
((Fraig_Regular((pFanout)->p1) == (pNode))? \
(pFanout)->pFanFanin1 : (pFanout)->pFanFanin2) )
// getting hold of the place where the next fanout will be attached
#define Fraig_NodeReadNextFanoutPlace( pNode, pFanout ) \
( (Fraig_Regular((pFanout)->p1) == (pNode))? \
&(pFanout)->pFanFanin1 : &(pFanout)->pFanFanin2 )
// iterator through the fanouts of the node
#define Fraig_NodeForEachFanout( pNode, pFanout ) \
for ( pFanout = (pNode)->pFanPivot; pFanout; \
pFanout = Fraig_NodeReadNextFanout(pNode, pFanout) )
// safe iterator through the fanouts of the node
#define Fraig_NodeForEachFanoutSafe( pNode, pFanout, pFanout2 ) \
for ( pFanout = (pNode)->pFanPivot, \
pFanout2 = Fraig_NodeReadNextFanout(pNode, pFanout); \
pFanout; \
pFanout = pFanout2, \
pFanout2 = Fraig_NodeReadNextFanout(pNode, pFanout) )
// iterators through the entries in the linked lists of nodes
// the list of nodes in the structural hash table
#define Fraig_TableBinForEachEntryS( pBin, pEnt ) \
for ( pEnt = pBin; \
pEnt; \
pEnt = pEnt->pNextS )
#define Fraig_TableBinForEachEntrySafeS( pBin, pEnt, pEnt2 ) \
for ( pEnt = pBin, \
pEnt2 = pEnt? pEnt->pNextS: NULL; \
pEnt; \
pEnt = pEnt2, \
pEnt2 = pEnt? pEnt->pNextS: NULL )
// the list of nodes in the functional (simulation) hash table
#define Fraig_TableBinForEachEntryF( pBin, pEnt ) \
for ( pEnt = pBin; \
pEnt; \
pEnt = pEnt->pNextF )
#define Fraig_TableBinForEachEntrySafeF( pBin, pEnt, pEnt2 ) \
for ( pEnt = pBin, \
pEnt2 = pEnt? pEnt->pNextF: NULL; \
pEnt; \
pEnt = pEnt2, \
pEnt2 = pEnt? pEnt->pNextF: NULL )
// the list of nodes with the same simulation and different functionality
#define Fraig_TableBinForEachEntryD( pBin, pEnt ) \
for ( pEnt = pBin; \
pEnt; \
pEnt = pEnt->pNextD )
#define Fraig_TableBinForEachEntrySafeD( pBin, pEnt, pEnt2 ) \
for ( pEnt = pBin, \
pEnt2 = pEnt? pEnt->pNextD: NULL; \
pEnt; \
pEnt = pEnt2, \
pEnt2 = pEnt? pEnt->pNextD: NULL )
// the list of nodes with the same functionality
#define Fraig_TableBinForEachEntryE( pBin, pEnt ) \
for ( pEnt = pBin; \
pEnt; \
pEnt = pEnt->pNextE )
#define Fraig_TableBinForEachEntrySafeE( pBin, pEnt, pEnt2 ) \
for ( pEnt = pBin, \
pEnt2 = pEnt? pEnt->pNextE: NULL; \
pEnt; \
pEnt = pEnt2, \
pEnt2 = pEnt? pEnt->pNextE: NULL )
////////////////////////////////////////////////////////////////////////
/// GLOBAL VARIABLES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/*=== fraigCanon.c =============================================================*/
extern Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2 );
/*=== fraigFanout.c =============================================================*/
extern void Fraig_NodeAddFaninFanout( Fraig_Node_t * pFanin, Fraig_Node_t * pFanout );
extern void Fraig_NodeRemoveFaninFanout( Fraig_Node_t * pFanin, Fraig_Node_t * pFanoutToRemove );
extern int Fraig_NodeGetFanoutNum( Fraig_Node_t * pNode );
/*=== fraigFeed.c =============================================================*/
extern void Fraig_FeedBackInit( Fraig_Man_t * p );
extern void Fraig_FeedBack( Fraig_Man_t * p, int * pModel, Msat_IntVec_t * vVars, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
extern void Fraig_FeedBackTest( Fraig_Man_t * p );
extern int Fraig_FeedBackCompress( Fraig_Man_t * p );
extern int * Fraig_ManAllocCounterExample( Fraig_Man_t * p );
extern int * Fraig_ManSaveCounterExample( Fraig_Man_t * p, Fraig_Node_t * pNode );
/*=== fraigMan.c =============================================================*/
extern void Fraig_ManCreateSolver( Fraig_Man_t * p );
/*=== fraigMem.c =============================================================*/
extern Fraig_MemFixed_t * Fraig_MemFixedStart( int nEntrySize );
extern void Fraig_MemFixedStop( Fraig_MemFixed_t * p, int fVerbose );
extern char * Fraig_MemFixedEntryFetch( Fraig_MemFixed_t * p );
extern void Fraig_MemFixedEntryRecycle( Fraig_MemFixed_t * p, char * pEntry );
extern void Fraig_MemFixedRestart( Fraig_MemFixed_t * p );
extern int Fraig_MemFixedReadMemUsage( Fraig_MemFixed_t * p );
/*=== fraigNode.c =============================================================*/
extern Fraig_Node_t * Fraig_NodeCreateConst( Fraig_Man_t * p );
extern Fraig_Node_t * Fraig_NodeCreatePi( Fraig_Man_t * p );
extern Fraig_Node_t * Fraig_NodeCreate( Fraig_Man_t * p, Fraig_Node_t * p1, Fraig_Node_t * p2 );
extern void Fraig_NodeSimulate( Fraig_Node_t * pNode, int iWordStart, int iWordStop, int fUseRand );
/*=== fraigPrime.c =============================================================*/
extern int s_FraigPrimes[FRAIG_MAX_PRIMES];
extern unsigned int Cudd_PrimeFraig( unsigned int p );
/*=== fraigSat.c ===============================================================*/
extern int Fraig_NodeIsImplication( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit );
/*=== fraigTable.c =============================================================*/
extern Fraig_HashTable_t * Fraig_HashTableCreate( int nSize );
extern void Fraig_HashTableFree( Fraig_HashTable_t * p );
extern int Fraig_HashTableLookupS( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_Node_t * p2, Fraig_Node_t ** ppNodeRes );
extern Fraig_Node_t * Fraig_HashTableLookupF( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
extern Fraig_Node_t * Fraig_HashTableLookupF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
extern void Fraig_HashTableInsertF0( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
extern int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand );
extern int Fraig_CompareSimInfoUnderMask( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask );
extern int Fraig_FindFirstDiff( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int fCompl, int iWordLast, int fUseRand );
extern void Fraig_CollectXors( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWordLast, int fUseRand, unsigned * puMask );
extern void Fraig_TablePrintStatsS( Fraig_Man_t * pMan );
extern void Fraig_TablePrintStatsF( Fraig_Man_t * pMan );
extern void Fraig_TablePrintStatsF0( Fraig_Man_t * pMan );
extern int Fraig_TableRehashF0( Fraig_Man_t * pMan, int fLinkEquiv );
/*=== fraigUtil.c ===============================================================*/
extern int Fraig_NodeCountPis( Msat_IntVec_t * vVars, int nVarsPi );
extern int Fraig_NodeCountSuppVars( Fraig_Man_t * p, Fraig_Node_t * pNode, int fSuppStr );
extern int Fraig_NodesCompareSupps( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
extern int Fraig_NodeAndSimpleCase_rec( Fraig_Node_t * pOld, Fraig_Node_t * pNew );
extern int Fraig_NodeIsExorType( Fraig_Node_t * pNode );
extern void Fraig_ManSelectBestChoice( Fraig_Man_t * p );
extern int Fraig_BitStringCountOnes( unsigned * pString, int nWords );
extern void Fraig_PrintBinary( FILE * pFile, unsigned * pSign, int nBits );
extern int Fraig_NodeIsExorType( Fraig_Node_t * pNode );
extern int Fraig_NodeIsExor( Fraig_Node_t * pNode );
extern int Fraig_NodeIsMuxType( Fraig_Node_t * pNode );
extern Fraig_Node_t * Fraig_NodeRecognizeMux( Fraig_Node_t * pNode, Fraig_Node_t ** ppNodeT, Fraig_Node_t ** ppNodeE );
extern int Fraig_ManCountExors( Fraig_Man_t * pMan );
extern int Fraig_ManCountMuxes( Fraig_Man_t * pMan );
extern int Fraig_NodeSimsContained( Fraig_Man_t * pMan, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 );
extern int Fraig_NodeIsInSupergate( Fraig_Node_t * pOld, Fraig_Node_t * pNew );
extern Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fStopAtMux );
extern int Fraig_CountPis( Fraig_Man_t * p, Msat_IntVec_t * vVarNums );
extern void Fraig_ManIncrementTravId( Fraig_Man_t * pMan );
extern void Fraig_NodeSetTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
extern int Fraig_NodeIsTravIdCurrent( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
extern int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
/*=== fraigVec.c ===============================================================*/
extern void Fraig_NodeVecSortByRefCount( Fraig_NodeVec_t * p );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
#endif
|
