Version abc60723

abc.dsp

@@ -1058,6 +1058,10 @@ SOURCE=.\src\sat\fraig\fraigCanon.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\fraig\fraigChoice.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\fraig\fraigFanout.c
 # End Source File
 # Begin Source File
@@ -2106,15 +2110,19 @@ SOURCE=.\src\temp\ivy\ivyDsd.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\temp\ivy\ivyFanout.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\temp\ivy\ivyMan.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\temp\ivy\ivyMulti.c
+SOURCE=.\src\temp\ivy\ivyMem.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\temp\ivy\ivyMulti8.c
+SOURCE=.\src\temp\ivy\ivyMulti.c
 # End Source File
 # Begin Source File
 
@@ -2130,14 +2138,6 @@ SOURCE=.\src\temp\ivy\ivyResyn.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\temp\ivy\ivyRewrite.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\temp\ivy\ivyRwrAlg.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\temp\ivy\ivyRwrPre.c
 # End Source File
 # Begin Source File
@@ -2150,10 +2150,6 @@ SOURCE=.\src\temp\ivy\ivyTable.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\temp\ivy\ivyUndo.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\temp\ivy\ivyUtil.c
 # End Source File
 # End Group
@@ -2166,19 +2162,15 @@ SOURCE=.\src\temp\player\player.h
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\temp\player\playerAbc.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\temp\player\playerBuild.c
+SOURCE=.\src\temp\player\playerCore.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\temp\player\playerCore.c
+SOURCE=.\src\temp\player\playerMan.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\temp\player\playerMan.c
+SOURCE=.\src\temp\player\playerToAbc.c
 # End Source File
 # Begin Source File
 

src/base/abc/abc.h

@@ -544,6 +544,7 @@ extern char *             Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits
 extern char *             Abc_NtkLogicStoreName( Abc_Obj_t * pNodeNew, char * pNameOld );
 extern char *             Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pNodeNew, char * pNameOld, char * pSuffix );
 extern void               Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+extern void               Abc_NtkDupCioNamesTableNoLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern void               Abc_NtkDupCioNamesTableDual( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern Vec_Ptr_t *        Abc_NodeGetFaninNames( Abc_Obj_t * pNode );
 extern Vec_Ptr_t *        Abc_NodeGetFakeNames( int nNames );
@@ -571,6 +572,7 @@ extern void               Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk );
 /*=== abcNtk.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
+extern Abc_Ntk_t *        Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern Abc_Ntk_t *        Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern void               Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern Abc_Ntk_t *        Abc_NtkStartRead( char * pName );

src/base/abc/abcAig.c

@@ -78,9 +78,20 @@ struct Abc_Aig_t_
           pEnt2 = pEnt? pEnt->pNext: NULL )
 
 // hash key for the structural hash table
-static inline unsigned Abc_HashKey2( Abc_Obj_t * p0, Abc_Obj_t * p1, int TableSize ) { return ((unsigned)(p0) + (unsigned)(p1) * 12582917) % TableSize; }
+//static inline unsigned Abc_HashKey2( Abc_Obj_t * p0, Abc_Obj_t * p1, int TableSize ) { return ((unsigned)(p0) + (unsigned)(p1) * 12582917) % TableSize; }
 //static inline unsigned Abc_HashKey2( Abc_Obj_t * p0, Abc_Obj_t * p1, int TableSize ) { return ((unsigned)((a)->Id + (b)->Id) * ((a)->Id + (b)->Id + 1) / 2) % TableSize; }
 
+// hashing the node
+static unsigned Abc_HashKey2( Abc_Obj_t * p0, Abc_Obj_t * p1, int TableSize ) 
+{
+    unsigned Key = 0;
+    Key ^= Abc_ObjRegular(p0)->Id * 7937;
+    Key ^= Abc_ObjRegular(p1)->Id * 2971;
+    Key ^= Abc_ObjIsComplement(p0) * 911;
+    Key ^= Abc_ObjIsComplement(p1) * 353;
+    return Key % TableSize;
+}
+
 // structural hash table procedures
 static Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
 static Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, Abc_Obj_t * pAnd );

src/base/abc/abcNames.c

@@ -190,6 +190,35 @@ void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_NtkDupCioNamesTableNoLatches( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) );
+    assert( Abc_NtkPoNum(pNtk) == Abc_NtkPoNum(pNtkNew) );
+    assert( Abc_NtkAssertNum(pNtk) == Abc_NtkAssertNum(pNtkNew) );
+    assert( Nm_ManNumEntries(pNtk->pManName) > 0 );
+    assert( Nm_ManNumEntries(pNtkNew->pManName) == 0 );
+    // copy the CI/CO names if given
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i),      Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) );
+    Abc_NtkForEachPo( pNtk, pObj, i ) 
+        Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i),      Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) );
+    Abc_NtkForEachAssert( pNtk, pObj, i ) 
+        Abc_NtkLogicStoreName( Abc_NtkAssert(pNtkNew,i),  Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the name arrays.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_NtkDupCioNamesTableDual( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
 {
     Abc_Obj_t * pObj;

src/base/abc/abcNtk.c

@@ -164,6 +164,52 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkStartFromNoLatches( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj;
+    int i;
+    if ( pNtk == NULL )
+        return NULL;
+    // start the network
+    pNtkNew = Abc_NtkAlloc( Type, Func );
+    // duplicate the name and the spec
+    pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+    // clean the node copy fields
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pCopy = NULL;
+    // map the constant nodes
+    if ( Abc_NtkConst1(pNtk) )
+        Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew);
+    // clone the PIs/POs/latches
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachAssert( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
+    // transfer the names
+    if ( Type != ABC_NTK_NETLIST )
+        Abc_NtkDupCioNamesTableNoLatches( pNtk, pNtkNew );
+    Abc_ManTimeDup( pNtk, pNtkNew );
+    // check that the CI/CO/latches are copied correctly
+    assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) );
+    assert( Abc_NtkPoNum(pNtk) == Abc_NtkPoNum(pNtkNew) );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts a new network using existing network as a model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func )
 {
     Abc_Ntk_t * pNtkNew; 

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;
 }
 

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                                ///
 ////////////////////////////////////////////////////////////////////////

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 );

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) );    

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) )
         {

src/base/io/ioWriteVer.c

@@ -114,16 +114,15 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk )
     fprintf( pFile, "  wire" );
     Io_WriteVerilogWires( pFile, pNtk, 4 );
     fprintf( pFile, ";\n" );
-    // write registers
-    Io_WriteVerilogLatches( pFile, pNtk );
     // write the nodes
     if ( Abc_NtkHasMapping(pNtk) )
         Io_WriteVerilogGates( pFile, pNtk );
     else
         Io_WriteVerilogNodes( pFile, pNtk );
+    // write registers
+    Io_WriteVerilogLatches( pFile, pNtk );
     // finalize the file
     fprintf( pFile, "endmodule\n\n" );
-    fclose( pFile );
 } 
 
 /**Function*************************************************************
@@ -354,6 +353,23 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
     }
 }
 
+/* // fix by Zhihong
+void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pLatch;
+    int i;
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO )
+            fprintf( pFile, "  initial begin %s <= 1\'b0; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+        else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE )
+            fprintf( pFile, "  initial begin %s <= 1\'b1; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+        fprintf( pFile, "  always@(posedge  gclk) begin %s",     Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+        fprintf( pFile, " <= %s; end\n", Abc_ObjName(Abc_ObjFanin0(pLatch)) );
+    }
+}
+*/
+
 /**Function*************************************************************
 
   Synopsis    [Writes the gates.]
@@ -423,8 +439,14 @@ void Io_WriteVerilogNodes2( FILE * pFile, Abc_Ntk_t * pNtk )
         }
         pName = Abc_SopIsComplement(pObj->pData)? "or" : "and";
         fprintf( pFile, "  %s(%s, ", pName, Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
-        Abc_ObjForEachFanin( pObj, pFanin, k )
-            fprintf( pFile, "%s%s", Io_WriteVerilogGetName(pFanin), (k==nFanins-1? "" : ", ") );
+//        Abc_ObjForEachFanin( pObj, pFanin, k )
+//            fprintf( pFile, "%s%s", Io_WriteVerilogGetName(pFanin), (k==nFanins-1? "" : ", ") );
+        Abc_ObjForEachFanin( pObj, pFanin, k ) 
+        {
+            char *cube = pObj->pData;
+            fprintf( pFile, "%s", cube[k] == '0' ? "~" : "");
+                fprintf( pFile, "%s%s", Io_WriteVerilogGetName(pFanin), (k==nFanins-1? "" : ", ") );
+        }
         fprintf( pFile, ");\n" );
     }
 }

src/base/main/mainFrame.c

@@ -134,9 +134,11 @@ Abc_Frame_t * Abc_FrameAllocate()
 ***********************************************************************/
 void Abc_FrameDeallocate( Abc_Frame_t * p )
 {
+    extern void Rwt_ManGlobalStop();
     extern void undefine_cube_size();
 //    Abc_HManStop();
     undefine_cube_size();
+    Rwt_ManGlobalStop();
     if ( p->pManDec ) Dec_ManStop( p->pManDec );
     if ( p->dd )      Extra_StopManager( p->dd );
     Abc_FrameDeleteAllNetworks( p );

src/map/fpga/fpgaCut.c

@@ -35,9 +35,9 @@ struct Fpga_CutTableStrutct_t
 };
 
 // the largest number of cuts considered
-#define  FPGA_CUTS_MAX_COMPUTE   500
+#define  FPGA_CUTS_MAX_COMPUTE   5000
 // the largest number of cuts used
-#define  FPGA_CUTS_MAX_USE       200
+#define  FPGA_CUTS_MAX_USE       2000
 
 // primes used to compute the hash key
 static int s_HashPrimes[10] = { 109, 499, 557, 619, 631, 709, 797, 881, 907, 991 };

src/misc/extra/extra.h

@@ -433,6 +433,14 @@ static inline int Extra_TruthIsConst1( unsigned * pIn, int nVars )
             return 0;
     return 1;
 }
+static inline int Extra_TruthIsImply( unsigned * pIn1, unsigned * pIn2, int nVars )
+{
+    int w;
+    for ( w = Extra_TruthWordNum(nVars)-1; w >= 0; w-- )
+        if ( pIn1[w] & ~pIn2[w] )
+            return 0;
+    return 1;
+}
 static inline void Extra_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
 {
     int w;
@@ -491,7 +499,9 @@ extern int      Extra_TruthSupportSize( unsigned * pTruth, int nVars );
 extern int      Extra_TruthSupport( unsigned * pTruth, int nVars );
 extern void     Extra_TruthCofactor0( unsigned * pTruth, int nVars, int iVar );
 extern void     Extra_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
-extern void     Extra_TruthCombine( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
+extern void     Extra_TruthExist( unsigned * pTruth, int nVars, int iVar );
+extern void     Extra_TruthForall( unsigned * pTruth, int nVars, int iVar );
+extern void     Extra_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
 extern void     Extra_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
 extern int      Extra_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
 extern int      Extra_TruthCountOnes( unsigned * pTruth, int nVars );

src/misc/extra/extraUtilTruth.c

@@ -506,6 +506,116 @@ void Extra_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
     }
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Existentially quantifies the variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_TruthExist( unsigned * pTruth, int nVars, int iVar )
+{
+    int nWords = Extra_TruthWordNum( nVars );
+    int i, k, Step;
+
+    assert( iVar < nVars );
+    switch ( iVar )
+    {
+    case 0:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] |=  ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
+        return;
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] |=  ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
+        return;
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] |=  ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
+        return;
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] |=  ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
+        return;
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] |=  ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
+        return;
+    default:
+        Step = (1 << (iVar - 5));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+            {
+                pTruth[i]     |= pTruth[Step+i];
+                pTruth[Step+i] = pTruth[i];
+            }
+            pTruth += 2*Step;
+        }
+        return;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Existentially quantifies the variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Extra_TruthForall( unsigned * pTruth, int nVars, int iVar )
+{
+    int nWords = Extra_TruthWordNum( nVars );
+    int i, k, Step;
+
+    assert( iVar < nVars );
+    switch ( iVar )
+    {
+    case 0:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] &=  ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
+        return;
+    case 1:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] &=  ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
+        return;
+    case 2:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] &=  ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
+        return;
+    case 3:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] &=  ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
+        return;
+    case 4:
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] &=  ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
+        return;
+    default:
+        Step = (1 << (iVar - 5));
+        for ( k = 0; k < nWords; k += 2*Step )
+        {
+            for ( i = 0; i < Step; i++ )
+            {
+                pTruth[i]     &= pTruth[Step+i];
+                pTruth[Step+i] = pTruth[i];
+            }
+            pTruth += 2*Step;
+        }
+        return;
+    }
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Computes negative cofactor of the function.]
@@ -517,7 +627,7 @@ void Extra_TruthCofactor0( unsigned * pTruth, int nVars, int iVar )
   SeeAlso     []
 
 ***********************************************************************/
-void Extra_TruthCombine( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar )
+void Extra_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar )
 {
     int nWords = Extra_TruthWordNum( nVars );
     int i, k, Step;

src/misc/nm/nmTable.c

@@ -44,7 +44,7 @@ static unsigned Nm_HashString( char * pName, int TableSize )
     };
     unsigned i, Key = 0;
     for ( i = 0; pName[i] != '\0'; i++ )
-        Key ^= s_Primes[i%10]*pName[i];
+        Key ^= s_Primes[i%10]*pName[i]*pName[i];
     return Key % TableSize;
 }
 
