diff options
Diffstat (limited to 'src/sat/fraig/fraigMan.c')
| -rw-r--r-- | src/sat/fraig/fraigMan.c | 310 |
1 files changed, 305 insertions, 5 deletions
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index e5979c93..7fd937d5 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -26,7 +26,7 @@ int timeSelect; int timeAssign; //////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFITIONS /// +/// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* @@ -40,12 +40,89 @@ int timeAssign; 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 @@ -55,6 +132,39 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams ) 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************************************************************* @@ -74,7 +184,8 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ) Fraig_Man_t * p; // set the random seed for simulation - srand( 0xFEEDDEAF ); +// srand( 0xFEEDDEAF ); + srand( 0xDEADCAFE ); // set parameters for equivalence checking if ( pParams == NULL ) @@ -100,6 +211,7 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ) 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) @@ -108,6 +220,7 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ) 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) ); @@ -153,7 +266,7 @@ void Fraig_ManFree( Fraig_Man_t * p ) // Fraig_TablePrintStatsF( p ); // Fraig_TablePrintStatsF0( p ); } - + for ( i = 0; i < p->vNodes->nSize; i++ ) if ( p->vNodes->pArray[i]->vFanins ) { @@ -194,6 +307,31 @@ void Fraig_ManFree( Fraig_Man_t * p ) 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************************************************************* @@ -214,8 +352,8 @@ void Fraig_ManPrintStats( Fraig_Man_t * p ) (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( "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 ); @@ -233,6 +371,168 @@ void Fraig_ManPrintStats( Fraig_Man_t * p ) // 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 /// |