Version abc60723

7 files changed, 784 insertions, 36 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 02f74f30..eb98c722 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -88,6 +88,11 @@ static int Abc_CommandGen            ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandXyz            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTest           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
+static int Abc_CommandIStrash        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandICut           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandIRewrite       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandIResyn         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 static int Abc_CommandFraig          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFraigTrust     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFraigStore     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -199,6 +204,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "xyz",           Abc_CommandXyz,              1 );
     Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
 
+    Cmd_CommandAdd( pAbc, "New AIG",      "istrash",       Abc_CommandIStrash,          1 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "icut",          Abc_CommandICut,             0 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "irw",           Abc_CommandIRewrite,         1 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "iresyn",        Abc_CommandIResyn,           1 );
+
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_trust",   Abc_CommandFraigTrust,       1 );
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_store",   Abc_CommandFraigStore,       0 );
@@ -4073,10 +4083,12 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
     pParams->fDrop     = 0;     // drop cuts on the fly
     pParams->fDag      = 0;     // compute DAG cuts
     pParams->fTree     = 0;     // compute tree cuts
+    pParams->fGlobal   = 0;     // compute global cuts
+    pParams->fLocal    = 0;     // compute local cuts
     pParams->fFancy    = 0;     // compute something fancy
     pParams->fVerbose  = 0;     // the verbosiness flag
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KMtfdxyzvoh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KMtfdxyglzvoh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -4117,6 +4129,12 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'y':
             pParams->fTree ^= 1;
             break;
+        case 'g':
+            pParams->fGlobal ^= 1;
+            break;
+        case 'l':
+            pParams->fLocal ^= 1;
+            break;
         case 'z':
             pParams->fFancy ^= 1;
             break;
@@ -4178,6 +4196,8 @@ usage:
     fprintf( pErr, "\t-d     : toggle dropping when fanouts are done [default = %s]\n",    pParams->fDrop?    "yes": "no" );
     fprintf( pErr, "\t-x     : toggle computing only DAG cuts [default = %s]\n",           pParams->fDag?     "yes": "no" );
     fprintf( pErr, "\t-y     : toggle computing only tree cuts [default = %s]\n",          pParams->fTree?    "yes": "no" );
+    fprintf( pErr, "\t-g     : toggle computing only global cuts [default = %s]\n",        pParams->fGlobal?  "yes": "no" );
+    fprintf( pErr, "\t-l     : toggle computing only local cuts [default = %s]\n",         pParams->fLocal?   "yes": "no" );
     fprintf( pErr, "\t-z     : toggle fancy computations [default = %s]\n",                pParams->fFancy?   "yes": "no" );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",      pParams->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
@@ -4462,7 +4482,7 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nPlaMax;
     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 fVerbose );
+    extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -4647,11 +4667,11 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Ivy_TruthTest();
 
 
-    Ivy_TruthEstimateNodesTest();
+//    Ivy_TruthEstimateNodesTest();
 
-//    pNtkRes = Abc_NtkIvy( pNtk );
+    pNtkRes = Abc_NtkIvy( pNtk );
 //    pNtkRes = Abc_NtkPlayer( pNtk, nLevels, 0 );
