diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b104f618a..4eee95227 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -468,6 +468,9 @@ static int Abc_CommandAbc9Times              ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Frames             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Retime             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Enable             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Resyn3             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Resyn3rs           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Compress3rs        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Dc2                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Dsd                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Bidec              ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1299,6 +1302,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&frames",       Abc_CommandAbc9Frames,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&retime",       Abc_CommandAbc9Retime,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&enable",       Abc_CommandAbc9Enable,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&resyn3",       Abc_CommandAbc9Resyn3,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&resyn3rs",     Abc_CommandAbc9Resyn3rs,     0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&compress3rs",  Abc_CommandAbc9Compress3rs,  0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&dc2",          Abc_CommandAbc9Dc2,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&dsd",          Abc_CommandAbc9Dsd,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&bidec",        Abc_CommandAbc9Bidec,        0 );
@@ -39197,6 +39203,147 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Resyn3( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManResyn3( Gia_Man_t * pGia, int fVerbose );
+    Gia_Man_t * pTemp;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Resyn3(): There is no AIG.\n" );
+        return 1;
+    }
+    pTemp = Gia_ManResyn3( pAbc->pGia, fVerbose );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &resyn3 [-vh]\n" );
+    Abc_Print( -2, "\t         performs rewriting of the AIG while preserving logic level\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Resyn3rs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManCompress3rs( Gia_Man_t * pGia, int fUpdateLevel, int fVerbose );
+    Gia_Man_t * pTemp;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Resyn3rs(): There is no AIG.\n" );
+        return 1;
+    }
+    pTemp = Gia_ManCompress3rs( pAbc->pGia, 1, fVerbose );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &resyn3rs [-vh]\n" );
+    Abc_Print( -2, "\t         performs rewriting of the AIG while preserving logic level\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Compress3rs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_ManCompress3rs( Gia_Man_t * pGia, int fUpdateLevel, int fVerbose );
+    Gia_Man_t * pTemp;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Compress3rs(): There is no AIG.\n" );
+        return 1;
+    }
+    pTemp = Gia_ManCompress3rs( pAbc->pGia, 0, fVerbose );
+    Abc_FrameUpdateGia( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &compress3rs [-vh]\n" );
+    Abc_Print( -2, "\t         performs rewriting of the AIG without preserving logic level\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index e7874b0ea..6b0322361 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -662,6 +662,45 @@ Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManResub( Aig_Man_t * pMan, int nCutsMax, int nNodesMax, int fUpdateLevel, int fUseZeros, int fVerbose )
+{
+    extern int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nMinSaved, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose, int Log2Probs, int Log2Divs );
+    Abc_Ntk_t * pNtk = Abc_NtkFromAigPhase( pMan );
+    Aig_Man_t * pRes = NULL;
+    char * pName = NULL, * pSpec = NULL;
+    int nMinSaved = fUseZeros ? 0 : 1;
+    if ( pMan->pName )
+        pName = Abc_UtilStrsav( pMan->pName );
+    if ( pMan->pSpec )
+        pSpec = Abc_UtilStrsav( pMan->pSpec );
+    if ( pName )
+    {
+        ABC_FREE( pNtk->pName );
+        pNtk->pName = pName;
+    }
+    if ( pSpec )
+    {
+        ABC_FREE( pNtk->pSpec );
+        pNtk->pSpec = pSpec;
+    }
+    if ( !Abc_NtkResubstitute( pNtk, nCutsMax, nNodesMax, nMinSaved, 0, fUpdateLevel, fVerbose, 0, 0, 0 ) )
+        Abc_Print( 0, "Dar_ManResub(): Resubstitution has failed.\n" );
+    pRes = Abc_NtkToDar( pNtk, 0, 1 );
+    Abc_NtkDelete( pNtk );
+    return pRes;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -5181,4 +5220,3 @@ Gia_Man_t * Abc_NtkDarTestFiles()
 
 #include "abcDarUnfold2.c"
 ABC_NAMESPACE_IMPL_END
-
diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c
index 8cb30bddb..9bb1965f9 100644
--- a/src/opt/dar/darScript.c
+++ b/src/opt/dar/darScript.c
@@ -907,6 +907,244 @@ pPars->timeSynth = Abc_Clock() - clk;
     return pMan;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Reproduces script "resyn2".]
+
+  Description [Equivalent to: b; rw; rf; b; rw; rwz; b; rfz; rwz; b.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManResyn3( Gia_Man_t * pGia, int fVerbose )
+{
+    Gia_Man_t * pGiaRes;
+    Aig_Man_t * pAig, * pTemp;
+    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
+    int fUpdateLevel = 1;
+
+    if ( pGia->pManTime && pGia->vLevels == NULL )
+        Gia_ManLevelWithBoxes( pGia );
+
+    Dar_ManDefaultRwrParams( pParsRwr );
+    Dar_ManDefaultRefParams( pParsRef );
+    pParsRwr->nCutsMax = 250;
+    pParsRef->nLeafMax = 10;
+    pParsRef->nMffcMin = 1;
+    pParsRwr->fUpdateLevel = fUpdateLevel;
+    pParsRef->fUpdateLevel = fUpdateLevel;
+    pParsRwr->fVerbose = 0;
+    pParsRef->fVerbose = 0;
+
+    pAig = Gia_ManToAig( pGia, 0 );
+    if ( fVerbose ) printf( "Starting:  " ), Aig_ManPrintStats( pAig );
+
+    // b
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
+
+    // rw
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDupDfs( pTemp = pAig );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
+
+    // rf
+    Dar_ManRefactor( pAig, pParsRef );
+    pAig = Aig_ManDupDfs( pTemp = pAig );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Refactor:  " ), Aig_ManPrintStats( pAig );
+
+    // b
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
+
+    // rw
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDupDfs( pTemp = pAig );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
+
+    // rwz
+    pParsRwr->fUseZeros = 1;
+    pParsRef->fUseZeros = 1;
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDupDfs( pTemp = pAig );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "RewriteZ:  " ), Aig_ManPrintStats( pAig );
+
+    // b
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
+
+    // rfz
+    Dar_ManRefactor( pAig, pParsRef );
+    pAig = Aig_ManDupDfs( pTemp = pAig );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "RefactorZ: " ), Aig_ManPrintStats( pAig );
+
+    // rwz
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDupDfs( pTemp = pAig );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "RewriteZ:  " ), Aig_ManPrintStats( pAig );
+
+    // b
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
+
+    pGiaRes = Gia_ManFromAig( pAig );
+    Aig_ManStop( pAig );
+    Gia_ManTransferTiming( pGiaRes, pGia );
+    return pGiaRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reproduces script "compress2rs".]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManCompress3rs( Gia_Man_t * pGia, int fUpdateLevel, int fVerbose )
+{
+    Gia_Man_t * pGiaRes;
+    Aig_Man_t * pAig, * pTemp;
+    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
+    extern Aig_Man_t * Dar_ManResub( Aig_Man_t * pAig, int nCutsMax, int nNodesMax, int fUpdateLevel, int fUseZeros, int fVerbose );
+
+    if ( pGia->pManTime && pGia->vLevels == NULL )
+        Gia_ManLevelWithBoxes( pGia );
+
+    Dar_ManDefaultRwrParams( pParsRwr );
+    Dar_ManDefaultRefParams( pParsRef );
+    pParsRwr->nCutsMax = 250;
+    pParsRef->nLeafMax = 10;
+    pParsRef->nMffcMin = 1;
+    pParsRwr->fUpdateLevel = fUpdateLevel;
+    pParsRef->fUpdateLevel = fUpdateLevel;
+    pParsRwr->fVerbose = 0;
+    pParsRef->fVerbose = 0;
+
+    pAig = Gia_ManToAig( pGia, 0 );
+    if ( fVerbose ) printf( "Starting:  " ), Aig_ManPrintStats( pAig );
+
+    // b -l
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
+
+    // rs -K 6 -l
+    pAig = Dar_ManResub( pTemp = pAig, 6, 1, fUpdateLevel, 0, 0 );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Resub6:    " ), Aig_ManPrintStats( pAig );
+
+    // rw -l
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDupDfs( pTemp = pAig );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
+
+    // rs -K 6 -N 2 -l
+    pAig = Dar_ManResub( pTemp = pAig, 6, 2, fUpdateLevel, 0, 0 );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Resub6x2:  " ), Aig_ManPrintStats( pAig );
+
+    // rf -l
+    Dar_ManRefactor( pAig, pParsRef );
+    pAig = Aig_ManDupDfs( pTemp = pAig );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Refactor:  " ), Aig_ManPrintStats( pAig );
+
+    // rs -K 8 -l
+    pAig = Dar_ManResub( pTemp = pAig, 8, 1, fUpdateLevel, 0, 0 );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Resub8:    " ), Aig_ManPrintStats( pAig );
+
+    // b -l
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
+
+    // rs -K 8 -N 2 -l
+    pAig = Dar_ManResub( pTemp = pAig, 8, 2, fUpdateLevel, 0, 0 );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Resub8x2:  " ), Aig_ManPrintStats( pAig );
+
+    // rw -l
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDupDfs( pTemp = pAig );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Rewrite:   " ), Aig_ManPrintStats( pAig );
+
+    // rs -K 10 -l
+    pAig = Dar_ManResub( pTemp = pAig, 10, 1, fUpdateLevel, 0, 0 );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Resub10:   " ), Aig_ManPrintStats( pAig );
+
+    // rwz -l
+    pParsRwr->fUseZeros = 1;
+    pParsRef->fUseZeros = 1;
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDupDfs( pTemp = pAig );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "RewriteZ:  " ), Aig_ManPrintStats( pAig );
+
+    // rs -K 10 -N 2 -l
+    pAig = Dar_ManResub( pTemp = pAig, 10, 2, fUpdateLevel, 0, 0 );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Resub10x2: " ), Aig_ManPrintStats( pAig );
+
+    // b -l
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
+
+    // rs -K 12 -l
+    pAig = Dar_ManResub( pTemp = pAig, 12, 1, fUpdateLevel, 0, 0 );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Resub12:   " ), Aig_ManPrintStats( pAig );
+
+    // rfz -l
+    Dar_ManRefactor( pAig, pParsRef );
+    pAig = Aig_ManDupDfs( pTemp = pAig );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "RefactorZ: " ), Aig_ManPrintStats( pAig );
+
+    // rs -K 12 -N 2 -l
+    pAig = Dar_ManResub( pTemp = pAig, 12, 2, fUpdateLevel, 0, 0 );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Resub12x2: " ), Aig_ManPrintStats( pAig );
+
+    // rwz -l
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDupDfs( pTemp = pAig );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "RewriteZ:  " ), Aig_ManPrintStats( pAig );
+
+    // b -l
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) printf( "Balance:   " ), Aig_ManPrintStats( pAig );
+
+    pGiaRes = Gia_ManFromAig( pAig );
+    Aig_ManStop( pAig );
+    Gia_ManTransferTiming( pGiaRes, pGia );
+    return pGiaRes;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
@@ -914,4 +1152,3 @@ pPars->timeSynth = Abc_Clock() - clk;
 
 
 ABC_NAMESPACE_IMPL_END
-