Version abc70731

5 files changed, 214 insertions, 31 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8ae5bb9e..3a916fdc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -157,6 +157,7 @@ static int Abc_CommandIf             ( Abc_Frame_t * pAbc, int argc, char ** arg
 
 static int Abc_CommandScut           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandInit           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandZero           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPipe           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeq            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandUnseq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -320,6 +321,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
 //    Cmd_CommandAdd( pAbc, "Sequential",   "scut",          Abc_CommandScut,             0 );
     Cmd_CommandAdd( pAbc, "Sequential",   "init",          Abc_CommandInit,             1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "zero",          Abc_CommandZero,             1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "pipe",          Abc_CommandPipe,             1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "seq",           Abc_CommandSeq,              1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "unseq",         Abc_CommandUnseq,            1 );
@@ -371,6 +373,10 @@ void Abc_End()
 //    Dar_LibDumpPriorities();
 
     {
+        extern void Cnf_ClearMemory();
+        Cnf_ClearMemory();
+    }
+    {
         extern void Dar_LibStop();
         Dar_LibStop();
     }
@@ -4080,19 +4086,20 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "The network is not strashed.\n" );
         return 1;
     }
-
+/*
     if ( Abc_NtkPoNum(pNtk) == 1 )
     {
         fprintf( pErr, "The network already has one PO.\n" );
         return 1;
     }
-
+*/
+/*
     if ( Abc_NtkLatchNum(pNtk) )
     {
         fprintf( pErr, "The miter has latches. ORing is not performed.\n" );
         return 1;
     }
-
+*/
     // get the new network
     if ( !Abc_NtkCombinePos( pNtk, 0 ) )
     {
@@ -10113,6 +10120,78 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandZero( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+
+    extern Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup );
+
+    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_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "The current network is combinational.\n" );
+        return 0;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for AIGs.\n" );
+        return 0;
+    }
+
+    // get the new network
+    pNtkRes = Abc_NtkRestrashZero( pNtk, 0 );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Converting to sequential AIG has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: zero [-h]\n" );
+    fprintf( pErr, "\t        converts latches to have const-0 initial value\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandPipe( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -10736,8 +10815,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nFramesK;
     int fExdc;
     int fImp;
+    int fRewrite;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -10747,9 +10827,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     nFramesK = 1;
     fExdc    = 1;
     fImp     = 0;
+    fRewrite = 0;
     fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Feivh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Feirvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10770,6 +10851,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'i':
             fImp ^= 1;
             break;
+        case 'r':
+            fRewrite ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -10799,7 +10883,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fVerbose );
+    pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -10810,11 +10894,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ssweep [-F num] [-eivh]\n" );
-    fprintf( pErr, "\t         performs sequential sweep using van Eijk's method\n" );
+    fprintf( pErr, "usage: ssweep [-F num] [-rvh]\n" );
+    fprintf( pErr, "\t         performs sequential sweep using K-step induction\n" );
     fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
 //    fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
 //    fprintf( pErr, "\t-i     : toggle computing implications [default = %s]\n", fImp? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 035daeff..ca80fec8 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -36,24 +36,48 @@
 
   Synopsis    [Converts the network from the AIG manager into ABC.]
 