-    pNtkRes = NULL;
+//    pNtkRes = NULL;
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -4670,6 +4690,290 @@ usage:
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandIStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Only works for non-sequential networks.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Only works for combinatinally strashed AIG networks.\n" );
+        return 1;
+    }
+
+    pNtkRes = Abc_NtkIvyStrash( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: istrash [-h]\n" );
+    fprintf( pErr, "\t         perform sequential structural hashing\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandICut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c, nInputs;
+    extern void Abc_NtkIvyCuts( Abc_Ntk_t * pNtk, int nInputs );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nInputs = 5;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Kh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nInputs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nInputs < 0 ) 
+                goto usage;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Only works for non-sequential networks.\n" );
+        return 1;
+    }
+
+    Abc_NtkIvyCuts( pNtk, nInputs );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: icut [-K num] [-h]\n" );
+    fprintf( pErr, "\t         computes sequential cuts of the given size\n" );
+    fprintf( pErr, "\t-K num : the number of cut inputs (2 <= num <= 6) [default = %d]\n", nInputs );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandIRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c, fUpdateLevel, fUseZeroCost, fVerbose;
+    extern Abc_Ntk_t * Abc_NtkIvyRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeroCost, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUpdateLevel = 1;
+    fUseZeroCost = 0;
+    fVerbose     = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "lzvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'l':
+            fUpdateLevel ^= 1;
+            break;
+        case 'z':
+            fUseZeroCost ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Only works for non-sequential networks.\n" );
+        return 1;
+    }
+
+    pNtkRes = Abc_NtkIvyRewrite( pNtk, fUpdateLevel, fUseZeroCost, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: irw [-lzvh]\n" );
+    fprintf( pErr, "\t         perform combinational AIG rewriting\n" );
+    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", fUseZeroCost? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandIResyn( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c, fUpdateLevel, fVerbose;
+    extern Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUpdateLevel = 1;
+    fVerbose     = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "lzvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'l':
+            fUpdateLevel ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Only works for non-sequential networks.\n" );
+        return 1;
+    }
+
+    pNtkRes = Abc_NtkIvyResyn( pNtk, fUpdateLevel, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: iresyn [-lvh]\n" );
+    fprintf( pErr, "\t         performs combinational resynthesis\n" );
+    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index 9e9212aa..389a7977 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -265,6 +265,9 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
     pNodeOld->pCopy = vSuper->pArray[0];
     Abc_HManAddProto( pNodeOld->pCopy, pNodeOld );
     vSuper->nSize = 0;
+//    if ( Abc_ObjRegular(pNodeOld->pCopy) == Abc_NtkConst1(pNtkNew) )
+//        printf( "Constant node\n" );
+//    assert( pNodeOld->Level >= Abc_ObjRegular(pNodeOld->pCopy)->Level );
     return pNodeOld->pCopy;
 }
 
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 135e35d2..00045bf4 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -29,9 +29,10 @@
 static void Abc_NtkPrintCuts( void * p, Abc_Ntk_t * pNtk, int fSeq );
 static void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq );
 
-
 extern int nTotal, nGood, nEqual;
 
+static Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -66,6 +67,13 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     // start the manager
     pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
     p = Cut_ManStart( pParams );
+    // compute node attributes if local or global cuts are requested
+    if ( pParams->fGlobal || pParams->fLocal )
+    {
+        extern Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk );
+        Cut_ManSetNodeAttrs( p, Abc_NtkGetNodeAttributes(pNtk) );
+    }
+    // prepare for cut dropping
     if ( pParams->fDrop )
         Cut_ManSetFanoutCounts( p, Abc_NtkFanoutCounts(pNtk) );
     // set cuts for PIs
@@ -316,6 +324,8 @@ void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
     int fDagNode, fTriv, TreeCode = 0;
 //    assert( Abc_NtkIsStrash(pObj->pNtk) );
     assert( Abc_ObjFaninNum(pObj) == 2 );
+
+
     // check if the node is a DAG node
     fDagNode = (Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj));
     // increment the counter of DAG nodes
@@ -330,6 +340,25 @@ void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
         pFanin = Abc_ObjFanin1(pObj);
         TreeCode |= ((Abc_ObjFanoutNum(pFanin) > 1 && !Abc_NodeIsMuxControlType(pFanin)) << 1);
     }
