From 5de12aa6b3a91850596326954eaca0c997cc499e Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 23 Oct 2023 11:30:44 -0700
Subject: [PATCH] Experiments with SAT solving.

---
 src/base/io/io.c     | 13 +++++++++----
 src/base/io/ioUtil.c | 33 ++++++++++++++++++++++++++++-----
 2 files changed, 37 insertions(+), 9 deletions(-)

diff --git a/src/base/io/io.c b/src/base/io/io.c
index f988a0078..55a02dee2 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1224,17 +1224,21 @@ usage:
 ***********************************************************************/
 int IoCommandReadCnf( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Vec_Ptr_t * Io_FileReadCnf( char * pFileName );
+    extern Vec_Ptr_t * Io_FileReadCnf( char * pFileName, int fMulti );
     FILE * pFile;
     Abc_Ntk_t * pNtk;
     Vec_Ptr_t * vSops;
+    int fMulti = 0;
     int c;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF )
     {
         switch ( c )
         {
+            case 'm':
+                fMulti ^= 1;
+                break;            
             case 'h':
                 goto usage;
             default:
@@ -1253,7 +1257,7 @@ int IoCommandReadCnf( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else 
         fclose( pFile );
-    vSops = Io_FileReadCnf( argv[globalUtilOptind] );
+    vSops = Io_FileReadCnf( argv[globalUtilOptind], fMulti );
     if ( Vec_PtrSize(vSops) == 0 )
     {
         Vec_PtrFreeFree( vSops );
@@ -1273,8 +1277,9 @@ int IoCommandReadCnf( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: read_cnf [-h] <file>\n" );
+    fprintf( pAbc->Err, "usage: read_cnf [-mh] <file>\n" );
     fprintf( pAbc->Err, "\t         creates network with one node\n" );
+    fprintf( pAbc->Err, "\t-m     : toggles generating multi-output network [default = %s]\n", fMulti?  "yes":"no" );    
     fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
     fprintf( pAbc->Err, "\tfile   : file name with the truth table\n" );
     return 1;
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index d11ee7408..eee2dda53 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -931,8 +931,9 @@ void Io_TransformSF2PLA( char * pNameIn, char * pNameOut )
   SeeAlso     []
 
 ***********************************************************************/
-char * Io_ConvertNumsToSop( Vec_Wec_t * vNums, int nVars )
+Vec_Ptr_t * Io_ConvertNumsToSop( Vec_Wec_t * vNums, int nVars )
 {
+    Vec_Ptr_t * vSops = Vec_PtrAlloc(1);
     Vec_Int_t * vLevel; int i, k, Num;
     int nSize = (nVars + 3)*Vec_WecSize(vNums);
     char * pStr = ABC_ALLOC( char, nSize+1 );
@@ -947,11 +948,30 @@ char * Io_ConvertNumsToSop( Vec_Wec_t * vNums, int nVars )
         pCube[nVars+1] = '0';
         pCube[nVars+2] = '\n';                
     }
-    return pStr;
+    Vec_PtrPush( vSops, pStr );
+    return vSops;
 }
-Vec_Ptr_t * Io_FileReadCnf( char * pFileName )
+Vec_Ptr_t * Io_ConvertNumsToSopMulti( Vec_Wec_t * vNums, int nVars )
 {
-    Vec_Ptr_t * vSops = Vec_PtrAlloc( 1 );
+    Vec_Ptr_t * vSops = Vec_PtrAlloc( Vec_WecSize(vNums) );
+    Vec_Int_t * vLevel; int i, k, Num;
+    Vec_WecForEachLevel( vNums, vLevel, i )
+    {
+        char * pCube = ABC_ALLOC( char, nVars + 4 );
+        memset( pCube, '-', nVars );
+        Vec_IntForEachEntry( vLevel, Num, k )
+            pCube[Abc_Lit2Var(Num)] = '0' + Abc_LitIsCompl(Num);
+        pCube[nVars+0] = ' ';
+        pCube[nVars+1] = '0';
+        pCube[nVars+2] = '\n';     
+        pCube[nVars+3] = '\0';    
+        Vec_PtrPush( vSops, pCube );               
+    }
+    return vSops;
+}
+Vec_Ptr_t * Io_FileReadCnf( char * pFileName, int fMulti )
+{
+    Vec_Ptr_t * vSops = NULL;
     Vec_Wec_t * vNums = Vec_WecAlloc( 100 );
     Vec_Int_t * vLevel;
     char * pThis, pLine[10000];
@@ -1002,7 +1022,10 @@ Vec_Ptr_t * Io_FileReadCnf( char * pFileName )
     if ( nClas != Vec_WecSize(vNums) )
         printf( "Warning: The number of clauses (%d) listed is different from the actual number (%d).\n", nClas, Vec_WecSize(vNums) );
     //Vec_WecPrint( vNums, 0 );
-    Vec_PtrPush( vSops, Io_ConvertNumsToSop(vNums, nVars) );
+    if ( fMulti )
+        vSops = Io_ConvertNumsToSopMulti(vNums, nVars);
+    else
+        vSops = Io_ConvertNumsToSop(vNums, nVars);
     Vec_WecFree( vNums );
     return vSops;
 }