Version abc90714

committer: Baruch Sterin <baruchs@gmail.com>

4 files changed, 26 insertions, 32 deletions

diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h
index 6157a811..38978164 100644
--- a/src/aig/dch/dch.h
+++ b/src/aig/dch/dch.h
@@ -50,6 +50,7 @@ struct Dch_Pars_t_
     int              fPower;        // uses power-aware rewriting
     int              fUseGia;       // uses GIA package 
     int              fUseCSat;      // uses circuit-based solver
+    int              fLightSynth;   // uses lighter version of synthesis
     int              fVerbose;      // verbose stats
     int              timeSynth;     // synthesis runtime
     int              nNodesAhead;   // the lookahead in terms of nodes
@@ -66,7 +67,7 @@ struct Dch_Pars_t_
 
 /*=== dchCore.c ==========================================================*/
 extern void          Dch_ManSetDefaultParams( Dch_Pars_t * p );
-extern Aig_Man_t *   Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
+extern Aig_Man_t *   Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
 
 
 #ifdef __cplusplus
diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c
index 8e854355..4a8d8b53 100644
--- a/src/aig/dch/dchCore.c
+++ b/src/aig/dch/dchCore.c
@@ -49,6 +49,7 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p )
     p->fPolarFlip     =     1;  // uses polarity adjustment
     p->fSimulateTfo   =     1;  // simulate TFO
     p->fPower         =     0;  // power-aware rewriting
+    p->fLightSynth    =     0;  // uses lighter version of synthesis
     p->fVerbose       =     0;  // verbose stats
     p->nNodesAhead    =  1000;  // the lookahead in terms of nodes
     p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
@@ -65,37 +66,35 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
+Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     Dch_Man_t * p;
     Aig_Man_t * pResult;
     int clk, clkTotal = clock();
-    assert( Vec_PtrSize(vAigs) > 0 );
     // reset random numbers
     Aig_ManRandom(1);
     // start the choicing manager
-    p = Dch_ManCreate( vAigs, pPars );
+    p = Dch_ManCreate( pAig, pPars );
     // compute candidate equivalence classes
 clk = clock(); 
-    p->ppClasses = Dch_CreateCandEquivClasses( p->pAigTotal, pPars->nWords, pPars->fVerbose );
+    p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
 p->timeSimInit = clock() - clk;
 //    Dch_ClassesPrint( p->ppClasses, 0 );
     p->nLits = Dch_ClassesLitNum( p->ppClasses );
     // perform SAT sweeping
     Dch_ManSweep( p );
-    // count the number of representatives
-    p->nReprs = Dch_DeriveChoiceCountReprs( p->pAigTotal );
-    // create choices
-clk = clock();
-    pResult = Dch_DeriveChoiceAig( p->pAigTotal );
-p->timeChoice = clock() - clk;
-//    Aig_ManCleanup( p->pAigTotal );
-//    pResult = Aig_ManDupSimpleDfs( p->pAigTotal );
-    // count the number of equivalences and choices
-    p->nEquivs = Dch_DeriveChoiceCountEquivs( pResult );
-    p->nChoices = Aig_ManChoiceNum( pResult );
+    // free memory ahead of time
 p->timeTotal = clock() - clkTotal;
     Dch_ManStop( p );
+    // create choices
+    ABC_FREE( pAig->pTable );
+    pResult = Dch_DeriveChoiceAig( pAig );
+    // count the number of representatives
+    if ( pPars->fVerbose )
+        printf( "STATS:  Reprs = %6d.  Equivs = %6d.  Choices = %6d.\n", 
+               Dch_DeriveChoiceCountReprs( pAig ),
+               Dch_DeriveChoiceCountEquivs( pResult ),
+               Aig_ManChoiceNum( pResult ) );
     return pResult;
 }
 
