From 12b70d49463ae87486d1a4080c67140e2aa9fa4e Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 17 Oct 2011 10:39:05 +0300
Subject: Changes to CNF generation code.

---
 src/base/io/io.c | 32 ++++++++++++++++++++++++++------
 1 file changed, 26 insertions(+), 6 deletions(-)

(limited to 'src/base/io')

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;
-- 
cgit v1.2.3