Version abc90410

3 files changed, 19 insertions, 11 deletions

diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c
index cfa4594d..7b23aa33 100644
--- a/src/aig/dar/darLib.c
+++ b/src/aig/dar/darLib.c
@@ -730,7 +730,7 @@ int Dar_LibCutMarkMffc( Aig_Man_t * p, Aig_Obj_t * pRoot, int nLeaves, float * p
     for ( i = 0; i < nLeaves; i++ )
         Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs++;
     // label MFFC with current ID
-    nNodes = Aig_NodeMffsLabel( p, pRoot, pPower );
+    nNodes = Aig_NodeMffcLabel( p, pRoot, pPower );
     // unmark the cut leaves
     for ( i = 0; i < nLeaves; i++ )
         Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs--;
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index 6118dd71..5f6c5520 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -376,14 +376,14 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
         pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore );
         if ( Kit_TruthIsConst0(pTruth, Vec_PtrSize(vCut)) )
         {
-            p->GainBest = Aig_NodeMffsSupp( p->pAig, pObj, 0, NULL );
+            p->GainBest = Aig_NodeMffcSupp( p->pAig, pObj, 0, NULL );
             p->pGraphBest = Kit_GraphCreateConst0();
             Vec_PtrCopy( p->vLeavesBest, vCut );
             return p->GainBest;
         }
         if ( Kit_TruthIsConst1(pTruth, Vec_PtrSize(vCut)) )
         {
-            p->GainBest = Aig_NodeMffsSupp( p->pAig, pObj, 0, NULL );
+            p->GainBest = Aig_NodeMffcSupp( p->pAig, pObj, 0, NULL );
             p->pGraphBest = Kit_GraphCreateConst1();
             Vec_PtrCopy( p->vLeavesBest, vCut );
             return p->GainBest;
@@ -528,7 +528,7 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
         // get the bounded MFFC size
 clk = clock();
         nLevelMin = ABC_MAX( 0, Aig_ObjLevel(pObj) - 10 );
-        nNodesSaved = Aig_NodeMffsSupp( pAig, pObj, nLevelMin, vCut );
+        nNodesSaved = Aig_NodeMffcSupp( pAig, pObj, nLevelMin, vCut );
         if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider
         {
 p->timeCuts += clock() - clk;
@@ -538,15 +538,15 @@ p->timeCuts += clock() - clk;
         if ( Vec_PtrSize(vCut) > p->pPars->nLeafMax ) // get one reconv-driven cut
         {
             Aig_ManFindCut( pObj, vCut, p->vCutNodes, p->pPars->nLeafMax, 50 );
-            nNodesSaved = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut );
+            nNodesSaved = Aig_NodeMffcLabelCut( p->pAig, pObj, vCut );
         }
         else if ( Vec_PtrSize(vCut) < p->pPars->nLeafMax - 2 && p->pPars->fExtend )
         {
             if ( !Dar_ObjCutLevelAchieved(vCut, nLevelMin) )
             {
-                if ( Aig_NodeMffsExtendCut( pAig, pObj, vCut, vCut2 ) )
+                if ( Aig_NodeMffcExtendCut( pAig, pObj, vCut, vCut2 ) )
                 {
-                    nNodesSaved2 = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut );
+                    nNodesSaved2 = Aig_NodeMffcLabelCut( p->pAig, pObj, vCut );
                     assert( nNodesSaved2 == nNodesSaved );
                 }
                 if ( Vec_PtrSize(vCut2) > p->pPars->nLeafMax )
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 383b5b6b..66e6371d 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -435,6 +435,7 @@ ABC_PRT( "Choicing time ", clock() - clk );
 Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
+    extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
 
     int fVerbose = pPars->fVerbose;
     int fConstruct = 0;
@@ -444,7 +445,8 @@ Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 
 clk = clock();
 //    vAigs = Dar_ManChoiceSynthesisExt();
-    vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
+//    vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
+    vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, 0 );
 
     // swap the first and last network
     // this should lead to the primary choice being "better" because of synthesis
@@ -458,9 +460,9 @@ clk = clock();
 
 if ( fVerbose )
 {
-ABC_PRT( "Synthesis time", clock() - clk );
+//ABC_PRT( "Synthesis time", clock() - clk );
 }
-//    pPars->timeSynth = clock() - clk;
+    pPars->timeSynth = clock() - clk;
 
 clk = clock();
 /*
@@ -469,7 +471,11 @@ clk = clock();
     else
         pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
 */
-    pMan = Dch_ComputeChoices( vAigs, pPars );
+    // perform choice computation
+    if ( pPars->fUseGia )
+        pMan = Cec_ComputeChoices( vAigs, pPars );
+    else
+        pMan = Dch_ComputeChoices( vAigs, pPars );
 
     // reconstruct the network
     pMan = Aig_ManDupDfsGuided( pTemp = pMan, Vec_PtrEntry(vAigs,0) );
@@ -483,6 +489,8 @@ clk = clock();
     }
     // reset levels
     Aig_ManChoiceLevel( pMan );
+    ABC_FREE( pMan->pName );
+    ABC_FREE( pMan->pSpec );
     pMan->pName = Aig_UtilStrsav( pTemp->pName );
     pMan->pSpec = Aig_UtilStrsav( pTemp->pSpec );