Prepared &gla to try abstracting and proving concurrently.

1 files changed, 43 insertions, 50 deletions

diff --git a/src/sat/cnf/cnfCore.c b/src/sat/cnf/cnfCore.c
index f08ea6d1..b32d0c7a 100644
--- a/src/sat/cnf/cnfCore.c
+++ b/src/sat/cnf/cnfCore.c
@@ -32,6 +32,37 @@ static Cnf_Man_t * s_pManCnf = NULL;
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cnf_ManPrepare()
+{
+    if ( s_pManCnf == NULL )
+    {
+        printf( "\n\nCreating CNF manager!!!!!\n\n" );
+        s_pManCnf = Cnf_ManStart();
+    }
+}
+Cnf_Man_t * Cnf_ManRead()
+{
+    return s_pManCnf;
+}
+void Cnf_ManFree()
+{
+    if ( s_pManCnf == NULL )
+        return;
+    Cnf_ManStop( s_pManCnf );
+    s_pManCnf = NULL;
+}
+
 
 /**Function*************************************************************
 
@@ -52,10 +83,7 @@ Vec_Int_t * Cnf_DeriveMappingArray( Aig_Man_t * pAig )
     Aig_MmFixed_t * pMemCuts;
     clock_t clk;
     // allocate the CNF manager
-    if ( s_pManCnf == NULL )
-        s_pManCnf = Cnf_ManStart();
-    // connect the managers
-    p = s_pManCnf;
+    p = Cnf_ManStart();
     p->pManAig = pAig;
 
     // generate cuts for all nodes, assign cost, and find best cuts
@@ -83,6 +111,7 @@ p->timeSave = clock() - clk;
 //ABC_PRT( "Cuts   ", p->timeCuts );
 //ABC_PRT( "Map    ", p->timeMap  );
 //ABC_PRT( "Saving ", p->timeSave );
+    Cnf_ManStop( p );
     return vResult;
 }
  
@@ -97,18 +126,13 @@ p->timeSave = clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs )
+Cnf_Dat_t * Cnf_DeriveWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int nOutputs )
 {
-    Cnf_Man_t * p;
     Cnf_Dat_t * pCnf;
     Vec_Ptr_t * vMapped;
     Aig_MmFixed_t * pMemCuts;
     clock_t 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
@@ -138,6 +162,11 @@ p->timeSave = clock() - clk;
 //ABC_PRT( "Saving ", p->timeSave );
     return pCnf;
 }
+Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs )
+{
+    Cnf_ManPrepare();
+    return Cnf_DeriveWithMan( s_pManCnf, pAig, nOutputs );
+}
  
 /**Function*************************************************************
 
@@ -150,18 +179,13 @@ p->timeSave = clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin )
+Cnf_Dat_t * Cnf_DeriveOtherWithMan( Cnf_Man_t * p, Aig_Man_t * pAig, int fSkipTtMin )
 {
-    Cnf_Man_t * p;
     Cnf_Dat_t * pCnf;
     Vec_Ptr_t * vMapped;
     Aig_MmFixed_t * pMemCuts;
     clock_t 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
@@ -192,43 +216,12 @@ p->timeSave = clock() - clk;
 //ABC_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()
+Cnf_Dat_t * Cnf_DeriveOther( Aig_Man_t * pAig, int fSkipTtMin )
 {
-    if ( s_pManCnf == NULL )
-        return;
-    Cnf_ManStop( s_pManCnf );
-    s_pManCnf = NULL;
+    Cnf_ManPrepare();
+    return Cnf_DeriveOtherWithMan( s_pManCnf, pAig, fSkipTtMin );
 }
 
-
 #if 0
 
 /**Function*************************************************************