mirror of https://github.com/YosysHQ/abc.git
437 lines
25 KiB
C
437 lines
25 KiB
C
/**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 ABC__sat__fraig__fraigInt_h
|
|
#define ABC__sat__fraig__fraigInt_h
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// INCLUDES ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
#include <stdio.h>
|
|
#include <stdlib.h>
|
|
#include <string.h>
|
|
#include <assert.h>
|
|
|
|
#include "misc/util/abc_global.h"
|
|
#include "fraig.h"
|
|
#include "sat/msat/msat.h"
|
|
|
|
ABC_NAMESPACE_HEADER_START
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// 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 DEFINITIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
// 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)>>5) + (((n)&31) > 0))
|
|
|
|
// generating random unsigned (#define RAND_MAX 0x7fff)
|
|
//#define FRAIG_RANDOM_UNSIGNED ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
|
|
#define FRAIG_RANDOM_UNSIGNED Aig_ManRandom(0)
|
|
|
|
// 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 "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) (((ABC_PTRUINT_T)(a) + (ABC_PTRUINT_T)(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)
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// 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
|
|
ABC_INT64_T nInspLimit; // the inspection limit
|
|
|
|
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 due to resource limit or prediction
|
|
int nSatFailsReal; // the number of times the SAT solver failed to complete due to resource limit
|
|
|
|
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
|
|
abctime timeToAig; // time to transfer to the mapping structure
|
|
abctime timeSims; // time to compute k-feasible cuts
|
|
abctime timeTrav; // time to traverse the network
|
|
abctime timeFeed; // time for solver feedback (recording and resimulating)
|
|
abctime timeImply; // time to analyze implications
|
|
abctime timeSat; // time to compute the truth table for each cut
|
|
abctime timeToNet; // time to transfer back to the network
|
|
abctime timeTotal; // the total mapping time
|
|
abctime time1; // time to perform one task
|
|
abctime time2; // time to perform another task
|
|
abctime time3; // time to perform another task
|
|
abctime 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 fFailTfo : 1; // the node is in the TFO of the failed SAT run
|
|
unsigned nFanouts : 2; // the indicator of fanouts (none, one, or many)
|
|
unsigned nOnes : 20; // 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 ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
// random number generator imported from another package
|
|
extern unsigned Aig_ManRandom( int fReset );
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// FUNCTION DEFINITIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
/*=== 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];
|
|
/*=== 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 );
|
|
|
|
|
|
|
|
ABC_NAMESPACE_HEADER_END
|
|
|
|
#endif
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|