luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding option to dump CNF after preprocessing in &glucose.

This commit is contained in:
Alan Mishchenko 2022-02-02 17:21:30 -08:00
parent 0b4350a0ee
commit 6097ac1d1a
6 changed files with 22 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/sat/bsat2/Solver.cpp
View File

@ -820,7 +820,7 @@ void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)
void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
{
FILE* f = fopen(file, "wr");
FILE* f = fopen(file, "wb");
if (f == NULL)
fprintf(stderr, "could not open file %s\n", file), exit(1);
toDimacs(f, assumps);

11
src/sat/glucose/AbcGlucose.cpp
View File

@ -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;

2
src/sat/glucose/AbcGlucose.h
View File

@ -105,7 +105,7 @@ extern void bmcg_sat_solver_start_new_round( bmcg_sat_solver * s );
extern void bmcg_sat_solver_mark_cone( bmcg_sat_solver * s, int var );
extern void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars );
extern void Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars, int fDumpCnf );
extern int Glucose_SolveAig( Gia_Man_t * p, Glucose_Pars * pPars );
ABC_NAMESPACE_HEADER_END

11
src/sat/glucose/AbcGlucoseCmd.cpp
View File

@ -81,10 +81,11 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv )
int pre = 1;
int verb = 0;
int nConfls = 0;
int fDumpCnf = 0;
Glucose_Pars pPars;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Cpvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Cpdvh" ) ) != EOF )
{
switch ( c )
{
@ -102,6 +103,9 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'p':
pre ^= 1;
break;
case 'd':
fDumpCnf ^= 1;
break;
case 'v':
verb ^= 1;
break;
@ -116,7 +120,7 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( argc == globalUtilOptind + 1 )
{
Glucose_SolveCnf( argv[globalUtilOptind], &pPars );
Glucose_SolveCnf( argv[globalUtilOptind], &pPars, fDumpCnf );
return 0;
}
@ -132,10 +136,11 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &glucose [-C num] [-pvh] <file.cnf>\n" );
Abc_Print( -2, "usage: &glucose [-C num] [-pdvh] <file.cnf>\n" );
Abc_Print( -2, "\t run Glucose 3.0 by Gilles Audemard and Laurent Simon\n" );
Abc_Print( -2, "\t-C num : conflict limit [default = %d]\n", nConfls );
Abc_Print( -2, "\t-p : enable preprocessing [default = %d]\n",pre);
Abc_Print( -2, "\t-d : enable dumping CNF after proprocessing [default = %d]\n",fDumpCnf);
Abc_Print( -2, "\t-v : verbosity [default = %d]\n",verb);
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file.cnf> : (optional) CNF file to solve\n");

2
src/sat/glucose/Glucose.cpp
View File

@ -1330,7 +1330,7 @@ void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)
void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
{
FILE* f = fopen(file, "wr");
FILE* f = fopen(file, "wb");
if (f == NULL)
fprintf(stderr, "could not open file %s\n", file), exit(1);
toDimacs(f, assumps);

2
src/sat/glucose2/Glucose2.cpp
View File

@ -1535,7 +1535,7 @@ void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)
void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
{
FILE* f = fopen(file, "wr");
FILE* f = fopen(file, "wb");
if (f == NULL)
fprintf(stderr, "could not open file %s\n", file), exit(1);
toDimacs(f, assumps);