New command &write_cnf.

3 files changed, 95 insertions, 2 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index b2cc1a8f..c6ace8db 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -254,6 +254,7 @@ struct Jf_Par_t_
     int            fFuncDsd;
     int            fGenCnf;
     int            fCnfObjIds;
+    int            fAddOrCla;
     int            fPureAig;
     int            fVerbose;
     int            fVeryVerbose;
diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c
index 8ba81c4c..0e737adc 100644
--- a/src/aig/gia/giaJf.c
+++ b/src/aig/gia/giaJf.c
@@ -159,11 +159,17 @@ void Jf_ManGenCnf( word uTruth, int iLitOut, Vec_Int_t * vLeaves, Vec_Int_t * vL
         }
     }
 }
-Cnf_Dat_t * Jf_ManCreateCnfRemap( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas )
+Cnf_Dat_t * Jf_ManCreateCnfRemap( Gia_Man_t * p, Vec_Int_t * vLits, Vec_Int_t * vClas, int fAddOrCla )
 {
     Cnf_Dat_t * pCnf; 
     Gia_Obj_t * pObj;
     int i, Entry, * pMap, nVars = 0;
+    if ( fAddOrCla )
+    {
+        Vec_IntPush( vClas, Vec_IntSize(vLits) );
+        Gia_ManForEachPo( p, pObj, i )
+            Vec_IntPush( vLits, Abc_Var2Lit(Gia_ObjId(p, pObj), 0) );
+    }
     // label nodes present in the mapping
     Vec_IntForEachEntry( vLits, Entry, i )
         Gia_ManObj(p, Abc_Lit2Var(Entry))->fMark0 = 1;
@@ -1543,7 +1549,7 @@ Gia_Man_t * Jf_ManDeriveMappingGia( Jf_Man_t * p )
         if ( p->pPars->fCnfObjIds )
             pNew->pData = Jf_ManCreateCnf( pNew, vLits, vClas );
         else
-            pNew->pData = Jf_ManCreateCnfRemap( pNew, vLits, vClas );
+            pNew->pData = Jf_ManCreateCnfRemap( pNew, vLits, vClas, p->pPars->fAddOrCla );
     }
     Vec_IntFreeP( &vLits );
     Vec_IntFreeP( &vClas );
@@ -1760,6 +1766,26 @@ Gia_Man_t * Jf_ManDeriveCnf( Gia_Man_t * p, int fCnfObjIds )
     pPars->fCnfObjIds = fCnfObjIds;
     return Jf_ManPerformMapping( p, pPars );
 }
+Gia_Man_t * Jf_ManDeriveCnfMiter( Gia_Man_t * p )
+{
+    Jf_Par_t Pars, * pPars = &Pars;
+    Jf_ManSetDefaultPars( pPars );
+    pPars->fGenCnf = 1;
+    pPars->fCnfObjIds = 0;
+    pPars->fAddOrCla = 1;
+    return Jf_ManPerformMapping( p, pPars );
+}
+void Jf_ManDumpCnf( Gia_Man_t * p, char * pFileName )
+{
+    Gia_Man_t * pNew;
+    Cnf_Dat_t * pCnf;
+    pNew = Jf_ManDeriveCnfMiter( p );
+    pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
+    Cnf_DataWriteIntoFile( pCnf, pFileName, 0, NULL, NULL );
+    Gia_ManStop( pNew );
+    Cnf_DataFree(pCnf);
+}
+
 void Jf_ManTestCnf( Gia_Man_t * p )
 {
     Gia_Man_t * pNew;
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 14646894..fa97ea1e 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -59,6 +59,7 @@ static int IoCommandWriteBench  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBook   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteCnf    ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteCnf2   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteDot    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteEqn    ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -125,6 +126,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "write_cellnet", IoCommandWriteCellNet, 0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_cnf",     IoCommandWriteCnf,     0 );
+    Cmd_CommandAdd( pAbc, "I/O", "&write_cnf",    IoCommandWriteCnf2,    0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_dot",     IoCommandWriteDot,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_eqn",     IoCommandWriteEqn,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_gml",     IoCommandWriteGml,     0 );
@@ -2031,6 +2033,70 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandWriteCnf2( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    extern void Jf_ManDumpCnf( Gia_Man_t * p, char * pFileName );
+    FILE * pFile;
+    char * pFileName;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "IoCommandWriteCnf2(): There is no AIG.\n" );
+        return 1;
+    } 
+    if ( Gia_ManRegNum(pAbc->pGia) > 0 )
+    {
+        Abc_Print( -1, "IoCommandWriteCnf2(): Works only for combinational miters.\n" );
+        return 0;
+    }
+    if ( argc != globalUtilOptind + 1 )
+        goto usage;
+    // get the input file name
+    pFileName = argv[globalUtilOptind];
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+        return 0;
+    }
+    Jf_ManDumpCnf( pAbc->pGia, pFileName );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: &write_cnf [-vh] <file>\n" );
+    fprintf( pAbc->Err, "\t         writes CNF produced by new DSD-based generator\n" );
+    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;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;