Version abc70121

4 files changed, 29 insertions, 12 deletions

diff --git a/src/base/io/io.c b/src/base/io/io.c
index f50faa11..8d5b8ad6 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1212,12 +1212,17 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
     int c;
+    int fAllPrimes;
 
+    fAllPrimes = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'p':
+                fAllPrimes ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -1228,13 +1233,23 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
         goto usage;
     // get the output file name
     pFileName = argv[globalUtilOptind];
+    // check if the feature will be used
+    if ( Abc_NtkIsStrash(pAbc->pNtkCur) && fAllPrimes )
+    {
+        fAllPrimes = 0;
+        printf( "Warning: Selected option to write all primes has no effect when deriving CNF from AIG.\n" );
+    }
     // call the corresponding file writer
-    Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_CNF );
+    if ( fAllPrimes )
+        Io_WriteCnf( pAbc->pNtkCur, pFileName, 1 );
+    else
+        Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_CNF );
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_cnf [-h] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_cnf [-ph] <file>\n" );
     fprintf( pAbc->Err, "\t         write the miter cone into a CNF file\n" );
+    fprintf( pAbc->Err, "\t-p     : toggle using all primes to enhance implicativity [default = %s]\n", fAllPrimes? "yes" : "no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
     return 1;
diff --git a/src/base/io/io.h b/src/base/io/io.h
index 55339790..78bc4563 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -100,7 +100,7 @@ extern void               Io_WriteBlifMvNetlist( Abc_Ntk_t * pNtk, char * FileNa
 /*=== abcWriteBench.c =========================================================*/
 extern int                Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteCnf.c ===========================================================*/
-extern int                Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName );
+extern int                Io_WriteCnf( Abc_Ntk_t * pNtk, char * FileName, int fAllPrimes );
 /*=== abcWriteDot.c ===========================================================*/
 extern void               Io_WriteDot( Abc_Ntk_t * pNtk, char * FileName );
 extern void               Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesShow, char * pFileName, int fGateNames, int fUseReverse );
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index ba390a2f..ed197ab4 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -220,7 +220,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
     // write non-netlist types
     if ( FileType == IO_FILE_CNF )
     {
-        Io_WriteCnf( pNtk, pFileName );
+        Io_WriteCnf( pNtk, pFileName, 0 );
         return;
     }
     if ( FileType == IO_FILE_DOT )
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index 24612566..f12a1297 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -41,14 +41,13 @@ static Abc_Ntk_t * s_pNtk = NULL;
   SeeAlso     []
 
 ***********************************************************************/
-int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName )
+int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName, int fAllPrimes )
 {
     solver * pSat;
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        fprintf( stdout, "Io_WriteCnf(): Currently can only process AIGs.\n" );
-        return 0;
-    }
+    if ( Abc_NtkIsStrash(pNtk) )
+        printf( "Io_WriteCnf() warning: Generating CNF by applying heuristic AIG to CNF conversion.\n" );
+    else
+        printf( "Io_WriteCnf() warning: Generating CNF by convering logic nodes into CNF clauses.\n" );
     if ( Abc_NtkPoNum(pNtk) != 1 )
     {
         fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter (the network with one PO).\n" );
@@ -64,8 +63,11 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName )
         fprintf( stdout, "The network has no logic nodes. No CNF file is generaled.\n" );
         return 0;
     }
+    // convert to logic BDD network
+    if ( Abc_NtkIsLogic(pNtk) )
+        Abc_NtkLogicToBdd( pNtk );
     // create solver with clauses
-    pSat = Abc_NtkMiterSatCreate( pNtk, 0 );
+    pSat = Abc_NtkMiterSatCreate( pNtk, 0, fAllPrimes );
     if ( pSat == NULL )
     {
         fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" );