+
+
+    // changes due to the global/local cut computation
+    {
+        Cut_Params_t * pParams = Cut_ManReadParams(p);
+        if ( pParams->fLocal )
+        {
+            Vec_Int_t * vNodeAttrs = Cut_ManReadNodeAttrs(p);
+            fDagNode = Vec_IntEntry( vNodeAttrs, pObj->Id );
+            if ( fDagNode ) Cut_ManIncrementDagNodes( p );
+//            fTriv = fDagNode || !pParams->fGlobal;
+            fTriv = !Vec_IntEntry( vNodeAttrs, pObj->Id );
+            TreeCode = 0;
+            pFanin = Abc_ObjFanin0(pObj);
+            TreeCode |=  Vec_IntEntry( vNodeAttrs, pFanin->Id );
+            pFanin = Abc_ObjFanin1(pObj);
+            TreeCode |= (Vec_IntEntry( vNodeAttrs, pFanin->Id ) << 1);
+        }
+    }
     return Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
         Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), fTriv, TreeCode );  
 }
@@ -436,6 +465,95 @@ void Abc_NtkPrintCuts_( void * p, Abc_Ntk_t * pNtk, int fSeq )
     Cut_CutPrintList( pList, fSeq );
 }
 
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns global attributes randomly.]
+
+  Description [Old code.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkGetNodeAttributes2( Abc_Ntk_t * pNtk ) 
+{
+    Vec_Int_t * vAttrs;
+    Abc_Obj_t * pObj;
+    int i;
+
+    vAttrs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) + 1 );
+//    Abc_NtkForEachCi( pNtk, pObj, i )
+//        Vec_IntWriteEntry( vAttrs, pObj->Id, 1 );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+//        if ( Abc_ObjIsNode(pObj) && (rand() % 4 == 0) )
+        if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj) && (rand() % 3 == 0) )
+            Vec_IntWriteEntry( vAttrs, pObj->Id, 1 );
+    }
+    return vAttrs; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns global attributes randomly.]
+
+  Description [Old code.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkSubDagSize_rec( Abc_Obj_t * pObj, Vec_Int_t * vAttrs ) 
+{
+    if ( Abc_NodeIsTravIdCurrent(pObj) )
+        return 0;
+    Abc_NodeSetTravIdCurrent(pObj);
+    if ( Vec_IntEntry( vAttrs, pObj->Id ) )
+        return 0;
+    if ( Abc_ObjIsCi(pObj) )
+        return 1;
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    return 1 + Abc_NtkSubDagSize_rec(Abc_ObjFanin0(pObj), vAttrs) +
+        Abc_NtkSubDagSize_rec(Abc_ObjFanin1(pObj), vAttrs);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assigns global attributes randomly.]
+
+  Description [Old code.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk ) 
+{
+    Vec_Int_t * vAttrs;
+    Abc_Obj_t * pObj;
+    int i, nSize;
+    assert( Abc_NtkIsDfsOrdered(pNtk) );
+    vAttrs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) + 1 );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        // skip no-nodes and nodes without fanouts
+        if ( pObj->Id == 0 || !(Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj)) )
+            continue;
+        // the node has more than one fanout - count its sub-DAG size
+        Abc_NtkIncrementTravId( pNtk );
+        nSize = Abc_NtkSubDagSize_rec( pObj, vAttrs );
+        if ( nSize > 15 )
+            Vec_IntWriteEntry( vAttrs, pObj->Id, 1 );
+    }
+    return vAttrs; 
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index c22532e9..49b24be8 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -62,6 +62,9 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int f
         fExdc = 0, printf( "Warning: Networks has no EXDC.\n" );
     // perform fraiging
     pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes, fExdc ); 
+    // add algebraic choices
+    if ( pPars->fChoicing )
+        Fraig_ManAddChoices( pMan, 0, 6 );
     // prove the miter if asked to
     if ( pPars->fTryProve )
         Fraig_ManProveMiter( pMan );
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index f69982a8..1ef84c20 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -27,6 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static Abc_Ntk_t *  Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
+static Abc_Ntk_t *  Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
 static Ivy_Man_t *  Abc_NtkToAig( Abc_Ntk_t * pNtkOld );
 
 static void         Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan );
