diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-09-18 08:10:18 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-09-18 08:10:18 -0700 |
| commit | 3b838b953d36c6293af51ddae55ec061e994b4c7 (patch) | |
| tree | af8d6fdfbcdb53a1e3d5ae403d9e7523b1cbba45 | |
| parent | c30a0af71c219dcdd42322c411b805bb674d14b7 (diff) | |
| download | abc-3b838b953d36c6293af51ddae55ec061e994b4c7.tar.gz abc-3b838b953d36c6293af51ddae55ec061e994b4c7.tar.bz2 abc-3b838b953d36c6293af51ddae55ec061e994b4c7.zip | |
Tuning SAT solver for QBF instances.
| -rw-r--r-- | src/base/abci/abc.c | 15 | ||||
| -rw-r--r-- | src/proof/fra/fraCec.c | 2 | ||||
| -rw-r--r-- | src/sat/cnf/cnfUtil.c | 12 |
3 files changed, 22 insertions, 7 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 809995c4..47da5723 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -21828,7 +21828,8 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( argc == globalUtilOptind + 1 ) { - extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int fVerbose ); + int * pModel = NULL; + extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel ); // get the input file name char * pFileName = argv[globalUtilOptind]; FILE * pFile = fopen( pFileName, "rb" ); @@ -21838,10 +21839,18 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } fclose( pFile ); - Cnf_DataSolveFromFile( pFileName, nConfLimit, fVerbose ); + Cnf_DataSolveFromFile( pFileName, nConfLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fVerbose, &pModel ); + if ( pModel && pNtk ) + { + int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pModel ); + if ( pSimInfo[0] != 1 ) + Abc_Print( 1, "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" ); + ABC_FREE( pSimInfo ); + pAbc->pCex = Abc_CexCreate( 0, Abc_NtkPiNum(pNtk), pNtk->pModel, 0, 0, 0 ); + } + ABC_FREE( pModel ); return 0; } - if ( pNtk == NULL ) { Abc_Print( -1, "Empty network.\n" ); diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c index fe113367..130036a6 100644 --- a/src/proof/fra/fraCec.c +++ b/src/proof/fra/fraCec.c @@ -194,7 +194,7 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi } if ( nLearnedStart ) - pSat->nLearntStart = nLearnedStart; + pSat->nLearntStart = pSat->nLearntMax = nLearnedStart; if ( nLearnedDelta ) pSat->nLearntDelta = nLearnedDelta; if ( nLearnedPerce ) diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c index ed38e735..7900b08c 100644 --- a/src/sat/cnf/cnfUtil.c +++ b/src/sat/cnf/cnfUtil.c @@ -399,7 +399,7 @@ finish: SeeAlso [] ***********************************************************************/ -int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int fVerbose ) +int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel ) { abctime clk = Abc_Clock(); Cnf_Dat_t * pCnf = Cnf_DataReadFromFile( pFileName ); @@ -420,9 +420,15 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int fVerbose ) printf( "The problem is trivially UNSAT.\n" ); return 1; } + if ( nLearnedStart ) + pSat->nLearntStart = pSat->nLearntMax = nLearnedStart; + if ( nLearnedDelta ) + pSat->nLearntDelta = nLearnedDelta; + if ( nLearnedPerce ) + pSat->nLearntRatio = nLearnedPerce; + if ( fVerbose ) + pSat->fVerbose = fVerbose; // solve the miter -// if ( fVerbose ) -// pSat->verbosity = 1; status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( status == l_Undef ) RetValue = -1; |