Version abc61102

Makefile

@@ -6,18 +6,18 @@ CP   := cp
 
 PROG := abc
 
-MODULES := src/base/abc src/base/abci src/base/seq src/base/cmd src/base/io src/base/main \
+MODULES := src/base/abc src/base/abci src/base/cmd src/base/io src/base/main \
 	src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo \
 	src/map/fpga src/map/pga src/map/mapper src/map/mio src/map/super \
 	src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/espresso src/misc/nm src/misc/vec src/misc/hash \
-	src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim \
+	src/opt/cut src/opt/dec src/opt/fxu src/opt/rwr src/opt/sim src/opt/ret \
 	src/sat/asat src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig \
 	src/temp/ivy src/temp/aig src/temp/rwt src/temp/deco src/temp/mem src/temp/ver
 
 default: $(PROG)
 
-OPTFLAGS  := -DNDEBUG -O3
-#OPTFLAGS  := -g -O
+#OPTFLAGS  := -DNDEBUG -O3
+OPTFLAGS  := -g -O
 
 CFLAGS   += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES)) 
 CXXFLAGS += $(CFLAGS) 

abc.dsp

@@ -186,6 +186,10 @@ SOURCE=.\src\base\abci\abcBalance.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcBmc.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcClpBdd.c
 # End Source File
 # Begin Source File
@@ -332,73 +336,9 @@ SOURCE=.\src\base\abci\abcUnreach.c
 
 SOURCE=.\src\base\abci\abcVerify.c
 # End Source File
-# End Group
-# Begin Group "seq"
-
-# PROP Default_Filter ""
-# Begin Source File
-
-SOURCE=.\src\base\seq\seq.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\seq\seqAigCore.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\seq\seqAigIter.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\seq\seqCreate.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\seq\seqFpgaCore.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\seq\seqFpgaIter.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\seq\seqInt.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\seq\seqLatch.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\seq\seqMan.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\seq\seqMapCore.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\seq\seqMapIter.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\seq\seqMaxMeanCycle.c
-# End Source File
 # Begin Source File
 
-SOURCE=.\src\base\seq\seqRetCore.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\seq\seqRetIter.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\seq\seqShare.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\seq\seqUtil.c
+SOURCE=.\src\base\abci\abcXsim.c
 # End Source File
 # End Group
 # Begin Group "cmd"
@@ -1389,6 +1329,42 @@ SOURCE=.\src\opt\sim\simSymStr.c
 SOURCE=.\src\opt\sim\simUtils.c
 # End Source File
 # End Group
+# Begin Group "ret"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retArea.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retBwd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retDelay.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retFlow.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retFwd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retInit.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\ret\retInt.h
+# End Source File
+# End Group
 # End Group
 # Begin Group "map"
 
@@ -2300,14 +2276,6 @@ SOURCE=.\src\temp\aig\aigTable.c
 
 SOURCE=.\src\temp\aig\aigUtil.c
 # End Source File
-# Begin Source File
-
-SOURCE=.\src\temp\aig\cudd2.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\temp\aig\cudd2.h
-# End Source File
 # End Group
 # End Group
 # End Group

abc.rc

 # global parameters
-#set check         # checks intermediate networks
+set check         # checks intermediate networks
 #set checkfio      # prints warnings when fanins/fanouts are duplicated
-#set checkread     # checks new networks after reading from file
+set checkread     # checks new networks after reading from file
 set backup        # saves backup networks retrived by "undo" and "recall"
 set savesteps 1   # sets the maximum number of backup networks to save 
 set progressbar   # display the progress bar
@@ -61,6 +61,7 @@ alias rez restructure -z
 alias rs resub
 alias rsz resub -z
 alias sa set autoexec ps
+alias scl scleanup
 alias so source -x
 alias st strash
 alias sw sweep
@@ -100,7 +101,7 @@ alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l;
 # temporaries
 #alias test        "rvl th/lib.v; rvv th/t2.v"
 #alias test         "so c/pure_sat/test.c"
-alias test         "r c/14/csat_998.bench; st; ps"
+#alias test         "r c/14/csat_998.bench; st; ps"
 
 
 

src/base/abc/abc.h

@@ -529,6 +529,8 @@ extern void               Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj );
 extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
 extern Vec_Ptr_t *        Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *        Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *        Abc_NtkDfsSeq( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *        Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkSupport( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
@@ -570,7 +572,8 @@ extern int                Abc_NtkLogicToAig( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch );
 extern int                Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk );
-/*=== abcLib.c ==========================================================*/
+extern Vec_Int_t *        Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk );
+ /*=== abcLib.c ==========================================================*/
 extern Abc_Lib_t *        Abc_LibCreate( char * pName );
 extern void               Abc_LibFree( Abc_Lib_t * pLib );
 extern Abc_Ntk_t *        Abc_LibDeriveRoot( Abc_Lib_t * pLib );
@@ -595,7 +598,7 @@ extern Abc_Obj_t *        Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
 extern void               Abc_ObjRecycle( Abc_Obj_t * pObj );
 extern Abc_Obj_t *        Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
 extern void               Abc_NtkDeleteObj( Abc_Obj_t * pObj );
-extern void               Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj );
+extern void               Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes );
 extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName );
 extern Abc_Obj_t *        Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, int fCopyName );
 extern Abc_Obj_t *        Abc_NtkCloneObj( Abc_Obj_t * pNode );
@@ -604,14 +607,14 @@ extern Abc_Obj_t *        Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t *        Abc_NodeCreateConst0( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NodeCreateConst1( Abc_Ntk_t * pNtk );
-extern Abc_Obj_t *        Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
-extern Abc_Obj_t *        Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
-extern Abc_Obj_t *        Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
-extern Abc_Obj_t *        Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
-extern Abc_Obj_t *        Abc_NodeCreateExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
-extern Abc_Obj_t *        Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
+extern Abc_Obj_t *        Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk );
+extern Abc_Obj_t *        Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk );
+extern Abc_Obj_t *        Abc_NtkCreateNodeInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
+extern Abc_Obj_t *        Abc_NtkCreateNodeBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
+extern Abc_Obj_t *        Abc_NtkCreateNodeAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
+extern Abc_Obj_t *        Abc_NtkCreateNodeOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
+extern Abc_Obj_t *        Abc_NtkCreateNodeExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
+extern Abc_Obj_t *        Abc_NtkCreateNodeMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
 extern bool               Abc_NodeIsConst( Abc_Obj_t * pNode );
 extern bool               Abc_NodeIsConst0( Abc_Obj_t * pNode );    
 extern bool               Abc_NodeIsConst1( Abc_Obj_t * pNode );    
@@ -673,9 +676,11 @@ extern void               Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, in
 extern void               Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames );
 extern void               Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes );
 extern void               Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode );
-extern void               Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll);
+extern void               Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll );
+extern void               Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj );
 /*=== abcProve.c ==========================================================*/
 extern int                Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pParams );
+extern int                Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
 /*=== abcReconv.c ==========================================================*/
 extern Abc_ManCut_t *     Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
 extern void               Abc_NtkManCutStop( Abc_ManCut_t * p );
@@ -751,7 +756,7 @@ extern Abc_Ntk_t *        Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels );
 /*=== abcSweep.c ==========================================================*/
 extern int                Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose );
 extern int                Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
-extern int                Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes );
+extern int                Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fVerbose );
 /*=== abcTiming.c ==========================================================*/
 extern Abc_Time_t *       Abc_NodeReadArrival( Abc_Obj_t * pNode );
 extern Abc_Time_t *       Abc_NodeReadRequired( Abc_Obj_t * pNode );
@@ -809,6 +814,7 @@ extern Vec_Int_t *        Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkCollectObjects( Abc_Ntk_t * pNtk );
 extern Vec_Int_t *        Abc_NtkGetCiIds( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkReassignIds( Abc_Ntk_t * pNtk );
+extern int                Abc_ObjPointerCompare( void ** pp1, void ** pp2 );
 /*=== abcVerify.c ==========================================================*/
 extern int *              Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames );
 extern int *              Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel );

src/base/abc/abcCheck.c

@@ -167,13 +167,8 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
     }
 
     // check the nodes
-    if ( Abc_NtkHasAig(pNtk) )
-    {
-        if ( Abc_NtkIsStrash(pNtk) ) 
-            Abc_AigCheck( pNtk->pManFunc );
-        else
-            Abc_NtkSeqCheck( pNtk );
-    }
+    if ( Abc_NtkIsStrash(pNtk) )
+        Abc_AigCheck( pNtk->pManFunc );
     else
     {
         Abc_NtkForEachNode( pNtk, pNode, i )
@@ -240,9 +235,10 @@ bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk )
     Vec_Int_t * vNameIds;
     char * pName;
     int i, NameId;
-
+/*
     if ( Abc_NtkIsNetlist(pNtk) )
     {
+
         // check that each net has a name
         Abc_NtkForEachNet( pNtk, pObj, i )
         {
@@ -254,6 +250,7 @@ bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk )
         }
     }
     else
+*/
     {
         // check that each CI/CO has a name
         Abc_NtkForEachCi( pNtk, pObj, i )

src/base/abc/abcDfs.c

@@ -209,6 +209,118 @@ void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 
 /**Function*************************************************************
 
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDfsSeq_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    // visit the transitive fanin of the node
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Abc_NtkDfsSeq_rec( pFanin, vNodes );
+    // add the node after the fanins have been added
+    Vec_PtrPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of nodes and latches reachable from POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkDfsSeq( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
+    int i;
+    assert( !Abc_NtkIsNetlist(pNtk) );
+    // set the traversal ID
+    Abc_NtkIncrementTravId( pNtk );
+    // start the array of nodes
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkDfsSeq_rec( pObj, vNodes );
+    // mark the PIs
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDfsSeq_rec( pObj, vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDfsSeqReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    // visit the transitive fanin of the node
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+        Abc_NtkDfsSeqReverse_rec( pFanout, vNodes );
+    // add the node after the fanins have been added
+    Vec_PtrPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of nodes and latches reachable from POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkDfsSeqReverse( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
+    int i;
+    assert( !Abc_NtkIsNetlist(pNtk) );
+    // set the traversal ID
+    Abc_NtkIncrementTravId( pNtk );
+    // start the array of nodes
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDfsSeqReverse_rec( pObj, vNodes );
+    // mark the logic feeding into POs
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Abc_NtkDfsSeq_rec( pObj, vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if the ordering of nodes is DFS.]
 
   Description []
@@ -611,9 +723,9 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
     Abc_Obj_t * pFanin;
     int fAcyclic, i;
     assert( !Abc_ObjIsNet(pNode) );
-    if ( Abc_ObjIsCi(pNode) || Abc_ObjIsBox(pNode) )
+    if ( Abc_ObjIsCi(pNode) || Abc_ObjIsBox(pNode) || (Abc_NtkIsStrash(pNode->pNtk) && Abc_AigNodeIsConst(pNode)) )
         return 1;
-    assert( Abc_ObjIsNode( pNode ) || Abc_ObjIsBox( pNode ) );
+    assert( Abc_ObjIsNode(pNode) );
     // make sure the node is not visited
     assert( !Abc_NodeIsTravIdPrevious(pNode) );
     // check if the node is part of the combinational loop

src/base/abc/abcFanio.c

@@ -223,8 +223,8 @@ void Abc_ObjTransferFanout( Abc_Obj_t * pNodeFrom, Abc_Obj_t * pNodeTo )
     int nFanoutsOld, i;
     assert( !Abc_ObjIsComplement(pNodeFrom) );
     assert( !Abc_ObjIsComplement(pNodeTo) );
-    assert( Abc_ObjIsNode(pNodeFrom) );
-    assert( Abc_ObjIsNode(pNodeTo) );
+    assert( Abc_ObjIsNode(pNodeFrom) || Abc_ObjIsCi(pNodeFrom) );
+    assert( !Abc_ObjIsPo(pNodeTo) );
     assert( pNodeFrom->pNtk == pNodeTo->pNtk );
     assert( pNodeFrom != pNodeTo );
     assert( Abc_ObjFanoutNum(pNodeFrom) > 0 );
@@ -255,12 +255,9 @@ void Abc_ObjReplace( Abc_Obj_t * pNodeOld, Abc_Obj_t * pNodeNew )
 {
     assert( !Abc_ObjIsComplement(pNodeOld) );
     assert( !Abc_ObjIsComplement(pNodeNew) );
-    assert( Abc_ObjIsNode(pNodeOld) );
-    assert( Abc_ObjIsNode(pNodeNew) );
     assert( pNodeOld->pNtk == pNodeNew->pNtk );
     assert( pNodeOld != pNodeNew );
     assert( Abc_ObjFanoutNum(pNodeOld) > 0 );
-    assert( Abc_ObjFanoutNum(pNodeNew) == 0 );
     // transfer the fanouts to the old node
     Abc_ObjTransferFanout( pNodeOld, pNodeNew );
     // remove the old node

src/base/abc/abcLatch.c

@@ -48,7 +48,7 @@ bool Abc_NtkLatchIsSelfFeed_rec( Abc_Obj_t * pLatch, Abc_Obj_t * pLatchRoot )
     pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch));
     if ( !Abc_ObjIsBi(pFanin) || !Abc_ObjIsLatch(Abc_ObjFanin0(pFanin)) )
         return 0;
-    return Abc_NtkLatchIsSelfFeed_rec( Abc_ObjFanin0(pFanin), pLatch );
+    return Abc_NtkLatchIsSelfFeed_rec( Abc_ObjFanin0(pFanin), pLatchRoot );
 }
 
 /**Function*************************************************************
@@ -120,7 +120,7 @@ int Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk )
             if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) )
                 pConst1 = Abc_AigConst1(pNtk);
             else
-                pConst1 = Abc_NodeCreateConst1(pNtk);
+                pConst1 = Abc_NtkCreateNodeConst1(pNtk);
             Abc_ObjPatchFanin( pLatch, Abc_ObjFanin0(Abc_ObjFanin0(pLatch)), pConst1 );
             Counter++;
         }
@@ -170,6 +170,28 @@ void Abc_NtkLatchPipe( Abc_Ntk_t * pNtk, int nLatches )
     Abc_NtkLogicMakeSimpleCos( pNtk, 0 );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk )
+{
+    Vec_Int_t * vArray;
+    Abc_Obj_t * pLatch;
+    int i;
+    vArray = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        Vec_IntPush( vArray, Abc_LatchIsInit1(pLatch) );
+    return vArray;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/abc/abcNetlist.c

@@ -253,9 +253,12 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect )
     }
     else if ( Abc_NtkIsSeq(pNtk) )
     {
+        assert( 0 );
+/*
         pNtkTemp = Abc_NtkSeqToLogicSop(pNtk);
         pNtkNew = Abc_NtkLogicSopToNetlist( pNtkTemp );
         Abc_NtkDelete( pNtkTemp );
+*/
     }
     else if ( Abc_NtkIsBddLogic(pNtk) )
     {
@@ -416,7 +419,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
     // if the constant node is used, duplicate it
     pObj = Abc_AigConst1(pNtk);
     if ( Abc_ObjFanoutNum(pObj) > 0 )
-        pObj->pCopy = Abc_NodeCreateConst1(pNtkNew);
+        pObj->pCopy = Abc_NtkCreateNodeConst1(pNtkNew);
     // duplicate the nodes and create node functions
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
@@ -505,19 +508,19 @@ Abc_Ntk_t * Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk )
     pObj = Abc_AigConst1(pNtk);
     if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) )
     {
-        pObj->pCopy = Abc_NodeCreateConst1(pNtkNew);
-        pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
+        pObj->pCopy = Abc_NtkCreateNodeConst1(pNtkNew);
+        pObj->pCopy->pCopy = Abc_NtkCreateNodeInv( pNtkNew, pObj->pCopy );
     }
     Abc_NtkForEachCi( pNtk, pObj, i )
         if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) )
-            pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
+            pObj->pCopy->pCopy = Abc_NtkCreateNodeInv( pNtkNew, pObj->pCopy );
     // duplicate the nodes, create node functions, and inverters
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         Abc_NtkDupObj( pNtkNew, pObj, 0 );
         pObj->pCopy->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, 2, NULL );
         if ( Abc_AigNodeHasComplFanoutEdgeTrav(pObj) )
-            pObj->pCopy->pCopy = Abc_NodeCreateInv( pNtkNew, pObj->pCopy );
+            pObj->pCopy->pCopy = Abc_NtkCreateNodeInv( pNtkNew, pObj->pCopy );
     }
     // connect the objects
     Vec_PtrForEachEntry( vNodes, pObj, i )

src/base/abc/abcNtk.c

@@ -69,8 +69,8 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan
     // start the functionality manager
     if ( Abc_NtkIsStrash(pNtk) )
         pNtk->pManFunc = Abc_AigAlloc( pNtk );
