diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abci/abc.c | 8 | ||||
-rw-r--r-- | src/sat/bsat/satUtil.c | 10 | ||||
-rw-r--r-- | src/sat/cnf/cnfUtil.c | 16 |
3 files changed, 22 insertions, 12 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; diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index dc431440..d782386e 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -185,13 +185,15 @@ void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumpBegin SeeAlso [] ***********************************************************************/ +static inline double Sat_Wrd2Dbl( word w ) { return (double)(unsigned)(w&0x3FFFFFFF) + (double)(1<<30)*(unsigned)(w>>30); } + void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ) { // printf( "calls : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 ); - printf( "starts : %10d\n", (int)p->stats.starts ); - printf( "conflicts : %10d\n", (int)p->stats.conflicts ); - printf( "decisions : %10d\n", (int)p->stats.decisions ); - printf( "propagations : %10d\n", (int)p->stats.propagations ); + printf( "starts : %16.0f\n", Sat_Wrd2Dbl(p->stats.starts) ); + printf( "conflicts : %16.0f\n", Sat_Wrd2Dbl(p->stats.conflicts) ); + printf( "decisions : %16.0f\n", Sat_Wrd2Dbl(p->stats.decisions) ); + printf( "propagations : %16.0f\n", Sat_Wrd2Dbl(p->stats.propagations) ); // printf( "inspects : %10d\n", (int)p->stats.inspects ); // printf( "inspects2 : %10d\n", (int)p->stats.inspects2 ); } diff --git a/src/sat/cnf/cnfUtil.c b/src/sat/cnf/cnfUtil.c index 7900b08c..a5037718 100644 --- a/src/sat/cnf/cnfUtil.c +++ b/src/sat/cnf/cnfUtil.c @@ -399,12 +399,12 @@ finish: SeeAlso [] ***********************************************************************/ -int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel ) +int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fVerbose, int ** ppModel, int nPis ) { abctime clk = Abc_Clock(); Cnf_Dat_t * pCnf = Cnf_DataReadFromFile( pFileName ); sat_solver * pSat; - int status, RetValue = -1; + int i, status, RetValue = -1; if ( pCnf == NULL ) return -1; if ( fVerbose ) @@ -414,10 +414,10 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, } // convert into SAT solver pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); - Cnf_DataFree( pCnf ); if ( pSat == NULL ) { printf( "The problem is trivially UNSAT.\n" ); + Cnf_DataFree( pCnf ); return 1; } if ( nLearnedStart ) @@ -440,7 +440,6 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, assert( 0 ); if ( fVerbose ) Sat_SolverPrintStats( stdout, pSat ); - sat_solver_delete( pSat ); if ( RetValue == -1 ) Abc_Print( 1, "UNDECIDED " ); else if ( RetValue == 0 ) @@ -449,6 +448,15 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart, Abc_Print( 1, "UNSATISFIABLE " ); //Abc_Print( -1, "\n" ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + // derive SAT assignment + if ( RetValue == 0 ) + { + *ppModel = ABC_ALLOC( int, nPis ); + for ( i = 0; i < nPis; i++ ) + (*ppModel)[i] = sat_solver_var_value( pSat, pCnf->nVars - nPis + i ); + } + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); return RetValue; } |