@@ -36,12 +37,210 @@ static Ivy_Obj_t *  Abc_NodeStrashAigExorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNod
 static Ivy_Obj_t *  Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
 extern char *       Mio_GateReadSop( void * pGate );
 
+typedef int   Abc_Edge_t;
+static inline Abc_Edge_t   Abc_EdgeCreate( int Id, int fCompl )                { return (Id << 1) | fCompl;             }
+static inline int          Abc_EdgeId( Abc_Edge_t Edge )                       { return Edge >> 1;                      }
+static inline int          Abc_EdgeIsComplement( Abc_Edge_t Edge )             { return Edge & 1;                       }
+static inline Abc_Edge_t   Abc_EdgeRegular( Abc_Edge_t Edge )                  { return (Edge >> 1) << 1;               }
+static inline Abc_Edge_t   Abc_EdgeNot( Abc_Edge_t Edge )                      { return Edge ^ 1;                       }
+static inline Abc_Edge_t   Abc_EdgeNotCond( Abc_Edge_t Edge, int fCond )       { return Edge ^ fCond;                   }
+static inline Abc_Edge_t   Abc_EdgeFromNode( Abc_Obj_t * pNode )               { return Abc_EdgeCreate( Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) );       }
+static inline Abc_Obj_t *  Abc_EdgeToNode( Abc_Ntk_t * p, Abc_Edge_t Edge )    { return Abc_ObjNotCond( Abc_NtkObj(p, Abc_EdgeId(Edge)), Abc_EdgeIsComplement(Edge) ); }
+
+static inline Abc_Obj_t *  Abc_ObjFanin0Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ); }
+static inline Abc_Obj_t *  Abc_ObjFanin1Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ); }
+
+static int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Prepares the IVY package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq )
+{
+    Ivy_Man_t * pMan;
+    int fCleanup = 1;
+    assert( !Abc_NtkIsNetlist(pNtk) );
+    assert( !Abc_NtkIsSeq(pNtk) );
+    if ( Abc_NtkIsBddLogic(pNtk) )
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return NULL;
+        }
+    }
+    if ( Abc_NtkCountSelfFeedLatches(pNtk) )
+    {
+        printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
+        return NULL;
+    }
+    // print warning about choice nodes
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+        printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
+    // convert to the AIG manager
+    pMan = Abc_NtkToAig( pNtk );
+    if ( !Ivy_ManCheck( pMan ) )
+    {
+        printf( "AIG check has failed.\n" );
+        Ivy_ManStop( pMan );
+        return NULL;
+    }
+//    Ivy_ManPrintStats( pMan );
+    if ( fSeq )
+    {
+        int nLatches = Abc_NtkLatchNum(pNtk);
+        int * pInit = Abc_NtkCollectLatchValues( pNtk );
+        Ivy_ManMakeSeq( pMan, nLatches, pInit );
+        FREE( pInit );
+//        Ivy_ManPrintStats( pMan );
+    }
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the IVY package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkIvyAfter( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, int fSeq )
+{
+    Abc_Ntk_t * pNtkAig;
+    int nNodes, fCleanup = 1;
+    // convert from the AIG manager
+    if ( fSeq )
+        pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan );
+    else
+        pNtkAig = Abc_NtkFromAig( pNtk, pMan );
+    // report the cleanup results
+    if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
+        printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
+    // duplicate EXDC 
+    if ( pNtk->pExdc )
+        pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkAig ) )
+    {
+        printf( "Abc_NtkStrash: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkAig );
+        return NULL;
+    }
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkIvyStrash( Abc_Ntk_t * pNtk )
+{
+    Abc_Ntk_t * pNtkAig;
+    Ivy_Man_t * pMan;
+    pMan = Abc_NtkIvyBefore( pNtk, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 1 );
+    Ivy_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkIvyCuts( Abc_Ntk_t * pNtk, int nInputs )
+{
+    extern void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs );
+    Ivy_Man_t * pMan;
+    pMan = Abc_NtkIvyBefore( pNtk, 1 );
+    if ( pMan == NULL )
+        return;
+    Ivy_CutComputeAll( pMan, nInputs );
+    Ivy_ManStop( pMan );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkIvyRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeroCost, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Ivy_Man_t * pMan;
+    pMan = Abc_NtkIvyBefore( pNtk, 0 );
+    if ( pMan == NULL )
+        return NULL;
+    Ivy_ManRewritePre( pMan, fUpdateLevel, fUseZeroCost, fVerbose );
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0 );
+    Ivy_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Ivy_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkIvyBefore( pNtk, 0 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Ivy_ManResyn( pTemp = pMan, fUpdateLevel, fVerbose );
+    Ivy_ManStop( pTemp );
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0 );
+    Ivy_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
 
   Description []
@@ -53,10 +252,12 @@ extern char *       Mio_GateReadSop( void * pGate );
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 {
-    Ivy_Man_t * pMan, * pTemp = NULL;
     Abc_Ntk_t * pNtkAig;
+    Ivy_Man_t * pMan, * pTemp;
     int fCleanup = 1;
     int nNodes;
+    int nLatches = Abc_NtkLatchNum(pNtk);
+    int * pInit = Abc_NtkCollectLatchValues( pNtk );
 
     assert( !Abc_NtkIsNetlist(pNtk) );
     assert( !Abc_NtkIsSeq(pNtk) );
@@ -64,10 +265,17 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
     {
         if ( !Abc_NtkBddToSop(pNtk, 0) )
         {
+            FREE( pInit );
             printf( "Converting to SOPs has failed.\n" );
             return NULL;
         }
     }
+    if ( Abc_NtkCountSelfFeedLatches(pNtk) )
+    {
+        printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
+        return NULL;
+    }
+
     // print warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
@@ -76,6 +284,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
     pMan = Abc_NtkToAig( pNtk );
     if ( !Ivy_ManCheck( pMan ) )
     {
+        FREE( pInit );
         printf( "AIG check has failed.\n" );
         Ivy_ManStop( pMan );
         return NULL;
@@ -92,21 +301,27 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 //    Ivy_ManTestCutsBool( pMan );
 //    Ivy_ManRewriteAlg( pMan, 1, 1 );
 
-//    pMan = Ivy_ManResyn( pTemp = pMan, 1 );
+//    pMan = Ivy_ManResyn( pTemp = pMan, 1, 0 );
 //    Ivy_ManStop( pTemp );
 
-//    Ivy_ManTestCutsAll( pMan );
+    Ivy_ManTestCutsAll( pMan );
 
 //    Ivy_ManPrintStats( pMan );
 
 //    Ivy_ManPrintStats( pMan );
 //    Ivy_ManRewritePre( pMan, 1, 0, 0 );
 //    Ivy_ManPrintStats( pMan );
+//    printf( "\n" );
+
+//    Ivy_ManPrintStats( pMan );
+//    Ivy_ManMakeSeq( pMan, nLatches, pInit );
+//    Ivy_ManPrintStats( pMan );
 
 //    Ivy_ManRequiredLevels( pMan );
 
     // convert from the AIG manager
     pNtkAig = Abc_NtkFromAig( pNtk, pMan );
+//    pNtkAig = Abc_NtkFromAigSeq( pNtk, pMan );
     Ivy_ManStop( pMan );
 
     // report the cleanup results
@@ -118,13 +333,18 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
     // make sure everything is okay
     if ( !Abc_NtkCheck( pNtkAig ) )
     {
+        FREE( pInit );
         printf( "Abc_NtkStrash: The network check has failed.\n" );
         Abc_NtkDelete( pNtkAig );
         return NULL;
     }
+
+    FREE( pInit );
     return pNtkAig;
 }
 
+
+
 /**Function*************************************************************
 
   Synopsis    [Converts the network from the AIG manager into ABC.]
@@ -142,47 +362,119 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
     Ivy_Obj_t * pNode;
-    int i, Fanin;
+    int i;
     // perform strashing
     pNtk = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
     // transfer the pointers to the basic nodes
-    Ivy_ManConst1(pMan)->TravId = (Abc_NtkConst1(pNtk)->Id << 1);
+    Ivy_ManConst1(pMan)->TravId = Abc_EdgeFromNode( Abc_NtkConst1(pNtk) );
     Abc_NtkForEachCi( pNtkOld, pObj, i )
-        Ivy_ManPi(pMan, i)->TravId = (pObj->pCopy->Id << 1);
+        Ivy_ManPi(pMan, i)->TravId = Abc_EdgeFromNode( pObj->pCopy );
     // rebuild the AIG
     vNodes = Ivy_ManDfs( pMan );
     Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i )
     {
         // add the first fanins
-        Fanin = Ivy_ObjFanin0(pNode)->TravId;
-        pFaninNew0 = Abc_NtkObj( pNtk, Fanin >> 1 );
-        pFaninNew0 = Abc_ObjNotCond( pFaninNew0, Ivy_ObjFaninC0(pNode) ^ (Fanin&1) );
+        pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode );
         if ( Ivy_ObjIsBuf(pNode) )
         {
-            pNode->TravId = (Abc_ObjRegular(pFaninNew0)->Id << 1) | Abc_ObjIsComplement(pFaninNew0);
+            pNode->TravId = Abc_EdgeFromNode( pFaninNew0 );
             continue;
         }
         // add the first second
-        Fanin = Ivy_ObjFanin1(pNode)->TravId;
-        pFaninNew1 = Abc_NtkObj( pNtk, Fanin >> 1 );
-        pFaninNew1 = Abc_ObjNotCond( pFaninNew1, Ivy_ObjFaninC1(pNode) ^ (Fanin&1) );
+        pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode );
         // create the new node
         if ( Ivy_ObjIsExor(pNode) )
             pObjNew = Abc_AigXor( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
         else
             pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
-        pNode->TravId = (Abc_ObjRegular(pObjNew)->Id << 1) | Abc_ObjIsComplement(pObjNew);
+        pNode->TravId = Abc_EdgeFromNode( pObjNew );
     }
-    Vec_IntFree( vNodes );
     // connect the PO nodes
     Abc_NtkForEachCo( pNtkOld, pObj, i )
     {
-        pNode = Ivy_ManPo(pMan, i);
-        Fanin = Ivy_ObjFanin0(pNode)->TravId;
-        pFaninNew = Abc_NtkObj( pNtk, Fanin >> 1 );
-        pFaninNew = Abc_ObjNotCond( pFaninNew, Ivy_ObjFaninC0(pNode) ^ (Fanin&1) );
+        pFaninNew = Abc_ObjFanin0Ivy( pNtk, Ivy_ManPo(pMan, i) );
         Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
     }
+    Vec_IntFree( vNodes );
+    if ( !Abc_NtkCheck( pNtk ) )
+        fprintf( stdout, "Abc_NtkFromAig(): Network check has failed.\n" );
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
+{
+    Vec_Int_t * vNodes, * vLatches;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
+    Ivy_Obj_t * pNode;
+    int i;
+    assert( Ivy_ManLatchNum(pMan) > 0 );
+    // perform strashing
+    pNtk = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // transfer the pointers to the basic nodes
+    Ivy_ManConst1(pMan)->TravId = Abc_EdgeFromNode( Abc_NtkConst1(pNtk) );
+    Abc_NtkForEachPi( pNtkOld, pObj, i )
+        Ivy_ManPi(pMan, i)->TravId = Abc_EdgeFromNode( pObj->pCopy );
+    // create latches of the new network
+    vNodes = Ivy_ManDfsSeq( pMan, &vLatches );
+    Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i )
+    {
+        pObjNew = Abc_NtkCreateLatch( pNtk );
+        if ( Ivy_ObjInit(pNode) == IVY_INIT_DC )
+            Abc_LatchSetInitDc( pObjNew );
+        else if ( Ivy_ObjInit(pNode) == IVY_INIT_1 )
+            Abc_LatchSetInit1( pObjNew );
+        else if ( Ivy_ObjInit(pNode) == IVY_INIT_0 )
+            Abc_LatchSetInit0( pObjNew );
+        else assert( 0 );
+        pNode->TravId = Abc_EdgeFromNode( pObjNew );
+    }
+    // rebuild the AIG
+    Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i )
+    {
+        // add the first fanins
+        pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode );
+        if ( Ivy_ObjIsBuf(pNode) )
+        {
+            pNode->TravId = Abc_EdgeFromNode( pFaninNew0 );
+            continue;
+        }
+        // add the first second
+        pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode );
+        // create the new node
+        if ( Ivy_ObjIsExor(pNode) )
+            pObjNew = Abc_AigXor( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
+        else
+            pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
+        pNode->TravId = Abc_EdgeFromNode( pObjNew );
+    }
+    // connect the PO nodes
+    Abc_NtkForEachPo( pNtkOld, pObj, i )
+    {
+        pFaninNew = Abc_ObjFanin0Ivy( pNtk, Ivy_ManPo(pMan, i) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+    // connect the latches
+    Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i )
+    {
+        pFaninNew = Abc_ObjFanin0Ivy( pNtk, pNode );
+        Abc_ObjAddFanin( Abc_NtkLatch(pNtk, i), pFaninNew );
+    }
+    Vec_IntFree( vLatches );
+    Vec_IntFree( vNodes );
+    if ( !Abc_NtkCheck( pNtk ) )
+        fprintf( stdout, "Abc_NtkFromAigSeq(): Network check has failed.\n" );
     return pNtk;
 }
 
@@ -205,14 +497,11 @@ Ivy_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld )
     int i;
     // create the manager
     assert( Abc_NtkHasSop(pNtkOld) || Abc_NtkHasAig(pNtkOld) );
-    if ( Abc_NtkHasSop(pNtkOld) )
-        pMan = Ivy_ManStart( Abc_NtkCiNum(pNtkOld), Abc_NtkCoNum(pNtkOld), Abc_NtkGetLitNum(pNtkOld) + 1000 );
-    else
-        pMan = Ivy_ManStart( Abc_NtkCiNum(pNtkOld), Abc_NtkCoNum(pNtkOld), Abc_NtkNodeNum(pNtkOld) + 1000 );
+    pMan = Ivy_ManStart();
     // create the PIs
     Abc_NtkConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Ivy_ManConst1(pMan);
     Abc_NtkForEachCi( pNtkOld, pObj, i )
-        pObj->pCopy = (Abc_Obj_t *)Ivy_ManPi(pMan, i);
+        pObj->pCopy = (Abc_Obj_t *)Ivy_ObjCreatePi(pMan);
     // perform the conversion of the internal nodes
     Abc_NtkStrashPerformAig( pNtkOld, pMan );
     // create the POs
@@ -220,7 +509,7 @@ Ivy_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld )
     {
         pFanin = (Ivy_Obj_t *)Abc_ObjFanin0(pObj)->pCopy;
         pFanin = Ivy_NotCond( pFanin, Abc_ObjFaninC0(pObj) );
-        Ivy_ObjConnect( Ivy_ManPo(pMan, i), pFanin );
+        Ivy_ObjCreatePo( pMan, pFanin );
     }
     Ivy_ManCleanup( pMan );
     return pMan;
@@ -283,7 +572,7 @@ Ivy_Obj_t * Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode )
         pFanin0 = Ivy_NotCond( pFanin0, Abc_ObjFaninC0(pNode) );
         pFanin1 = (Ivy_Obj_t *)Abc_ObjFanin1(pNode)->pCopy;
         pFanin1 = Ivy_NotCond( pFanin1, Abc_ObjFaninC1(pNode) );
-        return Ivy_And( pFanin0, pFanin1 );
+        return Ivy_And( pMan, pFanin0, pFanin1 );
     }
 
     // get the SOP of the node
@@ -336,12 +625,12 @@ Ivy_Obj_t * Abc_NodeStrashAigSopAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char *
         Abc_ObjForEachFanin( pNode, pFanin, i ) // pFanin can be a net
         {
             if ( pCube[i] == '1' )
-                pAnd = Ivy_And( pAnd, (Ivy_Obj_t *)pFanin->pCopy );
+                pAnd = Ivy_And( pMan, pAnd, (Ivy_Obj_t *)pFanin->pCopy );
             else if ( pCube[i] == '0' )
-                pAnd = Ivy_And( pAnd, Ivy_Not((Ivy_Obj_t *)pFanin->pCopy) );
+                pAnd = Ivy_And( pMan, pAnd, Ivy_Not((Ivy_Obj_t *)pFanin->pCopy) );
         }
         // add to the sum of cubes
-        pSum = Ivy_Or( pSum, pAnd );
+        pSum = Ivy_Or( pMan, pSum, pAnd );
     }
     // decide whether to complement the result
     if ( Abc_SopIsComplement(pSop) )
@@ -373,7 +662,7 @@ Ivy_Obj_t * Abc_NodeStrashAigExorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char
     for ( i = 0; i < nFanins; i++ )
     {
         pFanin = Abc_ObjFanin( pNode, i );
-        pSum = Ivy_Exor( pSum, (Ivy_Obj_t *)pFanin->pCopy );
+        pSum = Ivy_Exor( pMan, pSum, (Ivy_Obj_t *)pFanin->pCopy );
     }
     if ( Abc_SopIsComplement(pSop) )
         pSum = Ivy_Not(pSum);
@@ -417,6 +706,35 @@ Ivy_Obj_t * Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pRoot, cha
     return pAnd;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pLatch;
+    int * pArray, i;
+    pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        if ( Abc_LatchIsInitDc(pLatch) )
+            pArray[i] = IVY_INIT_DC;
+        else if ( Abc_LatchIsInit1(pLatch) )
+            pArray[i] = IVY_INIT_1;
+        else if ( Abc_LatchIsInit0(pLatch) )
+            pArray[i] = IVY_INIT_0;
+        else assert( 0 );
+    }
+    return pArray;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index a3cd227d..0124d7bf 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -185,6 +185,7 @@ void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk )
     fprintf( pFile, "Primary inputs (%d): ", Abc_NtkPiNum(pNtk) );    
     Abc_NtkForEachPi( pNtk, pObj, i )
         fprintf( pFile, " %s", Abc_ObjName(pObj) );
+//        fprintf( pFile, " %s(%d)", Abc_ObjName(pObj), Abc_ObjFanoutNum(pObj) );
     fprintf( pFile, "\n" );   
 
     fprintf( pFile, "Primary outputs (%d):", Abc_NtkPoNum(pNtk) );    
diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c
index 10400129..a81e94ad 100644
--- a/src/base/abci/abcReconv.c
+++ b/src/base/abci/abcReconv.c
@@ -321,6 +321,7 @@ int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int
     {
         CostCur = Abc_NodeGetLeafCostOne( pNode, nFaninLimit );
 //printf( "    Fanin %s has cost %d.\n", Abc_ObjName(pNode), CostCur );
+//        if ( CostBest > CostCur ) // performance improvement: expand the variable with the smallest level
         if ( CostBest > CostCur ||
              (CostBest == CostCur && pNode->Level > pFaninBest->Level) )
         {