-    else if ( Abc_NtkIsSeq(pNtk) )
-        pNtk->pManFunc = Seq_Create( pNtk );
+//    else if ( Abc_NtkIsSeq(pNtk) )
+//        pNtk->pManFunc = Seq_Create( pNtk );
     else if ( Abc_NtkHasSop(pNtk) )
         pNtk->pManFunc = Extra_MmFlexStart();
     else if ( Abc_NtkHasBdd(pNtk) )
@@ -301,6 +301,7 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
             printf( "Warning: Structural hashing during duplication reduced %d nodes (this is a minor bug).\n",
                 Abc_NtkNodeNum(pNtk) - Abc_NtkNodeNum(pNtkNew) );
     }
+/*
     else if ( Abc_NtkIsSeq(pNtk) )
     {
         // start the storage for initial states
@@ -333,6 +334,7 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
         Abc_SeqForEachCutsetNode( pNtk, pObj, i )
             Vec_PtrPush( pNtkNew->vCutSet, pObj->pCopy );
     }
+*/
     else
     {
         // duplicate the nets and nodes (CIs/COs/latches already dupped)
@@ -355,6 +357,65 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Attaches the second network at the bottom of the first.]
+
+  Description [Returns the first network. Deletes the second network.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkAttachBottom( Abc_Ntk_t * pNtkTop, Abc_Ntk_t * pNtkBottom )
+{
+    Abc_Obj_t * pObj, * pFanin, * pBuffer;
+    Vec_Ptr_t * vNodes;
+    int i, k;
+    assert( pNtkBottom != NULL );
+    if ( pNtkTop == NULL )
+        return pNtkBottom;
+    // make sure the networks are combinational
+    assert( Abc_NtkPiNum(pNtkTop) == Abc_NtkCiNum(pNtkTop) );
+    assert( Abc_NtkPiNum(pNtkBottom) == Abc_NtkCiNum(pNtkBottom) );
+    // make sure the POs of the bottom correspond to the PIs of the top
+    assert( Abc_NtkPoNum(pNtkBottom) == Abc_NtkPiNum(pNtkTop) );
+    assert( Abc_NtkPiNum(pNtkBottom) <  Abc_NtkPiNum(pNtkTop) );
+    // add buffers for the PIs of the top - save results in the POs of the bottom
+    Abc_NtkForEachPi( pNtkTop, pObj, i )
+    {
+        pBuffer = Abc_NtkCreateNodeBuf( pNtkTop, NULL );
+        Abc_ObjTransferFanout( pObj, pBuffer );
+        Abc_NtkPo(pNtkBottom, i)->pCopy = pBuffer;
+    }
+    // remove useless PIs of the top
+    for ( i = Abc_NtkPiNum(pNtkTop) - 1; i >= Abc_NtkPiNum(pNtkBottom); i-- )
+        Abc_NtkDeleteObj( Abc_NtkPi(pNtkTop, i) );
+    assert( Abc_NtkPiNum(pNtkBottom) == Abc_NtkPiNum(pNtkTop) );
+    // copy the bottom network
+    Abc_NtkForEachPi( pNtkBottom, pObj, i )
+        Abc_NtkPi(pNtkBottom, i)->pCopy = Abc_NtkPi(pNtkTop, i);
+    // construct all nodes
+    vNodes = Abc_NtkDfs( pNtkBottom, 0 );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        Abc_NtkDupObj(pNtkTop, pObj, 0);
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+    }
+    Vec_PtrFree( vNodes );
+    // connect the POs
+    Abc_NtkForEachPo( pNtkBottom, pObj, i )
+        Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
+    // delete old network
+    Abc_NtkDelete( pNtkBottom );
+    // return the network
+    if ( !Abc_NtkCheck( pNtkTop ) )
+        fprintf( stdout, "Abc_NtkAttachBottom(): Network check has failed.\n" );
+    return pNtkTop;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates the network composed of one logic cone.]
 
   Description []
@@ -720,8 +781,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     // start the functionality manager
     if ( Abc_NtkIsStrash(pNtk) )
         Abc_AigFree( pNtk->pManFunc );
-    else if ( Abc_NtkIsSeq(pNtk) )
-        Seq_Delete( pNtk->pManFunc );
+//    else if ( Abc_NtkIsSeq(pNtk) )
+//        Seq_Delete( pNtk->pManFunc );
     else if ( Abc_NtkHasSop(pNtk) )
         Extra_MmFlexStop( pNtk->pManFunc, 0 );
     else if ( Abc_NtkHasBdd(pNtk) )
@@ -777,7 +838,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk )
         if ( Abc_ObjFaninNum(pNet) > 0 )
             continue;
         // add the constant 0 driver
-        pNode = Abc_NodeCreateConst0( pNtk );
+        pNode = Abc_NtkCreateNodeConst0( pNtk );
         // add the fanout net
         Abc_ObjAddFanin( pNet, pNode );
         // add the net to those for which the warning will be printed

src/base/abc/abcObj.c

@@ -129,10 +129,10 @@ Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
             Vec_PtrPush( pNtk->vCos, pObj );
             break;
         case ABC_OBJ_BI:     
-            Vec_PtrPush( pNtk->vCis, pObj );
+            if ( pNtk->vCis ) Vec_PtrPush( pNtk->vCis, pObj );
             break;
         case ABC_OBJ_BO:     
-            Vec_PtrPush( pNtk->vCos, pObj );
+            if ( pNtk->vCos ) Vec_PtrPush( pNtk->vCos, pObj );
             break;
         case ABC_OBJ_ASSERT:     
             Vec_PtrPush( pNtk->vAsserts, pObj );
@@ -146,7 +146,7 @@ Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
             pObj->pData = (void *)ABC_INIT_NONE;
         case ABC_OBJ_TRI:     
         case ABC_OBJ_BLACKBOX:     
-            Vec_PtrPush( pNtk->vBoxes, pObj );
+            if ( pNtk->vBoxes ) Vec_PtrPush( pNtk->vBoxes, pObj );
             break;
         default:
             assert(0); 
@@ -171,6 +171,9 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
     Abc_Ntk_t * pNtk = pObj->pNtk;
     Vec_Ptr_t * vNodes;
     int i;
+    // remove from the table of names
+    if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) )
+        Nm_ManDeleteIdName(pObj->pNtk->pManName, pObj->Id);
     // delete fanins and fanouts
     assert( !Abc_ObjIsComplement(pObj) );
     vNodes = Vec_PtrAlloc( 100 );
@@ -186,9 +189,6 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
     pObj->Id = (1<<26)-1;
     pNtk->nObjCounts[pObj->Type]--;
     pNtk->nObjs--;
-    // remove from the table of names
-    if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) )
-        Nm_ManDeleteIdName(pObj->pNtk->pManName, pObj->Id);
     // perform specialized operations depending on the object type
     switch (pObj->Type)
     {
@@ -210,10 +210,10 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
             Vec_PtrRemove( pNtk->vCos, pObj );
             break;
         case ABC_OBJ_BI:     
-            Vec_PtrRemove( pNtk->vCis, pObj );
+            if ( pNtk->vCis ) Vec_PtrRemove( pNtk->vCis, pObj );
             break;
         case ABC_OBJ_BO:     
-            Vec_PtrRemove( pNtk->vCos, pObj );
+            if ( pNtk->vCos ) Vec_PtrRemove( pNtk->vCos, pObj );
             break;
         case ABC_OBJ_ASSERT:     
             Vec_PtrRemove( pNtk->vAsserts, pObj );
@@ -230,7 +230,7 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
         case ABC_OBJ_LATCH:     
         case ABC_OBJ_TRI:     
         case ABC_OBJ_BLACKBOX:     
-            Vec_PtrRemove( pNtk->vBoxes, pObj );
+            if ( pNtk->vBoxes ) Vec_PtrRemove( pNtk->vBoxes, pObj );
             break;
         default:
             assert(0); 
@@ -251,20 +251,30 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj )
+void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes )
 {
     Abc_Ntk_t * pNtk = pObj->pNtk;
     Vec_Ptr_t * vNodes;
     int i;
     assert( !Abc_ObjIsComplement(pObj) );
+    assert( !Abc_ObjIsPi(pObj) );
     assert( Abc_ObjFanoutNum(pObj) == 0 );
     // delete fanins and fanouts
     vNodes = Vec_PtrAlloc( 100 );
     Abc_NodeCollectFanins( pObj, vNodes );
     Abc_NtkDeleteObj( pObj );
-    Vec_PtrForEachEntry( vNodes, pObj, i )
-        if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) == 0 )
-            Abc_NtkDeleteObj_rec( pObj );
+    if ( fOnlyNodes )
+    {
+        Vec_PtrForEachEntry( vNodes, pObj, i )
+            if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) == 0 )
+                Abc_NtkDeleteObj_rec( pObj, fOnlyNodes );
+    }
+    else
+    {
+        Vec_PtrForEachEntry( vNodes, pObj, i )
+            if ( !Abc_ObjIsPi(pObj) && Abc_ObjFanoutNum(pObj) == 0 )
+                Abc_NtkDeleteObj_rec( pObj, fOnlyNodes );
+    }
     Vec_PtrFree( vNodes );
 }
 
