Adding more features to the synthesis script &syn2.

5 files changed, 56 insertions, 17 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index d5e3fbb5..463f11e6 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -969,7 +969,7 @@ extern void                Gia_AigerWriteSimple( Gia_Man_t * pInit, char * pFile
 /*=== giaBalance.c ===========================================================*/
 extern Gia_Man_t *         Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, int fVerbose );
 extern Gia_Man_t *         Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax, int fVerbose, int fVeryVerbose );
-extern Gia_Man_t *         Gia_ManAigSyn2( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
+extern Gia_Man_t *         Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fVerbose, int fVeryVerbose );
 extern Gia_Man_t *         Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
 extern Gia_Man_t *         Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
 /*=== giaBidec.c ===========================================================*/
diff --git a/src/aig/gia/giaBalance.c b/src/aig/gia/giaBalance.c
index dfbc6ca6..749a7c1e 100644
--- a/src/aig/gia/giaBalance.c
+++ b/src/aig/gia/giaBalance.c
@@ -1017,14 +1017,22 @@ void Gia_ManAigTransferPiLevels( Gia_Man_t * pNew, Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
+Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fVerbose, int fVeryVerbose )
 {
     Gia_Man_t * pNew, * pTemp;
     Jf_Par_t Pars, * pPars = &Pars;
-    Lf_ManSetDefaultPars( pPars );
-//    pPars->fVerbose = 1;
-    pPars->fCoarsen = 1;
-    pPars->nRelaxRatio = 20;
+    if ( fOldAlgo )
+    {
+        Jf_ManSetDefaultPars( pPars );
+        pPars->fCutMin     = fCutMin;
+    }
+    else
+    {
+        Lf_ManSetDefaultPars( pPars );
+        pPars->fCoarsen    = fCoarsen;
+        pPars->fCutMin     = fCutMin;
+        pPars->nRelaxRatio = nRelaxRatio;
+    }
     if ( fVerbose )     Gia_ManPrintStats( p, NULL );
     if ( Gia_ManAndNum(p) == 0 )
         return Gia_ManDup(p);
@@ -1033,7 +1041,10 @@ Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
     if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
     Gia_ManAigTransferPiLevels( pNew, p );
     // perform mapping
-    pNew = Lf_ManPerformMapping( pTemp = pNew, pPars );
+    if ( fOldAlgo )
+        pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
+    else
+        pNew = Lf_ManPerformMapping( pTemp = pNew, pPars );
     if ( fVerbose )     Gia_ManPrintStats( pNew, NULL );
 //    Gia_ManStop( pTemp );
     // perform balancing
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5ba68a33..068a355d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -27707,12 +27707,36 @@ int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp;
     int c, fVerbose = 0;
+    int fOldAlgo = 0;
+    int fCoarsen = 1;
+    int fCutMin = 0;
+    int nRelaxRatio = 20;
     int fVeryVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Rakmvwh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( 1, "Command line switch \"-R\" should be followed by a floating point number.\n" );
+                return 0;
+            }
+            nRelaxRatio = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nRelaxRatio < 0 ) 
+                goto usage;
+            break;
+        case 'a':
+            fOldAlgo ^= 1;
+            break;
+        case 'k':
+            fCoarsen ^= 1;
+            break;
+        case 'm':
+            fCutMin ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -27730,16 +27754,20 @@ int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Syn2(): There is no AIG.\n" );
         return 1;
     }
-    pTemp = Gia_ManAigSyn2( pAbc->pGia, fVerbose, fVeryVerbose );
+    pTemp = Gia_ManAigSyn2( pAbc->pGia, fOldAlgo, fCoarsen, fCutMin, nRelaxRatio, fVerbose, fVeryVerbose );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &syn2 [-lvh]\n" );
-    Abc_Print( -2, "\t         performs AIG optimization\n" );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-w     : toggle printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
+    Abc_Print( -2, "usage: &syn2 [-R num] [-akmlvh]\n" );
+    Abc_Print( -2, "\t           performs AIG optimization\n" );
+    Abc_Print( -2, "\t-R num   : the delay relaxation ratio (num >= 0) [default = %d]\n",  nRelaxRatio );
+    Abc_Print( -2, "\t-a       : toggles using the old algorithm [default = %s]\n",        fOldAlgo? "yes": "no" );
+    Abc_Print( -2, "\t-k       : toggles coarsening the subject graph [default = %s]\n",   fCoarsen? "yes": "no" );
+    Abc_Print( -2, "\t-m       : toggles cut minimization [default = %s]\n",               fCutMin? "yes": "no" );
+    Abc_Print( -2, "\t-v       : toggle printing verbose information [default = %s]\n",    fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w       : toggle printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h       : print the command usage\n");
     return 1;
 }
 
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
index e1869404..d8b063ce 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -786,7 +786,7 @@ int Gia_ManBmcPerform_old_cnf( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
     if ( pPars->fUseSynth )
     {
         Gia_Man_t * pTemp = p->pFrames;
-        p->pFrames = Gia_ManAigSyn2( pTemp, pPars->fVerbose, 0 );
+        p->pFrames = Gia_ManAigSyn2( pTemp, 1, 0, 0, 0, pPars->fVerbose, 0 );
         Gia_ManStop( pTemp );
     }
     else if ( pPars->fVerbose )
@@ -970,7 +970,7 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
     }
     if ( pPars->fUseSynth )
     {
-        p->pFrames = Gia_ManAigSyn2( pTemp = p->pFrames, pPars->fVerbose, 0 );  Gia_ManStop( pTemp );
+        p->pFrames = Gia_ManAigSyn2( pTemp = p->pFrames, 1, 0, 0, 0, pPars->fVerbose, 0 );  Gia_ManStop( pTemp );
     }
     else if ( pPars->fVerbose )
         Gia_ManPrintStats( p->pFrames, NULL );
diff --git a/src/sat/bmc/bmcMulti.c b/src/sat/bmc/bmcMulti.c
index cf04ab62..71085d62 100644
--- a/src/sat/bmc/bmcMulti.c
+++ b/src/sat/bmc/bmcMulti.c
@@ -140,7 +140,7 @@ Aig_Man_t * Gia_ManMultiProveSyn( Aig_Man_t * p, int fVerbose, int fVeryVerbose
     Aig_Man_t * pAig;
     Gia_Man_t * pGia, * pTemp;
     pGia = Gia_ManFromAig( p );
-    pGia = Gia_ManAigSyn2( pTemp = pGia, 0, 0 );
+    pGia = Gia_ManAigSyn2( pTemp = pGia, 1, 0, 0, 0, 0, 0 );
     Gia_ManStop( pTemp );
     pAig = Gia_ManToAig( pGia, 0 );
     Gia_ManStop( pGia );