diff options
-rw-r--r-- | src/aig/gia/giaSim4.c | 2 | ||||
-rw-r--r-- | src/base/abci/abc.c | 52 | ||||
-rw-r--r-- | src/base/acb/acbFunc.c | 48 | ||||
-rw-r--r-- | src/base/acb/acbUtil.c | 6 |
4 files changed, 92 insertions, 16 deletions
diff --git a/src/aig/gia/giaSim4.c b/src/aig/gia/giaSim4.c index 04352761..610bb098 100644 --- a/src/aig/gia/giaSim4.c +++ b/src/aig/gia/giaSim4.c @@ -41,7 +41,7 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int fOrder, int fVerbose ) +int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fVerbose ) { return 0; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 17741905..37bdc7ec 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -7128,11 +7128,11 @@ usage: ***********************************************************************/ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int fOrder, int fVerbose ); + extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fVerbose ); char * pFileNames[4] = {NULL, NULL, "out.v", NULL}; - int c, fOrder = 0, nWords = 1, fVerbose = 0; + int c, nWords = 4, nBeam = 4, LevL = 0, LevU = 0, fOrder = 0, fFancy = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Wovh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WBLUofvh" ) ) != EOF ) { switch ( c ) { @@ -7147,9 +7147,45 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nWords < 0 ) goto usage; break; + case 'B': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" ); + goto usage; + } + nBeam = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nBeam < 0 ) + goto usage; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + LevL = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( LevL < 0 ) + goto usage; + break; + case 'U': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-U\" should be followed by an integer.\n" ); + goto usage; + } + LevU = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( LevU < 0 ) + goto usage; + break; case 'o': fOrder ^= 1; break; + case 'f': + fFancy ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -7167,15 +7203,19 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ManRandom(1); for ( c = 0; c < argc - globalUtilOptind; c++ ) pFileNames[c] = argv[globalUtilOptind+c]; - Acb_NtkRunSim( pFileNames, nWords, fOrder, fVerbose ); + Acb_NtkRunSim( pFileNames, nWords, nBeam, LevL, LevU, fOrder, fFancy, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: runsim [-W] [-ovh] [-N <num>] <file1> <file2> <file3>\n" ); + Abc_Print( -2, "usage: runsim [-WBLU] [-ofvh] [-N <num>] <file1> <file2> <file3>\n" ); Abc_Print( -2, "\t experimental simulation command\n" ); Abc_Print( -2, "\t-W <num> : the number of words of simulation info [default = %d]\n", nWords ); + Abc_Print( -2, "\t-B <num> : the beam width parameter [default = %d]\n", nBeam ); + Abc_Print( -2, "\t-L <num> : the lower bound on level [default = %d]\n", LevL ); + Abc_Print( -2, "\t-U <num> : the upper bound on level [default = %d]\n", LevU ); Abc_Print( -2, "\t-o : toggle using a different node ordering [default = %s]\n", fOrder? "yes": "no" ); - Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-f : toggle using experimental feature [default = %s]\n", fFancy? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c index 1708e51d..6ffeb0e8 100644 --- a/src/base/acb/acbFunc.c +++ b/src/base/acb/acbFunc.c @@ -888,6 +888,12 @@ Vec_Int_t * Acb_FindSupportStart( sat_solver * pSat, int iFirstDiv, Vec_Int_t * //printf( "Selecting divisor %d with weight %d\n", i, Vec_IntEntry(vWeights, i) ); fFound = 1; } + if ( fFound == 0 ) + { + Vec_WrdFree( vPats ); + Vec_IntFree( vSupp ); + return NULL; + } assert( fFound ); iPat++; } @@ -1102,7 +1108,10 @@ Vec_Int_t * Acb_FindSupport( sat_solver * pSat, int iFirstDiv, Vec_Int_t * vWeig else vSupp = Acb_FindSupportNext( pSat, iFirstDiv, vWeights, vPats, &nPats ); if ( vSupp == NULL ) - break; + { + Vec_IntFree( vSuppBest ); + return NULL; + } //vSupp = Acb_FindSupportMin( pSat, iFirstDiv, vPats, &nPats, vTemp = vSupp ); //Vec_IntFree( vTemp ); if ( vSupp == NULL ) @@ -1241,6 +1250,7 @@ Vec_Int_t * Acb_DerivePatchSupport( Cnf_Dat_t * pCnf, int iTar, int nTargets, in // find minimum subset if ( fUseMinAssump ) { + int fUseSuppMin = 1; // solve in a standard way abctime clk = Abc_Clock(); nSuppNew = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 ); @@ -1250,20 +1260,25 @@ Vec_Int_t * Acb_DerivePatchSupport( Cnf_Dat_t * pCnf, int iTar, int nTargets, in Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); // perform minimization - if ( Vec_IntSize(vSupp) > 0 ) + if ( fUseSuppMin && Vec_IntSize(vSupp) > 0 ) { abctime clk = Abc_Clock(); + Vec_Int_t * vSupp2 = Vec_IntDup( vSupp ); Vec_Int_t * vTemp, * vWeights = Acb_DeriveWeights( vDivs, pNtkF ); vSupp = Acb_FindSupport( pSat, iDivVar, vWeights, vTemp = vSupp, TimeOut ); Vec_IntFree( vWeights ); Vec_IntFree( vTemp ); if ( vSupp == NULL ) { - printf( "Support minimization timed out after %d sec.\n", TimeOut ); - sat_solver_delete( pSat ); - return NULL; + printf( "Support minimization did not succeed. " ); + //sat_solver_delete( pSat ); + vSupp = vSupp2; + } + else + { + Vec_IntFree( vSupp2 ); + printf( "Minimized support to %d supp vars. ", Vec_IntSize(vSupp) ); } - printf( "Minimized support to %d supp vars. ", Vec_IntSize(vSupp) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } } @@ -1504,6 +1519,17 @@ char * Acb_EnumerateSatAssigns( sat_solver * pSat, int PivotVar, int FreeVar, Ve { if ( iMint == 1000 ) { + //if ( Vec_IntSize(vDivVars) == 0 ) + { + printf( "Assuming constant 0 function.\n" ); + Vec_StrClear( vTempSop ); + Vec_StrPush( vTempSop, ' ' ); + Vec_StrPush( vTempSop, '0' ); + Vec_StrPush( vTempSop, '\n' ); + Vec_StrPush( vTempSop, '\0' ); + return Vec_StrReleaseArray(vTempSop); + } + printf( "Reached the limit on the number of cubes (1000).\n" ); Vec_IntFree( vTemp ); Vec_IntFree( vLits ); @@ -2039,7 +2065,17 @@ Cnf_Dat_t * Acb_NtkDeriveMiterCnf( Gia_Man_t * p, int iTar, int nTars, int fVerb Cnf_Dat_t * pCnf; int v; for ( v = 0; v < iTar; v++ ) { + Gia_Man_t * pTemp; pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v ); + //pCof = Acb_NtkEcoSynthesize( pTemp = pCof ); + //pCof = Gia_ManCompress2( pTemp = pCof, 1, 0 ); + pCof = Gia_ManAigSyn2( pTemp = pCof, 0, 1, 0, 100, 0, 0, 0 ); + Gia_ManStop( pTemp ); + if ( Gia_ManAndNum(pCof) > 10000 ) + { + printf( "Quantifying target %3d ", v ); + Gia_ManPrintStats( pCof, NULL ); + } assert( Gia_ManCiNum(pCof) == Gia_ManCiNum(p) ); Gia_ManStop( p ); } diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c index 89163770..11ff6163 100644 --- a/src/base/acb/acbUtil.c +++ b/src/base/acb/acbUtil.c @@ -764,12 +764,12 @@ void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames SeeAlso [] ***********************************************************************/ -void Acb_NtkRunSim( char * pFileName[4], int nWords, int fOrder, int fVerbose ) +void Acb_NtkRunSim( char * pFileName[4], int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fVerbose ) { - extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int fOrder, int fVerbose ); + extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int nBeam, int LevL, int LevU, int fOrder, int fFancy, int fVerbose ); extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose ); char * pFileNames[4] = { pFileName[2], pFileName[1], NULL, pFileName[2] }; - if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, fOrder, fVerbose ) ) + if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, nBeam, LevL, LevU, fOrder, fFancy, fVerbose ) ) Acb_NtkRunEco( pFileNames, 1, fVerbose ); } |