@@ -530,7 +540,7 @@ Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
+Abc_Obj_t * Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
@@ -559,7 +569,7 @@ Abc_Obj_t * Abc_NodeCreateConst0( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk )
+Abc_Obj_t * Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
@@ -588,12 +598,12 @@ Abc_Obj_t * Abc_NodeCreateConst1( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
+Abc_Obj_t * Abc_NtkCreateNodeInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
 {
     Abc_Obj_t * pNode;
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
     pNode = Abc_NtkCreateNode( pNtk );   
-    Abc_ObjAddFanin( pNode, pFanin );
+    if ( pFanin ) Abc_ObjAddFanin( pNode, pFanin );
     if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, "0 1\n" );
     else if ( Abc_NtkHasBdd(pNtk) )
@@ -618,12 +628,12 @@ Abc_Obj_t * Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
+Abc_Obj_t * Abc_NtkCreateNodeBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
 {
     Abc_Obj_t * pNode;
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsNetlist(pNtk) );
-    pNode = Abc_NtkCreateNode( pNtk );   
-    Abc_ObjAddFanin( pNode, pFanin );
+    pNode = Abc_NtkCreateNode( pNtk ); 
+    if ( pFanin ) Abc_ObjAddFanin( pNode, pFanin );
     if ( Abc_NtkHasSop(pNtk) )
         pNode->pData = Abc_SopRegister( pNtk->pManFunc, "1 1\n" );
     else if ( Abc_NtkHasBdd(pNtk) )
@@ -648,7 +658,7 @@ Abc_Obj_t * Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
+Abc_Obj_t * Abc_NtkCreateNodeAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
 {
     Abc_Obj_t * pNode;
     int i;
@@ -678,7 +688,7 @@ Abc_Obj_t * Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
+Abc_Obj_t * Abc_NtkCreateNodeOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
 {
     Abc_Obj_t * pNode;
     int i;
@@ -708,7 +718,7 @@ Abc_Obj_t * Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
+Abc_Obj_t * Abc_NtkCreateNodeExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
 {
     Abc_Obj_t * pNode;
     int i;
@@ -738,7 +748,7 @@ Abc_Obj_t * Abc_NodeCreateExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Obj_t * Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 )
+Abc_Obj_t * Abc_NtkCreateNodeMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 )
 {
     Abc_Obj_t * pNode;
     assert( Abc_NtkIsLogic(pNtk) );
@@ -772,8 +782,7 @@ Abc_Obj_t * Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t *
 bool Abc_NodeIsConst( Abc_Obj_t * pNode )    
 { 
     assert( Abc_NtkIsLogic(pNode->pNtk) || Abc_NtkIsNetlist(pNode->pNtk) );
-    assert( Abc_ObjIsNode(pNode) );      
-    return Abc_ObjFaninNum(pNode) == 0;
+    return Abc_ObjIsNode(pNode) && Abc_ObjFaninNum(pNode) == 0;
 }
 
 /**Function*************************************************************

src/base/abc/abcRefs.c

@@ -316,12 +316,18 @@ void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSu
 void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode )
 {
     Vec_Ptr_t * vCone, * vSupp;
+    Abc_Obj_t * pObj;
+    int i;
     vCone = Vec_PtrAlloc( 100 );
     vSupp = Vec_PtrAlloc( 100 );
     Abc_NodeDeref_rec( pNode );
     Abc_NodeMffsConeSupp( pNode, vCone, vSupp );
     Abc_NodeRef_rec( pNode );
-    printf( "Cone = %6d. Supp = %6d. \n", Vec_PtrSize(vCone), Vec_PtrSize(vSupp) );
+    printf( "Node = %6s : Supp = %3d  Cone = %3d  (", 
+        Abc_ObjName(pNode), Vec_PtrSize(vSupp), Vec_PtrSize(vCone) );
+    Vec_PtrForEachEntry( vCone, pObj, i )
+        printf( " %s", Abc_ObjName(pObj) );
+    printf( " )\n" );
     Vec_PtrFree( vCone );
     Vec_PtrFree( vSupp );
 }

src/base/abc/abcShow.c

@@ -88,7 +88,7 @@ void Abc_NodeShowBdd( Abc_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
+void Abc_NtkShowAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodesShow )
 {
     FILE * pFile;
     Abc_Obj_t * pNode;
@@ -96,7 +96,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
     char FileNameDot[200];
     int i;
 
-    assert( Abc_NtkHasAig(pNtk) );
+    assert( Abc_NtkIsStrash(pNtk) );
     // create the file name
     Abc_ShowGetFileName( pNtk->pName, FileNameDot );
     // check that the file can be opened
@@ -112,7 +112,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
     Abc_NtkForEachObj( pNtk, pNode, i )
         Vec_PtrPush( vNodes, pNode );
     // write the DOT file
-    Io_WriteDotAig( pNtk, vNodes, NULL, FileNameDot, 0 );
+    Io_WriteDotAig( pNtk, vNodes, vNodesShow, FileNameDot, 0 );
     Vec_PtrFree( vNodes );
 
     // visualize the file 

src/base/abc/abcUtil.c

@@ -81,6 +81,17 @@ void Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk )
         Vec_PtrPush( pNtk->vCos, pObj );
     Abc_NtkForEachBox( pNtk, pObj, i )
     {
+        if ( Abc_ObjIsLatch(pObj) )
+            continue;
+        Abc_ObjForEachFanin( pObj, pTerm, k )
+            Vec_PtrPush( pNtk->vCos, pTerm );
+        Abc_ObjForEachFanout( pObj, pTerm, k )
+            Vec_PtrPush( pNtk->vCis, pTerm );
+    }
+    Abc_NtkForEachBox( pNtk, pObj, i )
+    {
+        if ( !Abc_ObjIsLatch(pObj) )
+            continue;
         Abc_ObjForEachFanin( pObj, pTerm, k )
             Vec_PtrPush( pNtk->vCos, pTerm );
         Abc_ObjForEachFanout( pObj, pTerm, k )
@@ -545,11 +556,11 @@ void Abc_NtkFixCoDriverProblem( Abc_Obj_t * pDriver, Abc_Obj_t * pNodeCo, int fD
         // add inverters and buffers when necessary
         if ( Abc_ObjFaninC0(pNodeCo) )
         {
-            pDriverNew = Abc_NodeCreateInv( pNtk, pDriver );
+            pDriverNew = Abc_NtkCreateNodeInv( pNtk, pDriver );
             Abc_ObjXorFaninC( pNodeCo, 0 );
         }
         else
-            pDriverNew = Abc_NodeCreateBuf( pNtk, pDriver );        
+            pDriverNew = Abc_NtkCreateNodeBuf( pNtk, pDriver );        
     }
     // update the fanin of the PO node
     Abc_ObjPatchFanin( pNodeCo, pDriver, pDriverNew );
@@ -925,13 +936,14 @@ int Abc_NtkPrepareTwoNtks( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc
         }
         else
             fclose( pFile );
-
+/*
         if ( Abc_NtkIsSeq(pNtk) )
         {
             pNtk1 = Abc_NtkSeqToLogicSop(pNtk);
             *pfDelete1 = 1;
         }
         else
+*/
             pNtk1 = pNtk;
         pNtk2 = Io_Read( pNtk->pSpec, fCheck );
         if ( pNtk2 == NULL )
@@ -945,12 +957,14 @@ int Abc_NtkPrepareTwoNtks( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc
             fprintf( pErr, "Empty current network.\n" );
             return 0;
         }
+/*
         if ( Abc_NtkIsSeq(pNtk) )
         {
             pNtk1 = Abc_NtkSeqToLogicSop(pNtk);
             *pfDelete1 = 1;
         }
         else
+*/
             pNtk1 = pNtk;
         pNtk2 = Io_Read( argv[util_optind], fCheck );
         if ( pNtk2 == NULL )
@@ -1265,6 +1279,26 @@ void Abc_NtkDetectMatching( Abc_Ntk_t * pNtk )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Compares the pointers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjPointerCompare( void ** pp1, void ** pp2 )
+{
+    if ( *pp1 < *pp2 )
+        return -1;
+    if ( *pp1 > *pp2 ) 
+        return 1;
+    return 0; 
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abcBmc.c

+/**CFile****************************************************************
+
+  FileName    [abcBmc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Performs bounded model check.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc );
+
+static void Abc_NtkBmcReport( Ivy_Man_t * pMan, Ivy_Man_t * pFrames, Ivy_Man_t * pFraig, Vec_Ptr_t * vMapping, int nFrames );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBmc( Abc_Ntk_t * pNtk, int nFrames, int fInit, int fVerbose )
+{
+    Ivy_FraigParams_t Params, * pParams = &Params; 
+    Ivy_Man_t * pMan, * pFrames, * pFraig;
+    Vec_Ptr_t * vMapping;
+    // convert to IVY manager
+    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
+    // generate timeframes
+    pFrames = Ivy_ManFrames( pMan, Abc_NtkLatchNum(pNtk), nFrames, fInit, &vMapping );
+    // fraig the timeframes
+    Ivy_FraigParamsDefault( pParams );
+    pParams->nBTLimitNode = ABC_INFINITY;
+    pParams->fVerbose = 0;
+    pParams->fProve = 0;
+    pFraig = Ivy_FraigPerform( pFrames, pParams );
+printf( "Frames have %6d nodes.  ", Ivy_ManNodeNum(pFrames) );
+printf( "Fraig has %6d nodes.\n", Ivy_ManNodeNum(pFraig) );
+    // report the classes
+//    if ( fVerbose )
+//        Abc_NtkBmcReport( pMan, pFrames, pFraig, vMapping, nFrames );
+    // free stuff
+    Vec_PtrFree( vMapping );
+    Ivy_ManStop( pFraig );
+    Ivy_ManStop( pFrames );
+    Ivy_ManStop( pMan );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBmcReport( Ivy_Man_t * pMan, Ivy_Man_t * pFrames, Ivy_Man_t * pFraig, Vec_Ptr_t * vMapping, int nFrames )
+{
+    Ivy_Obj_t * pFirst1, * pFirst2, * pFirst3;
+    int i, f, nIdMax, Prev2, Prev3;
+    nIdMax = Ivy_ManObjIdMax(pMan);
+    // check what is the number of nodes in each frame
+    Prev2 = Prev3 = 0;
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Ivy_ManForEachNode( pMan, pFirst1, i )
+        {
+            pFirst2 = Ivy_Regular( Vec_PtrEntry(vMapping, f * nIdMax + pFirst1->Id) );
+            if ( Ivy_ObjIsConst1(pFirst2) || pFirst2->Type == 0 )
+                continue;
+            pFirst3 = Ivy_Regular( pFirst2->pEquiv );
+            if ( Ivy_ObjIsConst1(pFirst3) || pFirst3->Type == 0 )
+                continue;
+            break;
+        }
+        if ( f )
+            printf( "Frame %3d :  Strash = %5d  Fraig = %5d\n", f, pFirst2->Id - Prev2, pFirst3->Id - Prev3 );
+        Prev2 = pFirst2->Id;
+        Prev3 = pFirst3->Id;   
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abci/abcDsd.c

@@ -172,7 +172,7 @@ void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t *
     int i, nNodesDsd;
 
     // save the CI nodes in the DSD nodes
-    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NodeCreateConst1(pNtkNew) );
+    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), (int)Abc_NtkCreateNodeConst1(pNtkNew) );
     Abc_NtkForEachCi( pNtk, pNode, i )
     {
         pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );

src/base/abci/abcFpga.c

@@ -210,7 +210,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
         Fpga_NodeSetData0( Fpga_ManReadInputs(pMan)[i], (char *)pNode->pCopy );
     // set the constant node
 //    if ( Fpga_NodeReadRefs(Fpga_ManReadConst1(pMan)) > 0 )
-        Fpga_NodeSetData0( Fpga_ManReadConst1(pMan), (char *)Abc_NodeCreateConst1(pNtkNew) );
+        Fpga_NodeSetData0( Fpga_ManReadConst1(pMan), (char *)Abc_NtkCreateNodeConst1(pNtkNew) );
     // process the nodes in topological order
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
     Abc_NtkForEachCo( pNtk, pNode, i )

src/base/abci/abcFpgaFast.c

@@ -99,7 +99,7 @@ Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan )
     // start the new ABC network
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
     // transfer the pointers to the basic nodes
-    Abc_ObjSetIvy2Abc( pMan, Ivy_ManConst1(pMan)->Id, Abc_NodeCreateConst1(pNtkNew) );
+    Abc_ObjSetIvy2Abc( pMan, Ivy_ManConst1(pMan)->Id, Abc_NtkCreateNodeConst1(pNtkNew) );
     Abc_NtkForEachCi( pNtkNew, pObjAbc, i )
         Abc_ObjSetIvy2Abc( pMan, Ivy_ManPi(pMan, i)->Id, pObjAbc ); 
     // recursively construct the network
@@ -112,7 +112,7 @@ Abc_Ntk_t * Ivy_ManFpgaToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan )
         if ( Ivy_ObjFaninC0(pObjIvy) ) // complement
         {
             if ( Abc_ObjIsCi(pObjAbc) )
-                pObjAbc = Abc_NodeCreateInv( pNtkNew, pObjAbc );
+                pObjAbc = Abc_NtkCreateNodeInv( pNtkNew, pObjAbc );
             else
             {
                 // clone the node

src/base/abci/abcIvy.c

@@ -51,7 +51,7 @@ static inline Abc_Obj_t *  Abc_EdgeToNode( Abc_Ntk_t * p, Abc_Edge_t Edge )    {
 static inline Abc_Obj_t *  Abc_ObjFanin0Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin0(pObj)->TravId), Ivy_ObjFaninC0(pObj) ); }
 static inline Abc_Obj_t *  Abc_ObjFanin1Ivy( Abc_Ntk_t * p, Ivy_Obj_t * pObj ) { return Abc_ObjNotCond( Abc_EdgeToNode(p, Ivy_ObjFanin1(pObj)->TravId), Ivy_ObjFaninC1(pObj) ); }
 
-static int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk, int fUseDcs );
+static Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -85,7 +85,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
     if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) )
     {
         printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) );
-        return NULL;
+//        return NULL;
     }
     // print warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
@@ -102,9 +102,9 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
     if ( fSeq )
     {
         int nLatches = Abc_NtkLatchNum(pNtk);
-        int * pInit = Abc_NtkCollectLatchValues( pNtk, fUseDc );
-        Ivy_ManMakeSeq( pMan, nLatches, pInit );
-        FREE( pInit );
+        Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, fUseDc );
+        Ivy_ManMakeSeq( pMan, nLatches, vInit->pArray );
+        Vec_IntFree( vInit );
 //        Ivy_ManPrintStats( pMan );
     }
     return pMan;
@@ -191,8 +191,8 @@ Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int
         return NULL;
 
     Ivy_ManHaigStart( pMan, fVerbose );
-    Ivy_ManRewriteSeq( pMan, 0, 0 );
-    for ( i = 1; i < nIters; i++ )
+//    Ivy_ManRewriteSeq( pMan, 0, 0 );
+    for ( i = 0; i < nIters; i++ )
         Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
     Ivy_ManHaigPostprocess( pMan, fVerbose );
 
@@ -486,7 +486,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
     int fCleanup = 1;
 //    int nNodes;
     int nLatches = Abc_NtkLatchNum(pNtk);
-    int * pInit = Abc_NtkCollectLatchValues( pNtk, 0 );
+    Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, 0 );
 
     assert( !Abc_NtkIsNetlist(pNtk) );
     assert( !Abc_NtkIsSeq(pNtk) );
@@ -494,7 +494,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
     {
         if ( !Abc_NtkBddToSop(pNtk, 0) )
         {
-            FREE( pInit );
+            Vec_IntFree( vInit );
             printf( "Abc_NtkIvy(): Converting to SOPs has failed.\n" );
             return NULL;
         }
@@ -513,7 +513,7 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
     pMan = Abc_NtkToAig( pNtk );
     if ( !Ivy_ManCheck( pMan ) )
     {
-        FREE( pInit );
+        Vec_IntFree( vInit );
         printf( "AIG check has failed.\n" );
         Ivy_ManStop( pMan );
         return NULL;
@@ -975,22 +975,23 @@ Ivy_Obj_t * Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pRoot, cha
   SeeAlso     []
 
 ***********************************************************************/
-int * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk, int fUseDcs )
+Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs )
 {
     Abc_Obj_t * pLatch;
-    int * pArray, i;
-    pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) );
+    Vec_Int_t * vArray;
+    int i;
+    vArray = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
         if ( fUseDcs || Abc_LatchIsInitDc(pLatch) )
-            pArray[i] = IVY_INIT_DC;
+            Vec_IntPush( vArray, IVY_INIT_DC );
         else if ( Abc_LatchIsInit1(pLatch) )
-            pArray[i] = IVY_INIT_1;
+            Vec_IntPush( vArray, IVY_INIT_1 );
         else if ( Abc_LatchIsInit0(pLatch) )
-            pArray[i] = IVY_INIT_0;
+            Vec_IntPush( vArray, IVY_INIT_0 );
         else assert( 0 );
     }
-    return pArray;
+    return vArray;
 }
 
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abcLut.c

@@ -148,7 +148,7 @@ int Abc_NtkSuperChoiceLut( Abc_Ntk_t * pNtk, int nLutSize, int nCutSizeMax, int
         // if there is no delay improvement, skip; otherwise, update level
         if ( pObjTop->Level >= pObj->Level )
         {
-            Abc_NtkDeleteObj_rec( pObjTop );
+            Abc_NtkDeleteObj_rec( pObjTop, 1 );
             continue;
         }
         pObj->Level = pObjTop->Level;
@@ -570,7 +570,7 @@ Abc_Obj_t * Abc_NodeSuperChoiceLut( Abc_ManScl_t * p, Abc_Obj_t * pObj )
         {
             Vec_PtrForEachEntry( p->vLeaves, pFanin, i )
                 if ( Abc_ObjIsNode(pFanin) && Abc_ObjFanoutNum(pFanin) == 0 )
-                    Abc_NtkDeleteObj_rec( pFanin );
+                    Abc_NtkDeleteObj_rec( pFanin, 1 );
             return NULL;
         }
     // create the topmost node

src/base/abci/abcMap.c

@@ -259,7 +259,7 @@ Abc_Obj_t * Abc_NodeFromMap_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int
 
     // check the case of constant node
     if ( Map_NodeIsConst(pNodeMap) )
-        return fPhase? Abc_NodeCreateConst1(pNtkNew) : Abc_NodeCreateConst0(pNtkNew);
+        return fPhase? Abc_NtkCreateNodeConst1(pNtkNew) : Abc_NtkCreateNodeConst0(pNtkNew);
 
     // check if the phase is already implemented
     pNodeNew = (Abc_Obj_t *)Map_NodeReadData( pNodeMap, fPhase );
@@ -369,7 +369,7 @@ Abc_Obj_t * Abc_NodeFromMapSuper_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap
              * (since the cut only has 4 variables). An interesting question is what
              * if the first variable (and not the fifth one is the redundant one;
              * can that happen?) */
-            return Abc_NodeCreateConst0(pNtkNew);
+            return Abc_NtkCreateNodeConst0(pNtkNew);
         }
     }
 
@@ -503,14 +503,14 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
     // set the pointers from the mapper to the new nodes
     Abc_NtkForEachCi( pNtk, pNode, i )
     {
-        Map_NodeSetData( Map_ManReadInputs(pMan)[i], 0, (char *)Abc_NodeCreateInv(pNtkNew,pNode->pCopy) );
+        Map_NodeSetData( Map_ManReadInputs(pMan)[i], 0, (char *)Abc_NtkCreateNodeInv(pNtkNew,pNode->pCopy) );
         Map_NodeSetData( Map_ManReadInputs(pMan)[i], 1, (char *)pNode->pCopy );
     }
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
 //        if ( Abc_NodeIsConst(pNode) )
 //            continue;
-        Map_NodeSetData( (Map_Node_t *)pNode->pNext, 0, (char *)Abc_NodeCreateInv(pNtkNew,pNode->pCopy) );
+        Map_NodeSetData( (Map_Node_t *)pNode->pNext, 0, (char *)Abc_NtkCreateNodeInv(pNtkNew,pNode->pCopy) );
         Map_NodeSetData( (Map_Node_t *)pNode->pNext, 1, (char *)pNode->pCopy );
     }
 
@@ -630,7 +630,7 @@ Abc_Obj_t * Abc_NodeFromMapSuperChoice_rec( Abc_Ntk_t * pNtkNew, Map_Super_t * p
              * (since the cut only has 4 variables). An interesting question is what
              * if the first variable (and not the fifth one is the redundant one;
              * can that happen?) */
-            return Abc_NodeCreateConst0(pNtkNew);
+            return Abc_NtkCreateNodeConst0(pNtkNew);
         }
     }
 

src/base/abci/abcNtbdd.c

@@ -195,7 +195,7 @@ Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew )
     pNodeNew = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(bFunc), pNtkNew, tBdd2Node );
     st_free_table( tBdd2Node );
     if ( Cudd_IsComplement(bFunc) )
-        pNodeNew = Abc_NodeCreateInv( pNtkNew, pNodeNew );
+        pNodeNew = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew );
     return pNodeNew;
 }
 
@@ -215,18 +215,18 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
     Abc_Obj_t * pNodeNew, * pNodeNew0, * pNodeNew1, * pNodeNewC;
     assert( !Cudd_IsComplement(bFunc) );
     if ( bFunc == b1 )
-        return Abc_NodeCreateConst1(pNtkNew);
+        return Abc_NtkCreateNodeConst1(pNtkNew);
     if ( st_lookup( tBdd2Node, (char *)bFunc, (char **)&pNodeNew ) )
         return pNodeNew;
     // solve for the children nodes
     pNodeNew0 = Abc_NodeBddToMuxes_rec( dd, Cudd_Regular(cuddE(bFunc)), pNtkNew, tBdd2Node );
     if ( Cudd_IsComplement(cuddE(bFunc)) )
-        pNodeNew0 = Abc_NodeCreateInv( pNtkNew, pNodeNew0 );
+        pNodeNew0 = Abc_NtkCreateNodeInv( pNtkNew, pNodeNew0 );
     pNodeNew1 = Abc_NodeBddToMuxes_rec( dd, cuddT(bFunc), pNtkNew, tBdd2Node );
     if ( !st_lookup( tBdd2Node, (char *)Cudd_bddIthVar(dd, bFunc->index), (char **)&pNodeNewC ) )
         assert( 0 );
     // create the MUX node
-    pNodeNew = Abc_NodeCreateMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 );
+    pNodeNew = Abc_NtkCreateNodeMux( pNtkNew, pNodeNewC, pNodeNew1, pNodeNew0 );
     st_insert( tBdd2Node, (char *)bFunc, (char *)pNodeNew );
     return pNodeNew;
 }

src/base/abci/abcPrint.c

@@ -61,10 +61,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     else
         fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
 
-    if ( !Abc_NtkIsSeq(pNtk) )
+//    if ( !Abc_NtkIsSeq(pNtk) )
         fprintf( pFile, "  lat = %4d", Abc_NtkLatchNum(pNtk) );
