diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-09-18 08:38:53 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-09-18 08:38:53 -0700 |
| commit | fdf00d8044661738aac2eed776520f5511d32607 (patch) | |
| tree | 8608985cfc5cf04d0a4d0b510d28c4e38179ffda /src/base/abci | |
| parent | 3b838b953d36c6293af51ddae55ec061e994b4c7 (diff) | |
| download | abc-fdf00d8044661738aac2eed776520f5511d32607.tar.gz abc-fdf00d8044661738aac2eed776520f5511d32607.tar.bz2 abc-fdf00d8044661738aac2eed776520f5511d32607.zip | |
Tuning SAT solver for QBF instances.
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abc.c | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 47da5723..0fb139d3 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -21829,7 +21829,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( argc == globalUtilOptind + 1 ) { int * pModel = NULL; - extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel ); + extern int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel, int nPis ); // get the input file name char * pFileName = argv[globalUtilOptind]; FILE * pFile = fopen( pFileName, "rb" ); @@ -21839,14 +21839,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } fclose( pFile ); - Cnf_DataSolveFromFile( pFileName, nConfLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fVerbose, &pModel ); + Cnf_DataSolveFromFile( pFileName, nConfLimit, nLearnedStart, nLearnedDelta, nLearnedPerce, fVerbose, &pModel, Abc_NtkPiNum(pNtk) ); 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_Print( 1, "ERROR in mapping PIs into SAT vars: Generated CEX is invalid.\n" ); ABC_FREE( pSimInfo ); - pAbc->pCex = Abc_CexCreate( 0, Abc_NtkPiNum(pNtk), pNtk->pModel, 0, 0, 0 ); + pAbc->pCex = Abc_CexCreate( 0, Abc_NtkPiNum(pNtk), pModel, 0, 0, 0 ); } ABC_FREE( pModel ); return 0; |