Version abc60804

5 files changed, 33 insertions, 18 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7bee7f40..bb8f5658 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -4487,22 +4487,26 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nPlaMax;
     int RankCost;
     int fFastMode;
+    int fRewriting;
+    int fSynthesis;
     int fVerbose;
-//    extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nPlaMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
-    extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose );
+//    extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nPlaMax, bool fEsop, bool fSop, bool fInvs, bool fVerbose );
+    extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nLutMax   = 8;
-    nPlaMax   = 128;
-    RankCost  = 96000;
-    fFastMode = 0;
-    fVerbose  = 0;
+    nLutMax    = 8;
+    nPlaMax    = 128;
+    RankCost   = 96000;
+    fFastMode  = 1;
+    fRewriting = 1;
+    fSynthesis = 0;
+    fVerbose   = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "LPRfvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "LPRfrsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4542,6 +4546,12 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'f':
             fFastMode ^= 1;
             break;
+        case 'r':
+            fRewriting ^= 1;
+            break;
+        case 's':
+            fSynthesis ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -4570,8 +4580,8 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // run the command
-//    pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fUseInvs, fVerbose );
-    pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fVerbose );
+//    pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fInvs, fVerbose );
+    pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -4582,12 +4592,14 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: xyz [-L num] [-P num] [-R num] [-fvh]\n" );
+    fprintf( pErr, "usage: xyz [-L num] [-P num] [-R num] [-frsvh]\n" );
     fprintf( pErr, "\t         specilized LUT/PLA decomposition\n" );
     fprintf( pErr, "\t-L num : maximum number of LUT inputs (2<=num<=8) [default = %d]\n", nLutMax );
     fprintf( pErr, "\t-P num : maximum number of PLA inputs/cubes (8<=num<=128) [default = %d]\n", nPlaMax );
     fprintf( pErr, "\t-R num : maximum are of one decomposition rank [default = %d]\n", RankCost );
     fprintf( pErr, "\t-f     : toggle using fast LUT mapping mode [default = %s]\n", fFastMode? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggle using one pass of AIG rewriting [default = %s]\n", fRewriting? "yes": "no" );
+    fprintf( pErr, "\t-s     : toggle using synthesis by AIG rewriting [default = %s]\n", fSynthesis? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index a3ffcf4e..380b3f8b 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -343,9 +343,11 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 
 //    Ivy_ManRequiredLevels( pMan );
 
-    Pla_ManFastLutMap( pMan, 8 );
-    Ivy_ManStop( pMan );
+//    Pla_ManFastLutMap( pMan, 8 );
+//    Ivy_ManStop( pMan );
     return NULL;
+
+
 /*
     // convert from the AIG manager
     pNtkAig = Abc_NtkFromAig( pNtk, pMan );
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index f447516f..b8491d06 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -408,7 +408,7 @@ void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNo
 int Abc_NtkNodeFactor( Abc_Obj_t * pObj, int nLevelMax )
 {
 //  nLevelMax = ((nLevelMax)/2)*3;
-    assert( pObj->Level <= nLevelMax );
+    assert( (int)pObj->Level <= nLevelMax );
 //    return (int)(100000000.0 * pow(0.999, nLevelMax - pObj->Level));
     return (int)(100000000.0 * (1 + 0.01 * pObj->Level));
 //    return (int)(100000000.0 / ((nLevelMax)/2)*3 - pObj->Level);
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index a40954bd..d2d731d9 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -647,9 +647,10 @@ void Abc_NtkStartReverseLevels( Abc_Ntk_t * pNtk )
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pObj, * pFanout;
     int i, k, nLevelsCur;
-    assert( Abc_NtkIsStrash(pNtk) );
+//    assert( Abc_NtkIsStrash(pNtk) );
     // remember the maximum number of direct levels
-    pNtk->LevelMax = Abc_AigGetLevelNum(pNtk);
+//    pNtk->LevelMax = Abc_AigGetLevelNum(pNtk);
+    pNtk->LevelMax = Abc_NtkGetLevelNum(pNtk);
     // start the reverse levels
     pNtk->vLevelsR = Vec_IntAlloc( 0 );
     Vec_IntFill( pNtk->vLevelsR, Abc_NtkObjNumMax(pNtk), 0 );
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index ecf77f70..5c4a0675 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -136,11 +136,11 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
 {
     extern void Rwt_ManGlobalStop();
     extern void undefine_cube_size();
-    extern void Ivy_TruthManStop();
+//    extern void Ivy_TruthManStop();
 //    Abc_HManStop();
     undefine_cube_size();
     Rwt_ManGlobalStop();
-    Ivy_TruthManStop();
+//    Ivy_TruthManStop();
     if ( p->pManDec ) Dec_ManStop( p->pManDec );
     if ( p->dd )      Extra_StopManager( p->dd );
     Abc_FrameDeleteAllNetworks( p );