@@ -142,7 +142,7 @@ Nm_Entry_t * Nm_ManTableLookupId( Nm_Man_t * p, int ObjId )
 Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** ppSecond )
 {
     Nm_Entry_t * pFirst, * pSecond;
-    int i;
+    int i, Counter = 0;
     pFirst = pSecond = NULL;
     for ( i = Nm_HashString(pName, p->nBins); p->pBinsN2I[i]; i = (i+1) % p->nBins )
         if ( strcmp(p->pBinsN2I[i]->Name, pName) == 0 )
@@ -154,6 +154,10 @@ Nm_Entry_t * Nm_ManTableLookupName( Nm_Man_t * p, char * pName, Nm_Entry_t ** pp
             else
                 assert( 0 ); // name appears more than 2 times
         }
+        else
+            Counter++;
+    if ( Counter > 100 )
+    printf( "%d ", Counter );
     // save the names
     if ( ppSecond )
         *ppSecond = pSecond;

src/misc/vec/vecPtr.h

@@ -293,6 +293,23 @@ static inline void * Vec_PtrEntry( Vec_Ptr_t * p, int i )
   SeeAlso     []
 
 ***********************************************************************/
+static inline void ** Vec_PtrEntryP( Vec_Ptr_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray + i;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline void Vec_PtrWriteEntry( Vec_Ptr_t * p, int i, void * Entry )
 {
     assert( i >= 0 && i < p->nSize );
@@ -371,7 +388,10 @@ static inline void Vec_PtrFillExtra( Vec_Ptr_t * p, int nSize, void * Entry )
     int i;
     if ( p->nSize >= nSize )
         return;
-    Vec_PtrGrow( p, nSize );
+    if ( p->nSize < 2 * nSize )
+        Vec_PtrGrow( p, 2 * nSize );
+    else
+        Vec_PtrGrow( p, p->nSize );
     for ( i = p->nSize; i < nSize; i++ )
         p->pArray[i] = Entry;
     p->nSize = nSize;

src/opt/cut/cut.h

@@ -61,6 +61,8 @@ struct Cut_ParamsStruct_t_
     int                fDrop;             // drop cuts on the fly
     int                fDag;              // compute only DAG cuts
     int                fTree;             // compute only tree cuts
+    int                fGlobal;           // compute only global cuts
+    int                fLocal;            // compute only local cuts
     int                fRecord;           // record the cut computation flow
     int                fFancy;            // perform fancy computations
     int                fVerbose;          // the verbosiness flag
@@ -118,7 +120,10 @@ extern void             Cut_ManStop( Cut_Man_t * p );
 extern void             Cut_ManPrintStats( Cut_Man_t * p );
 extern void             Cut_ManPrintStatsToFile( Cut_Man_t * p, char * pFileName, int TimeTotal );
 extern void             Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts );
+extern void             Cut_ManSetNodeAttrs( Cut_Man_t * p, Vec_Int_t * vFanCounts );
 extern int              Cut_ManReadVarsMax( Cut_Man_t * p );
+extern Cut_Params_t *   Cut_ManReadParams( Cut_Man_t * p );
+extern Vec_Int_t *      Cut_ManReadNodeAttrs( Cut_Man_t * p );
 extern void             Cut_ManIncrementDagNodes( Cut_Man_t * p );
 /*=== cutNode.c ==========================================================*/
 extern Cut_Cut_t *      Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv, int TreeCode ); 

src/opt/cut/cutInt.h

@@ -46,6 +46,7 @@ struct Cut_ManStruct_t_
     // user preferences
     Cut_Params_t *     pParams;          // computation parameters
     Vec_Int_t *        vFanCounts;       // the array of fanout counters
+    Vec_Int_t *        vNodeAttrs;       // node attributes (1 = global; 0 = local)
     // storage for cuts
     Vec_Ptr_t *        vCutsNew;         // new cuts by node ID
     Vec_Ptr_t *        vCutsOld;         // old cuts by node ID

src/opt/cut/cutMan.c

@@ -233,6 +233,22 @@ void Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts )
   SeeAlso     []
 
 ***********************************************************************/
+void Cut_ManSetNodeAttrs( Cut_Man_t * p, Vec_Int_t * vNodeAttrs )
+{
+    p->vNodeAttrs = vNodeAttrs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Cut_ManReadVarsMax( Cut_Man_t * p )
 {
     return p->pParams->nVarsMax;
@@ -249,6 +265,38 @@ int Cut_ManReadVarsMax( Cut_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+Cut_Params_t * Cut_ManReadParams( Cut_Man_t * p )
+{
+    return p->pParams;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Cut_ManReadNodeAttrs( Cut_Man_t * p )
+{
+    return p->vNodeAttrs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Cut_ManIncrementDagNodes( Cut_Man_t * p )
 {
     p->nNodesDag++;

src/opt/cut/cutNode.c

@@ -206,6 +206,32 @@ static inline int Cut_CutFilterOne( Cut_Man_t * p, Cut_List_t * pSuperList, Cut_
 
 /**Function*************************************************************
 
+  Synopsis    [Checks if the cut is local and can be removed.]
+
+  Description [Returns 1 if the cut is removed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cut_CutFilterGlobal( Cut_Man_t * p, Cut_Cut_t * pCut )
+{
+    int a;
+    if ( pCut->nLeaves == 1 )
+        return 0;
+    for ( a = 0; a < (int)pCut->nLeaves; a++ )
+        if ( Vec_IntEntry( p->vNodeAttrs, pCut->pLeaves[a] ) ) // global
+            return 0;
+    // there is no global nodes, the cut should be removed
+    p->nCutsFilter++;
+    Cut_CutRecycle( p, pCut );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Checks containment for one cut.]
 
   Description [Returns 1 if the cut is removed.]
@@ -306,6 +332,14 @@ static inline int Cut_CutProcessTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t
                 return 0;
         }
     }
+
+    if ( p->pParams->fGlobal )
+    {
+        assert( p->vNodeAttrs != NULL );
+        if ( Cut_CutFilterGlobal( p, pCut ) )
+            return 0;
+    }
+
     // compute the truth table
     if ( p->pParams->fTruth )
         Cut_TruthCompute( p, pCut, pCut0, pCut1, p->fCompl0, p->fCompl1 );
@@ -395,7 +429,7 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
         p->nNodeCuts++;
     }
     // get the cut lists of children
-    if ( pList0 == NULL || pList1 == NULL )
+    if ( pList0 == NULL || pList1 == NULL || (p->pParams->fLocal && TreeCode)  )
         return;
 
     // remember the old number of cuts

src/opt/cut/cutPre22.c

@@ -617,7 +617,7 @@ void Cut_CellCrossBar( Cut_Cell_t * pCell )
         Extra_TruthCofactor0( uTemp1, pCell->nVars, pCell->CrossBar1 );
     }
     else assert( 0 );
-    Extra_TruthCombine( pCell->uTruth, uTemp0, uTemp1, pCell->nVars, pCell->CrossBar0 );
+    Extra_TruthMux( pCell->uTruth, uTemp0, uTemp1, pCell->nVars, pCell->CrossBar0 );
 }
 
 /**Function*************************************************************

src/opt/cut/vec.h

+/**CFile****************************************************************
+
+  FileName    [vec.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __VEC_H__
+#define __VEC_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+#include "vecInt.h"
+#include "vecStr.h"
+#include "vecPtr.h"
+#include "vecVec.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+

src/opt/cut/vecVec.h

+/**CFile****************************************************************
+
+  FileName    [vecVec.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resizable arrays.]
+
+  Synopsis    [Resizable vector of resizable vectors.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: vecVec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __VEC_VEC_H__
+#define __VEC_VEC_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Vec_Vec_t_       Vec_Vec_t;
+struct Vec_Vec_t_ 
+{
+    int              nCap;
+    int              nSize;
+    void **          pArray;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+// iterators through levels 
+#define Vec_VecForEachLevel( vGlob, vVec, i )                                                 \
+    for ( i = 0; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
+#define Vec_VecForEachLevelStart( vGlob, vVec, i, LevelStart )                                \
+    for ( i = LevelStart; (i < Vec_VecSize(vGlob)) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
+#define Vec_VecForEachLevelStartStop( vGlob, vVec, i, LevelStart, LevelStop )                 \
+    for ( i = LevelStart; (i <= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i++ )
+#define Vec_VecForEachLevelReverse( vGlob, vVec, i )                                          \
+    for ( i = Vec_VecSize(vGlob) - 1; (i >= 0) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- )
+
+// iteratores through entries
+#define Vec_VecForEachEntry( vGlob, pEntry, i, k )                                            \
+    for ( i = 0; i < Vec_VecSize(vGlob); i++ )                                                \
+        Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 
+#define Vec_VecForEachEntryStart( vGlob, pEntry, i, k, LevelStart )                           \
+    for ( i = LevelStart; i < Vec_VecSize(vGlob); i++ )                                       \
+        Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 
+#define Vec_VecForEachEntryStartStop( vGlob, pEntry, i, k, LevelStart, LevelStop )            \
+    for ( i = LevelStart; i <= LevelStop; i++ )                                               \
+        Vec_PtrForEachEntry( Vec_VecEntry(vGlob, i), pEntry, k ) 
+#define Vec_VecForEachEntryReverse( vGlob, pEntry, i, k )                                     \
+    for ( i = 0; i < Vec_VecSize(vGlob); i++ )                                                \
+        Vec_PtrForEachEntryReverse( Vec_VecEntry(vGlob, i), pEntry, k ) 
+#define Vec_VecForEachEntryReverseReverse( vGlob, pEntry, i, k )                              \
+    for ( i = Vec_VecSize(vGlob) - 1; i >= 0; i-- )                                           \
+        Vec_PtrForEachEntryReverse( Vec_VecEntry(vGlob, i), pEntry, k ) 
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Vec_t * Vec_VecAlloc( int nCap )
+{
+    Vec_Vec_t * p;
+    p = ALLOC( Vec_Vec_t, 1 );
+    if ( nCap > 0 && nCap < 8 )
+        nCap = 8;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ALLOC( void *, p->nCap ) : NULL;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Vec_Vec_t * Vec_VecStart( int nSize )
+{
+    Vec_Vec_t * p;
+    int i;
+    p = Vec_VecAlloc( nSize );
+    for ( i = 0; i < nSize; i++ )
+        p->pArray[i] = Vec_PtrAlloc( 0 );
+    p->nSize = nSize;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates a vector with the given capacity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecExpand( Vec_Vec_t * p, int Level )
+{
+    int i;
+    if ( p->nSize >= Level + 1 )
+        return;
+    Vec_PtrGrow( (Vec_Ptr_t *)p, Level + 1 );
+    for ( i = p->nSize; i <= Level; i++ )
+        p->pArray[i] = Vec_PtrAlloc( 0 );
+    p->nSize = Level + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_VecSize( Vec_Vec_t * p )
+{
+    return p->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void * Vec_VecEntry( Vec_Vec_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray[i];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the vector.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecFree( Vec_Vec_t * p )
+{
+    Vec_Ptr_t * vVec;
+    int i;
+    Vec_VecForEachLevel( p, vVec, i )
+        Vec_PtrFree( vVec );
+    Vec_PtrFree( (Vec_Ptr_t *)p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the vector of vectors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_VecSizeSize( Vec_Vec_t * p )
+{
+    Vec_Ptr_t * vVec;
+    int i, Counter = 0;
+    Vec_VecForEachLevel( p, vVec, i )
+        Counter += vVec->nSize;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecClear( Vec_Vec_t * p )
+{
+    Vec_Ptr_t * vVec;
+    int i;
+    Vec_VecForEachLevel( p, vVec, i )
+        Vec_PtrClear( vVec );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecPush( Vec_Vec_t * p, int Level, void * Entry )
+{
+    if ( p->nSize < Level + 1 )
+    {
+        int i;
+        Vec_PtrGrow( (Vec_Ptr_t *)p, Level + 1 );
+        for ( i = p->nSize; i < Level + 1; i++ )
+            p->pArray[i] = Vec_PtrAlloc( 0 );
+        p->nSize = Level + 1;
+    }
+    Vec_PtrPush( (Vec_Ptr_t*)p->pArray[Level], Entry );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry )
+{
+    if ( p->nSize < Level + 1 )
+        Vec_VecPush( p, Level, Entry );
+    else
+        Vec_PtrPushUnique( (Vec_Ptr_t*)p->pArray[Level], Entry );
+}
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+

src/opt/dec/decAbc.c

@@ -267,7 +267,7 @@ Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph )
     {
         pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
         pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
-        pNode->pFunc = Ivy_And( pAnd0, pAnd1 );
+        pNode->pFunc = Ivy_And( pMan, pAnd0, pAnd1 );
     }
     // complement the result if necessary
     return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );

src/sat/fraig/fraigChoice.c

+/**CFile****************************************************************
+
+  FileName    [fraigTrans.c]
+
+  PackageName [MVSIS 1.3: Multi-valued logic synthesis system.]
+
+  Synopsis    [Adds the additive and distributive choices to the AIG.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - February 1, 2003.]
+
+  Revision    [$Id: fraigTrans.c,v 1.1 2005/02/28 05:34:34 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fraigInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Adds choice nodes based on associativity.]
+
+  Description [Make nLimit big AND gates and add all decompositions
+               to the Fraig.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_ManAddChoices( Fraig_Man_t * pMan, int fVerbose, int nLimit )
+{
+//    ProgressBar * pProgress;
+    char Buffer[100];
+    int clkTotal = clock();
+    int i, nNodesBefore, nNodesAfter, nInputs, nMaxNodes;
+    int /*nMaxLevel,*/ nDistributive;
+    Fraig_Node_t *pNode, *pRepr;
+    Fraig_Node_t *pX, *pA, *pB, *pC, /* *pD,*/ *pN, /* *pQ, *pR,*/ *pT;
+    int fShortCut = 0;
+
+    nDistributive = 0;
+
+//    Fraig_ManSetApprox( pMan, 1 );
+
+    // NO functional reduction
+    if (fShortCut) Fraig_ManSetFuncRed( pMan, 0 );
+
+    // First we mark critical functions i.e. compute those
+    // nodes which lie on the critical path. Note that this
+    // doesn't update the required times on any choice nodes
+    // which are not the representatives
+/*
+    nMaxLevel = Fraig_GetMaxLevel( pMan );
+    for ( i = 0; i < pMan->nOutputs; i++ )
+    {
+        Fraig_SetNodeRequired( pMan, pMan->pOutputs[i], nMaxLevel );
+    }
+*/
+    nNodesBefore = Fraig_ManReadNodeNum( pMan );
+    nInputs      = Fraig_ManReadInputNum( pMan );
+    nMaxNodes    = nInputs + nLimit * ( nNodesBefore - nInputs );
+
+    printf ("Limit = %d, Before = %d\n", nMaxNodes, nNodesBefore );
+
+    if (0) 
+    {
+        char buffer[128];
+        sprintf (buffer, "test" );
+//        Fraig_MappingShow( pMan, buffer );
+    }
+
+//    pProgress = Extra_ProgressBarStart( stdout, nMaxNodes );
+Fraig_ManCheckConsistency( pMan );
+
+    for ( i = nInputs+1; (i < Fraig_ManReadNodeNum( pMan )) 
+            && (nMaxNodes > Fraig_ManReadNodeNum( pMan )); ++i )
+    {
+//        if ( i == nNodesBefore )
+//            break;
+
+        pNode = Fraig_ManReadIthNode( pMan, i );
+        assert ( pNode );
+
+        pRepr = pNode->pRepr ? pNode->pRepr : pNode;
+        //printf ("Slack: %d\n", Fraig_NodeReadSlack( pRepr ));
+        
+        // All the new associative choices we add will have huge slack
+        // since we do not redo timing, and timing doesnt handle choices
+        // well anyway. However every newly added node is a choice of an
+        // existing critical node, so they are considered critical.
+//        if ( (Fraig_NodeReadSlack( pRepr ) > 3) && (i < nNodesBefore)  )     
+//            continue;
+
+//        if ( pNode->pRepr )
+//            continue;
+
+        // Try ((ab)c), x = ab -> (a(bc)) and (b(ac))
+        pX = Fraig_NodeReadOne(pNode);
+        pC = Fraig_NodeReadTwo(pNode);
+        if (Fraig_NodeIsAnd(pX) && !Fraig_IsComplement(pX))
+        {
+            pA = Fraig_NodeReadOne(Fraig_Regular(pX));
+            pB = Fraig_NodeReadTwo(Fraig_Regular(pX));
+
+//            pA = Fraig_NodeGetRepr( pA );
+//            pB = Fraig_NodeGetRepr( pB );
+//            pC = Fraig_NodeGetRepr( pC );
+
+            if (fShortCut) 
+            {
+                pT = Fraig_NodeAnd(pMan, pB, pC);
+                if ( !pT->pRepr )
+                {
+                    pN = Fraig_NodeAnd(pMan, pA, pT);
+//                    Fraig_NodeAddChoice( pMan, pNode, pN );
+                }
+            }
+            else
+                pN = Fraig_NodeAnd(pMan, pA, Fraig_NodeAnd(pMan, pB, pC));
+            // assert ( Fraig_NodesEqual(pN, pNode) );
+
+
+            if (fShortCut) 
+            {
+                pT = Fraig_NodeAnd(pMan, pA, pC);
+                if ( !pT->pRepr )
+                {
+                    pN = Fraig_NodeAnd(pMan, pB, pT);
+//                    Fraig_NodeAddChoice( pMan, pNode, pN );
+                }
+            }
+            else
+                pN = Fraig_NodeAnd(pMan, pB, Fraig_NodeAnd(pMan, pA, pC));
+            // assert ( Fraig_NodesEqual(pN, pNode) );
+        }
+
+
+        // Try (a(bc)), x = bc -> ((ab)c) and ((ac)b)
+        pA = Fraig_NodeReadOne(pNode);
+        pX = Fraig_NodeReadTwo(pNode);
+        if (Fraig_NodeIsAnd(pX) && !Fraig_IsComplement(pX))
+        {
+            pB = Fraig_NodeReadOne(Fraig_Regular(pX));
+            pC = Fraig_NodeReadTwo(Fraig_Regular(pX));
+
+//            pA = Fraig_NodeGetRepr( pA );
+//            pB = Fraig_NodeGetRepr( pB );
+//            pC = Fraig_NodeGetRepr( pC );
+
+            if (fShortCut) 
+            {
+                pT = Fraig_NodeAnd(pMan, pA, pB);
+                if ( !pT->pRepr )
+                {
+                    pN = Fraig_NodeAnd(pMan, pC, pT);
+//                    Fraig_NodeAddChoice( pMan, pNode, pN );
+                }
+            }
+            else
+                pN = Fraig_NodeAnd(pMan, Fraig_NodeAnd(pMan, pA, pB), pC);
+            // assert ( Fraig_NodesEqual(pN, pNode) );
+
+            if (fShortCut) 
+            {
+                pT = Fraig_NodeAnd(pMan, pA, pC);
+                if ( !pT->pRepr )
+                {
+                    pN = Fraig_NodeAnd(pMan, pB, pT);
+//                    Fraig_NodeAddChoice( pMan, pNode, pN );
+                }
+            }
+            else
+                pN = Fraig_NodeAnd(pMan, Fraig_NodeAnd(pMan, pA, pC), pB);
+            // assert ( Fraig_NodesEqual(pN, pNode) );
+        }
+
+
+/*
+        // Try distributive transform
+        pQ = Fraig_NodeReadOne(pNode);
+        pR = Fraig_NodeReadTwo(pNode);
+        if ( (Fraig_IsComplement(pQ) && Fraig_NodeIsAnd(pQ))
+             && (Fraig_IsComplement(pR) && Fraig_NodeIsAnd(pR)) )
+        {
+            pA = Fraig_NodeReadOne(Fraig_Regular(pQ));
+            pB = Fraig_NodeReadTwo(Fraig_Regular(pQ));
+            pC = Fraig_NodeReadOne(Fraig_Regular(pR));
+            pD = Fraig_NodeReadTwo(Fraig_Regular(pR));
+
+            // Now detect the !(xy + xz) pattern, store 
+            // x in pA, y in pB and z in pC and set pD = 0 to indicate
+            // pattern was found
+            assert (pD != 0);
+            if (pA == pC) { pC = pD;                   pD = 0; } 
+            if (pA == pD) {                            pD = 0; } 
+            if (pB == pC) { pB = pA; pA = pC; pC = pD; pD = 0; }
+            if (pB == pD) { pB = pA; pA = pD;          pD = 0; }
+            if (pD == 0)
+            {
+                nDistributive++;
+                pN = Fraig_Not(Fraig_NodeAnd(pMan, pA, 
+                        Fraig_NodeOr(pMan, pB, pC)));
+                if (fShortCut) Fraig_NodeAddChoice( pMan, pNode, pN );
+                // assert ( Fraig_NodesEqual(pN, pNode) );
+            }
+        }
+*/            
+        if ( i % 1000 == 0 )
+        {
+            sprintf( Buffer, "Adding choice %6d...", i - nNodesBefore );
+//            Extra_ProgressBarUpdate( pProgress, i, Buffer );
+        }
+    }
+
+//    Extra_ProgressBarStop( pProgress );
+
+Fraig_ManCheckConsistency( pMan );
+
+    nNodesAfter = Fraig_ManReadNodeNum( pMan );
+    printf ( "Nodes before = %6d. Nodes with associative choices = %6d. Increase = %4.2f %%.\n", 
+            nNodesBefore, nNodesAfter, ((float)(nNodesAfter - nNodesBefore)) * 100.0/(nNodesBefore - nInputs) );
+    printf ( "Distributive = %d\n", nDistributive );
+
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/temp/esop/esopUtil.c

@@ -134,7 +134,7 @@ void Esop_CoverWriteFile( Esop_Cube_t * pCover, char * pName, int fEsop )
         if ( Buffer[i] == '<' || Buffer[i] == '>' )
             Buffer[i] = '_';
     pFile = fopen( Buffer, "w" );
-    fprintf( pFile, "# %s cover for output %s generated by ABC on %s\n", fEsop? "ESOP":"SOP", pName, Extra_TimeStamp() );
+    fprintf( pFile, "# %s cover for output %s generated by ABC\n", fEsop? "ESOP":"SOP", pName );
     fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 );
     fprintf( pFile, ".o %d\n", 1 );
     fprintf( pFile, ".p %d\n", Esop_CoverCountCubes(pCover) );

src/temp/ivy/ivyBalance.c

@@ -27,7 +27,7 @@
 static int         Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level, int fUpdateLevel );
 static Vec_Ptr_t * Ivy_NodeBalanceCone( Ivy_Obj_t * pObj, Vec_Vec_t * vStore, int Level );
 static int         Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper );
-static void        Ivy_NodeBalancePermute( Vec_Ptr_t * vSuper, int LeftBound, int fExor );
+static void        Ivy_NodeBalancePermute( Ivy_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor );
 static void        Ivy_NodeBalancePushUniqueOrderByLevel( Vec_Ptr_t * vStore, Ivy_Obj_t * pObj );
 
 ////////////////////////////////////////////////////////////////////////
@@ -54,11 +54,11 @@ Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
     // clean the old manager
     Ivy_ManCleanTravId( p );
     // create the new manager 
-    pNew = Ivy_ManStart( Ivy_ManPiNum(p), Ivy_ManPoNum(p), Ivy_ManNodeNum(p) + 20000 );
+    pNew = Ivy_ManStart();
     // map the nodes
     Ivy_ManConst1(p)->TravId = Ivy_EdgeFromNode( Ivy_ManConst1(pNew) );
     Ivy_ManForEachPi( p, pObj, i )
-        pObj->TravId = Ivy_EdgeFromNode( Ivy_ManPi(pNew, i) );
+        pObj->TravId = Ivy_EdgeFromNode( Ivy_ObjCreatePi(pNew) );
     // balance the AIG
     vStore = Vec_VecAlloc( 50 );
     Ivy_ManForEachPo( p, pObj, i )
@@ -66,7 +66,7 @@ Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
         pDriver   = Ivy_ObjReal( Ivy_ObjChild0(pObj) );
         NewNodeId = Ivy_NodeBalance_rec( pNew, Ivy_Regular(pDriver), vStore, 0, fUpdateLevel );
         NewNodeId = Ivy_EdgeNotCond( NewNodeId, Ivy_IsComplement(pDriver) );
-        Ivy_ObjConnect( Ivy_ManPo(pNew, i), Ivy_EdgeToNode(pNew, NewNodeId) );
+        Ivy_ObjCreatePo( pNew, Ivy_EdgeToNode(pNew, NewNodeId) );
     }
     Vec_VecFree( vStore );
     if ( i = Ivy_ManCleanup( pNew ) )
@@ -139,11 +139,12 @@ int Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld, Vec_Vec_t * vSto
         vSuper->pArray[i] = Ivy_EdgeToNode( pNew, NewNodeId );
     }
     // build the supergate
-    pObjNew = Ivy_NodeBalanceBuildSuper( vSuper, Ivy_ObjType(pObjOld), fUpdateLevel );
+    pObjNew = Ivy_NodeBalanceBuildSuper( pNew, vSuper, Ivy_ObjType(pObjOld), fUpdateLevel );
     vSuper->nSize = 0;
     // make sure the balanced node is not assigned
     assert( pObjOld->TravId == 0 );
     pObjOld->TravId = Ivy_EdgeFromNode( pObjNew );
+//    assert( pObjOld->Level >= Ivy_Regular(pObjNew)->Level );
     return pObjOld->TravId;
 }
 
@@ -158,7 +159,7 @@ int Ivy_NodeBalance_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld, Vec_Vec_t * vSto
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel )
+Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Ivy_Man_t * p, Vec_Ptr_t * vSuper, Ivy_Type_t Type, int fUpdateLevel )
 {
     Ivy_Obj_t * pObj1, * pObj2;
     int LeftBound;
@@ -171,11 +172,11 @@ Ivy_Obj_t * Ivy_NodeBalanceBuildSuper( Vec_Ptr_t * vSuper, Ivy_Type_t Type, int
         // find the left bound on the node to be paired
         LeftBound = (!fUpdateLevel)? 0 : Ivy_NodeBalanceFindLeft( vSuper );
         // find the node that can be shared (if no such node, randomize choice)
-        Ivy_NodeBalancePermute( vSuper, LeftBound, Type == IVY_EXOR );
+        Ivy_NodeBalancePermute( p, vSuper, LeftBound, Type == IVY_EXOR );
         // pull out the last two nodes
         pObj1 = Vec_PtrPop(vSuper);
         pObj2 = Vec_PtrPop(vSuper);
-        Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(pObj1, pObj2, Type) );
+        Ivy_NodeBalancePushUniqueOrderByLevel( vSuper, Ivy_Oper(p, pObj1, pObj2, Type) );
     }
     return Vec_PtrEntry(vSuper, 0);
 }
