diff options
Diffstat (limited to 'src/sat/fraig/fraigInt.h')
| -rw-r--r-- | src/sat/fraig/fraigInt.h | 451 |
1 files changed, 0 insertions, 451 deletions
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h deleted file mode 100644 index 9c6e0d47..00000000 --- a/src/sat/fraig/fraigInt.h +++ /dev/null @@ -1,451 +0,0 @@ -/**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 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)) - -// 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 - sint64 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 - 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 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 /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// 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]; -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 ); - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// |