diff --git a/src/aig/dch/dchInt.h b/src/aig/dch/dchInt.h
index 4e6315a4..a419335d 100644
--- a/src/aig/dch/dchInt.h
+++ b/src/aig/dch/dchInt.h
@@ -51,7 +51,7 @@ struct Dch_Man_t_
     // parameters
     Dch_Pars_t *     pPars;          // choicing parameters
     // AIGs used in the package
-    Vec_Ptr_t *      vAigs;          // user-given AIGs
+//    Vec_Ptr_t *      vAigs;          // user-given AIGs
     Aig_Man_t *      pAigTotal;      // intermediate AIG
     Aig_Man_t *      pAigFraig;      // final AIG
     // equivalence classes
@@ -142,7 +142,7 @@ extern int           Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vR
 /*=== dchCnf.c ===================================================*/
 extern void          Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj );
 /*=== dchMan.c ===================================================*/
-extern Dch_Man_t *   Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
+extern Dch_Man_t *   Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars );
 extern void          Dch_ManStop( Dch_Man_t * p );
 extern void          Dch_ManSatSolverRecycle( Dch_Man_t * p );
 /*=== dchSat.c ===================================================*/
diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c
index caed0ed5..c8bd8533 100644
--- a/src/aig/dch/dchMan.c
+++ b/src/aig/dch/dchMan.c
@@ -39,15 +39,14 @@
   SeeAlso     []
 
 ***********************************************************************/
-Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
+Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     Dch_Man_t * p;
     // create interpolation manager
     p = ABC_ALLOC( Dch_Man_t, 1 );
     memset( p, 0, sizeof(Dch_Man_t) );
     p->pPars        = pPars;
-    p->vAigs        = vAigs;
-    p->pAigTotal    = Dch_DeriveTotalAig( vAigs );
+    p->pAigTotal    = pAig; //Dch_DeriveTotalAig( vAigs );
     Aig_ManFanoutStart( p->pAigTotal );
     // SAT solving
     p->nSatVars     = 1;
@@ -74,18 +73,14 @@ Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
 ***********************************************************************/
 void Dch_ManPrintStats( Dch_Man_t * p )
 {
-//    Aig_Man_t * pAig;
-//    int i;
-//    printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) );
-//    Vec_PtrForEachEntry( p->vAigs, pAig, i )
-//        Aig_ManPrintStats( pAig );
+    int nNodeNum = Aig_ManNodeNum(p->pAigTotal) / 3;
     printf( "Parameters: Sim words = %d. Conf limit = %d. SAT var max = %d.\n", 
         p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax );
     printf( "AIG nodes : Total = %6d. Dangling = %6d. Main = %6d. (%6.2f %%)\n", 
         Aig_ManNodeNum(p->pAigTotal), 
-        Aig_ManNodeNum(p->pAigTotal)-Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0)),
-        Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0)),
-        100.0 * Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0))/Aig_ManNodeNum(p->pAigTotal) );
+        Aig_ManNodeNum(p->pAigTotal)-nNodeNum,
+        nNodeNum,
+        100.0 * nNodeNum/Aig_ManNodeNum(p->pAigTotal) );
     printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d.\n", 
         p->nSatVars, p->nConeMax, p->nRecycles );
     printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n", 
@@ -108,7 +103,7 @@ void Dch_ManPrintStats( Dch_Man_t * p )
     {
     ABC_PRT( "Synthesis  ", p->pPars->timeSynth );
     }
-}
+} 
 
 /**Function*************************************************************
 
@@ -123,10 +118,9 @@ void Dch_ManPrintStats( Dch_Man_t * p )
 ***********************************************************************/
 void Dch_ManStop( Dch_Man_t * p )
 {
+    Aig_ManFanoutStop( p->pAigTotal );
     if ( p->pPars->fVerbose )
         Dch_ManPrintStats( p );
-    if ( p->pAigTotal )
-        Aig_ManStop( p->pAigTotal );
     if ( p->pAigFraig )
         Aig_ManStop( p->pAigFraig );
     if ( p->ppClasses )