From 6097ac1d1aa67732a98caab517a510731fb2f0b1 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 2 Feb 2022 17:21:30 -0800
Subject: Adding option to dump CNF after preprocessing in &glucose.

---
 src/sat/glucose/AbcGlucose.cpp    | 11 ++++++++++-
 src/sat/glucose/AbcGlucose.h      |  2 +-
 src/sat/glucose/AbcGlucoseCmd.cpp | 11 ++++++++---
 src/sat/glucose/Glucose.cpp       |  2 +-
 4 files changed, 20 insertions(+), 6 deletions(-)

(limited to 'src/sat/glucose')

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;
diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h
index 89a3652f..c73f9918 100644
--- a/src/sat/glucose/AbcGlucose.h
+++ b/src/sat/glucose/AbcGlucose.h
@@ -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
diff --git a/src/sat/glucose/AbcGlucoseCmd.cpp b/src/sat/glucose/AbcGlucoseCmd.cpp
index 2e819e49..bb957547 100644
--- a/src/sat/glucose/AbcGlucoseCmd.cpp
+++ b/src/sat/glucose/AbcGlucoseCmd.cpp
@@ -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");
diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp
index c975c6ca..cfb388de 100644
--- a/src/sat/glucose/Glucose.cpp
+++ b/src/sat/glucose/Glucose.cpp
@@ -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);
-- 
cgit v1.2.3