@@ -314,7 +315,7 @@ int Ivy_NodeBalanceFindLeft( Vec_Ptr_t * vSuper )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_NodeBalancePermute( Vec_Ptr_t * vSuper, int LeftBound, int fExor )
+void Ivy_NodeBalancePermute( Ivy_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int fExor )
 {
     Ivy_Obj_t * pObj1, * pObj2, * pObj3, * pGhost;
     int RightBound, i;
@@ -330,8 +331,8 @@ void Ivy_NodeBalancePermute( Vec_Ptr_t * vSuper, int LeftBound, int fExor )
     for ( i = RightBound; i >= LeftBound; i-- )
     {
         pObj3 = Vec_PtrEntry( vSuper, i );
-        pGhost = Ivy_ObjCreateGhost( pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE );
-        if ( Ivy_TableLookup( pGhost ) )
+        pGhost = Ivy_ObjCreateGhost( p, pObj1, pObj3, fExor? IVY_EXOR : IVY_AND, IVY_INIT_NONE );
+        if ( Ivy_TableLookup( p, pGhost ) )
         {
             if ( pObj3 == pObj2 )
                 return;

src/temp/ivy/ivyCanon.c

@@ -24,7 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Ivy_Obj_t * Ivy_TableLookupPair_rec( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int fCompl0, int fCompl1, Ivy_Type_t Type );
+static Ivy_Obj_t * Ivy_TableLookupPair_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int fCompl0, int fCompl1, Ivy_Type_t Type );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -41,7 +41,7 @@ static Ivy_Obj_t * Ivy_TableLookupPair_rec( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost )
+Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
 {
     Ivy_Obj_t * pResult, * pLat0, * pLat1;
     Ivy_Init_t Init, Init0, Init1;
@@ -53,9 +53,9 @@ Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost )
     // consider the case when the pair is canonical
     if ( !Ivy_ObjIsLatch(Ivy_ObjFanin0(pGhost)) || !Ivy_ObjIsLatch(Ivy_ObjFanin1(pGhost)) )
     {
-        if ( pResult = Ivy_TableLookup( pGhost ) )
+        if ( pResult = Ivy_TableLookup( p, pGhost ) )
             return pResult;
-        return Ivy_ObjCreate( pGhost );
+        return Ivy_ObjCreate( p, pGhost );
     }
     /// remember the latches
     pLat0 = Ivy_ObjFanin0(pGhost);
@@ -64,16 +64,13 @@ Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost )
     Type = Ivy_ObjType(pGhost);
     fCompl0 = Ivy_ObjFaninC0(pGhost);
     fCompl1 = Ivy_ObjFaninC1(pGhost);
-    // modify the fanins to be latch fanins
-    pGhost->Fanin0 = Ivy_ObjFaninId0(pLat0);
-    pGhost->Fanin1 = Ivy_ObjFaninId0(pLat1);
     // call recursively
-    pResult = Ivy_CanonPair_rec( pGhost );
+    pResult = Ivy_Oper( p, Ivy_NotCond(Ivy_ObjFanin0(pLat0), fCompl0), Ivy_NotCond(Ivy_ObjFanin0(pLat1), fCompl1), Type );
     // build latch on top of this
     Init0 = Ivy_InitNotCond( Ivy_ObjInit(pLat0), fCompl0 );
     Init1 = Ivy_InitNotCond( Ivy_ObjInit(pLat1), fCompl1 );
     Init  = (Type == IVY_AND)? Ivy_InitAnd(Init0, Init1) : Ivy_InitExor(Init0, Init1);
-    return Ivy_CanonLatch( pResult, Init );
+    return Ivy_Latch( p, pResult, Init );
 }
 
 /**Function*************************************************************
@@ -87,11 +84,11 @@ Ivy_Obj_t * Ivy_CanonPair_rec( Ivy_Obj_t * pGhost )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_CanonAnd( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
+Ivy_Obj_t * Ivy_CanonAnd( Ivy_Man_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
 {
     Ivy_Obj_t * pGhost, * pResult;
-    pGhost = Ivy_ObjCreateGhost( pObj0, pObj1, IVY_AND, IVY_INIT_NONE );
-    pResult = Ivy_CanonPair_rec( pGhost );
+    pGhost = Ivy_ObjCreateGhost( p, pObj0, pObj1, IVY_AND, IVY_INIT_NONE );
+    pResult = Ivy_CanonPair_rec( p, pGhost );
     return pResult;
 }
 
@@ -106,14 +103,14 @@ Ivy_Obj_t * Ivy_CanonAnd( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_CanonExor( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
+Ivy_Obj_t * Ivy_CanonExor( Ivy_Man_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
 {
     Ivy_Obj_t * pGhost, * pResult;
     int fCompl = Ivy_IsComplement(pObj0) ^ Ivy_IsComplement(pObj1);
     pObj0 = Ivy_Regular(pObj0);
     pObj1 = Ivy_Regular(pObj1);
-    pGhost = Ivy_ObjCreateGhost( pObj0, pObj1, IVY_EXOR, IVY_INIT_NONE );
-    pResult = Ivy_CanonPair_rec( pGhost );
+    pGhost = Ivy_ObjCreateGhost( p, pObj0, pObj1, IVY_EXOR, IVY_INIT_NONE );
+    pResult = Ivy_CanonPair_rec( p, pGhost );
     return Ivy_NotCond( pResult, fCompl );
 }
 
@@ -128,15 +125,15 @@ Ivy_Obj_t * Ivy_CanonExor( Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_CanonLatch( Ivy_Obj_t * pObj, Ivy_Init_t Init )
+Ivy_Obj_t * Ivy_CanonLatch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init )
 {
     Ivy_Obj_t * pGhost, * pResult;
     int fCompl = Ivy_IsComplement(pObj);
     pObj = Ivy_Regular(pObj);
-    pGhost = Ivy_ObjCreateGhost( pObj, Ivy_ObjConst1(pObj), IVY_LATCH, Ivy_InitNotCond(Init, fCompl) );
-    pResult = Ivy_TableLookup( pGhost );
+    pGhost = Ivy_ObjCreateGhost( p, pObj, NULL, IVY_LATCH, Ivy_InitNotCond(Init, fCompl) );
+    pResult = Ivy_TableLookup( p, pGhost );
     if ( pResult == NULL )
-        pResult = Ivy_ObjCreate( pGhost );
+        pResult = Ivy_ObjCreate( p, pGhost );
     return Ivy_NotCond( pResult, fCompl );
 }
 

src/temp/ivy/ivyCheck.c

@@ -39,15 +39,18 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_ManCheck( Ivy_Man_t * pMan )
+int Ivy_ManCheck( Ivy_Man_t * p )
 {
     Ivy_Obj_t * pObj, * pObj2;
     int i;
-    Ivy_ManForEachObj( pMan, pObj, i )
+    Ivy_ManForEachObj( p, pObj, i )
     {
         // skip deleted nodes
-        if ( Ivy_ObjIsNone(pObj) )
-            continue;
+        if ( Ivy_ObjId(pObj) != i )
+        {
+            printf( "Ivy_ManCheck: Node with ID %d is listed as number %d in the array of objects.\n", pObj->Id, i );
+            return 0;
+        }
         // consider the constant node and PIs
         if ( i == 0 || Ivy_ObjIsPi(pObj) )
         {
@@ -69,44 +72,54 @@ int Ivy_ManCheck( Ivy_Man_t * pMan )
         }
         if ( Ivy_ObjIsBuf(pObj) )
         {
+            if ( Ivy_ObjFanin1(pObj) )
+            {
+                printf( "Ivy_ManCheck: The buffer with ID \"%d\" contains second fanin.\n", pObj->Id );
+                return 0;
+            }
             continue;
         }
         if ( Ivy_ObjIsLatch(pObj) )
         {
-            if ( Ivy_ObjFaninId1(pObj) != 0 )
+            if ( Ivy_ObjFanin1(pObj) )
             {
                 printf( "Ivy_ManCheck: The latch with ID \"%d\" contains second fanin.\n", pObj->Id );
                 return 0;
             }
-            if ( Ivy_ObjInit(pObj) == 0 )
+            if ( Ivy_ObjInit(pObj) == IVY_INIT_NONE )
             {
                 printf( "Ivy_ManCheck: The latch with ID \"%d\" does not have initial state.\n", pObj->Id );
                 return 0;
             }
-            pObj2 = Ivy_TableLookup( pObj );
+            pObj2 = Ivy_TableLookup( p, pObj );
             if ( pObj2 != pObj )
                 printf( "Ivy_ManCheck: Latch with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
                 continue;
         }
         // consider the AND node
-        if ( !Ivy_ObjFaninId0(pObj) || !Ivy_ObjFaninId1(pObj) )
+        if ( !Ivy_ObjFanin0(pObj) || !Ivy_ObjFanin1(pObj) )
         {
-            printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a constant fanin.\n", pObj->Id );
+            printf( "Ivy_ManCheck: The AIG has internal node \"%d\" with a NULL fanin.\n", pObj->Id );
             return 0;
         }
-        if ( Ivy_ObjFaninId0(pObj) <= Ivy_ObjFaninId1(pObj) )
+        if ( Ivy_ObjFaninId0(pObj) >= Ivy_ObjFaninId1(pObj) )
         {
             printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id );
             return 0;
         }
 //        if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) )
-//            printf( "Ivy_ManCheck: Node with ID \"%d\" has level that does not agree with the fanin levels.\n", pObj->Id );
-        pObj2 = Ivy_TableLookup( pObj );
+//            printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) );
+        pObj2 = Ivy_TableLookup( p, pObj );
         if ( pObj2 != pObj )
             printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id );
+        if ( Ivy_ObjRefs(pObj) == 0 )
+            printf( "Ivy_ManCheck: Node with ID \"%d\" has no fanouts.\n", pObj->Id );
+        // check fanouts
+        if ( p->vFanouts && Ivy_ObjRefs(pObj) != Ivy_ObjFanoutNum(p, pObj) )
+            printf( "Ivy_ManCheck: Node with ID \"%d\" has mismatch between the number of fanouts and refs.\n", pObj->Id );
     }
     // count the number of nodes in the table
-    if ( Ivy_TableCountEntries(pMan) != Ivy_ManAndNum(pMan) + Ivy_ManExorNum(pMan) + Ivy_ManLatchNum(pMan) )
+    if ( Ivy_TableCountEntries(p) != Ivy_ManAndNum(p) + Ivy_ManExorNum(p) + Ivy_ManLatchNum(p) )
     {
         printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
         return 0;

src/temp/ivy/ivyCut.c

@@ -175,7 +175,7 @@ printf( "%d", Counter );
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize )
+void Ivy_ManSeqFindCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInside, int nSize )
 {
     assert( !Ivy_IsComplement(pRoot) );
     assert( Ivy_ObjIsNode(pRoot) );
@@ -194,7 +194,7 @@ void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInsi
     Vec_IntPush( vInside, Ivy_LeafCreate(Ivy_ObjFaninId1(pRoot), 0) );
 
     // compute the cut
-    while ( Ivy_ManSeqFindCut_int( Ivy_ObjMan(pRoot), vFront, vInside, nSize ) );
+    while ( Ivy_ManSeqFindCut_int( p, vFront, vInside, nSize ) );
     assert( Vec_IntSize(vFront) <= nSize );
 }
 
@@ -213,7 +213,7 @@ void Ivy_ManSeqFindCut( Ivy_Obj_t * pRoot, Vec_Int_t * vFront, Vec_Int_t * vInsi
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_ManFindBoolCut_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume, Ivy_Obj_t * pPivot )
+int Ivy_ManFindBoolCut_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume, Ivy_Obj_t * pPivot )
 {
     int RetValue0, RetValue1;
     if ( pObj == pPivot )
@@ -231,15 +231,15 @@ int Ivy_ManFindBoolCut_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * v
 
     if ( Ivy_ObjIsBuf(pObj) )
     {
-        RetValue0 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot );
+        RetValue0 = Ivy_ManFindBoolCut_rec( p, Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot );
         if ( !RetValue0 )
             return 0;
         Vec_PtrPushUnique( vVolume, pObj );
         return 1;
     }
     assert( Ivy_ObjIsNode(pObj) );
-    RetValue0 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot );
-    RetValue1 = Ivy_ManFindBoolCut_rec( Ivy_ObjFanin1(pObj), vLeaves, vVolume, pPivot );
+    RetValue0 = Ivy_ManFindBoolCut_rec( p, Ivy_ObjFanin0(pObj), vLeaves, vVolume, pPivot );
+    RetValue1 = Ivy_ManFindBoolCut_rec( p, Ivy_ObjFanin1(pObj), vLeaves, vVolume, pPivot );
     if ( !RetValue0 && !RetValue1 )
         return 0;
     // add new leaves
@@ -296,7 +296,7 @@ int Ivy_ManFindBoolCutCost( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_ManFindBoolCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVolume, Vec_Ptr_t * vLeaves )
+int Ivy_ManFindBoolCut( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVolume, Vec_Ptr_t * vLeaves )
 {
     Ivy_Obj_t * pObj, * pFaninC, * pFanin0, * pFanin1, * pPivot;
     int RetValue, LevelLimit, Lev, k;
@@ -405,7 +405,7 @@ int Ivy_ManFindBoolCut( Ivy_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVolu
     // cut exists, collect all the nodes on the shortest path to the pivot
     Vec_PtrClear( vLeaves );
     Vec_PtrClear( vVolume );
-    RetValue = Ivy_ManFindBoolCut_rec( pRoot, vLeaves, vVolume, pPivot );
+    RetValue = Ivy_ManFindBoolCut_rec( p, pRoot, vLeaves, vVolume, pPivot );
     assert( RetValue == 1 );
     // unmark the nodes on the frontier (including the pivot)
     Vec_PtrForEachEntry( vFront, pObj, k )
@@ -481,7 +481,7 @@ void Ivy_ManTestCutsBool( Ivy_Man_t * p )
         }
         if ( Ivy_ObjIsExor(pObj) )
             printf( "x" );
-        RetValue = Ivy_ManFindBoolCut( pObj, vFront, vVolume, vLeaves );
+        RetValue = Ivy_ManFindBoolCut( p, pObj, vFront, vVolume, vLeaves );
         if ( RetValue == 0 )
             printf( "- " );
         else
@@ -783,11 +783,11 @@ void Ivy_NodePrintCuts( Ivy_Store_t * pCutStore )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Obj_t * pObj, int nLeaves )
+Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves )
 {
     static Ivy_Store_t CutStore, * pCutStore = &CutStore;
     Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut;
-    Ivy_Man_t * pMan = Ivy_ObjMan(pObj);
+    Ivy_Man_t * pMan = p;
     Ivy_Obj_t * pLeaf;
     int i, k;
 
@@ -815,7 +815,7 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Obj_t * pObj, int nLeaves )
             continue;
         for ( k = 0; k < pCut->nSize; k++ )
         {
-            pLeaf = Ivy_ObjObj( pObj, pCut->pArray[k] );
+            pLeaf = Ivy_ManObj( p, pCut->pArray[k] );
             if ( Ivy_ObjIsCi(pLeaf) )
                 continue;
             *pCutNew = *pCut;
@@ -859,7 +859,7 @@ void Ivy_ManTestCutsAll( Ivy_Man_t * p )
     {
         if ( !Ivy_ObjIsNode(pObj) )
             continue;
-        nCutsCut    = Ivy_NodeFindCutsAll( pObj, 4 )->nCuts;
+        nCutsCut    = Ivy_NodeFindCutsAll( p, pObj, 5 )->nCuts;
         nCutsTotal += nCutsCut;
         nNodeOver  += (nCutsCut == IVY_CUT_LIMIT);
         nNodeTotal++;

src/temp/ivy/ivyDfs.c

@@ -69,17 +69,14 @@ Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p )
     Vec_Int_t * vNodes;
     Ivy_Obj_t * pObj;
     int i;
+    assert( Ivy_ManLatchNum(p) == 0 );
     // make sure the nodes are not marked
     Ivy_ManForEachObj( p, pObj, i )
         assert( !pObj->fMarkA && !pObj->fMarkB );
     // collect the nodes
     vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
-    if ( Ivy_ManLatchNum(p) > 0 )
-        Ivy_ManForEachCo( p, pObj, i )
-            Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
-    else
-        Ivy_ManForEachPo( p, pObj, i )
-            Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+    Ivy_ManForEachPo( p, pObj, i )
+        Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
     // unmark the collected nodes
     Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
         Ivy_ObjClearMarkA(pObj);
@@ -90,34 +87,7 @@ Vec_Int_t * Ivy_ManDfs( Ivy_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Collects nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManDfsExt_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
-{
-    Vec_Int_t * vFanins;
-    int i, Fanin;
-    if ( !Ivy_ObjIsNodeExt(pObj) || Ivy_ObjIsMarkA(pObj) )
-        return;
-    // mark the node as visited
-    Ivy_ObjSetMarkA(pObj);
-    // traverse the fanins
-    vFanins = Ivy_ObjGetFanins( pObj );
-    Vec_IntForEachEntry( vFanins, Fanin, i )
-        Ivy_ManDfsExt_rec( Ivy_ObjObj(pObj, Ivy_EdgeId(Fanin)), vNodes );
-    // add the node
-    Vec_IntPush( vNodes, pObj->Id );
-} 
-
-/**Function*************************************************************
-
-  Synopsis    [Collects nodes in the DFS order.]
+  Synopsis    [Collects AND/EXOR nodes in the DFS order from CIs to COs.]
 
   Description []
                
@@ -126,25 +96,31 @@ void Ivy_ManDfsExt_rec( Ivy_Obj_t * pObj, Vec_Int_t * vNodes )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Ivy_ManDfsExt( Ivy_Man_t * p )
+Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches )
 {
-    Vec_Int_t * vNodes;
-    Ivy_Obj_t * pObj, * pFanin;
+    Vec_Int_t * vNodes, * vLatches;
+    Ivy_Obj_t * pObj;
     int i;
-    assert( p->fExtended ); 
-    assert( Ivy_ManLatchNum(p) == 0 ); 
-    // make sure network does not have buffers
-    vNodes = Vec_IntAlloc( 10 );
+    assert( Ivy_ManLatchNum(p) > 0 );
+    // make sure the nodes are not marked
+    Ivy_ManForEachObj( p, pObj, i )
+        assert( !pObj->fMarkA && !pObj->fMarkB );
+    // collect the latches
+    vLatches = Vec_IntAlloc( Ivy_ManLatchNum(p) );
+    Ivy_ManForEachLatch( p, pObj, i )
+        Vec_IntPush( vLatches, pObj->Id );
+    // collect the nodes
+    vNodes = Vec_IntAlloc( Ivy_ManNodeNum(p) );
     Ivy_ManForEachPo( p, pObj, i )
-    {
-        pFanin = Ivy_ManObj( p, Ivy_EdgeId( Ivy_ObjReadFanin(pObj,0) ) );
-        Ivy_ManDfsExt_rec( pFanin, vNodes );
-    }
+        Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+    Ivy_ManForEachNodeVec( p, vLatches, pObj, i )
+        Ivy_ManDfs_rec( Ivy_ObjFanin0(pObj), vNodes );
+    // unmark the collected nodes
     Ivy_ManForEachNodeVec( p, vNodes, pObj, i )
         Ivy_ObjClearMarkA(pObj);
     // make sure network does not have dangling nodes
-    // the network may have dangling nodes if some fanins of ESOPs do not appear in cubes
-//    assert( p->nNodes == Vec_PtrSize(vNodes) );
+    assert( Vec_IntSize(vNodes) == Ivy_ManNodeNum(p) + Ivy_ManBufNum(p) );
+    *pvLatches = vLatches;
     return vNodes;
 }
 
@@ -249,7 +225,7 @@ Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p )
     int i, k, Level, LevelMax;
     assert( p->vRequired == NULL );
     // start the required times
-    vLevelsR = Vec_IntStart( Ivy_ManObjIdNext(p) );
+    vLevelsR = Vec_IntStart( Ivy_ManObjIdMax(p) + 1 );
     // iterate through the nodes in the reverse order
     vNodes = Ivy_ManLevelize( p );
     Vec_VecForEachEntryReverseReverse( vNodes, pObj, i, k )
@@ -262,7 +238,7 @@ Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p )
     }
     Vec_VecFree( vNodes );
     // convert it into the required times
-    LevelMax = Ivy_ManReadLevels( p );
+    LevelMax = Ivy_ManLevels( p );
 //printf( "max %5d\n",LevelMax );
     Ivy_ManForEachObj( p, pObj, i )
     {

src/temp/ivy/ivyDsd.c

@@ -608,7 +608,7 @@ Ivy_Obj_t * Ivy_ManDsdConstruct_rec( Ivy_Man_t * p, Vec_Int_t * vFront, int iNod
 
 //        Ivy_MultiEval( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
 
-        pResult = Ivy_Multi( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
+        pResult = Ivy_Multi( p, pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
         return Ivy_NotCond( pResult, Node.fCompl );
     }
     assert( Node.fCompl == 0 );
@@ -626,9 +626,9 @@ Ivy_Obj_t * Ivy_ManDsdConstruct_rec( Ivy_Man_t * p, Vec_Int_t * vFront, int iNod
         pNodes[1] = Ivy_NotCond( pNodes[1], (Var1 & 1) );
         pNodes[2] = Ivy_NotCond( pNodes[2], (Var0 & 1) );
         if ( Node.Type == IVY_DEC_MUX )
-            return Ivy_Mux( pNodes[0], pNodes[1], pNodes[2] );
+            return Ivy_Mux( p, pNodes[0], pNodes[1], pNodes[2] );
         else
-            return Ivy_Maj( pNodes[0], pNodes[1], pNodes[2] );
+            return Ivy_Maj( p, pNodes[0], pNodes[1], pNodes[2] );
     }
     assert( 0 );
     return 0;

src/temp/ivy/ivyIsop.c

+/**CFile****************************************************************
+
+  FileName    [ivyIsop.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Computing irredundant SOP using truth table.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyIsop.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ivy_Sop_t_ Ivy_Sop_t;
+struct Ivy_Sop_t_
+{
+    unsigned * pCubes;
+    int        nCubes;
+};
+
+static Mem_Flex_t * s_Man = NULL;
+
+static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TruthManStart()
+{
+    s_Man = Mem_FlexStart();
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_TruthManStop()
+{
+    Mem_FlexStop( s_Man, 0 );
+    s_Man = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Ivy_TruthIsop( unsigned * uTruth, int nVars )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes ISOP for 5 variables or less.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes )
+{
+    Ivy_Sop_t cRes0, cRes1, cRes2;
+    Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
+    unsigned * puRes0, * puRes1, * puRes2;
+    unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp0, * pTemp1;
+    int i, k, Var, nWords;
+    assert( nVars > 5 );
+    assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) );
+    if ( Extra_TruthIsConst0( puOn, nVars ) )
+    {
+        pcRes->nCubes = 0;
+        pcRes->pCubes = NULL;
+        return puOn;
+    }
+    if ( Extra_TruthIsConst1( puOnDc, nVars ) )
+    {
+        pcRes->nCubes = 1;
+        pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 );
+        pcRes->pCubes[0] = 0;
+        return puOnDc;
+    }
+    // find the topmost var
+    for ( Var = nVars-1; Var >= 0; Var-- )
+        if ( Extra_TruthVarInSupport( puOn, nVars, Var ) || 
+             Extra_TruthVarInSupport( puOnDc, nVars, Var ) )
+             break;
+    assert( Var >= 0 );
+    if ( Var < 5 )
+    {
+        unsigned * puRes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 );
+        *puRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var + 1, pcRes );
+        return puRes;
+    }
+    nWords = Extra_TruthWordNum( Var+1 );
+    // cofactor
+    puOn0 = puOn;
+    puOn1 = puOn + nWords;
+    puOnDc0 = puOnDc;
+    puOnDc1 = puOnDc + nWords;
+    // intermediate copies
+    pTemp0 = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWords );
+    pTemp1 = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWords );
+    // solve for cofactors
+    Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var + 1 );
+    puRes0 = Ivy_TruthIsop5_rec( pTemp0, uOnDc0, Var-1, pcRes0 );
+    Extra_TruthSharp( pTemp0, puOn1, puOnDc0, Var + 1 );
+    puRes1 = Ivy_TruthIsop5_rec( pTemp1, uOnDc1, Var-1, pcRes1 );
+    Extra_TruthSharp( pTemp0, puOn0, puRes0, Var + 1 );
+    Extra_TruthSharp( pTemp1, puOn1, puRes1, Var + 1 );
+    Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var + 1 );
+    Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var + 1 );
+    puRes2 = Ivy_TruthIsop5_rec( pTemp0, pTemp1, Var-1, pcRes2 );
+    // create the resulting cover
+    pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
+    pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes );
+    k = 0;
+    for ( i = 0; i < pcRes0->nCubes; i++ )
+        pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
+    for ( i = 0; i < pcRes1->nCubes; i++ )
+        pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0));
+    for ( i = 0; i < pcRes1->nCubes; i++ )
+        pcRes->pCubes[k++] = pcRes2->pCubes[i];
+    assert( k == pcRes->nCubes );
+    // create the resulting truth table
+    Extra_TruthSharp( pTemp0, Var, uRes0, uRes1, Var + 1 );
+    Extra_TruthOr( pTemp0, pTemp0, uRes2, Var + 1 );
+    return pTemp0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes ISOP for 5 variables or less.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes )
+{
+    unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+    Ivy_Sop_t cRes0, cRes1, cRes2;
+    Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
+    unsigned uRes0, uRes1, uRes2;
+    unsigned uOn0, uOn1, uOnDc0, uOnDc1;
+    int i, k, Var;
+    assert( nVars <= 5 );
+    assert( uOn & ~uOnDc == 0 );
+    if ( Extra_TruthIsConst0( uOn == 0 )
+    {
+        pcRes->nCubes = 0;
+        pcRes->pCubes = NULL;
+        return 0;
+    }
+    if ( uOnDc == 0xFFFFFFFF )
+    {
+        pcRes->nCubes = 1;
+        pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 );
+        pcRes->pCubes[0] = 0;
+        return 0xFFFFFFFF;
+    }
+    // find the topmost var
+    for ( Var = nVars-1; Var >= 0; Var-- )
+        if ( Extra_TruthVarInSupport( &uOn, 5, Var ) || 
+             Extra_TruthVarInSupport( &uOnDc, 5, Var ) )
+             break;
+    assert( Var >= 0 );
+    // cofactor
+    uOn0 = uOn1 = uOn;
+    uOnDc0 = uOnDc1 = uOnDc;
+    Extra_TruthCofactor0( &uOn0, 5, Var );
+    Extra_TruthCofactor1( &uOn1, 5, Var );
+    Extra_TruthCofactor0( &uOnDc0, 5, Var );
+    Extra_TruthCofactor1( &uOnDc1, 5, Var );
+    // solve for cofactors
+    uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var-1, pcRes0 );
+    uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var-1, pcRes1 );
+    uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var-1, pcRes2 );
+    // create the resulting cover
+    pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
+    pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes );
+    k = 0;
+    for ( i = 0; i < pcRes0->nCubes; i++ )
+        pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1));
+    for ( i = 0; i < pcRes1->nCubes; i++ )
+        pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0));
+    for ( i = 0; i < pcRes1->nCubes; i++ )
+        pcRes->pCubes[k++] = pcRes2->pCubes[i];
+    assert( k == pcRes->nCubes );
+    return (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]) | uRes2;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/temp/ivy/ivyMan.c

@@ -39,53 +39,32 @@
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax )
+Ivy_Man_t * Ivy_ManStart()
 {
     Ivy_Man_t * p;
-    Ivy_Obj_t * pObj;
-    int i, nTotalSize;
     // start the manager
     p = ALLOC( Ivy_Man_t, 1 );
     memset( p, 0, sizeof(Ivy_Man_t) );
+    // perform initializations
+    p->Ghost.Id = -1;
     p->nTravIds = 1;
     p->fCatchExor = 1;
-    // AIG nodes
-    p->nObjsAlloc = 1 + nPis + nPos + nNodesMax;
-//    p->nObjsAlloc += (p->nObjsAlloc & 1); // make it even
-    nTotalSize = p->nObjsAlloc + IVY_SANDBOX_SIZE + 1;
-    p->pObjs = ALLOC( Ivy_Obj_t, nTotalSize );
-    memset( p->pObjs, 0, sizeof(Ivy_Obj_t) * nTotalSize );
-    // temporary storage for deleted entries
-    p->vFree  = Vec_IntAlloc( 100 );
-    // set the node IDs
-    for ( i = 0, pObj = p->pObjs; i < nTotalSize; i++, pObj++ )
-        pObj->Id = i - IVY_SANDBOX_SIZE - 1;
-    // remember the manager in the first entry
-    *((Ivy_Man_t **)p->pObjs) = p; 
-    p->pObjs += IVY_SANDBOX_SIZE + 1;
+    // allocate arrays for nodes
+    p->vPis = Vec_PtrAlloc( 100 );
+    p->vPos = Vec_PtrAlloc( 100 );
+    p->vBufs = Vec_PtrAlloc( 100 );
+    p->vObjs = Vec_PtrAlloc( 100 );
+    // prepare the internal memory manager
+    Ivy_ManStartMemory( p );
     // create the constant node
+    p->pConst1 = Ivy_ManFetchMemory( p );
+    p->pConst1->fPhase = 1;
+    Vec_PtrPush( p->vObjs, p->pConst1 );
     p->nCreated = 1;
-    p->ObjIdNext = 1;
-    Ivy_ManConst1(p)->fPhase = 1;
-    // create PIs
-    pObj = Ivy_ManGhost(p);
-    pObj->Type = IVY_PI;
-    p->vPis = Vec_IntAlloc( 100 );
-    for ( i = 0; i < nPis; i++ )
-        Ivy_ObjCreate( pObj );
-    // create POs
-    pObj->Type = IVY_PO;
-    p->vPos = Vec_IntAlloc( 100 );
-    for ( i = 0; i < nPos; i++ )
-        Ivy_ObjCreate( pObj );
     // start the table
-    p->nTableSize = p->nObjsAlloc*5/2+13;
+    p->nTableSize = 10007;
     p->pTable = ALLOC( int, p->nTableSize );
     memset( p->pTable, 0, sizeof(int) * p->nTableSize );
-    // allocate undo storage
-    p->nUndosAlloc = 100;
-    p->pUndos = ALLOC( Ivy_Obj_t, p->nUndosAlloc );
-    memset( p->pUndos, 0, sizeof(Ivy_Obj_t) * p->nUndosAlloc );
     return p;
 }
 
@@ -102,22 +81,15 @@ Ivy_Man_t * Ivy_ManStart( int nPis, int nPos, int nNodesMax )
 ***********************************************************************/
 void Ivy_ManStop( Ivy_Man_t * p )
 {
-    if ( p->fExtended )
-    {
-        Ivy_Obj_t * pObj;
-        int i;
-        Ivy_ManForEachObj( p, pObj, i )
-            if ( Ivy_ObjGetFanins(pObj) )
-                Vec_IntFree( Ivy_ObjGetFanins(pObj) );
-    }
-    if ( p->vFree )   Vec_IntFree( p->vFree );
-    if ( p->vTruths ) Vec_IntFree( p->vTruths );
-    if ( p->vPis )    Vec_IntFree( p->vPis );
-    if ( p->vPos )    Vec_IntFree( p->vPos );
-    FREE( p->pMemory );
-    free( p->pObjs - IVY_SANDBOX_SIZE - 1 );
+//    Ivy_TableProfile( p );
+    if ( p->vFanouts )  Ivy_ManStopFanout( p );
+    if ( p->vChunks )   Ivy_ManStopMemory( p );
+    if ( p->vRequired ) Vec_IntFree( p->vRequired );
+    if ( p->vPis )      Vec_PtrFree( p->vPis );
+    if ( p->vPos )      Vec_PtrFree( p->vPos );
+    if ( p->vBufs )     Vec_PtrFree( p->vBufs );
+    if ( p->vObjs )     Vec_PtrFree( p->vObjs );
     free( p->pTable );
-    free( p->pUndos );
     free( p );
 }
 