-    else
-        fprintf( pFile, "  lat = %4d(%d,%d)", Seq_NtkLatchNum(pNtk), Seq_NtkLatchNumShared(pNtk), Seq_NtkLatchNumMax(pNtk) );
+//    else
+//        fprintf( pFile, "  lat = %4d(%d,%d)", Seq_NtkLatchNum(pNtk), Seq_NtkLatchNumShared(pNtk), Seq_NtkLatchNumMax(pNtk) );
 
     if ( Abc_NtkIsNetlist(pNtk) )
     {
@@ -228,6 +228,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
     int InitNums[4], Init;
 
     assert( !Abc_NtkIsNetlist(pNtk) );
+/*
     if ( Abc_NtkIsSeq(pNtk) )
     {
         Seq_NtkLatchGetInitNums( pNtk, InitNums );
@@ -236,7 +237,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
             Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] );
         return;
     }
-
+*/
     if ( Abc_NtkLatchNum(pNtk) == 0 )
     {
         fprintf( pFile, "The network is combinational.\n" );
@@ -383,6 +384,26 @@ void Abc_NodePrintFanio( FILE * pFile, Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
+  Synopsis    [Prints the MFFCs of the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkPrintMffc( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    extern void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Abc_NodeMffsConeSuppPrint( pNode );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prints the factored form of one node.]
 
   Description []
@@ -833,6 +854,84 @@ void Abc_NtkPrintSkews( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintAll ) {
   fprintf( pFile, "Endpoint Skews : Total |Skew| = %.2f\t Avg |Skew| = %.2f\t Non-Zero Skews = %d\n", 
            sum, avg, nNonZero );
 }
+
+/**Function*************************************************************
+
+  Synopsis    [Prints information about the object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    fprintf( pFile, "Object %5d : ", pObj->Id );
+    switch ( pObj->Type )
+    {
+        case ABC_OBJ_NONE: 
+            fprintf( pFile, "NONE   " );  
+            break;
+        case ABC_OBJ_CONST1: 
+            fprintf( pFile, "Const1 " );  
+            break;
+        case ABC_OBJ_PIO:    
+            fprintf( pFile, "PIO    " );  
+            break;
+        case ABC_OBJ_PI:     
+            fprintf( pFile, "PI     " );  
+            break;
+        case ABC_OBJ_PO:     
+            fprintf( pFile, "PO     " );  
+            break;
+        case ABC_OBJ_BI:     
+            fprintf( pFile, "BI     " );  
+            break;
+        case ABC_OBJ_BO:     
+            fprintf( pFile, "BO     " );  
+            break;
+        case ABC_OBJ_ASSERT:     
+            fprintf( pFile, "Assert " );  
+            break;
+        case ABC_OBJ_NET:  
+            fprintf( pFile, "Net    " );  
+            break;
+        case ABC_OBJ_NODE: 
+            fprintf( pFile, "Node   " );  
+            break;
+        case ABC_OBJ_GATE: 
+            fprintf( pFile, "Gate   " );  
+            break;
+        case ABC_OBJ_LATCH:     
+            fprintf( pFile, "Latch  " );  
+            break;
+        case ABC_OBJ_TRI:     
+            fprintf( pFile, "Tristate" );  
+            break;
+        case ABC_OBJ_BLACKBOX:     
+            fprintf( pFile, "Blackbox" );  
+            break;
+        default:
+            assert(0); 
+            break;
+    }
+    // print the fanins
+    fprintf( pFile, " Fanins ( " );
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        fprintf( pFile, "%d ", pFanin->Id );
+    fprintf( pFile, ") " );
+    // print the logic function
+    if ( Abc_ObjIsNode(pObj) && Abc_NtkIsSopLogic(pObj->pNtk) )
+        fprintf( pFile, " %s", pObj->pData );
+    else
+        fprintf( pFile, "\n" );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abcSweep.c

@@ -32,6 +32,7 @@ static void           Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t
 static void           Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose );
 static int            Abc_NodeDroppingCost( Abc_Obj_t * pNode );
 
+static int            Abc_NtkReduceNodes( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes );
 static void           Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose );
 static void           Abc_NodeConstantInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin, bool fConst0 );
 static void           Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin );
@@ -425,7 +426,7 @@ void Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv,
         return;
 
     // add the invertor
-    pNodeMinInv = Abc_NodeCreateInv( pNtk, pNodeMin );
+    pNodeMinInv = Abc_NtkCreateNodeInv( pNtk, pNodeMin );
    
     // move the fanouts of the inverted nodes
     for ( pNode = pListInv; pNode; pNode = pNode->pNext )
@@ -583,7 +584,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
         if ( Abc_ObjFanoutNum(pNode) > 0 )
             Vec_PtrPush( vNodes, pNode );
         else
-            Abc_NtkDeleteObj_rec( pNode );
+            Abc_NtkDeleteObj_rec( pNode, 1 );
     }
     Vec_PtrFree( vNodes );
     // sweep a node into its CO fanout if all of this is true:
@@ -672,6 +673,263 @@ void Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pFanin )
     Cudd_RecursiveDeref( dd, bCof1 );
 }
 
+
+
+/**Function*************************************************************
+
+  Synopsis    [Removes all objects whose trav ID is not current.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeRemoveNonCurrentObjects( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int Counter, i;
+    int fVerbose = 0;
+
+    // report on the nodes to be deleted
+    if ( fVerbose )
+    {
+        printf( "These nodes will be deleted: \n" );
+        Abc_NtkForEachObj( pNtk, pObj, i )
+            if ( !Abc_NodeIsTravIdCurrent( pObj ) )
+            {
+                printf( "    " );
+                Abc_ObjPrint( stdout, pObj );
+            }
+    }
+    
+    // delete the nodes    
+    Counter = 0;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( !Abc_NodeIsTravIdCurrent( pObj ) )
+        {
+            Abc_NtkDeleteObj( pObj );
+            Counter++;
+        }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the fanin of this latch is a constant.]
+
+  Description [Returns 0/1 if constant; -1 if not a constant.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSetTravId_rec( Abc_Obj_t * pObj )
+{
+    Abc_NodeSetTravIdCurrent(pObj);
+    if ( Abc_ObjFaninNum(pObj) == 0 )
+        return;
+    assert( Abc_ObjFaninNum(pObj) == 1 );
+    Abc_NtkSetTravId_rec( Abc_ObjFanin0(pObj) );    
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Check if the fanin of this latch is a constant.]
+
+  Description [Returns 0/1 if constant; -1 if not a constant.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCheckConstant_rec( Abc_Obj_t * pObj )
+{
+    if ( Abc_ObjFaninNum(pObj) == 0 )
+    {
+        if ( !Abc_ObjIsNode(pObj) )
+            return -1;
+        if ( Abc_NodeIsConst0(pObj) )
+            return 0;
+        if ( Abc_NodeIsConst1(pObj) )
+            return 1;
+        assert( 0 );
+        return -1;
+    }
+    if ( Abc_ObjIsLatch(pObj) || Abc_ObjFaninNum(pObj) > 1 )
+        return -1;
+    if ( !Abc_ObjIsNode(pObj) || Abc_NodeIsBuf(pObj) )
+        return Abc_NtkCheckConstant_rec( Abc_ObjFanin0(pObj) );
+    if ( Abc_NodeIsInv(pObj) )
+    {
+        int RetValue = Abc_NtkCheckConstant_rec( Abc_ObjFanin0(pObj) );
+        if ( RetValue == 0 )
+            return 1;
+        if ( RetValue == 1 )
+            return 0;
+        return RetValue;
+    }
+    assert( 0 );
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes redundant latches.]
+
+  Description [The redundant latches are of two types:
+  - Latches fed by a constant which matches the init value of the latch.
+  - Latches fed by a constant which does not match the init value of the latch
+  can be all replaced by one latch.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkLatchSweep( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pFanin, * pLatch, * pLatchPivot = NULL;
+    int Counter, RetValue, i;
+    Counter = 0;
+    // go through the latches
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        // check if the latch has constant input
+        RetValue = Abc_NtkCheckConstant_rec( Abc_ObjFanin0(pLatch) );
+        if ( RetValue == -1 )
+            continue;
+        // found a latch with constant fanin
+        if ( (RetValue == 1 && Abc_LatchIsInit0(pLatch)) ||
+             (RetValue == 0 && Abc_LatchIsInit1(pLatch)) )
+        {
+            // fanin constant differs from the latch init value
+            if ( pLatchPivot == NULL )
+            {
+                pLatchPivot = pLatch;
+                continue;
+            }
+            if ( Abc_LatchInit(pLatch) != Abc_LatchInit(pLatchPivot) ) // add inverter
+                pFanin = Abc_NtkCreateNodeInv( pNtk, Abc_ObjFanout0(pLatchPivot) );
+            else
+                pFanin = Abc_ObjFanout0(pLatchPivot);
+        }
+        else
+            pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch));
+        // replace latch
+        Abc_ObjTransferFanout( Abc_ObjFanout0(pLatch), pFanin );
+        // delete the extra nodes
+        Abc_NtkDeleteObj_rec( Abc_ObjFanout0(pLatch), 0 );
+        Counter++;
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces autonumnous logic by free inputs.]
+
+  Description [Assumes that non-autonomous logic is marked with
+  the current ID.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkReplaceAutonomousLogic( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode, * pFanin;
+    Vec_Ptr_t * vNodes;
+    int i, k, Counter;
+    // collect the nodes that feed into the reachable logic
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachObj( pNtk, pNode, i )
+    {
+        // skip non-visited fanins
+        if ( !Abc_NodeIsTravIdCurrent(pNode) )
+            continue;
+        // look for non-visited fanins
+        Abc_ObjForEachFanin( pNode, pFanin, k )
+        {
+            // skip visited fanins
+            if ( Abc_NodeIsTravIdCurrent(pFanin) )
+                continue;
+            // skip constants and latches fed by constants
+            if ( Abc_NtkCheckConstant_rec(pFanin) != -1 ||
+                 (Abc_ObjIsBi(pFanin) && Abc_NtkCheckConstant_rec(Abc_ObjFanin0(Abc_ObjFanin0(pFanin))) != -1) )
+            {
+                Abc_NtkSetTravId_rec( pFanin );
+                continue;
+            }
+            assert( !Abc_ObjIsLatch(pFanin) );
+            Vec_PtrPush( vNodes, pFanin );
+        }
+    }
+    Vec_PtrUniqify( vNodes, Abc_ObjPointerCompare );
+    // replace these nodes by the PIs
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        pFanin = Abc_NtkCreatePi(pNtk);
+        Abc_NodeSetTravIdCurrent( pFanin );
+        Abc_ObjTransferFanout( pNode, pFanin );
+    }
+    Counter = Vec_PtrSize(vNodes);
+    Vec_PtrFree( vNodes );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sequential cleanup.]
+
+  Description [Performs three tasks:
+  - Removes logic that does not feed into POs.
+  - Removes latches driven by constant values equal to the initial state.
+  - Replaces the autonomous components by additional PI variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCleanupSeq( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Vec_Ptr_t * vNodes;
+    int Counter;
+    assert( Abc_NtkIsLogic(pNtk) );
+    // mark the nodes reachable from the POs
+    vNodes = Abc_NtkDfsSeq( pNtk );
+    Vec_PtrFree( vNodes );
+    // remove the non-marked nodes
+    Counter = Abc_NodeRemoveNonCurrentObjects( pNtk );
+    if ( fVerbose )
+        printf( "Cleanup removed %4d dangling objects.\n", Counter );
+    // check if some of the latches can be removed
+    Counter = Abc_NtkLatchSweep( pNtk );
+    if ( fVerbose )
+        printf( "Cleanup removed %4d redundant latches.\n", Counter );
+    // detect the autonomous components
+    vNodes = Abc_NtkDfsSeqReverse( pNtk );
+    Vec_PtrFree( vNodes );
+    // replace them by PIs
+    Counter = Abc_NtkReplaceAutonomousLogic( pNtk );
+    if ( fVerbose )
+        printf( "Cleanup added   %4d additional PIs.\n", Counter );
+    // remove the non-marked nodes
+    Counter = Abc_NodeRemoveNonCurrentObjects( pNtk );
+    if ( fVerbose )
+        printf( "Cleanup removed %4d autonomous objects.\n", Counter );
+    // check
+    if ( !Abc_NtkCheck( pNtk ) )
+        printf( "Abc_NtkCleanupSeq: The network check has failed.\n" );
+    return 1;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abci/abcVerify.c

@@ -333,7 +333,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
         printf( "Networks are NOT EQUIVALENT after framing.\n" );
         // report the error
         pFrames->pModel = Abc_NtkVerifyGetCleanModel( pFrames, 1 );
-        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames );
+//        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames );
         FREE( pFrames->pModel );
         Abc_NtkDelete( pFrames );
         return;
@@ -365,7 +365,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
     else if ( RetValue == 0 )
     {
         printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
-        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, Fraig_ManReadModel(pMan), nFrames );
+//        Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, Fraig_ManReadModel(pMan), nFrames );
     }
     else assert( 0 );
     // delete the fraig manager

src/base/abci/abcXsim.c

+/**CFile****************************************************************
+
+  FileName    [abcXsim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Using X-valued simulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcXsim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define XVS0   1
+#define XVS1   2
+#define XVSX   3
+
+static inline void Abc_ObjSetXsim( Abc_Obj_t * pObj, int Value )  { pObj->pCopy = (void *)Value;  }
+static inline int  Abc_ObjGetXsim( Abc_Obj_t * pObj )             { return (int)pObj->pCopy;      }
+static inline int  Abc_XsimInv( int Value )   
+{ 
+    if ( Value == XVS0 )
+        return XVS1;
+    if ( Value == XVS1 )
+        return XVS0;
+    assert( Value == XVSX );       
+    return XVSX;
+}
+static inline int  Abc_XsimAnd( int Value0, int Value1 )   
+{ 
+    if ( Value0 == XVS0 || Value1 == XVS0 )
+        return XVS0;
+    if ( Value0 == XVSX || Value1 == XVSX )
+        return XVSX;
+    assert( Value0 == XVS1 && Value1 == XVS1 );
+    return XVS1;
+}
+static inline int  Abc_XsimRand2()   
+{
+    return (rand() & 1) ? XVS1 : XVS0;
+}
+static inline int  Abc_XsimRand3()   
+{
+    int RetValue;
+    do { 
+        RetValue = rand() & 3; 
+    } while ( RetValue == 0 );
+    return RetValue;
+}
+static inline int  Abc_ObjGetXsimFanin0( Abc_Obj_t * pObj )       
+{ 
+    int RetValue;
+    RetValue = Abc_ObjGetXsim(Abc_ObjFanin0(pObj));
+    return Abc_ObjFaninC0(pObj)? Abc_XsimInv(RetValue) : RetValue;
+}
+static inline int  Abc_ObjGetXsimFanin1( Abc_Obj_t * pObj )       
+{ 
+    int RetValue;
+    RetValue = Abc_ObjGetXsim(Abc_ObjFanin1(pObj));
+    return Abc_ObjFaninC1(pObj)? Abc_XsimInv(RetValue) : RetValue;
+}
+static inline void Abc_XsimPrint( FILE * pFile, int Value )   
+{ 
+    if ( Value == XVS0 )
+    {
+        fprintf( pFile, "0" );
+        return;
+    }
+    if ( Value == XVS1 )
+    {
+        fprintf( pFile, "1" );
+        return;
+    }
+    assert( Value == XVSX );       
+    fprintf( pFile, "x" );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs X-valued simulation of the sequential network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose )
+{
+    Abc_Obj_t * pObj;
+    int i, f;
+    assert( Abc_NtkIsStrash(pNtk) );
+    srand( 0x12341234 );
+    // start simulation
+    Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
+    if ( fInputs )
+    {
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            Abc_ObjSetXsim( pObj, XVSX );
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) );
+    }
+    else
+    {
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_ObjSetXsim( Abc_ObjFanout0(pObj), XVSX );
+    }
+    // simulate and print the result
+    fprintf( stdout, "Frame : Inputs : Latches : Outputs\n" );
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Abc_AigForEachAnd( pNtk, pObj, i )
+            Abc_ObjSetXsim( pObj, Abc_XsimAnd(Abc_ObjGetXsimFanin0(pObj), Abc_ObjGetXsimFanin1(pObj)) );
+        Abc_NtkForEachCo( pNtk, pObj, i )
+            Abc_ObjSetXsim( pObj, Abc_ObjGetXsimFanin0(pObj) );
+        // print out
+        fprintf( stdout, "%2d : ", f );
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
+        fprintf( stdout, " : " );
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_XsimPrint( stdout, Abc_ObjGetXsim(Abc_ObjFanout0(pObj)) );
+        fprintf( stdout, " : " );
+        Abc_NtkForEachPo( pNtk, pObj, i )
+            Abc_XsimPrint( stdout, Abc_ObjGetXsim(pObj) );
+        fprintf( stdout, "\n" );
+        // assign input values
+        if ( fInputs )
+            Abc_NtkForEachPi( pNtk, pObj, i )
+                Abc_ObjSetXsim( pObj, XVSX );
+        else
+            Abc_NtkForEachPi( pNtk, pObj, i )
+                Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
+        // transfer the latch values
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_ObjGetXsim(Abc_ObjFanin0(pObj)) );
+    }
+}
+
+///////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abci/module.make

@@ -2,6 +2,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcAttach.c \
     src/base/abci/abcAuto.c \
     src/base/abci/abcBalance.c \
+    src/base/abci/abcBmc.c \
     src/base/abci/abcClpBdd.c \
     src/base/abci/abcClpSop.c \
     src/base/abci/abcCut.c \
@@ -37,4 +38,5 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcTiming.c \
     src/base/abci/abcUnate.c \
     src/base/abci/abcUnreach.c \
-    src/base/abci/abcVerify.c 
+    src/base/abci/abcVerify.c \
+    src/base/abci/abcXsim.c 

src/base/io/ioUtil.c

@@ -179,7 +179,7 @@ Abc_Obj_t * Io_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut, char * pNamesI
 Abc_Obj_t * Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 )
 {
     Abc_Obj_t * pNet, * pTerm;
-    pTerm = fConst1? Abc_NodeCreateConst1(pNtk) : Abc_NodeCreateConst0(pNtk);
+    pTerm = fConst1? Abc_NtkCreateNodeConst1(pNtk) : Abc_NtkCreateNodeConst0(pNtk);
     pNet  = Abc_NtkFindNet(pNtk, pName);    assert( pNet );
     Abc_ObjAddFanin( pNet, pTerm );
     return pTerm;
@@ -200,7 +200,7 @@ Abc_Obj_t * Io_ReadCreateInv( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut
 {
     Abc_Obj_t * pNet, * pNode;
     pNet  = Abc_NtkFindNet(pNtk, pNameIn);     assert( pNet );
-    pNode = Abc_NodeCreateInv(pNtk, pNet);
+    pNode = Abc_NtkCreateNodeInv(pNtk, pNet);
     pNet  = Abc_NtkFindNet(pNtk, pNameOut);    assert( pNet );
     Abc_ObjAddFanin( pNet, pNode );
     return pNode;
@@ -221,7 +221,7 @@ Abc_Obj_t * Io_ReadCreateBuf( Abc_Ntk_t * pNtk, char * pNameIn, char * pNameOut
 {
     Abc_Obj_t * pNet, * pNode;
     pNet  = Abc_NtkFindNet(pNtk, pNameIn);     assert( pNet );
-    pNode = Abc_NodeCreateBuf(pNtk, pNet);
+    pNode = Abc_NtkCreateNodeBuf(pNtk, pNet);
     pNet  = Abc_NtkFindNet(pNtk, pNameOut);    assert( pNet );
     Abc_ObjAddFanin( pNet, pNode );
     return pNet;

src/base/io/ioWriteDot.c

@@ -112,10 +112,13 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
     fprintf( pFile, "\n" );
     fprintf( pFile, "digraph AIG {\n" );
     fprintf( pFile, "size = \"7.5,10\";\n" );
+//    fprintf( pFile, "size = \"10,8.5\";\n" );
+//    fprintf( pFile, "size = \"14,11\";\n" );
+//    fprintf( pFile, "page = \"8,11\";\n" );
 //  fprintf( pFile, "ranksep = 0.5;\n" );
 //  fprintf( pFile, "nodesep = 0.5;\n" );
     fprintf( pFile, "center = true;\n" );
-//  fprintf( pFile, "orientation = landscape;\n" );
+//    fprintf( pFile, "orientation = landscape;\n" );
 //  fprintf( pFile, "edge [fontsize = 10];\n" );
 //  fprintf( pFile, "edge [dir = none];\n" );
     fprintf( pFile, "edge [dir = back];\n" );
@@ -320,8 +323,8 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
             fprintf( pFile, "Node%d%s",  Abc_ObjFaninId0(pNode), (Abc_ObjIsLatch(Abc_ObjFanin0(pNode))? "_out":"") );
             fprintf( pFile, " [" );
             fprintf( pFile, "style = %s", Abc_ObjFaninC0(pNode)? "dotted" : "bold" );
-            if ( Abc_NtkIsSeq(pNode->pNtk) && Seq_ObjFaninL0(pNode) > 0 )
-            fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) );
+//            if ( Abc_NtkIsSeq(pNode->pNtk) && Seq_ObjFaninL0(pNode) > 0 )
+//            fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) );
             fprintf( pFile, "]" );
             fprintf( pFile, ";\n" );
         }
@@ -335,8 +338,8 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
             fprintf( pFile, "Node%d%s",  Abc_ObjFaninId1(pNode), (Abc_ObjIsLatch(Abc_ObjFanin1(pNode))? "_out":"") );
             fprintf( pFile, " [" );
             fprintf( pFile, "style = %s", Abc_ObjFaninC1(pNode)? "dotted" : "bold" );
-            if ( Abc_NtkIsSeq(pNode->pNtk) && Seq_ObjFaninL1(pNode) > 0 )
-            fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) );
+//            if ( Abc_NtkIsSeq(pNode->pNtk) && Seq_ObjFaninL1(pNode) > 0 )
+//            fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) );
             fprintf( pFile, "]" );
             fprintf( pFile, ";\n" );
         }

src/base/seq/seqUtil.c

@@ -580,7 +580,8 @@ int Seq_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose )
         Abc_NtkNodeNum(pNtk), Vec_PtrSize(vNodesPo), Vec_PtrSize(vNodesPi) );
     if ( Abc_NtkNodeNum(pNtk) > Vec_PtrSize(vNodesPo) )
     {
-        Counter = Abc_NtkReduceNodes( pNtk, vNodesPo );
+//        Counter = Abc_NtkReduceNodes( pNtk, vNodesPo );
+        Counter = 0;
         if ( fVerbose )
             printf( "Cleanup removed %d nodes that are not reachable from the POs.\n", Counter );
     }

src/bdd/dsd/dsd.h

@@ -63,10 +63,10 @@ enum Dsd_Type_t_ {
 ////////////////////////////////////////////////////////////////////////
 
 // complementation and testing for pointers for decomposition entries
-#define Dsd_IsComplement(p)  (((int)((long) (p) & 01)))
-#define Dsd_Regular(p)       ((Dsd_Node_t *)((unsigned)(p) & ~01)) 
-#define Dsd_Not(p)           ((Dsd_Node_t *)((long)(p) ^ 01)) 
-#define Dsd_NotCond(p,c)     ((Dsd_Node_t *)((long)(p) ^ (c)))
+#define Dsd_IsComplement(p)  (((int)((unsigned long) (p) & 01)))
+#define Dsd_Regular(p)       ((Dsd_Node_t *)((unsigned long)(p) & ~01)) 
+#define Dsd_Not(p)           ((Dsd_Node_t *)((unsigned long)(p) ^ 01)) 
+#define Dsd_NotCond(p,c)     ((Dsd_Node_t *)((unsigned long)(p) ^ (c)))
 
 ////////////////////////////////////////////////////////////////////////
 ///                         ITERATORS                                ///

src/bdd/reo/reo.h

@@ -172,8 +172,8 @@ struct _reo_man
 
 // used to manipulate units
 #define Unit_Regular(u)     ((reo_unit *)((unsigned long)(u) & ~01))
-#define Unit_Not(u)         ((reo_unit *)((long)(u) ^ 01))
-#define Unit_NotCond(u,c)   ((reo_unit *)((long)(u) ^ (c)))
+#define Unit_Not(u)         ((reo_unit *)((unsigned long)(u) ^ 01))
+#define Unit_NotCond(u,c)   ((reo_unit *)((unsigned long)(u) ^ (c)))
 #define Unit_IsConstant(u)  ((int)((u)->lev == REO_CONST_LEVEL))
 
 ////////////////////////////////////////////////////////////////////////

src/map/fpga/fpga.h

@@ -52,10 +52,10 @@ typedef struct Fpga_LutLibStruct_t_      Fpga_LutLib_t;
 ///                       MACRO DEFINITIONS                          ///
 ////////////////////////////////////////////////////////////////////////
  
-#define Fpga_IsComplement(p)    (((int)((long) (p) & 01)))
-#define Fpga_Regular(p)         ((Fpga_Node_t *)((unsigned)(p) & ~01)) 
-#define Fpga_Not(p)             ((Fpga_Node_t *)((long)(p) ^ 01)) 
-#define Fpga_NotCond(p,c)       ((Fpga_Node_t *)((long)(p) ^ (c)))
+#define Fpga_IsComplement(p)    (((int)((unsigned long) (p) & 01)))
+#define Fpga_Regular(p)         ((Fpga_Node_t *)((unsigned long)(p) & ~01)) 
+#define Fpga_Not(p)             ((Fpga_Node_t *)((unsigned long)(p) ^ 01)) 
+#define Fpga_NotCond(p,c)       ((Fpga_Node_t *)((unsigned long)(p) ^ (c)))
 
 #define Fpga_Ref(p)   
 #define Fpga_Deref(p)

src/map/fpga/fpgaInt.h

@@ -67,16 +67,16 @@
 #define FPGA_SEQ_SIGN(p)        (1 << (((unsigned)p)%31));
 
 // internal macros to work with cuts
-#define Fpga_CutIsComplement(p)  (((int)((long) (p) & 01)))
-#define Fpga_CutRegular(p)       ((Fpga_Cut_t *)((unsigned)(p) & ~01)) 
-#define Fpga_CutNot(p)           ((Fpga_Cut_t *)((long)(p) ^ 01)) 
-#define Fpga_CutNotCond(p,c)     ((Fpga_Cut_t *)((long)(p) ^ (c)))
+#define Fpga_CutIsComplement(p)  (((int)((unsigned long) (p) & 01)))
+#define Fpga_CutRegular(p)       ((Fpga_Cut_t *)((unsigned long)(p) & ~01)) 
+#define Fpga_CutNot(p)           ((Fpga_Cut_t *)((unsigned long)(p) ^ 01)) 
+#define Fpga_CutNotCond(p,c)     ((Fpga_Cut_t *)((unsigned long)(p) ^ (c)))
 
 // the cut nodes
-#define Fpga_SeqIsComplement( p )      (((int)((long) (p) & 01)))
-#define Fpga_SeqRegular( p )           ((Fpga_Node_t *)((unsigned)(p) & ~015))
-#define Fpga_SeqIndex( p )             ((((unsigned)(p)) >> 1) & 07)
-#define Fpga_SeqIndexCreate( p, Ind )  (((unsigned)(p)) | (1 << (((unsigned)(Ind)) & 07)))
+#define Fpga_SeqIsComplement( p )      (((int)((unsigned long) (p) & 01)))
+#define Fpga_SeqRegular( p )           ((Fpga_Node_t *)((unsigned long)(p) & ~015))
+#define Fpga_SeqIndex( p )             ((((unsigned long)(p)) >> 1) & 07)
+#define Fpga_SeqIndexCreate( p, Ind )  (((unsigned long)(p)) | (1 << (((unsigned)(Ind)) & 07)))
 
 // internal macros for referencing of nodes
 #define Fpga_NodeReadRef(p)      ((Fpga_Regular(p))->nRefs)

src/map/mapper/mapper.h

@@ -63,10 +63,10 @@ struct Map_TimeStruct_t_
 ///                       MACRO DEFINITIONS                          ///
 ////////////////////////////////////////////////////////////////////////
  
-#define Map_IsComplement(p)    (((int)((long) (p) & 01)))
-#define Map_Regular(p)         ((Map_Node_t *)((unsigned)(p) & ~01)) 
-#define Map_Not(p)             ((Map_Node_t *)((long)(p) ^ 01)) 
-#define Map_NotCond(p,c)       ((Map_Node_t *)((long)(p) ^ (c)))
+#define Map_IsComplement(p)    (((int)((unsigned long) (p) & 01)))
+#define Map_Regular(p)         ((Map_Node_t *)((unsigned long)(p) & ~01)) 
+#define Map_Not(p)             ((Map_Node_t *)((unsigned long)(p) ^ 01)) 
+#define Map_NotCond(p,c)       ((Map_Node_t *)((unsigned long)(p) ^ (c)))
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///

src/map/mapper/mapperInt.h

@@ -61,10 +61,10 @@
 #define MAP_RANDOM_UNSIGNED   ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()))
 
 // internal macros to work with cuts
-#define Map_CutIsComplement(p)  (((int)((long) (p) & 01)))
-#define Map_CutRegular(p)       ((Map_Cut_t *)((unsigned)(p) & ~01)) 
-#define Map_CutNot(p)           ((Map_Cut_t *)((long)(p) ^ 01)) 
-#define Map_CutNotCond(p,c)     ((Map_Cut_t *)((long)(p) ^ (c)))
+#define Map_CutIsComplement(p)  (((int)((unsigned long) (p) & 01)))
+#define Map_CutRegular(p)       ((Map_Cut_t *)((unsigned long)(p) & ~01)) 
+#define Map_CutNot(p)           ((Map_Cut_t *)((unsigned long)(p) ^ 01)) 
+#define Map_CutNotCond(p,c)     ((Map_Cut_t *)((unsigned long)(p) ^ (c)))
 
 // internal macros for referencing of nodes
 #define Map_NodeReadRef(p)      ((Map_Regular(p))->nRefs)

src/map/super/superAnd.c

@@ -61,10 +61,10 @@ struct Super2_GateStruct_t_
 
 
 // manipulation of complemented attributes
-#define Super2_IsComplement(p)    (((int)((long) (p) & 01)))
-#define Super2_Regular(p)         ((Super2_Gate_t *)((unsigned)(p) & ~01)) 
-#define Super2_Not(p)             ((Super2_Gate_t *)((long)(p) ^ 01)) 
-#define Super2_NotCond(p,c)       ((Super2_Gate_t *)((long)(p) ^ (c)))
+#define Super2_IsComplement(p)    (((int)((unsigned long) (p) & 01)))
+#define Super2_Regular(p)         ((Super2_Gate_t *)((unsigned long)(p) & ~01)) 
+#define Super2_Not(p)             ((Super2_Gate_t *)((unsigned long)(p) ^ 01)) 
+#define Super2_NotCond(p,c)       ((Super2_Gate_t *)((unsigned long)(p) ^ (c)))
 
 // iterating through the gates in the library
 #define Super2_LibForEachGate( Lib, Gate )                        \

src/misc/nm/nmApi.c

@@ -120,7 +120,7 @@ char * Nm_ManStoreIdName( Nm_Man_t * p, int ObjId, int Type, char * pName, char
     nEntrySize = sizeof(Nm_Entry_t) + strlen(pName) + (pSuffix?strlen(pSuffix):0) + 1;
     nEntrySize = (nEntrySize / 4 + ((nEntrySize % 4) > 0)) * 4;
     pEntry = (Nm_Entry_t *)Extra_MmFlexEntryFetch( p->pMem, nEntrySize );
-    pEntry->pNextI2N = pEntry->pNextN2I = NULL;
+    pEntry->pNextI2N = pEntry->pNextN2I = pEntry->pNameSake = NULL;
     pEntry->ObjId = ObjId;
     pEntry->Type = Type;
     sprintf( pEntry->Name, "%s%s", pName, pSuffix? pSuffix : "" );

src/misc/vec/vecPtr.h

@@ -574,8 +574,34 @@ static inline void Vec_PtrReorder( Vec_Ptr_t * p, int nItems )
 ***********************************************************************/
 static inline void Vec_PtrSort( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
 {
+    if ( p->nSize < 2 )
+        return;
+    qsort( (void *)p->pArray, p->nSize, sizeof(void *), 
+            (int (*)(const void *, const void *)) Vec_PtrSortCompare );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorting the entries by their integer value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrUniqify( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
+{
+    int i, k;
+    if ( p->nSize < 2 )
+        return;
     qsort( (void *)p->pArray, p->nSize, sizeof(void *), 
             (int (*)(const void *, const void *)) Vec_PtrSortCompare );
+    for ( i = k = 1; i < p->nSize; i++ )
+        if ( p->pArray[i] != p->pArray[i-1] )
+            p->pArray[k++] = p->pArray[i];
+    p->nSize = k;
 }
 
 #endif

src/opt/ret/module.make

+SRC +=  src/opt/dec/retArea.c \
+        src/opt/dec/retBwd.c \
+        src/opt/dec/retCore.c \
+        src/opt/dec/retDelay.c \
+        src/opt/dec/retFlow.c \
+        src/opt/dec/retFwd.c \
+        src/opt/dec/retInit.c
+

src/opt/ret/retBwd.c

+/**CFile****************************************************************
+
+  FileName    [retBwd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Retiming package.]
+
+  Synopsis    [Most backward retiming.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Oct 31, 2006.]
+
+  Revision    [$Id: retBwd.c,v 1.00 2006/10/31 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "retInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRetimeBackward( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    printf( "Not implemented.\n" );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/ret/retCore.c

+/**CFile****************************************************************
+
+  FileName    [retCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Retiming package.]
+
+  Synopsis    [The core retiming procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Oct 31, 2006.]
+
+  Revision    [$Id: retCore.c,v 1.00 2006/10/31 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "retInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Implementation of retiming.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fVerbose )
+{
+    int RetValue;
+    assert( Mode > 0 && Mode < 6 );
+    // perform forward retiming
+    switch ( Mode )
+    {
+    case 1: // forward 
+        RetValue = Abc_NtkRetimeForward( pNtk, fVerbose );
+        break;
+    case 2: // backward 
+        RetValue = Abc_NtkRetimeBackward( pNtk, fVerbose );
+        break;
+    case 3: // min-area 
+        RetValue = Abc_NtkRetimeMinArea( pNtk, fVerbose );
+        break;
+    case 4: // min-delay
+        RetValue = Abc_NtkRetimeMinDelay( pNtk, fVerbose );
+        break;
+    case 5: // min-area + min-delay
+        RetValue  = Abc_NtkRetimeMinArea( pNtk, fVerbose );
+        RetValue += Abc_NtkRetimeMinDelay( pNtk, fVerbose );
+        break;
+    default:
+        printf( "Unknown retiming option.\n" );
+        break;
+    }
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/ret/retDelay.c

+/**CFile****************************************************************
+
+  FileName    [retDelay.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Retiming package.]
+
+  Synopsis    [Incremental retiming for optimum delay.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Oct 31, 2006.]
+
+  Revision    [$Id: retDelay.c,v 1.00 2006/10/31 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "retInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRetimeMinDelay( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    printf( "Not implemented.\n" );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/ret/retFwd.c

+/**CFile****************************************************************
+
+  FileName    [retFwd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Retiming package.]
+
+  Synopsis    [Most forward retiming.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Oct 31, 2006.]
+
+  Revision    [$Id: retFwd.c,v 1.00 2006/10/31 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "retInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRetimeForward( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    printf( "Not implemented.\n" );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/ret/retInit.c

+/**CFile****************************************************************
+
+  FileName    [ret_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Retiming package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Oct 31, 2006.]
+
+  Revision    [$Id: ret_.c,v 1.00 2006/10/31 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "retInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes initial values of the new latches.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, int fVerbose )
+{
+    Abc_Obj_t * pLatch;
+    int * pModel, RetValue, clk, i;
+    if ( fVerbose )
+        printf( "The number of ANDs in the AIG = %5d.\n", Abc_NtkNodeNum(pNtkMiter) );
+    // solve the miter
+clk = clock();
+    RetValue = Abc_NtkMiterSat( pNtkMiter, (sint64)500000, (sint64)50000000, 0, 0, NULL, NULL );
+if ( fVerbose && clock() - clk > 100 )
+{
+PRT( "SAT solving time", clock() - clk );
+}
+    // analyze the result
+    if ( RetValue == 1 )
+        printf( "Abc_NtkRetimeInitialValues(): The problem is unsatisfiable. DC latch values are used.\n" );
+    else if ( RetValue == -1 )
+        printf( "Abc_NtkRetimeInitialValues(): The SAT problem timed out. DC latch values are used.\n" );
+    // set the values of the latches
+    pModel = pNtkMiter->pModel;  pNtkMiter->pModel = NULL;
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        pLatch->pData = (void *)(pModel? (pModel[i]? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC);
+    FREE( pModel );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/ret/retInt.h

+/**CFile****************************************************************
+
+  FileName    [retInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Retiming package.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Oct 31, 2006.]
+
+  Revision    [$Id: retInt.h,v 1.00 2006/10/31 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __RET_INT_H__
+#define __RET_INT_H__
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    STRUCTURE DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== retArea.c ========================================================*/
+extern int         Abc_NtkRetimeMinArea( Abc_Ntk_t * pNtk, int fVerbose );
+/*=== retBwd.c ========================================================*/
+extern int         Abc_NtkRetimeBackward( Abc_Ntk_t * pNtk, int fVerbose );
+/*=== retCore.c ========================================================*/
+extern int         Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fVerbose );
+/*=== retDelay.c ========================================================*/
+extern int         Abc_NtkRetimeMinDelay( Abc_Ntk_t * pNtk, int fVerbose );
+/*=== retFlow.c ========================================================*/
+extern void        Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t * Abc_NtkMaxFlow( Abc_Ntk_t * pNtk, int fForward, int fVerbose );
+/*=== retFwd.c ========================================================*/
+extern int         Abc_NtkRetimeForward( Abc_Ntk_t * pNtk, int fVerbose );
+/*=== retInit.c ========================================================*/
+extern void        Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, int fVerbose );
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/ret/ret_.c

+/**CFile****************************************************************
+
+  FileName    [ret_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Retiming package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Oct 31, 2006.]
+
+  Revision    [$Id: ret_.c,v 1.00 2006/10/31 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "retInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/opt/rwr/rwr.h

@@ -106,10 +106,10 @@ struct Rwr_Node_t_ // 24 bytes
 };
 
 // manipulation of complemented attributes
-static inline bool         Rwr_IsComplement( Rwr_Node_t * p )    { return (bool)(((unsigned)p) & 01);           }
-static inline Rwr_Node_t * Rwr_Regular( Rwr_Node_t * p )         { return (Rwr_Node_t *)((unsigned)(p) & ~01);  }
-static inline Rwr_Node_t * Rwr_Not( Rwr_Node_t * p )             { return (Rwr_Node_t *)((unsigned)(p) ^  01);  }
-static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c )  { return (Rwr_Node_t *)((unsigned)(p) ^ (c));  }
+static inline bool         Rwr_IsComplement( Rwr_Node_t * p )    { return (bool)(((unsigned long)p) & 01);           }
+static inline Rwr_Node_t * Rwr_Regular( Rwr_Node_t * p )         { return (Rwr_Node_t *)((unsigned long)(p) & ~01);  }
+static inline Rwr_Node_t * Rwr_Not( Rwr_Node_t * p )             { return (Rwr_Node_t *)((unsigned long)(p) ^  01);  }
+static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c )  { return (Rwr_Node_t *)((unsigned long)(p) ^ (c));  }
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///

src/sat/fraig/fraig.h

@@ -104,10 +104,10 @@ struct Prove_ParamsStruct_t_
 ////////////////////////////////////////////////////////////////////////
  
 // macros working with complemented attributes of the nodes
-#define Fraig_IsComplement(p)    (((int)((long) (p) & 01)))
-#define Fraig_Regular(p)         ((Fraig_Node_t *)((unsigned)(p) & ~01)) 
-#define Fraig_Not(p)             ((Fraig_Node_t *)((long)(p) ^ 01)) 
-#define Fraig_NotCond(p,c)       ((Fraig_Node_t *)((long)(p) ^ (c)))
+#define Fraig_IsComplement(p)    (((int)((unsigned long) (p) & 01)))
+#define Fraig_Regular(p)         ((Fraig_Node_t *)((unsigned long)(p) & ~01)) 
+#define Fraig_Not(p)             ((Fraig_Node_t *)((unsigned long)(p) ^ 01)) 
+#define Fraig_NotCond(p,c)       ((Fraig_Node_t *)((unsigned long)(p) ^ (c)))
 
 // these are currently not used
 #define Fraig_Ref(p)              

src/temp/aig/aig.h

@@ -30,6 +30,11 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 #include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+
 #include "vec.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -104,16 +109,20 @@ struct Aig_Man_t_
 #define AIG_MIN(a,b)       (((a) < (b))? (a) : (b))
 #define AIG_MAX(a,b)       (((a) > (b))? (a) : (b))
 
+#ifndef PRT
+#define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
+#endif
+
 static inline int          Aig_BitWordNum( int nBits )            { return (nBits>>5) + ((nBits&31) > 0);           }
 static inline int          Aig_TruthWordNum( int nVars )          { return nVars <= 5 ? 1 : (1 << (nVars - 5));     }
 static inline int          Aig_InfoHasBit( unsigned * p, int i )  { return (p[(i)>>5] & (1<<((i) & 31))) > 0;       }
 static inline void         Aig_InfoSetBit( unsigned * p, int i )  { p[(i)>>5] |= (1<<((i) & 31));                   }
 static inline void         Aig_InfoXorBit( unsigned * p, int i )  { p[(i)>>5] ^= (1<<((i) & 31));                   }
 
-static inline Aig_Obj_t *  Aig_Regular( Aig_Obj_t * p )           { return (Aig_Obj_t *)((unsigned)(p) & ~01);      }
-static inline Aig_Obj_t *  Aig_Not( Aig_Obj_t * p )               { return (Aig_Obj_t *)((unsigned)(p) ^  01);      }
-static inline Aig_Obj_t *  Aig_NotCond( Aig_Obj_t * p, int c )    { return (Aig_Obj_t *)((unsigned)(p) ^ (c));      }
-static inline int          Aig_IsComplement( Aig_Obj_t * p )      { return (int )(((unsigned)p) & 01);              }
+static inline Aig_Obj_t *  Aig_Regular( Aig_Obj_t * p )           { return (Aig_Obj_t *)((unsigned long)(p) & ~01);      }
+static inline Aig_Obj_t *  Aig_Not( Aig_Obj_t * p )               { return (Aig_Obj_t *)((unsigned long)(p) ^  01);      }
+static inline Aig_Obj_t *  Aig_NotCond( Aig_Obj_t * p, int c )    { return (Aig_Obj_t *)((unsigned long)(p) ^ (c));      }
+static inline int          Aig_IsComplement( Aig_Obj_t * p )      { return (int )(((unsigned long)p) & 01);              }
 
 static inline Aig_Obj_t *  Aig_ManConst0( Aig_Man_t * p )         { return Aig_Not(p->pConst1);                     }
 static inline Aig_Obj_t *  Aig_ManConst1( Aig_Man_t * p )         { return p->pConst1;                              }

src/temp/aig/aigBalance.c

@@ -17,7 +17,7 @@
   Revision    [$Id: aigBalance.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
- 
+
 #include "aig.h"
 
 ////////////////////////////////////////////////////////////////////////

src/temp/aig/cudd2.c

@@ -53,7 +53,9 @@ static Aig_CuddMan_t * s_pCuddMan = NULL;
 void Cudd2_Init( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void * pCudd )
 {
     int v;
-    assert( s_pCuddMan == NULL );
+    // start the BDD-to-AIG manager when the first BDD manager is allocated
+    if ( s_pCuddMan != NULL )
+        return;
     s_pCuddMan = ALLOC( Aig_CuddMan_t, 1 );
     s_pCuddMan->pAig = Aig_ManStart();
     s_pCuddMan->pTable = st_init_table( st_ptrcmp, st_ptrhash );
@@ -127,6 +129,22 @@ static void Cudd2_SetArg( Aig_Obj_t * pNode, void * pResult )
 
 /**Function*************************************************************
 
+  Synopsis    [Registers constant 1 node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cudd2_bddOne( void * pCudd, void * pResult )
+{
+    Cudd2_SetArg( Aig_ManConst1(s_pCuddMan->pAig), pResult );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Adds elementary variable.]
 
   Description []

src/temp/aig/cudd2.h

@@ -25,6 +25,11 @@
 extern "C" {
 #endif 
 
+// HA: Added for printing messages
+#ifndef MSG 
+#define MSG(msg) (printf("%s = \n",(msg)));
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -52,6 +57,7 @@ extern "C" {
 
 extern void Cudd2_Init      ( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void * pCudd );
 extern void Cudd2_Quit      ( void * pCudd );
+extern void Cudd2_bddOne    ( void * pCudd, void * pResult );
 extern void Cudd2_bddIthVar ( void * pCudd, int iVar, void * pResult );
 extern void Cudd2_bddAnd    ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
 extern void Cudd2_bddOr     ( void * pCudd, void * pArg0, void * pArg1, void * pResult );

src/temp/aig_free/aigCheck.c

+/**CFile****************************************************************
+
+  FileName    [aigCheck.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Minimalistic And-Inverter Graph package.]
+
+  Synopsis    [AIG checking procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: aigCheck.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the consistency of the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCheck( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pObj2;
+    int i;
+    // check primary inputs
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        if ( Aig_ObjFanin0(pObj) || Aig_ObjFanin1(pObj) )
+        {
+            printf( "Aig_ManCheck: The PI node \"%p\" has fanins.\n", pObj );
+            return 0;
+        }
+    }
+    // check primary outputs
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        if ( !Aig_ObjFanin0(pObj) )
+        {
+            printf( "Aig_ManCheck: The PO node \"%p\" has NULL fanin.\n", pObj );
+            return 0;
+        }
+        if ( Aig_ObjFanin1(pObj) )
+        {
+            printf( "Aig_ManCheck: The PO node \"%p\" has second fanin.\n", pObj );
+            return 0;
+        }
+    }
+    // check internal nodes
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        if ( !Aig_ObjFanin0(pObj) || !Aig_ObjFanin1(pObj) )
+        {
+            printf( "Aig_ManCheck: The AIG has internal node \"%p\" with a NULL fanin.\n", pObj );
+            return 0;
+        }
+        if ( Aig_ObjFanin0(pObj) >= Aig_ObjFanin1(pObj) )
+        {
+            printf( "Aig_ManCheck: The AIG has node \"%p\" with a wrong ordering of fanins.\n", pObj );
+            return 0;
+        }
+        pObj2 = Aig_TableLookup( p, pObj );
+        if ( pObj2 != pObj )
+        {
+            printf( "Aig_ManCheck: Node \"%p\" is not in the structural hashing table.\n", pObj );
+            return 0;
+        }
+    }
+    // count the total number of nodes
+    if ( Aig_ManObjNum(p) != 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) )
+    {
+        printf( "Aig_ManCheck: The number of created nodes is wrong.\n" );
+        return 0;
+    }
+    // count the number of nodes in the table
+    if ( Aig_TableCountEntries(p) != Aig_ManAndNum(p) + Aig_ManExorNum(p) )
+    {
+        printf( "Aig_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
+        return 0;
+    }
+//    if ( !Aig_ManIsAcyclic(p) )
+//        return 0;
+    return 1; 
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/temp/aig_free/aigMan.c

+/**CFile****************************************************************
+
+  FileName    [aigMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Minimalistic And-Inverter Graph package.]
+
+  Synopsis    [AIG manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: aig_.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManStart()
+{
+    Aig_Man_t * p;
+    // start the manager
+    p = ALLOC( Aig_Man_t, 1 );
+    memset( p, 0, sizeof(Aig_Man_t) );
+    // perform initializations
+    p->nTravIds = 1;
+    p->fRefCount = 1;
+    p->fCatchExor = 0;
+    // allocate arrays for nodes
+    p->vPis = Vec_PtrAlloc( 100 );
+    p->vPos = Vec_PtrAlloc( 100 );
+    // prepare the internal memory manager
+    Aig_ManStartMemory( p );
+    // create the constant node
+    p->pConst1 = Aig_ManFetchMemory( p );
+    p->pConst1->Type = AIG_CONST1;
+    p->pConst1->fPhase = 1;
+    p->nCreated = 1;
+    // start the table
+    p->nTableSize = 10007;
+    p->pTable = ALLOC( Aig_Obj_t *, p->nTableSize );
+    memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManStop( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    // make sure the nodes have clean marks
+    pObj = Aig_ManConst1(p);
+    assert( !pObj->fMarkA && !pObj->fMarkB );
+    Aig_ManForEachPi( p, pObj, i )
+        assert( !pObj->fMarkA && !pObj->fMarkB );
+    Aig_ManForEachPo( p, pObj, i )
+        assert( !pObj->fMarkA && !pObj->fMarkB );
+    Aig_ManForEachNode( p, pObj, i )
+        assert( !pObj->fMarkA && !pObj->fMarkB );
+    // print time
+    if ( p->time1 ) { PRT( "time1", p->time1 ); }
+    if ( p->time2 ) { PRT( "time2", p->time2 ); }
+//    Aig_TableProfile( p );
+    if ( p->vChunks )   Aig_ManStopMemory( p );
+    if ( p->vPis )      Vec_PtrFree( p->vPis );
+    if ( p->vPos )      Vec_PtrFree( p->vPos );
+    free( p->pTable );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of dangling nodes removed.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCleanup( Aig_Man_t * p )
+{
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pNode;
+    int i, nNodesOld;
+    assert( p->fRefCount );
+    nNodesOld = Aig_ManNodeNum(p);
+    // collect roots of dangling nodes
+    vNodes = Vec_PtrAlloc( 100 );
+    Aig_ManForEachNode( p, pNode, i )
+        if ( Aig_ObjRefs(pNode) == 0 )
+            Vec_PtrPush( vNodes, pNode );
+    // recursively remove dangling nodes
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+        Aig_ObjDelete_rec( p, pNode );
+    Vec_PtrFree( vNodes );
+    return nNodesOld - Aig_ManNodeNum(p);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPrintStats( Aig_Man_t * p )
+{
+    printf( "PI/PO = %d/%d. ", Aig_ManPiNum(p), Aig_ManPoNum(p) );
+    printf( "A = %7d. ",       Aig_ManAndNum(p) );
+    printf( "X = %5d. ",       Aig_ManExorNum(p) );
+    printf( "Cre = %7d. ",     p->nCreated );
+    printf( "Del = %7d. ",     p->nDeleted );
+    printf( "Lev = %3d. ",     Aig_ManCountLevels(p) );
+    printf( "\n" );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/temp/aig_free/aigMem.c

+/**CFile****************************************************************
+
+  FileName    [aigMem.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Minimalistic 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: aigMem.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.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 Aig_ManStartMemory( Aig_Man_t * p )
+{
+    p->vChunks = Vec_PtrAlloc( 128 );
+    p->vPages = Vec_PtrAlloc( 128 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the internal memory manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManStopMemory( Aig_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 Aig_ManAddMemory( Aig_Man_t * p )
+{
+    char * pMemory;
+    int i, nBytes;
+    assert( sizeof(Aig_Obj_t) <= 64 );
+    assert( p->pListFree == NULL );
+//    assert( (Aig_ManObjNum(p) & IVY_PAGE_MASK) == 0 );
+    // allocate new memory page
+    nBytes = sizeof(Aig_Obj_t) * (1<<IVY_PAGE_SIZE) + 64;
+    pMemory = ALLOC( char, nBytes );
+    Vec_PtrPush( p->vChunks, pMemory );
+    // align memory at the 32-byte boundary
+    pMemory = pMemory + 64 - (((int)pMemory) & 63);
+    // remember the manager in the first entry
+    Vec_PtrPush( p->vPages, pMemory );
+    // break the memory down into nodes
+    p->pListFree = (Aig_Obj_t *)pMemory;
+    for ( i = 1; i <= IVY_PAGE_MASK; i++ )
+    {
+        *((char **)pMemory) = pMemory + sizeof(Aig_Obj_t);
+        pMemory += sizeof(Aig_Obj_t);
+    }
+    *((char **)pMemory) = NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/temp/aig_free/aigObj.c

+/**CFile****************************************************************
+
+  FileName    [aigObj.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Minimalistic And-Inverter Graph package.]
+
+  Synopsis    [Adding/removing objects.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: aigObj.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates primary input.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ObjCreatePi( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    pObj = Aig_ManFetchMemory( p );
+    pObj->Type = AIG_PI;
+    Vec_PtrPush( p->vPis, pObj );
+    p->nObjs[AIG_PI]++;
+    p->nCreated++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates primary output with the given driver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver )
+{
+    Aig_Obj_t * pObj;
+    pObj = Aig_ManFetchMemory( p );
+    pObj->Type = AIG_PO;
+    Vec_PtrPush( p->vPos, pObj );
+    // add connections
+    pObj->pFanin0 = pDriver;
+    if ( p->fRefCount )
+        Aig_ObjRef( Aig_Regular(pDriver) );
+    else
+        pObj->nRefs = Aig_ObjLevel( Aig_Regular(pDriver) );
+    // update node counters of the manager
+    p->nObjs[AIG_PO]++;
+    p->nCreated++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create the new node assuming it does not exist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
+{
+    Aig_Obj_t * pObj;
+    assert( !Aig_IsComplement(pGhost) );
+    assert( Aig_ObjIsNode(pGhost) );
+    assert( pGhost == &p->Ghost );
+    // get memory for the new object
+    pObj = Aig_ManFetchMemory( p );
+    pObj->Type = pGhost->Type;
+    // add connections
+    Aig_ObjConnect( p, pObj, pGhost->pFanin0, pGhost->pFanin1 );
+    // update node counters of the manager
+    p->nObjs[Aig_ObjType(pObj)]++;
+    p->nCreated++;
+    return pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connect the object to the fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj_t * pFan1 )
+{
+    assert( !Aig_IsComplement(pObj) );
+    assert( Aig_ObjIsNode(pObj) );
+    // add the first fanin
+    pObj->pFanin0 = pFan0;
+    pObj->pFanin1 = pFan1;
+    // increment references of the fanins and add their fanouts
+    if ( p->fRefCount )
+    {
+        if ( pFan0 != NULL )
+            Aig_ObjRef( Aig_ObjFanin0(pObj) );
+        if ( pFan1 != NULL )
+            Aig_ObjRef( Aig_ObjFanin1(pObj) );
+    }
+    else
+        pObj->nRefs = Aig_ObjLevelNew( pObj );
+    // add the node to the structural hash table
+    Aig_TableInsert( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Connect the object to the fanin.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    assert( !Aig_IsComplement(pObj) );
+    assert( Aig_ObjIsNode(pObj) );
+    // remove connections
+    if ( pObj->pFanin0 != NULL )
+        Aig_ObjDeref(Aig_ObjFanin0(pObj));
+    if ( pObj->pFanin1 != NULL )
+        Aig_ObjDeref(Aig_ObjFanin1(pObj));
+    // remove the node from the structural hash table
+    Aig_TableDelete( p, pObj );
+    // add the first fanin
+    pObj->pFanin0 = NULL;
+    pObj->pFanin1 = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    assert( !Aig_IsComplement(pObj) );
+    assert( !Aig_ObjIsTerm(pObj) );
+    assert( Aig_ObjRefs(pObj) == 0 );
+    // update node counters of the manager
+    p->nObjs[pObj->Type]--;
+    p->nDeleted++;
+    // remove connections
+    Aig_ObjDisconnect( p, pObj );
+    // remove PIs/POs from the arrays
+    if ( Aig_ObjIsPi(pObj) )
+        Vec_PtrRemove( p->vPis, pObj );
+    // free the node
+    Aig_ManRecycleMemory( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the MFFC of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pFanin0, * pFanin1;
+    assert( !Aig_IsComplement(pObj) );
+    if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsPi(pObj) )
+        return;
+    assert( Aig_ObjIsNode(pObj) );
+    pFanin0 = Aig_ObjFanin0(pObj);
+    pFanin1 = Aig_ObjFanin1(pObj);
+    Aig_ObjDelete( p, pObj );
+    if ( pFanin0 && !Aig_ObjIsNone(pFanin0) && Aig_ObjRefs(pFanin0) == 0 )
+        Aig_ObjDelete_rec( p, pFanin0 );
+    if ( pFanin1 && !Aig_ObjIsNone(pFanin1) && Aig_ObjRefs(pFanin1) == 0 )
+        Aig_ObjDelete_rec( p, pFanin1 );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/temp/aig_free/aigTable.c

+/**CFile****************************************************************
+
+  FileName    [aigTable.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Minimalistic And-Inverter Graph package.]
+
+  Synopsis    [Structural hashing table.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006. ]
+
+  Revision    [$Id: aigTable.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// hashing the node
+static unsigned long Aig_Hash( Aig_Obj_t * pObj, int TableSize ) 
+{
+    unsigned long Key = Aig_ObjIsExor(pObj) * 1699;
+    Key ^= (long)Aig_ObjFanin0(pObj) * 7937;
+    Key ^= (long)Aig_ObjFanin1(pObj) * 2971;
+    Key ^= Aig_ObjFaninC0(pObj) * 911;
+    Key ^= Aig_ObjFaninC1(pObj) * 353;
+    return Key % TableSize;
+}
+
+// returns the place where this node is stored (or should be stored)
+static Aig_Obj_t ** Aig_TableFind( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    int i;
+    assert( Aig_ObjChild0(pObj) && Aig_ObjChild1(pObj) );
+    assert( Aig_ObjChild0(pObj) <  Aig_ObjChild1(pObj) );
+    for ( i = Aig_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
+        if ( p->pTable[i] == pObj )
+            break;
+    return p->pTable + i;
+}
+
+static void         Aig_TableResize( Aig_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.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost )
+{
+    int i;
+    assert( !Aig_IsComplement(pGhost) );
+    assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) );
+    assert( Aig_ObjChild0(pGhost) <  Aig_ObjChild1(pGhost) );
+    if ( p->fRefCount && (!Aig_ObjRefs(Aig_ObjFanin0(pGhost)) || !Aig_ObjRefs(Aig_ObjFanin1(pGhost))) )
+        return NULL;
+    for ( i = Aig_Hash(pGhost, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize )
+    {
+        if ( Aig_ObjChild0(p->pTable[i]) == Aig_ObjChild0(pGhost) && 
+             Aig_ObjChild1(p->pTable[i]) == Aig_ObjChild1(pGhost) && 
+             Aig_ObjType(p->pTable[i]) == Aig_ObjType(pGhost) )
+            return p->pTable[i];
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the new node to the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t ** ppPlace;
+    assert( !Aig_IsComplement(pObj) );
+    assert( Aig_TableLookup(p, pObj) == NULL );
+    if ( p->nTableSize < 2 * Aig_ManNodeNum(p) )
+        Aig_TableResize( p );
+    ppPlace = Aig_TableFind( p, pObj );
+    assert( *ppPlace == NULL );
+    *ppPlace = pObj;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node from the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pEntry, ** ppPlace;
+    int i;
+    assert( !Aig_IsComplement(pObj) );
+    ppPlace = Aig_TableFind( p, pObj );
+    assert( *ppPlace == pObj ); // node should be in the table
+    *ppPlace = NULL;
+    // rehash the adjacent entries
+    i = ppPlace - p->pTable;
+    for ( i = (i+1) % p->nTableSize; p->pTable[i]; i = (i+1) % p->nTableSize )
+    {
+        pEntry = p->pTable[i];
+        p->pTable[i] = 0;
+        Aig_TableInsert( p, pEntry );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count the number of nodes in the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_TableCountEntries( Aig_Man_t * p )
+{
+    int i, Counter = 0;
+    for ( i = 0; i < p->nTableSize; i++ )
+        Counter += (p->pTable[i] != NULL);
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the table.]
+
+  Description [Typically this procedure should not be called.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TableResize( Aig_Man_t * p )
+{
+    Aig_Obj_t ** pTableOld, ** ppPlace;
+    int nTableSizeOld, Counter, nEntries, e, clk;
+clk = clock();
+    // save the old table
+    pTableOld = p->pTable;
+    nTableSizeOld = p->nTableSize;
+    // get the new table
+    p->nTableSize = Cudd_PrimeAig( 5 * Aig_ManNodeNum(p) ); 
+    p->pTable = ALLOC( Aig_Obj_t *, p->nTableSize );
+    memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
+    // rehash the entries from the old table
+    Counter = 0;
+    for ( e = 0; e < nTableSizeOld; e++ )
+    {
+        if ( pTableOld[e] == 0 )
+            continue;
+        Counter++;
+        // get the place where this entry goes in the table table
+        ppPlace = Aig_TableFind( p, pTableOld[e] );
+        assert( *ppPlace == NULL ); // should not be in the table
+        *ppPlace = pTableOld[e];
+    }
+    nEntries = Aig_ManNodeNum(p);
+//    assert( Counter == nEntries );
+//    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
+//    PRT( "Time", clock() - clk );
+    // replace the table and the parameters
+    free( pTableOld );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Profiles the hash table.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Aig_TableProfile( Aig_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/aig_free/cudd2.h

+/**CFile****************************************************************
+
+  FileName    [cudd2.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Minimalistic And-Inverter Graph package.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - October 3, 2006.]
+
+  Revision    [$Id: cudd2.h,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __CUDD2_H__
+#define __CUDD2_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
+// HA: Added for printing messages
+#ifndef MSG 
+#define MSG(msg) (printf("%s = \n",(msg)));
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                             ITERATORS                            ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+   extern void Cudd2_Init      ( unsigned int numVars, unsigned int numVarsZ, unsigned int numSlots, unsigned int cacheSize, unsigned long maxMemory, void * pCudd );
+   extern void Cudd2_Quit      ( void * pCudd );
+   extern void Cudd2_bddOne    ( void * pCudd, void * pResult );
+   
+   extern void Cudd2_bddIthVar ( void * pCudd, int iVar, void * pResult );
+   extern void Cudd2_bddAnd    ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
+   extern void Cudd2_bddOr     ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
+   extern void Cudd2_bddNand   ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
+   extern void Cudd2_bddNor    ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
+   extern void Cudd2_bddXor    ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
+   extern void Cudd2_bddXnor   ( void * pCudd, void * pArg0, void * pArg1, void * pResult );
+   extern void Cudd2_bddIte    ( void * pCudd, void * pArg0, void * pArg1, void * pArg2, void * pResult );
+   extern void Cudd2_bddCompose( void * pCudd, void * pArg0, void * pArg1, int v, void * pResult );
+   extern void Cudd2_bddLeq    ( void * pCudd, void * pArg0, void * pArg1, int Result );
+   extern void Cudd2_bddEqual  ( void * pCudd, void * pArg0, void * pArg1, int Result );
+   
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+

src/temp/aig_free/st.h

+/*
+ * Revision Control Information
+ *
+ * /projects/hsis/CVS/utilities/st/st.h,v
+ * serdar
+ * 1.1
+ * 1993/07/29 01:00:21
+ *
+ */
+/* LINTLIBRARY */
+
+/* /projects/hsis/CVS/utilities/st/st.h,v 1.1 1993/07/29 01:00:21 serdar Exp */
+
+#ifndef ST_INCLUDED
+#define ST_INCLUDED
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+typedef struct st_table_entry st_table_entry;
+struct st_table_entry {
+    char *key;
+    char *record;
+    st_table_entry *next;
+};
+
+typedef struct st_table st_table;
+struct st_table {
+    int (*compare)();
+    int (*hash)();
+    int num_bins;
+    int num_entries;
+    int max_density;
+    int reorder_flag;
+    double grow_factor;
+    st_table_entry **bins;
+};
+
+typedef struct st_generator st_generator;
+struct st_generator {
+    st_table *table;
+    st_table_entry *entry;
+    int index;
+};
+
+#define st_is_member(table,key) st_lookup(table,key,(char **) 0)
+#define st_count(table) ((table)->num_entries)
+
+enum st_retval {ST_CONTINUE, ST_STOP, ST_DELETE};
+
+typedef enum st_retval (*ST_PFSR)();
+typedef int (*ST_PFI)();
+
+extern st_table *st_init_table_with_params (ST_PFI, ST_PFI, int, int, double, int);
+extern st_table *st_init_table (ST_PFI, ST_PFI); 
+extern void st_free_table (st_table *);
+extern int st_lookup (st_table *, char *, char **);
+extern int st_lookup_int (st_table *, char *, int *);
+extern int st_insert (st_table *, char *, char *);
+extern int st_add_direct (st_table *, char *, char *);
+extern int st_find_or_add (st_table *, char *, char ***);
+extern int st_find (st_table *, char *, char ***);
+extern st_table *st_copy (st_table *);
+extern int st_delete (st_table *, char **, char **);
+extern int st_delete_int (st_table *, long *, char **);
+extern int st_foreach (st_table *, ST_PFSR, char *);
+extern int st_strhash (char *, int);
+extern int st_numhash (char *, int);
+extern int st_ptrhash (char *, int);
+extern int st_numcmp (char *, char *);
+extern int st_ptrcmp (char *, char *);
+extern st_generator *st_init_gen (st_table *);
+extern int st_gen (st_generator *, char **, char **);
+extern int st_gen_int (st_generator *, char **, long *);
+extern void st_free_gen (st_generator *);
+
+
+#define ST_DEFAULT_MAX_DENSITY 5
+#define ST_DEFAULT_INIT_TABLE_SIZE 11
+#define ST_DEFAULT_GROW_FACTOR 2.0
+#define ST_DEFAULT_REORDER_FLAG 0
+
+#define st_foreach_item(table, gen, key, value) \
+    for(gen=st_init_gen(table); st_gen(gen,key,value) || (st_free_gen(gen),0);)
+
+#define st_foreach_item_int(table, gen, key, value) \
+    for(gen=st_init_gen(table); st_gen_int(gen,key,value) || (st_free_gen(gen),0);)
+
+#define ST_OUT_OF_MEM -10000
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif /* ST_INCLUDED */

src/temp/aig_free/subdir.mk

+################################################################################
+# Automatically-generated file. Do not edit!
+################################################################################
+
+INCPATHS = -I$(ROOT)/aig-alan
+
+# Add inputs and outputs from these tool invocations to the build variables 
+PURE_C_SRCS += \
+${addprefix $(ROOT)/aig-alan/, \
+aigBalance.c \
+aigCheck.c \
+aigDfs.c \
+aigMan.c \
+aigMem.c \
+aigObj.c \
+aigOper.c \
+aigTable.c \
+aigUtil.c \
+cudd2.c \
+st.c \
+}
+
+C_SRCS += $(PURE_C_SRCS)
+
+
+PURE_C_OBJS += \
+${addprefix $(ROOT)/obj/aig-alan/, \
+aigBalance.o \
+aigCheck.o \
+aigDfs.o \
+aigMan.o \
+aigMem.o \
+aigObj.o \
+aigOper.o \
+aigTable.o \
+aigUtil.o \
+cudd2.o \
+st.o \
+}
+
+OBJS += $(PURE_C_OBJS) 
+
+PURE_C_DEPS += \
+${addprefix $(ROOT)/obj/aig-alan, \
+aigBalance.d \
+aigCheck.d \
+aigDfs.d \
+aigMan.d \
+aigMem.d \
+aigObj.d \
+aigOper.d \
+aigTable.d \
+aigUtil.d \
+cudd2.d \
+st.d \
+}
+
+DEPS += $(PURE_C_DEPS)
+
+
+OCAML_OBJS += 
+
+
+DEPEND_SRCS += 
+
+# Each subdirectory must supply rules for building sources it contributes
+$(ROOT)/obj/aig-alan/%.o: $(ROOT)/aig-alan/%.c
+	@echo 'Building file: $<'
+	@echo 'Invoking: GCC C Compiler: $(CC)'
+	@echo $(CC) $(GPCC_OPTS) $(INCPATHS)  -O3 -g3 -Wall -c -fmessage-length=0 -o$@ $<
+	@$(CC)  $(GPCC_OPTS)  $(INCPATHS) -O3 -g3 -Wall -c -fmessage-length=0 -o$@ $< && \
+	echo -n $(@:%.o=%.d) $(dir $@) > $(@:%.o=%.d) && \
+	$(CC) -MM -MG -P -w  $(GPCC_OPTS) $(INCPATHS) -O3 -g3 -Wall -c -fmessage-length=0  $< >> $(@:%.o=%.d)
+	@echo 'Finished building: $<'
+	@echo ' '
+
+$(ROOT)/obj/aig-alan/%.o: $(ROOT)/aig-alan/%.cpp
+	@echo 'Building file: $<'
+	@echo 'Invoking: G++ C Compiler: $(GPCC)'
+	@echo $(GPPCC) $(GPCC_OPTS) $(INCPATHS)  -O3 -g3 -Wall -c -fmessage-length=0 -o$@ $<
+	@$(GPPCC)  $(GPCC_OPTS)  $(INCPATHS) -O3 -g3 -Wall -c -fmessage-length=0 -o$@ $< && \
+	echo -n $(@:%.o=%.d) $(dir $@) > $(@:%.o=%.d) && \
+	$(GPPCC) -MM -MG -P -w  $(GPCC_OPTS) $(INCPATHS) -O3 -g3 -Wall -c -fmessage-length=0  $< >> $(@:%.o=%.d)
+	@echo 'Finished building: $<'
+	@echo ' '
+
+

src/temp/aig_free/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
+
+#ifndef ALLOC
+#define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
+#endif
+
+#ifndef FREE
+#define FREE(obj)             ((obj) ? (free((char *) (obj)), (obj) = 0) : 0)
+#endif
+
+#ifndef REALLOC
+#define REALLOC(type, obj, num)    \
+        ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
+         ((type *) malloc(sizeof(type) * (num))))
+#endif
+
+
+#include "vecInt.h"
+#include "vecFlt.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/temp/aig_free/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/temp/esop/esopMan.c

+/**CFile****************************************************************
+
+  FileName    [esopMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [SOP manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: esopMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "esop.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the minimization manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Esop_Man_t * Esop_ManAlloc( int nVars )
+{
+    Esop_Man_t * pMan;
+    // start the manager
+    pMan = ALLOC( Esop_Man_t, 1 );
+    memset( pMan, 0, sizeof(Esop_Man_t) );
+    pMan->nVars    = nVars;
+    pMan->nWords   = Esop_BitWordNum( nVars * 2 );
+    pMan->pMemMan1 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (1 - 1) );
+    pMan->pMemMan2 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (2 - 1) );
+    pMan->pMemMan4 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (4 - 1) );
+    pMan->pMemMan8 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (8 - 1) );
+    // allocate storage for the temporary cover
+    pMan->ppStore = ALLOC( Esop_Cube_t *, pMan->nVars + 1 );
+    // create tautology cubes
+    Esop_ManClean( pMan, nVars );
+    pMan->pOne0  = Esop_CubeAlloc( pMan );
+    pMan->pOne1  = Esop_CubeAlloc( pMan );
+    pMan->pTemp  = Esop_CubeAlloc( pMan );
+    pMan->pBubble = Esop_CubeAlloc( pMan );  pMan->pBubble->uData[0] = 0;
+    // create trivial cubes
+    Esop_ManClean( pMan, 1 );
+    pMan->pTriv0 = Esop_CubeAllocVar( pMan, 0, 0 );
+    pMan->pTriv1 = Esop_CubeAllocVar( pMan, 0, 0 );
+    Esop_ManClean( pMan, nVars );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the minimization manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Esop_ManClean( Esop_Man_t * p, int nSupp )
+{
+    // set the size of the cube manager
+    p->nVars  = nSupp;
+    p->nWords = Esop_BitWordNum(2*nSupp);
+    // clean the storage
+    memset( p->ppStore, 0, sizeof(Esop_Cube_t *) * (nSupp + 1) );
+    p->nCubes = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the minimization manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Esop_ManFree( Esop_Man_t * p )
+{
+    Mem_FixedStop ( p->pMemMan1, 0 );
+    Mem_FixedStop ( p->pMemMan2, 0 );
+    Mem_FixedStop ( p->pMemMan4, 0 );
+    Mem_FixedStop ( p->pMemMan8, 0 );
+    free( p->ppStore );
+    free( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/temp/esop/esopMin.c

+/**CFile****************************************************************
+
+  FileName    [esopMin.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [ESOP manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: esopMin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "esop.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void Esop_EsopRewrite( Esop_Man_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [ESOP minimization procedure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Esop_EsopMinimize( Esop_Man_t * p )
+{
+    int nCubesInit, nCubesOld, nIter;
+    if ( p->nCubes < 3 )
+        return;
+    nIter = 0;
+    nCubesInit = p->nCubes;
+    do {
+        nCubesOld = p->nCubes;
+        Esop_EsopRewrite( p );
+        nIter++;
+    }
+    while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
+
+//    printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of rewriting using distance 2 cubes.]
+
+  Description [The weakness of this procedure is that it tries each cube
+  with only one distance-2 cube. If this pair does not lead to improvement
+  the cube is inserted into the cover anyhow, and we try another pair.
+  A possible improvement would be to try this cube with all distance-2
+  cubes, until an improvement is found, or until all such cubes are tried.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Esop_EsopRewrite( Esop_Man_t * p )
+{
+    Esop_Cube_t * pCube, ** ppPrev;
+    Esop_Cube_t * pThis, ** ppPrevT;
+    int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld;
+    int nPairs = 0;
+
+    // insert the bubble before the first cube
+    p->pBubble->pNext = p->ppStore[0];
+    p->ppStore[0] = p->pBubble;
+    p->pBubble->nLits = 0;
+
+    // go through the cubes
+    while ( 1 )
+    {
+        // get the index of the bubble
+        Index = p->pBubble->nLits;
+
+        // find the bubble
+        Esop_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev )
+            if ( pCube == p->pBubble )
+                break;
+        assert( pCube == p->pBubble );
+
+        // remove the bubble, get the next cube after the bubble
+        *ppPrev = p->pBubble->pNext;
+        pCube = p->pBubble->pNext;
+        if ( pCube == NULL )
+            for ( Index++; Index <= p->nVars; Index++ )
+                if ( p->ppStore[Index] )
+                {
+                    ppPrev = &(p->ppStore[Index]);
+                    pCube = p->ppStore[Index];
+                    break;
+                }
+        // stop if there is no more cubes
+        if ( pCube == NULL )
+            break;
+
+        // find the first dist2 cube
+        Esop_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT )
+            if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        if ( pThis == NULL && Index < p->nVars )
+        Esop_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT )
+            if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        if ( pThis == NULL && Index < p->nVars - 1 )
+        Esop_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT )
+            if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) )
+                break;
+        // continue if there is no dist2 cube
+        if ( pThis == NULL )
+        {
+            // insert the bubble after the cube
+            p->pBubble->pNext = pCube->pNext;
+            pCube->pNext = p->pBubble;
+            p->pBubble->nLits = pCube->nLits;
+            continue;
+        }
+        nPairs++;
+
+        // remove the cubes, insert the bubble instead of pCube
+        *ppPrevT = pThis->pNext;
+        *ppPrev = p->pBubble;
+        p->pBubble->pNext = pCube->pNext;
+        p->pBubble->nLits = pCube->nLits;
+        p->nCubes -= 2;
+
+        // Exorlink-2:
+        // A{v00}     B{v01}      +  A{v10}     B{v11}     =
+        // A{v00+v10} B{v01}      +  A{v10}     B{v01+v11} =
+        // A{v00}     B{v01+v11}  +  A{v00+v10} B{v11}
+
+        // save the dist2 parameters
+        v00 = Esop_CubeGetVar( pCube, Var0 );
+        v01 = Esop_CubeGetVar( pCube, Var1 );
+        v10 = Esop_CubeGetVar( pThis, Var0 );
+        v11 = Esop_CubeGetVar( pThis, Var1 );
+//printf( "\n" );
+//Esop_CubeWrite( stdout, pCube );
+//Esop_CubeWrite( stdout, pThis );
+
+        // derive the first pair of resulting cubes
+        Esop_CubeXorVar( pCube, Var0, v10 );
+        pCube->nLits -= (v00 != 3);
+        pCube->nLits += ((v00 ^ v10) != 3);
+        Esop_CubeXorVar( pThis, Var1, v01 );
+        pThis->nLits -= (v11 != 3);
+        pThis->nLits += ((v01 ^ v11) != 3);
+
+        // add the cubes
+        nCubesOld = p->nCubes;
+        Esop_EsopAddCube( p, pCube );
+        Esop_EsopAddCube( p, pThis );
+        // check if the cubes were absorbed
+        if ( p->nCubes < nCubesOld + 2 )
+            continue;
+
+        // pull out both cubes
+        assert( pThis == p->ppStore[pThis->nLits] );
+        p->ppStore[pThis->nLits] = pThis->pNext;
+        assert( pCube == p->ppStore[pCube->nLits] );
+        p->ppStore[pCube->nLits] = pCube->pNext;
+        p->nCubes -= 2;
+
+        // derive the second pair of resulting cubes
+        Esop_CubeXorVar( pCube, Var0, v10 );
+        pCube->nLits -= ((v00 ^ v10) != 3);
+        pCube->nLits += (v00 != 3);
+        Esop_CubeXorVar( pCube, Var1, v11 );
+        pCube->nLits -= (v01 != 3);
+        pCube->nLits += ((v01 ^ v11) != 3);
+
+        Esop_CubeXorVar( pThis, Var0, v00 );
+        pThis->nLits -= (v10 != 3);
+        pThis->nLits += ((v00 ^ v10) != 3);
+        Esop_CubeXorVar( pThis, Var1, v01 );
+        pThis->nLits -= ((v01 ^ v11) != 3);
+        pThis->nLits += (v11 != 3);
+
+        // add them anyhow
+        Esop_EsopAddCube( p, pCube );
+        Esop_EsopAddCube( p, pThis );
+    }
+//    printf( "Pairs = %d  ", nPairs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cube to storage.]
+
+  Description [Returns 0 if the cube is added or removed. Returns 1
+  if the cube is glued with some other cube and has to be added again.
+  Do not forget to clean the storage!]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Esop_EsopAddCubeInt( Esop_Man_t * p, Esop_Cube_t * pCube )
+{
+    Esop_Cube_t * pThis, ** ppPrev;
+    // try to find the identical cube
+    Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+    {
+        if ( Esop_CubesAreEqual( pCube, pThis ) )
+        {
+            *ppPrev = pThis->pNext;
+            Esop_CubeRecycle( p, pCube );
+            Esop_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 0;
+        }
+    }
+    // find a distance-1 cube if it exists
+    if ( pCube->nLits < pCube->nVars )
+    Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev )
+    {
+        if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) )
+        {
+            *ppPrev = pThis->pNext;
+            Esop_CubesTransform( pCube, pThis, p->pTemp );
+            pCube->nLits++;
+            Esop_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
+    Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
+    {
+        if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) )
+        {
+            *ppPrev = pThis->pNext;
+            Esop_CubesTransform( pCube, pThis, p->pTemp );
+            pCube->nLits--;
+            Esop_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
+    if ( pCube->nLits > 0 )
+    Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev )
+    {
+        if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) )
+        {
+            *ppPrev = pThis->pNext;
+            Esop_CubesTransform( pCube, pThis, p->pTemp );
+            Esop_CubeRecycle( p, pThis );
+            p->nCubes--;
+            return 1;
+        }
+    }
+    // add the cube
+    pCube->pNext = p->ppStore[pCube->nLits];
+    p->ppStore[pCube->nLits] = pCube;
+    p->nCubes++;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cube to storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Esop_EsopAddCube( Esop_Man_t * p, Esop_Cube_t * pCube )
+{
+    assert( pCube != p->pBubble );
+    assert( (int)pCube->nLits == Esop_CubeCountLits(pCube) );
+    while ( Esop_EsopAddCubeInt( p, pCube ) );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/temp/esop/esopUtil.c

+/**CFile****************************************************************
+
+  FileName    [esopUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cover manipulation package.]
+
+  Synopsis    [Utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: esopUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "esop.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Esop_CubeWrite( FILE * pFile, Esop_Cube_t * pCube )
+{
+    int i;
+    assert( (int)pCube->nLits == Esop_CubeCountLits(pCube) );
+    for ( i = 0; i < (int)pCube->nVars; i++ )
+        if ( Esop_CubeHasBit(pCube, i*2) )
+        {
+            if ( Esop_CubeHasBit(pCube, i*2+1) )
+                fprintf( pFile, "-" );
+            else
+                fprintf( pFile, "0" );
+        }
+        else
+        {
+            if ( Esop_CubeHasBit(pCube, i*2+1) )
+                fprintf( pFile, "1" );
+            else
+                fprintf( pFile, "?" );
+        }
+    fprintf( pFile, " 1\n" );
+//    fprintf( pFile, " %d\n", pCube->nLits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Esop_CoverWrite( FILE * pFile, Esop_Cube_t * pCover )
+{
+    Esop_Cube_t * pCube;
+    Esop_CoverForEachCube( pCover, pCube )
+        Esop_CubeWrite( pFile, pCube );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Esop_CoverWriteStore( FILE * pFile, Esop_Man_t * p )
+{
+    Esop_Cube_t * pCube;
+    int i;
+    for ( i = 0; i <= p->nVars; i++ )
+    {
+        Esop_CoverForEachCube( p->ppStore[i], pCube )
+        {
+            printf( "%2d : ", i );
+            if ( pCube == p->pBubble )
+            {
+                printf( "Bubble\n" );
+                continue;
+            }
+            Esop_CubeWrite( pFile, pCube );
+        }
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Esop_CoverWriteFile( Esop_Cube_t * pCover, char * pName, int fEsop )
+{
+    char Buffer[1000];
+    Esop_Cube_t * pCube;
+    FILE * pFile;
+    int i;
+    sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" );
+    for ( i = strlen(Buffer) - 1; i >= 0; i-- )
+        if ( Buffer[i] == '<' || Buffer[i] == '>' )
+            Buffer[i] = '_';
+    pFile = fopen( Buffer, "w" );
+    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) );
+    if ( fEsop ) fprintf( pFile, ".type esop\n" );
+    Esop_CoverForEachCube( pCover, pCube )
+        Esop_CubeWrite( pFile, pCube );
+    fprintf( pFile, ".e\n" );
+    fclose( pFile );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Esop_CoverCheck( Esop_Man_t * p )
+{
+    Esop_Cube_t * pCube;
+    int i;
+    for ( i = 0; i <= p->nVars; i++ )
+        Esop_CoverForEachCube( p->ppStore[i], pCube )
+            assert( i == (int)pCube->nLits );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Esop_CubeCheck( Esop_Cube_t * pCube )
+{
+    int i;
+    for ( i = 0; i < (int)pCube->nVars; i++ )
+        if ( Esop_CubeGetVar( pCube, i ) == 0 )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the cover from the sorted structure.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Esop_Cube_t * Esop_CoverCollect( Esop_Man_t * p, int nSuppSize )
+{
+    Esop_Cube_t * pCov = NULL, ** ppTail = &pCov;
+    Esop_Cube_t * pCube, * pCube2;
+    int i;
+    for ( i = 0; i <= nSuppSize; i++ )
+    {
+        Esop_CoverForEachCubeSafe( p->ppStore[i], pCube, pCube2 )
+        {
+            assert( i == (int)pCube->nLits );
+            *ppTail = pCube; 
+            ppTail = &pCube->pNext;
+            assert( pCube->uData[0] ); // not a bubble
+        }
+    }
+    *ppTail = NULL;
+    return pCov;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the cover in the increasing number of literals.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Esop_CoverExpand( Esop_Man_t * p, Esop_Cube_t * pCover )
+{
+    Esop_Cube_t * pCube, * pCube2;
+    Esop_ManClean( p, p->nVars );
+    Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 )
+    {
+        pCube->pNext = p->ppStore[pCube->nLits];
+        p->ppStore[pCube->nLits] = pCube;
+        p->nCubes++;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sorts the cover in the increasing number of literals.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Esop_CoverSuppVarNum( Esop_Man_t * p, Esop_Cube_t * pCover )
+{
+    Esop_Cube_t * pCube;
+    int i, Counter;
+    if ( pCover == NULL )
+        return 0;
+    // clean the cube
+    for ( i = 0; i < (int)pCover->nWords; i++ )
+        p->pTemp->uData[i]  = ~((unsigned)0);
+    // add the bit data
+    Esop_CoverForEachCube( pCover, pCube )
+        for ( i = 0; i < (int)pCover->nWords; i++ )
+            p->pTemp->uData[i] &= pCube->uData[i];
+    // count the vars
+    Counter = 0;
+    for ( i = 0; i < (int)pCover->nVars; i++ )
+        Counter += ( Esop_CubeGetVar(p->pTemp, i) != 3 );
+    return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+