/**CFile**************************************************************** FileName [fraigMan.c] PackageName [FRAIG: Functionally reduced AND-INV graphs.] Synopsis [Implementation of the FRAIG manager.] Author [Alan Mishchenko ] Affiliation [UC Berkeley] Date [Ver. 2.0. Started - October 1, 2004] Revision [$Id: fraigMan.c,v 1.11 2005/07/08 01:01:31 alanmi Exp $] ***********************************************************************/ #include "fraigInt.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// int timeSelect; int timeAssign; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Sets the default parameters of the package.] Description [This set of parameters is tuned for equivalence checking.] SideEffects [] SeeAlso [] ***********************************************************************/ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams ) { memset( pParams, 0, sizeof(Fraig_Params_t) ); pParams->nPatsRand = FRAIG_PATTERNS_RANDOM; // the number of words of random simulation info pParams->nPatsDyna = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info pParams->nBTLimit = 99; // the max number of backtracks to perform pParams->fFuncRed = 1; // performs only one level hashing pParams->fFeedBack = 1; // enables solver feedback pParams->fDist1Pats = 1; // enables distance-1 patterns pParams->fDoSparse = 0; // performs equiv tests for sparse functions pParams->fChoicing = 0; // enables recording structural choices pParams->fTryProve = 1; // tries to solve the final miter pParams->fVerbose = 0; // the verbosiness flag pParams->fVerboseP = 0; } /**Function************************************************************* Synopsis [Creates the new FRAIG manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ) { Fraig_Params_t Params; Fraig_Man_t * p; // set the random seed for simulation srand( 0xFEEDDEAF ); // set parameters for equivalence checking if ( pParams == NULL ) Fraig_ParamsSetDefault( pParams = &Params ); // adjust the amount of simulation info if ( pParams->nPatsRand < 128 ) pParams->nPatsRand = 128; if ( pParams->nPatsRand > 32768 ) pParams->nPatsRand = 32768; if ( pParams->nPatsDyna < 128 ) pParams->nPatsDyna = 128; if ( pParams->nPatsDyna > 32768 ) pParams->nPatsDyna = 32768; // if reduction is not performed, allocate minimum simulation info if ( !pParams->fFuncRed ) pParams->nPatsRand = pParams->nPatsDyna = 128; // start the manager p = ALLOC( Fraig_Man_t, 1 ); memset( p, 0, sizeof(Fraig_Man_t) ); // set the default parameters p->nWordsRand = FRAIG_NUM_WORDS( pParams->nPatsRand ); // the number of words of random simulation info p->nWordsDyna = FRAIG_NUM_WORDS( pParams->nPatsDyna ); // the number of patterns for dynamic simulation info p->nBTLimit = pParams->nBTLimit; // -1 means infinite backtrack limit p->fFuncRed = pParams->fFuncRed; // enables functional reduction (otherwise, only one-level hashing is performed) p->fFeedBack = pParams->fFeedBack; // enables solver feedback (the use of counter-examples in simulation) p->fDist1Pats = pParams->fDist1Pats; // enables solver feedback (the use of counter-examples in simulation) p->fDoSparse = pParams->fDoSparse; // performs equivalence checking for sparse functions (whose sim-info is 0) p->fChoicing = pParams->fChoicing; // disable accumulation of structural choices (keeps only the first choice) p->fTryProve = pParams->fTryProve; // disable accumulation of structural choices (keeps only the first choice) p->fVerbose = pParams->fVerbose; // disable verbose output p->fVerboseP = pParams->fVerboseP; // disable verbose output // start memory managers p->mmNodes = Fraig_MemFixedStart( sizeof(Fraig_Node_t) ); p->mmSims = Fraig_MemFixedStart( sizeof(unsigned) * (p->nWordsRand + p->nWordsDyna) ); // allocate node arrays p->vInputs = Fraig_NodeVecAlloc( 1000 ); // the array of primary inputs p->vOutputs = Fraig_NodeVecAlloc( 1000 ); // the array of primary outputs p->vNodes = Fraig_NodeVecAlloc( 1000 ); // the array of internal nodes // start the tables p->pTableS = Fraig_HashTableCreate( 1000 ); // hashing by structure p->pTableF = Fraig_HashTableCreate( 1000 ); // hashing by function p->pTableF0 = Fraig_HashTableCreate( 1000 ); // hashing by function (for sparse functions) // create the constant node p->pConst1 = Fraig_NodeCreateConst( p ); // initialize SAT solver feedback data structures Fraig_FeedBackInit( p ); // initialize other variables p->vProj = Msat_IntVecAlloc( 10 ); p->nTravIds = 1; p->nTravIds2 = 1; return p; } /**Function************************************************************* Synopsis [Deallocates the mapping manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Fraig_ManFree( Fraig_Man_t * p ) { int i; if ( p->fVerbose ) { if ( p->fChoicing ) Fraig_ManReportChoices( p ); Fraig_ManPrintStats( p ); // Fraig_TablePrintStatsS( p ); // Fraig_TablePrintStatsF( p ); // Fraig_TablePrintStatsF0( p ); } for ( i = 0; i < p->vNodes->nSize; i++ ) if ( p->vNodes->pArray[i]->vFanins ) { Fraig_NodeVecFree( p->vNodes->pArray[i]->vFanins ); p->vNodes->pArray[i]->vFanins = NULL; } if ( p->vInputs ) Fraig_NodeVecFree( p->vInputs ); if ( p->vNodes ) Fraig_NodeVecFree( p->vNodes ); if ( p->vOutputs ) Fraig_NodeVecFree( p->vOutputs ); if ( p->pTableS ) Fraig_HashTableFree( p->pTableS ); if ( p->pTableF ) Fraig_HashTableFree( p->pTableF ); if ( p->pTableF0 ) Fraig_HashTableFree( p->pTableF0 ); if ( p->pSat ) Msat_SolverFree( p->pSat ); if ( p->vProj ) Msat_IntVecFree( p->vProj ); if ( p->vCones ) Fraig_NodeVecFree( p->vCones ); if ( p->vPatsReal ) Msat_IntVecFree( p->vPatsReal ); if ( p->pModel ) free( p->pModel ); Fraig_MemFixedStop( p->mmNodes, 0 ); Fraig_MemFixedStop( p->mmSims, 0 ); if ( p->pSuppS ) { FREE( p->pSuppS[0] ); FREE( p->pSuppS ); } if ( p->pSuppF ) { FREE( p->pSuppF[0] ); FREE( p->pSuppF ); } FREE( p->ppOutputNames ); FREE( p->ppInputNames ); FREE( p ); } /**Function************************************************************* Synopsis [Deallocates the mapping manager.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Fraig_ManPrintStats( Fraig_Man_t * p ) { double nMemory; int clk = clock(); nMemory = ((double)(p->vInputs->nSize + p->vNodes->nSize) * (sizeof(Fraig_Node_t) + sizeof(unsigned)*(p->nWordsRand + p->nWordsDyna) /*+ p->nSuppWords*sizeof(unsigned)*/))/(1<<20); printf( "Words: Random = %d. Dynamic = %d. Used = %d. Memory = %0.2f Mb.\n", p->nWordsRand, p->nWordsDyna, p->iWordPerm, nMemory ); printf( "Proof = %d. Counter-example = %d. Fail = %d. Zero = %d.\n", p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatZeros ); printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) ClaVars = %d.\n", Fraig_CountNodes(p,0), p->vNodes->nSize, Fraig_ManCountMuxes(p), Fraig_ManCountExors(p), p->nVarsClauses ); if ( p->pSat ) Msat_SolverPrintStats( p->pSat ); Fraig_PrintTime( "AIG simulation ", p->timeSims ); Fraig_PrintTime( "AIG traversal ", p->timeTrav ); Fraig_PrintTime( "Solver feedback ", p->timeFeed ); Fraig_PrintTime( "SAT solving ", p->timeSat ); Fraig_PrintTime( "Network update ", p->timeToNet ); Fraig_PrintTime( "TOTAL RUNTIME ", p->timeTotal ); if ( p->time1 > 0 ) { Fraig_PrintTime( "time1", p->time1 ); } if ( p->time2 > 0 ) { Fraig_PrintTime( "time2", p->time2 ); } if ( p->time3 > 0 ) { Fraig_PrintTime( "time3", p->time3 ); } if ( p->time4 > 0 ) { Fraig_PrintTime( "time4", p->time4 ); } // PRT( "Selection ", timeSelect ); // PRT( "Assignment", timeAssign ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////