@@ -132,18 +104,15 @@ void Ivy_ManStop( Ivy_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManGrow( Ivy_Man_t * p )
+int Ivy_ManCleanup( Ivy_Man_t * p )
 {
-    int i;
-    assert( p->ObjIdNext == p->nObjsAlloc );
-    if ( p->ObjIdNext != p->nObjsAlloc )
-        return;
-//    printf( "Ivy_ObjCreate(): Reallocing the node array.\n" );
-    p->nObjsAlloc = 2 * p->nObjsAlloc;
-    p->pObjs = REALLOC( Ivy_Obj_t, p->pObjs - IVY_SANDBOX_SIZE - 1, p->nObjsAlloc + IVY_SANDBOX_SIZE + 1 ) + IVY_SANDBOX_SIZE + 1;
-    memset( p->pObjs + p->ObjIdNext, 0, sizeof(Ivy_Obj_t) * p->nObjsAlloc / 2 );
-    for ( i = p->nObjsAlloc / 2; i < p->nObjsAlloc; i++ )
-        Ivy_ManObj( p, i )->Id = i;
+    Ivy_Obj_t * pNode;
+    int i, nNodesOld;
+    nNodesOld = Ivy_ManNodeNum(p);
+    Ivy_ManForEachNode( p, pNode, i )
+        if ( Ivy_ObjRefs(pNode) == 0 )
+            Ivy_ObjDelete_rec( p, pNode, 1 );
+    return nNodesOld - Ivy_ManNodeNum(p);
 }
 
 /**Function*************************************************************
@@ -157,15 +126,19 @@ void Ivy_ManGrow( Ivy_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_ManCleanup( Ivy_Man_t * p )
+int Ivy_ManPropagateBuffers( Ivy_Man_t * p )
 {
     Ivy_Obj_t * pNode;
-    int i, nNodesOld;
-    nNodesOld = Ivy_ManNodeNum(p);
-    Ivy_ManForEachNode( p, pNode, i )
-        if ( Ivy_ObjRefs(pNode) == 0 )
-            Ivy_ObjDelete_rec( pNode, 1 );
-    return nNodesOld - Ivy_ManNodeNum(p);
+    int nSteps;
+    for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ )
+    {
+        pNode = Vec_PtrEntryLast(p->vBufs);
+        while ( Ivy_ObjIsBuf(pNode) )
+            pNode = Ivy_ObjReadFirstFanout( p, pNode );
+        Ivy_NodeFixBufferFanins( p, pNode );
+    }
+//    printf( "Number of steps = %d\n", nSteps );
+    return nSteps;
 }
 
 /**Function*************************************************************
@@ -182,24 +155,71 @@ int Ivy_ManCleanup( Ivy_Man_t * p )
 void Ivy_ManPrintStats( Ivy_Man_t * p )
 {
     printf( "PI/PO = %d/%d ", Ivy_ManPiNum(p), Ivy_ManPoNum(p) );
-    if ( p->fExtended )
-    {
-    printf( "Am = %d. ",    Ivy_ManAndMultiNum(p) );
-    printf( "Xm = %d. ",    Ivy_ManExorMultiNum(p) );
-    printf( "Lut = %d. ",   Ivy_ManLutNum(p) );
-    }
-    else
+    printf( "A = %d. ",       Ivy_ManAndNum(p) );
+    printf( "L = %d. ",       Ivy_ManLatchNum(p) );
+//    printf( "X = %d. ",       Ivy_ManExorNum(p) );
+    printf( "B = %d. ",       Ivy_ManBufNum(p) );
+    printf( "MaxID = %d. ",   Ivy_ManObjIdMax(p) );
+//    printf( "Cre = %d. ",     p->nCreated );
+//    printf( "Del = %d. ",     p->nDeleted );
+    printf( "Lev = %d. ",     Ivy_ManLatchNum(p)? -1 : Ivy_ManLevels(p) );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts a combinational AIG manager into a sequential one.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits )
+{
+    Ivy_Obj_t * pObj, * pLatch;
+    Ivy_Init_t Init;
+    int i;
+    if ( nLatches == 0 )
+        return;
+    assert( nLatches < Ivy_ManPiNum(p) && nLatches < Ivy_ManPoNum(p) );
+    assert( Ivy_ManPiNum(p) == Vec_PtrSize(p->vPis) );
+    assert( Ivy_ManPoNum(p) == Vec_PtrSize(p->vPos) );
+    assert( Vec_PtrSize( p->vBufs ) == 0 );
+    // create fanouts
+    if ( p->vFanouts == NULL )
+        Ivy_ManStartFanout( p );
+    // collect the POs to be converted into latches
+    for ( i = 0; i < nLatches; i++ )
     {
-    printf( "A = %d. ",     Ivy_ManAndNum(p) );
-    printf( "X = %d. ",     Ivy_ManExorNum(p) );
-    printf( "B = %4d. ",     Ivy_ManBufNum(p) );
+        // get the latch value
+        Init = pInits? pInits[i] : IVY_INIT_0;
+        // create latch
+        pObj = Ivy_ManPo( p, Ivy_ManPoNum(p) - nLatches + i );
+        pLatch = Ivy_Latch( p, Ivy_ObjChild0(pObj), Init );
+        Ivy_ObjDisconnect( p, pObj );
+        // convert the corresponding PI to a buffer and connect it to the latch
+        pObj = Ivy_ManPi( p, Ivy_ManPiNum(p) - nLatches + i );
+        pObj->Type = IVY_BUF;
+        Ivy_ObjConnect( p, pObj, pLatch, NULL );
+        // save the buffer
+        Vec_PtrPush( p->vBufs, pObj );
     }
-//    printf( "MaxID = %d. ", p->ObjIdNext-1 );
-//    printf( "All = %d. ",   p->nObjsAlloc );
-    printf( "Cre = %d. ",   p->nCreated );
-    printf( "Del = %d. ",   p->nDeleted );
-    printf( "Lev = %d. ",   Ivy_ManReadLevels(p) );
-    printf( "\n" );
+    // shrink the arrays
+    Vec_PtrShrink( p->vPis, Ivy_ManPiNum(p) - nLatches );
+    Vec_PtrShrink( p->vPos, Ivy_ManPoNum(p) - nLatches );
+    // update the counters of different objects
+    p->nObjs[IVY_PI] -= nLatches;
+    p->nObjs[IVY_PO] -= nLatches;
+    p->nObjs[IVY_BUF] += nLatches;
+    p->nDeleted -= 2 * nLatches;
+    // perform hashing by propagating the buffers
+    Ivy_ManPropagateBuffers( p );
+    // check the resulting network
+    if ( !Ivy_ManCheck(p) )
+        printf( "Ivy_ManMakeSeq(): The check has failed.\n" );
 }
 
 ////////////////////////////////////////////////////////////////////////

src/temp/ivy/ivyMem.c

+/**CFile****************************************************************
+
+  FileName    [ivyMem.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Memory management for the AIG nodes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyMem.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// memory management
+#define IVY_PAGE_SIZE      12        // page size containing 2^IVY_PAGE_SIZE nodes
+#define IVY_PAGE_MASK    4095        // page bitmask (2^IVY_PAGE_SIZE)-1
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the internal memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManStartMemory( Ivy_Man_t * p )
+{
+    p->vChunks = Vec_PtrAlloc( 128 );
+    p->vPages = Vec_PtrAlloc( 128 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the internal memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManStopMemory( Ivy_Man_t * p )
+{
+    void * pMemory;
+    int i;
+    Vec_PtrForEachEntry( p->vChunks, pMemory, i )
+        free( pMemory );
+    Vec_PtrFree( p->vChunks );
+    Vec_PtrFree( p->vPages );
+    p->pListFree = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Allocates additional memory for the nodes.]
+
+  Description [Allocates IVY_PAGE_SIZE nodes. Aligns memory by 32 bytes. 
+  Records the pointer to the AIG manager in the -1 entry.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_ManAddMemory( Ivy_Man_t * p )
+{
+    char * pMemory;
+    int i, nBytes;
+    assert( sizeof(Ivy_Obj_t) <= 32 );
+    assert( p->pListFree == NULL );
+    assert( (Ivy_ManObjNum(p) & IVY_PAGE_MASK) == 0 );
+    // allocate new memory page
+    nBytes = sizeof(Ivy_Obj_t) * (1<<IVY_PAGE_SIZE) + 32;
+    pMemory = ALLOC( char, nBytes );
+    Vec_PtrPush( p->vChunks, pMemory );
+    // align memory at the 32-byte boundary
+    pMemory = pMemory + 32 - (((int)pMemory) & 31);
+    // remember the manager in the first entry
+    Vec_PtrPush( p->vPages, pMemory );
+    // break the memory down into nodes
+    p->pListFree = (Ivy_Obj_t *)pMemory;
+    for ( i = 1; i <= IVY_PAGE_MASK; i++ )
+    {
+        *((char **)pMemory) = pMemory + sizeof(Ivy_Obj_t);
+        pMemory += sizeof(Ivy_Obj_t);
+    }
+    *((char **)pMemory) = NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/temp/ivy/ivyMulti.c

@@ -34,8 +34,8 @@ struct Ivy_Eva_t_
     int         Weight;   // the number of covered nodes
 };
 
-static void Ivy_MultiPrint( Ivy_Eva_t * pEvals, int nLeaves, int nEvals );
-static int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols );
+static void Ivy_MultiPrint( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals );
+static int Ivy_MultiCover( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -52,7 +52,7 @@ static int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLim
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSols )
+int Ivy_MultiPlus( Ivy_Man_t * p, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int nLimit, Vec_Ptr_t * vSols )
 {
     static Ivy_Eva_t pEvals[IVY_EVAL_LIMIT];
     Ivy_Eva_t * pEval, * pFan0, * pFan1;
@@ -122,7 +122,7 @@ int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int
     {
         pFan0 = pEvals + i;
         pFan1 = pEvals + k;
-        pTemp = Ivy_TableLookup(Ivy_ObjCreateGhost(pFan0->pArg, pFan1->pArg, Type, IVY_INIT_NONE));
+        pTemp = Ivy_TableLookup(p, Ivy_ObjCreateGhost(p, pFan0->pArg, pFan1->pArg, Type, IVY_INIT_NONE));
         // skip nodes in the cone
         if ( pTemp == NULL || pTemp->fMarkB )
             continue;
@@ -149,7 +149,7 @@ int Ivy_MultiPlus( Vec_Ptr_t * vLeaves, Vec_Ptr_t * vCone, Ivy_Type_t Type, int
 Outside:
 
 //    Ivy_MultiPrint( pEvals, nLeaves, nEvals );
-    if ( !Ivy_MultiCover( pEvals, nLeaves, nEvals, nLimit, vSols ) )
+    if ( !Ivy_MultiCover( p, pEvals, nLeaves, nEvals, nLimit, vSols ) )
         return 0;
     assert( Vec_PtrSize( vSols ) > 0 );
     return 1;
@@ -166,7 +166,7 @@ Outside:
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_MultiPrint( Ivy_Eva_t * pEvals, int nLeaves, int nEvals )
+void Ivy_MultiPrint( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals )
 {
     Ivy_Eva_t * pEval;
     int i, k;
@@ -215,7 +215,7 @@ static inline int Ivy_MultiWeight( unsigned uMask, int nMaskOnes, unsigned uFoun
   SeeAlso     []
 
 ***********************************************************************/
-int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols )
+int Ivy_MultiCover( Ivy_Man_t * p, Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec_Ptr_t * vSols )
 {
     int fVerbose = 0;
     Ivy_Eva_t * pEval, * pEvalBest;
@@ -294,6 +294,45 @@ int Ivy_MultiCover( Ivy_Eva_t * pEvals, int nLeaves, int nEvals, int nLimit, Vec
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Constructs the well-balanced tree of gates.]
+
+  Description [Disregards levels and possible logic sharing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi_rec( Ivy_Man_t * p, Ivy_Obj_t ** ppObjs, int nObjs, Ivy_Type_t Type )
+{
+    Ivy_Obj_t * pObj1, * pObj2;
+    if ( nObjs == 1 )
+        return ppObjs[0];
+    pObj1 = Ivy_Multi_rec( p, ppObjs,           nObjs/2,         Type );
+    pObj2 = Ivy_Multi_rec( p, ppObjs + nObjs/2, nObjs - nObjs/2, Type );
+    return Ivy_Oper( p, pObj1, pObj2, Type );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Old code.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Multi( Ivy_Man_t * p, Ivy_Obj_t ** pArgs, int nArgs, Ivy_Type_t Type )
+{
+    assert( Type == IVY_AND || Type == IVY_EXOR );
+    assert( nArgs > 0 );
+    return Ivy_Multi_rec( p, pArgs, nArgs, Type );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/temp/ivy/ivyOper.c

@@ -57,12 +57,12 @@ static inline int Ivy_ObjIsExorType( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Obj_t *
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type )
+Ivy_Obj_t * Ivy_Oper( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type )
 {
     if ( Type == IVY_AND )
-        return Ivy_And( p0, p1 );
+        return Ivy_And( p, p0, p1 );
     if ( Type == IVY_EXOR )
-        return Ivy_Exor( p0, p1 );
+        return Ivy_Exor( p, p0, p1 );
     assert( 0 );
     return NULL;
 }
@@ -78,23 +78,22 @@ Ivy_Obj_t * Ivy_Oper( Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
+Ivy_Obj_t * Ivy_And( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
 {
-    Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0));
 //    Ivy_Obj_t * pFan0, * pFan1;
     // check trivial cases
     if ( p0 == p1 )
         return p0;
     if ( p0 == Ivy_Not(p1) )
-        return Ivy_Not(pConst1);
-    if ( Ivy_Regular(p0) == pConst1 )
-        return p0 == pConst1 ? p1 : Ivy_Not(pConst1);
-    if ( Ivy_Regular(p1) == pConst1 )
-        return p1 == pConst1 ? p0 : Ivy_Not(pConst1);
+        return Ivy_Not(p->pConst1);
+    if ( Ivy_Regular(p0) == p->pConst1 )
+        return p0 == p->pConst1 ? p1 : Ivy_Not(p->pConst1);
+    if ( Ivy_Regular(p1) == p->pConst1 )
+        return p1 == p->pConst1 ? p0 : Ivy_Not(p->pConst1);
     // check if it can be an EXOR gate
 //    if ( Ivy_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) )
 //        return Ivy_CanonExor( pFan0, pFan1 );
-    return Ivy_CanonAnd( p0, p1 );
+    return Ivy_CanonAnd( p, p0, p1 );
 }
 
 /**Function*************************************************************
@@ -108,36 +107,22 @@ Ivy_Obj_t * Ivy_And( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_Exor( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
+Ivy_Obj_t * Ivy_Exor( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
 {
-    Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0));
+/*
     // check trivial cases
     if ( p0 == p1 )
-        return Ivy_Not(pConst1);
+        return Ivy_Not(p->pConst1);
     if ( p0 == Ivy_Not(p1) )
-        return pConst1;
-    if ( Ivy_Regular(p0) == pConst1 )
-        return Ivy_NotCond( p1, p0 == pConst1 );
-    if ( Ivy_Regular(p1) == pConst1 )
-        return Ivy_NotCond( p0, p1 == pConst1 );
+        return p->pConst1;
+    if ( Ivy_Regular(p0) == p->pConst1 )
+        return Ivy_NotCond( p1, p0 == p->pConst1 );
+    if ( Ivy_Regular(p1) == p->pConst1 )
+        return Ivy_NotCond( p0, p1 == p->pConst1 );
     // check the table
-    return Ivy_CanonExor( p0, p1 );
-}
- 
-/**Function*************************************************************
-
-  Synopsis    [Performs canonicization step.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ivy_Obj_t * Ivy_Latch( Ivy_Obj_t * pObj, Ivy_Init_t Init )
-{
-    return Ivy_CanonLatch( pObj, Init );
+    return Ivy_CanonExor( p, p0, p1 );
+*/
+    return Ivy_Or( p, Ivy_And(p, p0, Ivy_Not(p1)), Ivy_And(p, Ivy_Not(p0), p1) );
 }
 
 /**Function*************************************************************
@@ -151,9 +136,9 @@ Ivy_Obj_t * Ivy_Latch( Ivy_Obj_t * pObj, Ivy_Init_t Init )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_Or( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
+Ivy_Obj_t * Ivy_Or( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
 {
-    return Ivy_Not( Ivy_And( Ivy_Not(p0), Ivy_Not(p1) ) );
+    return Ivy_Not( Ivy_And( p, Ivy_Not(p0), Ivy_Not(p1) ) );
 }
 
 /**Function*************************************************************
@@ -167,43 +152,42 @@ Ivy_Obj_t * Ivy_Or( Ivy_Obj_t * p0, Ivy_Obj_t * p1 )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 )
+Ivy_Obj_t * Ivy_Mux( Ivy_Man_t * p, Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 )
 {
-    Ivy_Obj_t * pConst1 = Ivy_ObjConst1(Ivy_Regular(p0));
     Ivy_Obj_t * pTempA1, * pTempA2, * pTempB1, * pTempB2, * pTemp;
     int Count0, Count1;
     // consider trivial cases
     if ( p0 == Ivy_Not(p1) )
-        return Ivy_Exor( pC, p0 );
+        return Ivy_Exor( p, pC, p0 );
     // other cases can be added
     // implement the first MUX (F = C * x1 + C' * x0)
-    pTempA1 = Ivy_TableLookup( Ivy_ObjCreateGhost(pC,          p1, IVY_AND, IVY_INIT_NONE) );
-    pTempA2 = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pC), p0, IVY_AND, IVY_INIT_NONE) );
+    pTempA1 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pC,          p1, IVY_AND, IVY_INIT_NONE) );
+    pTempA2 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pC), p0, IVY_AND, IVY_INIT_NONE) );
     if ( pTempA1 && pTempA2 )
     {
-        pTemp = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pTempA1), Ivy_Not(pTempA2), IVY_AND, IVY_INIT_NONE) );
+        pTemp = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pTempA1), Ivy_Not(pTempA2), IVY_AND, IVY_INIT_NONE) );
         if ( pTemp ) return Ivy_Not(pTemp);
     }
     Count0 = (pTempA1 != NULL) + (pTempA2 != NULL);
     // implement the second MUX (F' = C * x1' + C' * x0')
-    pTempB1 = Ivy_TableLookup( Ivy_ObjCreateGhost(pC,          Ivy_Not(p1), IVY_AND, IVY_INIT_NONE) );
-    pTempB2 = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pC), Ivy_Not(p0), IVY_AND, IVY_INIT_NONE) );
+    pTempB1 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pC,          Ivy_Not(p1), IVY_AND, IVY_INIT_NONE) );
+    pTempB2 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pC), Ivy_Not(p0), IVY_AND, IVY_INIT_NONE) );
     if ( pTempB1 && pTempB2 )
     {
-        pTemp = Ivy_TableLookup( Ivy_ObjCreateGhost(Ivy_Not(pTempB1), Ivy_Not(pTempB2), IVY_AND, IVY_INIT_NONE) );
+        pTemp = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Not(pTempB1), Ivy_Not(pTempB2), IVY_AND, IVY_INIT_NONE) );
         if ( pTemp ) return pTemp;
     }
     Count1 = (pTempB1 != NULL) + (pTempB2 != NULL);
     // compare and decide which one to implement
     if ( Count0 >= Count1 )
     {
-        pTempA1 = pTempA1? pTempA1 : Ivy_And(pC,          p1);
-        pTempA2 = pTempA2? pTempA2 : Ivy_And(Ivy_Not(pC), p0);
-        return Ivy_Or( pTempA1, pTempA2 );
+        pTempA1 = pTempA1? pTempA1 : Ivy_And(p, pC,          p1);
+        pTempA2 = pTempA2? pTempA2 : Ivy_And(p, Ivy_Not(pC), p0);
+        return Ivy_Or( p, pTempA1, pTempA2 );
     }
-    pTempB1 = pTempB1? pTempB1 : Ivy_And(pC,          Ivy_Not(p1));
-    pTempB2 = pTempB2? pTempB2 : Ivy_And(Ivy_Not(pC), Ivy_Not(p0));
-    return Ivy_Not( Ivy_Or( pTempB1, pTempB2 ) );
+    pTempB1 = pTempB1? pTempB1 : Ivy_And(p, pC,          Ivy_Not(p1));
+    pTempB2 = pTempB2? pTempB2 : Ivy_And(p, Ivy_Not(pC), Ivy_Not(p0));
+    return Ivy_Not( Ivy_Or( p, pTempB1, pTempB2 ) );
 
 //    return Ivy_Or( Ivy_And(pC, p1), Ivy_And(Ivy_Not(pC), p0) );
 }
@@ -219,9 +203,9 @@ Ivy_Obj_t * Ivy_Mux( Ivy_Obj_t * pC, Ivy_Obj_t * p1, Ivy_Obj_t * p0 )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC )
+Ivy_Obj_t * Ivy_Maj( Ivy_Man_t * p, Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC )
 {
-    return Ivy_Or( Ivy_Or(Ivy_And(pA, pB), Ivy_And(pA, pC)), Ivy_And(pB, pC) );
+    return Ivy_Or( p, Ivy_Or(p, Ivy_And(p, pA, pB), Ivy_And(p, pA, pC)), Ivy_And(p, pB, pC) );
 }
 
 /**Function*************************************************************
@@ -235,16 +219,32 @@ Ivy_Obj_t * Ivy_Maj( Ivy_Obj_t * pA, Ivy_Obj_t * pB, Ivy_Obj_t * pC )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_Miter( Vec_Ptr_t * vPairs )
+Ivy_Obj_t * Ivy_Miter( Ivy_Man_t * p, Vec_Ptr_t * vPairs )
 {
     int i;
     assert( vPairs->nSize > 0 );
     assert( vPairs->nSize % 2 == 0 );
     // go through the cubes of the node's SOP
     for ( i = 0; i < vPairs->nSize; i += 2 )
-        vPairs->pArray[i/2] = Ivy_Not( Ivy_Exor( vPairs->pArray[i], vPairs->pArray[i+1] ) );
+        vPairs->pArray[i/2] = Ivy_Not( Ivy_Exor( p, vPairs->pArray[i], vPairs->pArray[i+1] ) );
     vPairs->nSize = vPairs->nSize/2;
-    return Ivy_Not( Ivy_Multi_rec( (Ivy_Obj_t **)vPairs->pArray, vPairs->nSize, IVY_AND ) );
+    return Ivy_Not( Ivy_Multi_rec( p, (Ivy_Obj_t **)vPairs->pArray, vPairs->nSize, IVY_AND ) );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Performs canonicization step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_Latch( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Init_t Init )
+{
+    return Ivy_CanonLatch( p, pObj, Init );
 }
 
 ////////////////////////////////////////////////////////////////////////

src/temp/ivy/ivyResyn.c

@@ -39,50 +39,59 @@
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel )
+Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * pMan, int fUpdateLevel, int fVerbose )
 {
-    int clk, fVerbose = 0;
+    int clk;
     Ivy_Man_t * pTemp;
 
+if ( fVerbose ) { printf( "Original:\n" ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
+
 clk = clock();
     pMan = Ivy_ManBalance( pMan, fUpdateLevel );
+if ( fVerbose ) { printf( "\n" ); }
 if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 //    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 0 );
 clk = clock();
     Ivy_ManRewritePre( pMan, fUpdateLevel, 0, 0 );
+if ( fVerbose ) { printf( "\n" ); }
 if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 clk = clock();
     pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
     Ivy_ManStop( pTemp );
+if ( fVerbose ) { printf( "\n" ); }
 if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 //    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 );
 clk = clock();
-if ( fVerbose ) Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 );
+    Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 );
+if ( fVerbose ) { printf( "\n" ); }
 if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 clk = clock();
     pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
     Ivy_ManStop( pTemp );
+if ( fVerbose ) { printf( "\n" ); }
 if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 //    Ivy_ManRewriteAlg( pMan, fUpdateLevel, 1 );
 clk = clock();
     Ivy_ManRewritePre( pMan, fUpdateLevel, 1, 0 );
+if ( fVerbose ) { printf( "\n" ); }
 if ( fVerbose ) { PRT( "Rewrite", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
 
 clk = clock();
     pMan = Ivy_ManBalance( pTemp = pMan, fUpdateLevel );
     Ivy_ManStop( pTemp );
+if ( fVerbose ) { printf( "\n" ); }
 if ( fVerbose ) { PRT( "Balance", clock() - clk ); }
 if ( fVerbose ) Ivy_ManPrintStats( pMan );
     return pMan;

src/temp/ivy/ivyTable.c

@@ -12,7 +12,7 @@
   
   Affiliation [UC Berkeley]
 
-  Date        [Ver. 1.0. Started - May 11, 2006.]
+  Date        [Ver. 1.0. Started - May 11, 2006. ]
 
   Revision    [$Id: ivyTable.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
 
@@ -37,22 +37,23 @@ static unsigned Ivy_Hash( Ivy_Obj_t * pObj, int TableSize )
 }
 
 // returns the place where this node is stored (or should be stored)
-static int * Ivy_TableFind( Ivy_Obj_t * pObj )
+static int * Ivy_TableFind( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
-    Ivy_Man_t * p;
     int i;
     assert( Ivy_ObjIsHash(pObj) );
-    p = Ivy_ObjMan(pObj);
     for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
         if ( p->pTable[i] == pObj->Id )
             break;
     return p->pTable + i;
 }
 
+static void         Ivy_TableResize( Ivy_Man_t * p );
+static unsigned int Cudd_PrimeAig( unsigned int  p );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Checks if node with the given attributes is in the hash table.]
@@ -64,27 +65,25 @@ static int * Ivy_TableFind( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Obj_t * Ivy_TableLookup( Ivy_Obj_t * pObj )
+Ivy_Obj_t * Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
-    Ivy_Man_t * p;
     Ivy_Obj_t * pEntry;
     int i;
     assert( !Ivy_IsComplement(pObj) );
     if ( !Ivy_ObjIsHash(pObj) )
         return NULL;
     assert( Ivy_ObjIsLatch(pObj) || Ivy_ObjFaninId0(pObj) > 0 );
-    assert( Ivy_ObjFaninId0(pObj) == 0 || Ivy_ObjFaninId0(pObj) > Ivy_ObjFaninId1(pObj) );
-    p = Ivy_ObjMan(pObj);
+    assert( Ivy_ObjFaninId1(pObj) == 0 || Ivy_ObjFaninId0(pObj) < Ivy_ObjFaninId1(pObj) );
+//    if ( Ivy_ObjFanin0(pObj)->nRefs == 0 || (!Ivy_ObjIsLatch(pObj) && Ivy_ObjFanin1(pObj)->nRefs == 0) )
+//        return NULL;
     for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
     {
-        pEntry = Ivy_ObjObj( pObj, p->pTable[i] );
-        if ( Ivy_ObjFaninId0(pEntry) == Ivy_ObjFaninId0(pObj) && 
-             Ivy_ObjFaninId1(pEntry) == Ivy_ObjFaninId1(pObj) && 
-             Ivy_ObjFaninC0(pEntry) == Ivy_ObjFaninC0(pObj) && 
-             Ivy_ObjFaninC1(pEntry) == Ivy_ObjFaninC1(pObj) && 
+        pEntry = Ivy_ManObj( p, p->pTable[i] );
+        if ( Ivy_ObjChild0(pEntry) == Ivy_ObjChild0(pObj) && 
+             Ivy_ObjChild1(pEntry) == Ivy_ObjChild1(pObj) && 
              Ivy_ObjInit(pEntry) == Ivy_ObjInit(pObj) && 
              Ivy_ObjType(pEntry) == Ivy_ObjType(pObj) )
-            return Ivy_ObjObj( pObj, p->pTable[i] );
+            return pEntry;
     }
     return NULL;
 }
@@ -100,13 +99,18 @@ Ivy_Obj_t * Ivy_TableLookup( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_TableInsert( Ivy_Obj_t * pObj )
+void Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
     int * pPlace;
     assert( !Ivy_IsComplement(pObj) );
     if ( !Ivy_ObjIsHash(pObj) )
         return;
-    pPlace = Ivy_TableFind( pObj );
+    if ( (pObj->Id & 63) == 0 )
+    {
+        if ( p->nTableSize < 2 * Ivy_ManHashObjNum(p) )
+            Ivy_TableResize( p );
+    }
+    pPlace = Ivy_TableFind( p, pObj );
     assert( *pPlace == 0 );
     *pPlace = pObj->Id;
 }
@@ -122,25 +126,23 @@ void Ivy_TableInsert( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_TableDelete( Ivy_Obj_t * pObj )
+void Ivy_TableDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj )
 {
-    Ivy_Man_t * p;
     Ivy_Obj_t * pEntry;
     int i, * pPlace;
     assert( !Ivy_IsComplement(pObj) );
     if ( !Ivy_ObjIsHash(pObj) )
         return;
-    pPlace = Ivy_TableFind( pObj );
+    pPlace = Ivy_TableFind( p, pObj );
     assert( *pPlace == pObj->Id ); // node should be in the table
     *pPlace = 0;
     // rehash the adjacent entries
-    p = Ivy_ObjMan(pObj);
     i = pPlace - p->pTable;
     for ( i = (i+1) % p->nTableSize; p->pTable[i]; i = (i+1) % p->nTableSize )
     {
-        pEntry = Ivy_ObjObj( pObj, p->pTable[i] );
+        pEntry = Ivy_ManObj( p, p->pTable[i] );
         p->pTable[i] = 0;
-        Ivy_TableInsert( pEntry );
+        Ivy_TableInsert( p, pEntry );
     }
 }
 
@@ -157,13 +159,13 @@ void Ivy_TableDelete( Ivy_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_TableUpdate( Ivy_Obj_t * pObj, int ObjIdNew )
+void Ivy_TableUpdate( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ObjIdNew )
 {
     int * pPlace;
     assert( !Ivy_IsComplement(pObj) );
     if ( !Ivy_ObjIsHash(pObj) )
         return;
-    pPlace = Ivy_TableFind( pObj );
+    pPlace = Ivy_TableFind( p, pObj );
     assert( *pPlace == pObj->Id ); // node should be in the table
     *pPlace = ObjIdNew;
 }
@@ -202,13 +204,12 @@ void Ivy_TableResize( Ivy_Man_t * p )
 {
     int * pTableOld, * pPlace;
     int nTableSizeOld, Counter, e, clk;
-    assert( 0 );
 clk = clock();
     // save the old table
     pTableOld = p->pTable;
     nTableSizeOld = p->nTableSize;
     // get the new table
-    p->nTableSize = p->nObjsAlloc*5/2+13; 
+    p->nTableSize = Cudd_PrimeAig( 5 * Ivy_ManHashObjNum(p) ); 
     p->pTable = ALLOC( int, p->nTableSize );
     memset( p->pTable, 0, sizeof(int) * p->nTableSize );
     // rehash the entries from the old table
@@ -219,17 +220,79 @@ clk = clock();
             continue;
         Counter++;
         // get the place where this entry goes in the table table
-        pPlace = Ivy_TableFind( Ivy_ManObj(p, pTableOld[e]) );
+        pPlace = Ivy_TableFind( p, Ivy_ManObj(p, pTableOld[e]) );
         assert( *pPlace == 0 ); // should not be in the table
         *pPlace = pTableOld[e];
     }
     assert( Counter == Ivy_ManHashObjNum(p) );
-//    printf( "Increasing the structural table size from %6d to %6d. ", p->nTableSize, nTableSizeNew );
+//    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
 //    PRT( "Time", clock() - clk );
     // replace the table and the parameters
-    free( p->pTable );
+    free( pTableOld );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Profiles the hash table.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Ivy_TableProfile( Ivy_Man_t * p )
+{
+    int i, Counter = 0;
+    for ( i = 0; i < p->nTableSize; i++ )
+    {
+        if ( p->pTable[i] )
+            Counter++;
+        else if ( Counter )
+        {
+            printf( "%d ", Counter );
+            Counter = 0;
+        }
+    }
 }
 
+/**Function********************************************************************
+
+  Synopsis    [Returns the next prime &gt;= p.]
+
+  Description [Copied from CUDD, for stand-aloneness.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+unsigned int Cudd_PrimeAig( unsigned int  p)
+{
+    int i,pn;
+
+    p--;
+    do {
+        p++;
+        if (p&1) {
+        pn = 1;
+        i = 3;
+        while ((unsigned) (i * i) <= p) {
+        if (p % i == 0) {
+            pn = 0;
+            break;
+        }
+        i += 2;
+        }
+    } else {
+        pn = 0;
+    }
+    } while (!pn);
+    return(p);
+
+} /* end of Cudd_Prime */
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/temp/ivy/ivyUndo.c

-/**CFile****************************************************************
-
-  FileName    [ivyUndo.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [And-Inverter Graph package.]
-
-  Synopsis    [Recording the results of recent deletion of logic cone.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - May 11, 2006.]
-
-  Revision    [$Id: ivyUndo.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "ivy.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManUndoStart( Ivy_Man_t * p )
-{
-    p->fRecording = 1;
-    p->nUndos = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManUndoStop( Ivy_Man_t * p )
-{
-    p->fRecording = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManUndoRecord( Ivy_Man_t * p, Ivy_Obj_t * pObj )
-{
-    Ivy_Obj_t * pObjUndo;
-    if ( p->nUndos >= p->nUndosAlloc )
-    {
-        printf( "Ivy_ManUndoRecord(): Not enough memory for undo.\n" );
-        return;
-    }
-    pObjUndo = p->pUndos + p->nUndos++;
-    // required data for Ivy_ObjCreateGhost()
-    pObjUndo->Type    = pObj->Type;
-    pObjUndo->Init    = pObj->Init;
-    pObjUndo->Fanin0  = pObj->Fanin0;
-    pObjUndo->Fanin1  = pObj->Fanin1;
-    pObjUndo->fComp0  = pObj->fComp0;
-    pObjUndo->fComp1  = pObj->fComp1;
-    // additional data
-    pObjUndo->Id      = pObj->Id;
-    pObjUndo->nRefs   = pObj->nRefs;
-    pObjUndo->Level   = pObj->Level;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Vec_IntPutLast( Vec_Int_t * vFree, int Last )
-{
-    int Place, i;
-    // find the entry
-    Place = Vec_IntFind( vFree, Last );
-    if ( Place == -1 )
-        return 0;
-    // shift entries by one
-    assert( vFree->pArray[Place] == Last );
-    for ( i = Place; i < Vec_IntSize(vFree) - 1; i++ )
-        vFree->pArray[i] = vFree->pArray[i+1];
-    // put the entry in the end
-    vFree->pArray[i] = Last;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ivy_ManUndoPerform( Ivy_Man_t * p, Ivy_Obj_t * pRoot )
-{
-    Ivy_Obj_t * pObjUndo, * pObjNew;
-    int i;
-    assert( p->nUndos > 0 );
-    assert( p->fRecording == 0 );
-    for ( i = p->nUndos - 1; i >= 0; i-- )
-    {
-        // get the undo object
-        pObjUndo = p->pUndos + i;
-        // if this is the last object
-        if ( i == 0 )
-            Vec_IntPush( p->vFree, pRoot->Id );
-        else
-            Vec_IntPutLast( p->vFree, pObjUndo->Id );
-        // create the new object
-        pObjNew  = Ivy_ObjCreate( Ivy_ObjCreateGhost2( p, pObjUndo) );
-        pObjNew->nRefs = pObjUndo->nRefs;
-        pObjNew->Level = pObjUndo->Level;
-        // make sure the object is created in the same place as before
-        assert( pObjNew->Id == pObjUndo->Id );
-    }
-    p->nUndos = 0;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-

src/temp/ivy/module.make

@@ -4,7 +4,9 @@ SRC +=    src/temp/ivy/ivyBalance.c \
     src/temp/ivy/ivyCut.c \
     src/temp/ivy/ivyDfs.c \
     src/temp/ivy/ivyDsd.c \
+    src/temp/ivy/ivyFanout.c \
     src/temp/ivy/ivyMan.c \
+    src/temp/ivy/ivyMem.c \
     src/temp/ivy/ivyMulti.c \
     src/temp/ivy/ivyObj.c \
     src/temp/ivy/ivyOper.c \
@@ -12,5 +14,4 @@ SRC +=    src/temp/ivy/ivyBalance.c \
     src/temp/ivy/ivyRwrPre.c \
     src/temp/ivy/ivySeq.c \
     src/temp/ivy/ivyTable.c \
-    src/temp/ivy/ivyUndo.c \
     src/temp/ivy/ivyUtil.c

src/temp/player/module.make

-SRC +=    src/temp/player/playerAbc.c \
-    src/temp/player/playerBuild.c \
+SRC +=    src/temp/player/playerToAbc.c \
     src/temp/player/playerCore.c \
     src/temp/player/playerMan.c \
     src/temp/player/playerUtil.c

src/temp/player/player.h

@@ -78,27 +78,17 @@ struct Pla_Man_t_
 
 #define PLA_EMPTY           ((Esop_Cube_t *)1)
 
-static inline Pla_Man_t *   Ivy_ObjPlaMan( Ivy_Obj_t * pObj )   { return (Pla_Man_t *)Ivy_ObjMan(pObj)->pData;       }
-static inline Pla_Obj_t *   Ivy_ObjPlaStr( Ivy_Obj_t * pObj )   { return Ivy_ObjPlaMan(pObj)->pPlaStrs + pObj->Id;   }
-
-static inline unsigned *    Ivy_ObjGetTruth( Ivy_Obj_t * pObj )  
-{ 
-    Ivy_Man_t * p = Ivy_ObjMan(pObj);
-    int Offset = Vec_IntEntry( p->vTruths, pObj->Id );
-    return Offset < 0 ? NULL : p->pMemory + Offset;
-    
-}
+static inline Pla_Man_t *   Ivy_ObjPlaMan( Ivy_Man_t * p, Ivy_Obj_t * pObj )  { return (Pla_Man_t *)p->pData;                        }
+static inline Pla_Obj_t *   Ivy_ObjPlaStr( Ivy_Man_t * p, Ivy_Obj_t * pObj )  { return ((Pla_Man_t *)p->pData)->pPlaStrs + pObj->Id; }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== playerAbc.c ==============================================================*/
+/*=== playerToAbc.c ==============================================================*/
 extern void *        Abc_NtkPlayer( void * pNtk, int nLutMax, int nFaninMax, int fVerbose );
-/*=== playerBuild.c ============================================================*/
-extern Ivy_Man_t *   Pla_ManToAig( Ivy_Man_t * p );
 /*=== playerCore.c =============================================================*/
-extern Ivy_Man_t *   Pla_ManDecompose( Ivy_Man_t * p, int nLutMax, int nPlaMax, int fVerbose );
+extern Pla_Man_t *   Pla_ManDecompose( Ivy_Man_t * p, int nLutMax, int nPlaMax, int fVerbose );
 /*=== playerMan.c ==============================================================*/
 extern Pla_Man_t *   Pla_ManAlloc( Ivy_Man_t * p, int nLutMax, int nPlaMax );
 extern void          Pla_ManFree( Pla_Man_t * p );

src/temp/player/playerAbc.c

@@ -32,6 +32,8 @@ static Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtkOld, Ivy_Man_t * p );
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#if 0
+
 /**Function*************************************************************
 
   Synopsis    [Gives the current ABC network to PLAyer for processing.]
@@ -65,7 +67,7 @@ void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int fVerbose )
     if ( fUseRewriting )
     {
         // simplify
-        pMan = Ivy_ManResyn( pManExt = pMan, 1 );
+        pMan = Ivy_ManResyn( pManExt = pMan, 1, 0 );
         Ivy_ManStop( pManExt );
         if ( fVerbose )
             Ivy_ManPrintStats( pMan );
@@ -217,6 +219,7 @@ Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
     return pNtkNew;
 }
 
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/temp/player/playerBuild.c

@@ -33,6 +33,8 @@ static int         Pla_ManToAigLutFuncs( Ivy_Man_t * pNew, Ivy_Man_t * pOld );
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#if 0
+
 /**Function*************************************************************
 
   Synopsis    [Constructs the AIG manager (IVY) for the network after mapping.]
@@ -93,7 +95,7 @@ Ivy_Obj_t * Pla_ManToAig_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld )
         return Ivy_ManObj( pNew, pObjOld->TravId );
     assert( Ivy_ObjIsAnd(pObjOld) || Ivy_ObjIsExor(pObjOld) );
     // get the support and the cover
-    pStr = Ivy_ObjPlaStr( pObjOld );
+    pStr = Ivy_ObjPlaStr( pNew, pObjOld );
     if ( Vec_IntSize( &pStr->vSupp[0] ) <= p->nLutMax )
     {
         vSupp = &pStr->vSupp[0]; 
@@ -246,10 +248,10 @@ int Pla_ManToAigLutFuncs( Ivy_Man_t * pNew, Ivy_Man_t * pOld )
         if ( !Ivy_ObjIsLut(pObjNew) )
             continue;
         pObjOld = Ivy_ManObj( pOld, pObjNew->TravId );
-        vSupp = Ivy_ObjPlaStr(pObjOld)->vSupp; 
+        vSupp = Ivy_ObjPlaStr(pNew, pObjOld)->vSupp; 
         assert( Vec_IntSize(vSupp) <= 8 );
         pTruth = Ivy_ObjGetTruth( pObjNew );
-        pComputed = Ivy_ManCutTruth( pObjOld, vSupp, vNodes, vTemp );
+        pComputed = Ivy_ManCutTruth( pNew, pObjOld, vSupp, vNodes, vTemp );
         // check if the truth table is constant 0
         for ( k = 0; k < 8; k++ )
             if ( pComputed[k] )
@@ -272,6 +274,8 @@ int Pla_ManToAigLutFuncs( Ivy_Man_t * pNew, Ivy_Man_t * pOld )
     return Counter;
 }
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/temp/player/playerCore.c

@@ -44,10 +44,9 @@ static void Pla_NodeGetSuppsAndCovers( Pla_Man_t * p, Ivy_Obj_t * pObj, int Leve
   SeeAlso     []
 
 ***********************************************************************/
-Ivy_Man_t * Pla_ManDecompose( Ivy_Man_t * pAig, int nLutMax, int nPlaMax, int fVerbose )
+Pla_Man_t * Pla_ManDecompose( Ivy_Man_t * pAig, int nLutMax, int nPlaMax, int fVerbose )
 {
     Pla_Man_t * p;
-    Ivy_Man_t * pAigNew;
     p = Pla_ManAlloc( pAig, nLutMax, nPlaMax );
     if ( !Pla_ManDecomposeInt( p ) )
     {
@@ -55,12 +54,7 @@ Ivy_Man_t * Pla_ManDecompose( Ivy_Man_t * pAig, int nLutMax, int nPlaMax, int fV
         Pla_ManFree( p );
         return NULL;
     }
-    pAigNew = Pla_ManToAig( pAig );
-//    if ( fVerbose )
-//    printf( "PLA stats: Both = %6d. Pla = %6d. Lut = %6d. Total = %6d. Deref = %6d.\n", 
-//        p->nNodesBoth, p->nNodesPla, p->nNodesLut, p->nNodes, p->nNodesDeref );
-    Pla_ManFree( p );
-    return pAigNew;
+    return p;
 }
 
 /**Function*************************************************************
@@ -84,7 +78,7 @@ int Pla_ManDecomposeInt( Pla_Man_t * p )
     // prepare the PI structures
     Ivy_ManForEachPi( pAig, pObj, i )
     {
-        pStr = Ivy_ObjPlaStr( pObj );
+        pStr = Ivy_ObjPlaStr( pAig, pObj );
         pStr->fFixed = 1;
         pStr->Depth  = 0;
         pStr->nRefs  = (unsigned)pObj->nRefs;
@@ -142,9 +136,9 @@ int Pla_ManDecomposeNode( Pla_Man_t * p, Ivy_Obj_t * pObj )
     p->nNodes++;
 
     // get the structures
-    pStr   = Ivy_ObjPlaStr( pObj );    
-    pStr0  = Ivy_ObjPlaStr( Ivy_ObjFanin0( pObj ) );
-    pStr1  = Ivy_ObjPlaStr( Ivy_ObjFanin1( pObj ) );
+    pStr   = Ivy_ObjPlaStr( p->pManAig, pObj );    
+    pStr0  = Ivy_ObjPlaStr( p->pManAig, Ivy_ObjFanin0( pObj ) );
+    pStr1  = Ivy_ObjPlaStr( p->pManAig, Ivy_ObjFanin1( pObj ) );
     vSupp0 = &pStr->vSupp[0];
     vSupp1 = &pStr->vSupp[1];
     pStr->pCover[0] = PLA_EMPTY;
@@ -263,9 +257,9 @@ void Pla_NodeGetSuppsAndCovers( Pla_Man_t * p, Ivy_Obj_t * pObj, int Level,
     pFan0 = Ivy_ObjFanin0( pObj );
     pFan1 = Ivy_ObjFanin1( pObj );
     // get the structures
-    pStr  = Ivy_ObjPlaStr( pObj );    
-    pStr0 = Ivy_ObjPlaStr( pFan0 );
-    pStr1 = Ivy_ObjPlaStr( pFan1 );
+    pStr  = Ivy_ObjPlaStr( p->pManAig, pObj );    
+    pStr0 = Ivy_ObjPlaStr( p->pManAig, pFan0 );
+    pStr1 = Ivy_ObjPlaStr( p->pManAig, pFan1 );
     // make sure the fanins are processed
     assert( Ivy_ObjIsPi(pFan0) || pStr0->Depth > 0 );
     assert( Ivy_ObjIsPi(pFan1) || pStr1->Depth > 0 );

src/temp/player/playerMan.c

@@ -58,8 +58,8 @@ Pla_Man_t * Pla_ManAlloc( Ivy_Man_t * pAig, int nLutMax, int nPlaMax )
     pMan->vTriv0  = Vec_IntAlloc( 1 );  Vec_IntPush( pMan->vTriv0, -1 ); 
     pMan->vTriv1  = Vec_IntAlloc( 1 );  Vec_IntPush( pMan->vTriv1, -1 ); 
     // allocate memory for object structures
-    pMan->pPlaStrs = ALLOC( Pla_Obj_t, sizeof(Pla_Obj_t) * Ivy_ManObjIdNext(pAig) );
-    memset( pMan->pPlaStrs, 0, sizeof(Pla_Obj_t) * Ivy_ManObjIdNext(pAig) );
+    pMan->pPlaStrs = ALLOC( Pla_Obj_t, sizeof(Pla_Obj_t) * (Ivy_ManObjIdMax(pAig)+1) );
+    memset( pMan->pPlaStrs, 0, sizeof(Pla_Obj_t) * (Ivy_ManObjIdMax(pAig)+1) );
     // create the cube manager
     pMan->pManMin = Esop_ManAlloc( nPlaMax );
     // save the resulting manager
@@ -90,7 +90,7 @@ void Pla_ManFree( Pla_Man_t * p )
     Vec_IntFree( p->vComTo1 );
     Vec_IntFree( p->vPairs0 );
     Vec_IntFree( p->vPairs1 );
-    for ( i = 0, pStr = p->pPlaStrs; i < Ivy_ManObjIdNext(p->pManAig); i++, pStr++ )
+    for ( i = 0, pStr = p->pPlaStrs; i <= Ivy_ManObjIdMax(p->pManAig); i++, pStr++ )
         FREE( pStr->vSupp[0].pArray ), FREE( pStr->vSupp[1].pArray );
     free( p->pPlaStrs );
     free( p );

src/temp/player/playerUtil.c

@@ -281,6 +281,8 @@ Esop_Cube_t * Pla_ManExorTwoCovers( Pla_Man_t * p, Esop_Cube_t * pCover0, Esop_C
     return pCover;
 }
 
+#if 0
+
 /**Function*************************************************************
 
   Synopsis    [Computes area/delay of the mapping.]
@@ -342,6 +344,8 @@ void Pla_ManComputeStats( Ivy_Man_t * p, Vec_Int_t * vNodes )
     printf( "Area = %d. Delay = %d.\n", Area, Delay );
 }
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/temp/rwt/rwtMan.c

@@ -64,10 +64,10 @@ void Rwt_ManGlobalStart()
 ***********************************************************************/
 void Rwt_ManGlobalStop()
 { 
-    if ( s_puCanons == NULL )  free( s_puCanons );
-    if ( s_pPhases == NULL )   free( s_pPhases );
-    if ( s_pPerms == NULL )    free( s_pPerms );
-    if ( s_pMap == NULL )      free( s_pMap );
+    FREE( s_puCanons );
+    FREE( s_pPhases );
+    FREE( s_pPerms );
+    FREE( s_pMap );
 } 
 
 /**Function*************************************************************

src/temp/vec/vecInt.h

@@ -289,6 +289,23 @@ static inline int Vec_IntEntry( Vec_Int_t * p, int i )
   SeeAlso     []
 
 ***********************************************************************/
+static inline int * Vec_IntEntryP( Vec_Int_t * p, int i )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray + i;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 static inline void Vec_IntWriteEntry( Vec_Int_t * p, int i, int Entry )
 {
     assert( i >= 0 && i < p->nSize );
@@ -385,7 +402,10 @@ static inline void Vec_IntFillExtra( Vec_Int_t * p, int nSize, int Entry )
     int i;
     if ( p->nSize >= nSize )
         return;
-    Vec_IntGrow( p, nSize );
+    if ( p->nSize < 2 * nSize )
+        Vec_IntGrow( p, 2 * nSize );
+    else
+        Vec_IntGrow( p, p->nSize );
     for ( i = p->nSize; i < nSize; i++ )
         p->pArray[i] = Entry;
     p->nSize = nSize;