Version abc80130_2

1 files changed, 53 insertions, 12 deletions

diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index 09824f38..e1b2d956 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -19,13 +19,16 @@
 ***********************************************************************/
 
 #include "io.h"
+#include "satSolver.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
+ 
+static Abc_Ntk_t * s_pNtk = NULL;
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -39,33 +42,71 @@
   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_NtkIsBddLogic(pNtk) )
+    sat_solver * pSat;
+    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 logic networks with BDDs.\n" );
+        fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter (the network with one PO).\n" );
         return 0;
     }
-    if ( Abc_NtkPoNum(pNtk) != 1 )
+    if ( Abc_NtkLatchNum(pNtk) != 0 )
     {
-        fprintf( stdout, "Io_WriteCnf(): Currently can only solve the miter (the network with one PO).\n" );
+        fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter for combinational circuits.\n" );
         return 0;
     }
-    if ( Abc_NtkLatchNum(pNtk) != 0 )
+    if ( Abc_NtkNodeNum(pNtk) == 0 )
     {
-        fprintf( stdout, "Io_WriteCnf(): Currently can only solve the miter for combinational circuits.\n" );
+        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_NtkToBdd( pNtk );
     // create solver with clauses
-    pSat = Abc_NtkMiterSatCreate( pNtk );
+    pSat = Abc_NtkMiterSatCreate( pNtk, fAllPrimes );
+    if ( pSat == NULL )
+    {
+        fprintf( stdout, "The problem is trivially UNSAT. No CNF file is generated.\n" );
+        return 1;
+    }        
     // write the clauses
-    Asat_SolverWriteDimacs( pSat, pFileName );
+    s_pNtk = pNtk;
+    Sat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 );
+    s_pNtk = NULL;
     // free the solver
-    solver_delete( pSat );
+    sat_solver_delete( pSat );
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Output the mapping of PIs into variable numbers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteCnfOutputPiMapping( FILE * pFile, int incrementVars )
+{
+    extern Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk );
+    Abc_Ntk_t * pNtk = s_pNtk;
+    Vec_Int_t * vCiIds;
+    Abc_Obj_t * pObj;
+    int i;
+    vCiIds = Abc_NtkGetCiSatVarNums( pNtk );
+    fprintf( pFile, "c PI variable numbers: <PI_name> <SAT_var_number>\n" );
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        fprintf( pFile, "c %s %d\n", Abc_ObjName(pObj), Vec_IntEntry(vCiIds, i) + (int)(incrementVars > 0) );
+    Vec_IntFree( vCiIds );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///