1 files changed, 89 insertions, 8 deletions
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c
index a3a7efaa..7480d45d 100644
--- a/src/aig/cnf/cnfCore.c
+++ b/src/aig/cnf/cnfCore.c
@@ -24,13 +24,15 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static Cnf_Man_t * s_pManCnf = NULL;
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Converts AIG into the SAT solver.]
 
   Description []
                
@@ -39,21 +41,97 @@
   SeeAlso     []
 
 ***********************************************************************/
-Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Aig_Man_t * pAig )
+Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig )
 {
-    Aig_MmFixed_t * pMemCuts;
-    Cnf_Dat_t * pCnf = NULL;
+    Cnf_Man_t * p;
+    Cnf_Dat_t * pCnf;
     Vec_Ptr_t * vMapped;
-    int nIters = 2;
+    Aig_MmFixed_t * pMemCuts;
     int clk;
-
+    // allocate the CNF manager
+    if ( s_pManCnf == NULL )
+        s_pManCnf = Cnf_ManStart();
     // connect the managers
+    p = s_pManCnf;
     p->pManAig = pAig;
 
     // generate cuts for all nodes, assign cost, and find best cuts
 clk = clock();
-    pMemCuts = Dar_ManComputeCuts( pAig );
-PRT( "Cuts", clock() - clk );
+    pMemCuts = Dar_ManComputeCuts( pAig, 10 );
+p->timeCuts = clock() - clk;
+
+    // find the mapping
+clk = clock();
+    Cnf_DeriveMapping( p );
+p->timeMap = clock() - clk;
+//    Aig_ManScanMapping( p, 1 );
+
+    // convert it into CNF
+clk = clock();
+    Cnf_ManTransferCuts( p );
+    vMapped = Cnf_ManScanMapping( p, 1, 1 );
+    pCnf = Cnf_ManWriteCnf( p, vMapped );
+    Vec_PtrFree( vMapped );
+    Aig_MmFixedStop( pMemCuts, 0 );
+p->timeSave = clock() - clk;
+
+PRT( "Cuts   ", p->timeCuts );
+PRT( "Map    ", p->timeMap  );
+PRT( "Saving ", p->timeSave );
+    return pCnf;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cnf_Man_t * Cnf_ManRead()
+{
+    return s_pManCnf;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_ClearMemory()
+{
+    if ( s_pManCnf == NULL )
+        return;
+    Cnf_ManStop( s_pManCnf );
+    s_pManCnf = NULL;
+}
+
+
+#if 0
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cnf_Dat_t * Cnf_Derive_old( Aig_Man_t * pAig )
+{
 /*
     // iteratively improve area flow
     for ( i = 0; i < nIters; i++ )
@@ -95,6 +173,9 @@ PRT( "Ext ", clock() - clk );
     return NULL;
 }
 
+#endif
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////