diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2022-02-02 17:21:30 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2022-02-02 17:21:30 -0800 |
commit | 6097ac1d1aa67732a98caab517a510731fb2f0b1 (patch) | |
tree | 01875a471162730843d72b505606285bf401f049 /src/sat/glucose/AbcGlucose.cpp | |
parent | 0b4350a0ee38becc9d5da6d55affb62d310f52be (diff) | |
download | abc-6097ac1d1aa67732a98caab517a510731fb2f0b1.tar.gz abc-6097ac1d1aa67732a98caab517a510731fb2f0b1.tar.bz2 abc-6097ac1d1aa67732a98caab517a510731fb2f0b1.zip |
Adding option to dump CNF after preprocessing in &glucose.
Diffstat (limited to 'src/sat/glucose/AbcGlucose.cpp')
-rw-r--r-- | src/sat/glucose/AbcGlucose.cpp | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index ad595ab9..9c23e0d0 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -818,7 +818,7 @@ void Glucose_ReadDimacs( char * pFileName, SimpSolver& s ) SeeAlso [] ***********************************************************************/ -void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars ) +void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars, int fDumpCnf ) { abctime clk = Abc_Clock(); @@ -844,6 +844,15 @@ void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars ) S.eliminate(true); printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + + if ( fDumpCnf ) + { + char * pFileCnf = Extra_FileNameGenericAppend( pFileName, "_out.cnf" ); + S.toDimacs(pFileCnf); + printf( "Finished dumping CNF after preprocessing into file \"%s\".\n", pFileCnf ); + printf( "SAT solving is not performed.\n" ); + return; + } } vec<Lit> dummy; |