-  Description []
+  Description [Assumes that registers are ordered after PIs/POs.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
+Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
 {
     Aig_Man_t * pMan;
+    Aig_Obj_t * pObjNew;
     Abc_Obj_t * pObj;
-    int i;
+    int i, nNodes;
+    // make sure the latches follow PIs/POs
+    if ( fRegisters )
+    {
+        assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
+        Abc_NtkForEachCi( pNtk, pObj, i )
+            if ( i < Abc_NtkPiNum(pNtk) )
+                assert( Abc_ObjIsPi(pObj) );
+            else
+                assert( Abc_ObjIsBo(pObj) );
+        Abc_NtkForEachCo( pNtk, pObj, i )
+            if ( i < Abc_NtkPoNum(pNtk) )
+                assert( Abc_ObjIsPo(pObj) );
+            else
+                assert( Abc_ObjIsBi(pObj) );
+    }
     // create the manager
     pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
+    // save the number of registers
+    if ( fRegisters )
+        pMan->nRegs = Abc_NtkLatchNum(pNtk);
     // transfer the pointers to the basic nodes
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
     Abc_NtkForEachCi( pNtk, pObj, i )
         pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreatePi(pMan);
+    // complement the 1-values registers
+    if ( fRegisters )
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            if ( Abc_LatchIsInit1(pObj) )
+                Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
     // perform the conversion of the internal nodes (assumes DFS ordering)
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
@@ -63,7 +87,14 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
     // create the POs
     Abc_NtkForEachCo( pNtk, pObj, i )
         Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
-    Aig_ManCleanup( pMan );
+    // complement the 1-valued registers
+    if ( fRegisters )
+        Aig_ManForEachLiSeq( pMan, pObjNew, i )
+            if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
+                pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
+    // remove dangling nodes
+    if ( nNodes = Aig_ManCleanup( pMan ) )
+        printf( "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
     if ( !Aig_ManCheck( pMan ) )
     {
         printf( "Abc_NtkToDar: AIG check has failed.\n" );
@@ -296,8 +327,8 @@ void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0));
 
 
-    pMan1 = Abc_NtkToDar( pNtk1 );
-    pMan2 = Abc_NtkToDar( pNtk2 );
+    pMan1 = Abc_NtkToDar( pNtk1, 0 );
+    pMan2 = Abc_NtkToDar( pNtk2, 0 );
 
     Aig_ManPrintStats( pMan1 );
     Aig_ManPrintStats( pMan2 );
@@ -342,7 +373,7 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
 
     assert( Abc_NtkIsStrash(pNtk) );
     // convert to the AIG manager
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
     if ( !Aig_ManCheck( pMan ) )
@@ -410,7 +441,7 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
     Fra_Par_t Pars, * pPars = &Pars; 
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
     Fra_ParamsDefault( pPars );
@@ -446,7 +477,7 @@ Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVe
     extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
     pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose );
@@ -473,7 +504,7 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
     Abc_Ntk_t * pNtkAig;
     int clk;
     assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManPrintStats( pMan );
@@ -517,7 +548,7 @@ Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
     Abc_Ntk_t * pNtkAig;
     int clk;
     assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManPrintStats( pMan );
@@ -554,7 +585,7 @@ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel,
     Abc_Ntk_t * pNtkAig;
     int clk;
     assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManPrintStats( pMan );
@@ -587,7 +618,7 @@ Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
     Abc_Ntk_t * pNtkAig;
     int clk;
     assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManPrintStats( pMan );
@@ -696,7 +727,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
     assert( Abc_NtkIsStrash(pNtk) );
 
     // convert to the AIG manager
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
     if ( !Aig_ManCheck( pMan ) )
@@ -751,7 +782,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
     assert( Abc_NtkPoNum(pNtk) == 1 );
 
     // conver to the manager
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     // derive CNF
 //    pCnf = Cnf_Derive( pMan, 0 );
     pCnf = Cnf_DeriveSimple( pMan, 0 );
@@ -809,7 +840,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
         assert( 0 );
 //    PRT( "SAT sat_solver time", clock() - clk );
 //    printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
-
+ 
     // if the problem is SAT, get the counterexample
     if ( status == l_True )
     {
@@ -836,16 +867,16 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fVerbose )
+Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
     pMan->nRegs = Abc_NtkLatchNum(pNtk);
 
-    pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fVerbose );
+    pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fVerbose );
     Aig_ManStop( pTemp );
 
     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 445c73c1..a33b9875 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -1099,7 +1099,9 @@ int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd )
     Abc_Obj_t * pNode, * pMiter;
     int i;
     assert( Abc_NtkIsStrash(pNtk) );
-    assert( Abc_NtkLatchNum(pNtk) == 0 );
+//    assert( Abc_NtkLatchNum(pNtk) == 0 );
+    if ( Abc_NtkPoNum(pNtk) == 1 )
+        return 1;
     // start the result
     if ( fAnd )
         pMiter = Abc_AigConst1(pNtk);
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 978b7cdb..4fdb7cbc 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -87,6 +87,71 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
 
 /**Function*************************************************************
 
+  Synopsis    [Reapplies structural hashing to the AIG.]
+
+  Description [Because of the structural hashing, this procedure should not 
+  change the number of nodes. It is useful to detect the bugs in the original AIG.]
+               
+  SideEffects []
+ 
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup )
+{
+    extern int timeRetime;
+    Abc_Ntk_t * pNtkAig;
+    Abc_Obj_t * pObj;
+    int i, nNodes;//, RetValue;
+    assert( Abc_NtkIsStrash(pNtk) );
+//timeRetime = clock();
+    // print warning about choice nodes
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+        printf( "Warning: The choice nodes in the original AIG are removed by strashing.\n" );
+    // start the new network (constants and CIs of the old network will point to the their counterparts in the new network)
+    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // complement the 1-values registers
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        if ( Abc_LatchIsInit1(pObj) )
+            Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
+    // restrash the nodes (assuming a topological order of the old network)
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+    // finalize the network
+    Abc_NtkFinalize( pNtk, pNtkAig );
+    // complement the 1-valued registers
+    Abc_NtkForEachLatch( pNtkAig, pObj, i )
+        if ( Abc_LatchIsInit1(pObj) )
+            Abc_ObjXorFaninC( Abc_ObjFanin0(pObj), 0 );
+    // set all constant-0 values
+    Abc_NtkForEachLatch( pNtkAig, pObj, i )
+        Abc_LatchSetInit0( pObj );
+
+    // print warning about self-feed latches
+//    if ( Abc_NtkCountSelfFeedLatches(pNtkAig) )
+//        printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) );
+    // perform cleanup if requested
+    if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) 
+        printf( "Abc_NtkRestrash(): AIG cleanup removed %d nodes (this is 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;
+    }
+//timeRetime = clock() - timeRetime;
+//    if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) )
+//        printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+    return pNtkAig;
+
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transforms logic network into structurally hashed AIG.]
 
   Description []
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index fe519476..23b5b350 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -123,7 +123,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
         // assign names to latch and its input
         Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
 
-        printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id );
+//        printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id );
     } 
     
     // remember the beginning of latch/PO literals
@@ -161,7 +161,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
         pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
         Abc_ObjAddFanin( pObj, pNode0 );
 
-        printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id );
+//        printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id );
 
     }
     // read the PO driver literals
@@ -233,7 +233,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
     }
 
     // remove the extra nodes
-//    Abc_AigCleanup( pNtkNew->pManFunc );
+    Abc_AigCleanup( pNtkNew->pManFunc );
 
     // check the result
     if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )