diff options
Diffstat (limited to 'abc70930/src/sat/fraig/fraigMan.c')
| -rw-r--r-- | abc70930/src/sat/fraig/fraigMan.c | 540 |
1 files changed, 540 insertions, 0 deletions
diff --git a/abc70930/src/sat/fraig/fraigMan.c b/abc70930/src/sat/fraig/fraigMan.c new file mode 100644 index 00000000..7fd937d5 --- /dev/null +++ b/abc70930/src/sat/fraig/fraigMan.c @@ -0,0 +1,540 @@ +/**CFile**************************************************************** + + FileName [fraigMan.c] + + PackageName [FRAIG: Functionally reduced AND-INV graphs.] + + Synopsis [Implementation of the FRAIG manager.] + + Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>] + + 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 DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Sets the default parameters of the package.] + + Description [This set of parameters is tuned for equivalence checking.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Prove_ParamsSetDefault( Prove_Params_t * pParams ) +{ + // clean the parameter structure + memset( pParams, 0, sizeof(Prove_Params_t) ); + // general parameters + pParams->fUseFraiging = 1; // enables fraiging + pParams->fUseRewriting = 1; // enables rewriting + pParams->fUseBdds = 0; // enables BDD construction when other methods fail + pParams->fVerbose = 0; // prints verbose stats + // iterations + pParams->nItersMax = 6; // the number of iterations + // mitering + pParams->nMiteringLimitStart = 300; // starting mitering limit + pParams->nMiteringLimitMulti = 2.0; // multiplicative coefficient to increase the limit in each iteration + // rewriting (currently not used) + pParams->nRewritingLimitStart = 3; // the number of rewriting iterations + pParams->nRewritingLimitMulti = 1.0; // multiplicative coefficient to increase the limit in each iteration + // fraiging + pParams->nFraigingLimitStart = 2; // starting backtrack(conflict) limit + pParams->nFraigingLimitMulti = 8.0; // multiplicative coefficient to increase the limit in each iteration + // last-gasp BDD construction + pParams->nBddSizeLimit = 1000000; // the number of BDD nodes when construction is aborted + pParams->fBddReorder = 1; // enables dynamic BDD variable reordering + // last-gasp mitering +// pParams->nMiteringLimitLast = 1000000; // final mitering limit + pParams->nMiteringLimitLast = 0; // final mitering limit + // global SAT solver limits + pParams->nTotalBacktrackLimit = 0; // global limit on the number of backtracks + pParams->nTotalInspectLimit = 0; // global limit on the number of clause inspects +// pParams->nTotalInspectLimit = 100000000; // global limit on the number of clause inspects +} + +/**Function************************************************************* + + Synopsis [Prints out the current values of CEC engine parameters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Prove_ParamsPrint( Prove_Params_t * pParams ) +{ + printf( "CEC enging parameters:\n" ); + printf( "Fraiging enabled: %s\n", pParams->fUseFraiging? "yes":"no" ); + printf( "Rewriting enabled: %s\n", pParams->fUseRewriting? "yes":"no" ); + printf( "BDD construction enabled: %s\n", pParams->fUseBdds? "yes":"no" ); + printf( "Verbose output enabled: %s\n", pParams->fVerbose? "yes":"no" ); + printf( "Solver iterations: %d\n", pParams->nItersMax ); + printf( "Starting mitering limit: %d\n", pParams->nMiteringLimitStart ); + printf( "Multiplicative coeficient for mitering: %.2f\n", pParams->nMiteringLimitMulti ); + printf( "Starting number of rewriting iterations: %d\n", pParams->nRewritingLimitStart ); + printf( "Multiplicative coeficient for rewriting: %.2f\n", pParams->nRewritingLimitMulti ); + printf( "Starting number of conflicts in fraiging: %d\n", pParams->nFraigingLimitMulti ); + printf( "Multiplicative coeficient for fraiging: %.2f\n", pParams->nRewritingLimitMulti ); + printf( "BDD size limit for bailing out: %.2f\n", pParams->nBddSizeLimit ); + printf( "BDD reordering enabled: %s\n", pParams->fBddReorder? "yes":"no" ); + printf( "Last-gasp mitering limit: %d\n", pParams->nMiteringLimitLast ); + printf( "Total conflict limit: %d\n", pParams->nTotalBacktrackLimit ); + printf( "Total inspection limit: %d\n", pParams->nTotalInspectLimit ); + printf( "Parameter dump complete.\n" ); +} + +/**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->nSeconds = 20; // the max number of seconds to solve the miter + 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; // the verbose flag for reporting the proof + pParams->fInternal = 0; // the flag indicates the internal run + pParams->nConfLimit = 0; // the limit on the number of conflicts + pParams->nInspLimit = 0; // the limit on the number of inspections +} + +/**Function************************************************************* + + Synopsis [Sets the default parameters of the package.] + + Description [This set of parameters is tuned for complete FRAIGing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ParamsSetDefaultFull( 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 = -1; // the max number of backtracks to perform + pParams->nSeconds = 20; // the max number of seconds to solve the miter + pParams->fFuncRed = 1; // performs only one level hashing + pParams->fFeedBack = 1; // enables solver feedback + pParams->fDist1Pats = 1; // enables distance-1 patterns + pParams->fDoSparse = 1; // performs equiv tests for sparse functions + pParams->fChoicing = 0; // enables recording structural choices + pParams->fTryProve = 0; // tries to solve the final miter + pParams->fVerbose = 0; // the verbosiness flag + pParams->fVerboseP = 0; // the verbose flag for reporting the proof + pParams->fInternal = 0; // the flag indicates the internal run + pParams->nConfLimit = 0; // the limit on the number of conflicts + pParams->nInspLimit = 0; // the limit on the number of inspections +} + +/**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 ); + srand( 0xDEADCAFE ); + + // 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->nSeconds = pParams->nSeconds; // the timeout for the final miter + 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 + p->nInspLimit = pParams->nInspLimit; // the limit on the number of inspections + + // 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 [Prepares the SAT solver to run on the two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManCreateSolver( Fraig_Man_t * p ) +{ + extern int timeSelect; + extern int timeAssign; + assert( p->pSat == NULL ); + // allocate data for SAT solving + p->pSat = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 ); + p->vVarsInt = Msat_SolverReadConeVars( p->pSat ); + p->vAdjacents = Msat_SolverReadAdjacents( p->pSat ); + p->vVarsUsed = Msat_SolverReadVarsUsed( p->pSat ); + timeSelect = 0; + timeAssign = 0; +} + + +/**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. FailReal = %d. Zero = %d.\n", + p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatFailsReal, 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 ); +} + +/**Function************************************************************* + + Synopsis [Allocates simulation information for all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, bool fClean ) +{ + Fraig_NodeVec_t * vInfo; + unsigned * pUnsigned; + int i; + assert( nSize > 0 && nWords > 0 ); + vInfo = Fraig_NodeVecAlloc( nSize ); + pUnsigned = ALLOC( unsigned, nSize * nWords ); + vInfo->pArray[0] = (Fraig_Node_t *)pUnsigned; + if ( fClean ) + memset( pUnsigned, 0, sizeof(unsigned) * nSize * nWords ); + for ( i = 1; i < nSize; i++ ) + vInfo->pArray[i] = (Fraig_Node_t *)(((unsigned *)vInfo->pArray[i-1]) + nWords); + vInfo->nSize = nSize; + return vInfo; +} + +/**Function************************************************************* + + Synopsis [Returns simulation info of all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fraig_NodeVec_t * Fraig_ManGetSimInfo( Fraig_Man_t * p ) +{ + Fraig_NodeVec_t * vInfo; + Fraig_Node_t * pNode; + unsigned * pUnsigned; + int nRandom, nDynamic; + int i, k, nWords; + + nRandom = Fraig_ManReadPatternNumRandom( p ); + nDynamic = Fraig_ManReadPatternNumDynamic( p ); + nWords = nRandom / 32 + nDynamic / 32; + + vInfo = Fraig_UtilInfoAlloc( p->vNodes->nSize, nWords, 0 ); + for ( i = 0; i < p->vNodes->nSize; i++ ) + { + pNode = p->vNodes->pArray[i]; + assert( i == pNode->Num ); + pUnsigned = (unsigned *)vInfo->pArray[i]; + for ( k = 0; k < nRandom / 32; k++ ) + pUnsigned[k] = pNode->puSimR[k]; + for ( k = 0; k < nDynamic / 32; k++ ) + pUnsigned[nRandom / 32 + k] = pNode->puSimD[k]; + } + return vInfo; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if A v B is always true based on the siminfo.] + + Description [A v B is always true iff A' * B' is always false.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 ) +{ + int fCompl1, fCompl2, i; + + fCompl1 = 1 ^ Fraig_IsComplement(pNode1) ^ Fraig_Regular(pNode1)->fInv; + fCompl2 = 1 ^ Fraig_IsComplement(pNode2) ^ Fraig_Regular(pNode2)->fInv; + + pNode1 = Fraig_Regular(pNode1); + pNode2 = Fraig_Regular(pNode2); + assert( pNode1 != pNode2 ); + + // check the simulation info + if ( fCompl1 && fCompl2 ) + { + for ( i = 0; i < p->nWordsRand; i++ ) + if ( ~pNode1->puSimR[i] & ~pNode2->puSimR[i] ) + return 0; + for ( i = 0; i < p->iWordStart; i++ ) + if ( ~pNode1->puSimD[i] & ~pNode2->puSimD[i] ) + return 0; + return 1; + } + if ( !fCompl1 && fCompl2 ) + { + for ( i = 0; i < p->nWordsRand; i++ ) + if ( pNode1->puSimR[i] & ~pNode2->puSimR[i] ) + return 0; + for ( i = 0; i < p->iWordStart; i++ ) + if ( pNode1->puSimD[i] & ~pNode2->puSimD[i] ) + return 0; + return 1; + } + if ( fCompl1 && !fCompl2 ) + { + for ( i = 0; i < p->nWordsRand; i++ ) + if ( ~pNode1->puSimR[i] & pNode2->puSimR[i] ) + return 0; + for ( i = 0; i < p->iWordStart; i++ ) + if ( ~pNode1->puSimD[i] & pNode2->puSimD[i] ) + return 0; + return 1; + } +// if ( fCompl1 && fCompl2 ) + { + for ( i = 0; i < p->nWordsRand; i++ ) + if ( pNode1->puSimR[i] & pNode2->puSimR[i] ) + return 0; + for ( i = 0; i < p->iWordStart; i++ ) + if ( pNode1->puSimD[i] & pNode2->puSimD[i] ) + return 0; + return 1; + } +} + +/**Function************************************************************* + + Synopsis [Adds clauses to the solver.] + + Description [This procedure is used to add external clauses to the solver. + The clauses are given by sets of nodes. Each node stands for one literal. + If the node is complemented, the literal is negated.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes ) +{ + Fraig_Node_t * pNode; + int i, fComp, RetValue; + if ( p->pSat == NULL ) + Fraig_ManCreateSolver( p ); + // create four clauses + Msat_IntVecClear( p->vProj ); + for ( i = 0; i < nNodes; i++ ) + { + pNode = Fraig_Regular(ppNodes[i]); + fComp = Fraig_IsComplement(ppNodes[i]); + Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) ); +// printf( "%d(%d) ", pNode->Num, fComp ); + } +// printf( "\n" ); + RetValue = Msat_SolverAddClause( p->pSat, p->vProj ); + assert( RetValue ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + |