Changes to CNF generation code.

2 files changed, 44 insertions, 11 deletions

diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 7efc062e..13aeaaa0 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1172,13 +1172,14 @@ Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
+Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, int fChangePol, int fVerbose )
 {
     Vec_Ptr_t * vMapped = NULL;
     Aig_Man_t * pMan;
     Cnf_Man_t * pManCnf = NULL;
     Cnf_Dat_t * pCnf;
     Abc_Ntk_t * pNtkNew = NULL;
+    int clk = clock();
     assert( Abc_NtkIsStrash(pNtk) );
 
     // convert to the AIG manager
@@ -1192,12 +1193,25 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
         return NULL;
     }
     // perform balance
+    if ( fVerbose )
     Aig_ManPrintStats( pMan );
 
     // derive CNF
-    pCnf = Cnf_Derive( pMan, 0 );
-    Cnf_DataTranformPolarity( pCnf, 0 );
-    printf( "Vars = %6d. Clauses = %7d. Literals = %8d.\n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
+    if ( fFastAlgo )
+        pCnf = Cnf_DeriveFast( pMan, 0 );
+    else
+        pCnf = Cnf_Derive( pMan, 0 );
+
+    // adjust polarity
+    if ( fChangePol )
+        Cnf_DataTranformPolarity( pCnf, 0 );
+
+    // print stats
+    if ( fVerbose )
+    {
+        printf( "Vars = %6d. Clauses = %7d. Literals = %8d.   ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
+        Abc_PrintTime( 1, "Time", clock() - clk );
+    }
 
 /*
     // write the network for verification
@@ -1210,7 +1224,6 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
     Cnf_DataWriteIntoFile( pCnf, pFileName, 0 );
     Cnf_DataFree( pCnf );
     Cnf_ClearMemory();
-
     Aig_ManStop( pMan );
     return pNtkNew;
 }
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 3b85a020..60085168 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1865,23 +1865,38 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
     int c;
-    int fAllPrimes;
     int fNewAlgo;
-    extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
+    int fFastAlgo;
+    int fAllPrimes;
+    int fChangePol;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, int fChangePol, int fVerbose );
 
     fNewAlgo = 1;
+    fFastAlgo = 0;
     fAllPrimes = 0;
+    fChangePol = 1;
+    fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "nph" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "nfpcvh" ) ) != EOF )
     {
         switch ( c )
         {
             case 'n':
                 fNewAlgo ^= 1;
                 break;
+            case 'f':
+                fFastAlgo ^= 1;
+                break;
             case 'p':
                 fAllPrimes ^= 1;
                 break;
+            case 'c':
+                fChangePol ^= 1;
+                break;
+            case 'v':
+                fVerbose ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -1904,8 +1919,10 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
         printf( "Warning: Selected option to write all primes has no effect when deriving CNF from AIG.\n" );
     }
     // call the corresponding file writer
-    if ( fNewAlgo )
-        Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName );
+    if ( fFastAlgo )
+        Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName, 1, fChangePol, fVerbose );
+    else if ( fNewAlgo )
+        Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName, 0, fChangePol, fVerbose );
     else if ( fAllPrimes )
         Io_WriteCnf( pAbc->pNtkCur, pFileName, 1 );
     else
@@ -1913,10 +1930,13 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_cnf [-nph] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_cnf [-nfpcvh] <file>\n" );
     fprintf( pAbc->Err, "\t         writes the miter cone into a CNF file\n" );
     fprintf( pAbc->Err, "\t-n     : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" );
+    fprintf( pAbc->Err, "\t-f     : toggle using fast algorithm [default = %s]\n", fFastAlgo? "yes" : "no" );
     fprintf( pAbc->Err, "\t-p     : toggle using all primes to enhance implicativity [default = %s]\n", fAllPrimes? "yes" : "no" );
+    fprintf( pAbc->Err, "\t-c     : toggle adjasting polarity of internal variables [default = %s]\n", fChangePol? "yes" : "no" );
+    fprintf( pAbc->Err, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "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;