Version abc70712

Makefile

@@ -10,7 +10,8 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
 	src/base/io src/base/main src/base/ver \
 	src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \
 	src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
-	src/aig/csw src/aig/ec \
+	src/aig/csw src/aig/ec src/aig/aig src/aig/kit \
+	src/aig/bdc \
 	src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr \
 	src/bdd/parse src/bdd/reo src/bdd/cas \
 	src/map/fpga src/map/mapper src/map/mio \
@@ -19,8 +20,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
 	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/ret src/opt/res src/opt/kit \
-	src/opt/lpk \
+	src/opt/sim src/opt/ret src/opt/res src/opt/lpk \
 	src/sat/bsat src/sat/csat src/sat/msat src/sat/fraig \
 	src/phys/place 	
 

abc.rc

@@ -166,6 +166,8 @@ alias tst6     "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_
 #alias t        "r pj/pj1.blif; st; dfraig -v"
 #alias t        "r c/16/csat_2.bench; st; dfraig -C 100 -v -r"
 #alias t        "r c/16/csat_147.bench; st; dfraig -C 10 -v -r"
-alias t        "r i10.blif; st; ps; csweep; ps; cec"
+#alias t        "r i10.blif; st; ps; csweep; ps; cec"
+#alias t        "r c/5/csat_777.bench; st; csweep -v"
+alias t        "r i10.blif; st; drw -v"
 
 

src/aig/dar/darCheck.c → src/aig/aig/aigCheck.c

 /**CFile****************************************************************
 
-  FileName    [darCheck.c]
+  FileName    [aigCheck.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [DAG-aware AIG rewriting.]
+  PackageName [AIG package.]
 
   Synopsis    [AIG checking procedures.]
 
@@ -14,11 +14,11 @@
 
   Date        [Ver. 1.0. Started - April 28, 2007.]
 
-  Revision    [$Id: darCheck.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+  Revision    [$Id: aigCheck.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
-#include "dar.h"
+#include "aig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -39,77 +39,77 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Dar_ManCheck( Dar_Man_t * p )
+int Aig_ManCheck( Aig_Man_t * p )
 {
-    Dar_Obj_t * pObj, * pObj2;
+    Aig_Obj_t * pObj, * pObj2;
     int i;
     // check primary inputs
-    Dar_ManForEachPi( p, pObj, i )
+    Aig_ManForEachPi( p, pObj, i )
     {
-        if ( Dar_ObjFanin0(pObj) || Dar_ObjFanin1(pObj) )
+        if ( Aig_ObjFanin0(pObj) || Aig_ObjFanin1(pObj) )
         {
-            printf( "Dar_ManCheck: The PI node \"%p\" has fanins.\n", pObj );
+            printf( "Aig_ManCheck: The PI node \"%p\" has fanins.\n", pObj );
             return 0;
         }
     }
     // check primary outputs
-    Dar_ManForEachPo( p, pObj, i )
+    Aig_ManForEachPo( p, pObj, i )
     {
-        if ( !Dar_ObjFanin0(pObj) )
+        if ( !Aig_ObjFanin0(pObj) )
         {
-            printf( "Dar_ManCheck: The PO node \"%p\" has NULL fanin.\n", pObj );
+            printf( "Aig_ManCheck: The PO node \"%p\" has NULL fanin.\n", pObj );
             return 0;
         }
-        if ( Dar_ObjFanin1(pObj) )
+        if ( Aig_ObjFanin1(pObj) )
         {
-            printf( "Dar_ManCheck: The PO node \"%p\" has second fanin.\n", pObj );
+            printf( "Aig_ManCheck: The PO node \"%p\" has second fanin.\n", pObj );
             return 0;
         }
     }
     // check internal nodes
-    Dar_ManForEachObj( p, pObj, i )
+    Aig_ManForEachObj( p, pObj, i )
     {
-        if ( !Dar_ObjIsNode(pObj) )
+        if ( !Aig_ObjIsNode(pObj) )
             continue;
-        if ( !Dar_ObjFanin0(pObj) || !Dar_ObjFanin1(pObj) )
+        if ( !Aig_ObjFanin0(pObj) || !Aig_ObjFanin1(pObj) )
         {
-            printf( "Dar_ManCheck: The AIG has internal node \"%p\" with a NULL fanin.\n", pObj );
+            printf( "Aig_ManCheck: The AIG has internal node \"%p\" with a NULL fanin.\n", pObj );
             return 0;
         }
-        if ( Dar_ObjFanin0(pObj)->Id >= Dar_ObjFanin1(pObj)->Id )
+        if ( Aig_ObjFanin0(pObj)->Id >= Aig_ObjFanin1(pObj)->Id )
         {
-            printf( "Dar_ManCheck: The AIG has node \"%p\" with a wrong ordering of fanins.\n", pObj );
+            printf( "Aig_ManCheck: The AIG has node \"%p\" with a wrong ordering of fanins.\n", pObj );
             return 0;
         }
-        pObj2 = Dar_TableLookup( p, pObj );
+        pObj2 = Aig_TableLookup( p, pObj );
         if ( pObj2 != pObj )
         {
-            printf( "Dar_ManCheck: Node \"%p\" is not in the structural hashing table.\n", pObj );
+            printf( "Aig_ManCheck: Node \"%p\" is not in the structural hashing table.\n", pObj );
             return 0;
         }
     }
     // count the total number of nodes
-    if ( Dar_ManObjNum(p) != 1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManBufNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) )
+    if ( Aig_ManObjNum(p) != 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) )
     {
-        printf( "Dar_ManCheck: The number of created nodes is wrong.\n" );
+        printf( "Aig_ManCheck: The number of created nodes is wrong.\n" );
         printf( "C1 = %d. Pi = %d. Po = %d. Buf = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n",
-            1, Dar_ManPiNum(p), Dar_ManPoNum(p), Dar_ManBufNum(p), Dar_ManAndNum(p), Dar_ManExorNum(p), Dar_ManLatchNum(p), 
-            1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManBufNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) );
+            1, Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManBufNum(p), Aig_ManAndNum(p), Aig_ManExorNum(p), Aig_ManLatchNum(p), 
+            1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) );
         printf( "Created = %d. Deleted = %d. Existing = %d.\n",
             p->nCreated, p->nDeleted, p->nCreated - p->nDeleted );
         return 0;
     }
     // count the number of nodes in the table
-    if ( Dar_TableCountEntries(p) != Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) )
+    if ( Aig_TableCountEntries(p) != Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) )
     {
-        printf( "Dar_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
+        printf( "Aig_ManCheck: The number of nodes in the structural hashing table is wrong.\n" );
         printf( "Entries = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n", 
-            Dar_TableCountEntries(p), Dar_ManAndNum(p), Dar_ManExorNum(p), Dar_ManLatchNum(p),
-            Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) );
+            Aig_TableCountEntries(p), Aig_ManAndNum(p), Aig_ManExorNum(p), Aig_ManLatchNum(p),
+            Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) );
 
         return 0;
     }
-//    if ( !Dar_ManIsAcyclic(p) )
+//    if ( !Aig_ManIsAcyclic(p) )
 //        return 0;
     return 1; 
 }

src/aig/aig/aigMan.c

+/**CFile****************************************************************
+
+  FileName    [aigMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [AIG manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigMan.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the AIG manager.]
+
+  Description [The argument of this procedure is a soft limit on the
+  the number of nodes, or 0 if the limit is unknown.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManStart( int nNodesMax )
+{
+    Aig_Man_t * p;
+    if ( nNodesMax <= 0 )
+        nNodesMax = 10007;
+    // start the manager
+    p = ALLOC( Aig_Man_t, 1 );
+    memset( p, 0, sizeof(Aig_Man_t) );
+    // perform initializations
+    p->nTravIds = 1;
+    p->fCatchExor = 0;
+    // allocate arrays for nodes
+    p->vPis = Vec_PtrAlloc( 100 );
+    p->vPos = Vec_PtrAlloc( 100 );
+    p->vObjs = Vec_PtrAlloc( 1000 );
+    // prepare the internal memory manager
+    p->pMemObjs = Aig_MmFixedStart( sizeof(Aig_Obj_t), nNodesMax );
+    // create the constant node
+    p->pConst1 = Aig_ManFetchMemory( p );
+    p->pConst1->Type = AIG_OBJ_CONST1;
+    p->pConst1->fPhase = 1;
+    p->nObjs[AIG_OBJ_CONST1]++;
+    // start the table
+    p->nTableSize = Aig_PrimeCudd( nNodesMax );
+    p->pTable = ALLOC( Aig_Obj_t *, p->nTableSize );
+    memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
+    // create the PIs
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi(pNew);
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDup( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
+    // create the PIs
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi(pNew);
+    // duplicate internal nodes
+    Aig_ManForEachObj( p, pObj, i )
+        if ( Aig_ObjIsBuf(pObj) )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        else if ( Aig_ObjIsNode(pObj) )
+            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // add the POs
+    Aig_ManForEachPo( p, pObj, i )
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDup(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManStop( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    // print time
+    if ( p->time1 ) { PRT( "time1", p->time1 ); }
+    if ( p->time2 ) { PRT( "time2", p->time2 ); }
+    // make sure the nodes have clean marks
+    Aig_ManForEachObj( p, pObj, i )
+        assert( !pObj->fMarkA && !pObj->fMarkB );
+//    Aig_TableProfile( p );
+    Aig_MmFixedStop( p->pMemObjs, 0 );
+    if ( p->vPis )        Vec_PtrFree( p->vPis );
+    if ( p->vPos )        Vec_PtrFree( p->vPos );
+    if ( p->vObjs )       Vec_PtrFree( p->vObjs );
+    if ( p->vRequired )   Vec_IntFree( p->vRequired );
+    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 * vObjs;
+    Aig_Obj_t * pNode;
+    int i, nNodesOld;
+    nNodesOld = Aig_ManNodeNum(p);
+    // collect roots of dangling nodes
+    vObjs = Vec_PtrAlloc( 100 );
+    Aig_ManForEachObj( p, pNode, i )
+        if ( Aig_ObjIsNode(pNode) && Aig_ObjRefs(pNode) == 0 )
+            Vec_PtrPush( vObjs, pNode );
+    // recursively remove dangling nodes
+    Vec_PtrForEachEntry( vObjs, pNode, i )
+        Aig_ObjDelete_rec( p, pNode, 1 );
+    Vec_PtrFree( vObjs );
+    return nNodesOld - Aig_ManNodeNum(p);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPrintStats( Aig_Man_t * p )
+{
+    printf( "PI/PO/Lat = %5d/%5d/%5d   ", Aig_ManPiNum(p), Aig_ManPoNum(p), Aig_ManLatchNum(p) );
+    printf( "A = %6d. ",    Aig_ManAndNum(p) );
+    if ( Aig_ManExorNum(p) )
+        printf( "X = %5d. ",    Aig_ManExorNum(p) );
+//    if ( Aig_ManBufNum(p) )
+        printf( "B = %3d. ",    Aig_ManBufNum(p) );
+    printf( "Cre = %6d. ",  p->nCreated );
+    printf( "Del = %6d. ",  p->nDeleted );
+//    printf( "Lev = %3d. ",  Aig_ManCountLevels(p) );
+    printf( "\n" );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/dar/darMem.c → src/aig/aig/aigMem.c

 /**CFile****************************************************************
 
-  FileName    [darMem.c]
+  FileName    [aigMem.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [DAG-aware AIG rewriting.]
+  PackageName [AIG package.]
 
   Synopsis    [Memory managers.]
 
@@ -14,21 +14,17 @@
 
   Date        [Ver. 1.0. Started - April 28, 2007.]
 
-  Revision    [$Id: darMem.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+  Revision    [$Id: aigMem.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
-#include <stdio.h>
-#include <stdlib.h>
-#include <string.h>
-#include <assert.h>
-#include "dar.h"
+#include "aig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-struct Dar_MmFixed_t_
+struct Aig_MmFixed_t_
 {
     // information about individual entries
     int           nEntrySize;    // the size of one entry
@@ -48,7 +44,7 @@ struct Dar_MmFixed_t_
     int           nMemoryAlloc;  // memory allocated
 };
 
-struct Dar_MmFlex_t_
+struct Aig_MmFlex_t_
 {
     // information about individual entries
     int           nEntriesUsed;  // the number of entries allocated
@@ -66,12 +62,12 @@ struct Dar_MmFlex_t_
     int           nMemoryAlloc;  // memory allocated
 };
 
-struct Dar_MmStep_t_
+struct Aig_MmStep_t_
 {
     int             nMems;    // the number of fixed memory managers employed
-    Dar_MmFixed_t **  pMems;    // memory managers: 2^1 words, 2^2 words, etc
+    Aig_MmFixed_t **  pMems;    // memory managers: 2^1 words, 2^2 words, etc
     int             nMapSize; // the size of the memory array
-    Dar_MmFixed_t **  pMap;     // maps the number of bytes into its memory manager
+    Aig_MmFixed_t **  pMap;     // maps the number of bytes into its memory manager
 };
 
 #define ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
@@ -96,12 +92,12 @@ struct Dar_MmStep_t_
   SeeAlso     []
 
 ***********************************************************************/
-Dar_MmFixed_t * Dar_MmFixedStart( int nEntrySize, int nEntriesMax )
+Aig_MmFixed_t * Aig_MmFixedStart( int nEntrySize, int nEntriesMax )
 {
-    Dar_MmFixed_t * p;
+    Aig_MmFixed_t * p;
 
-    p = ALLOC( Dar_MmFixed_t, 1 );
-    memset( p, 0, sizeof(Dar_MmFixed_t) );
+    p = ALLOC( Aig_MmFixed_t, 1 );
+    memset( p, 0, sizeof(Aig_MmFixed_t) );
 
     p->nEntrySize    = nEntrySize;
     p->nEntriesAlloc = 0;
@@ -132,7 +128,7 @@ Dar_MmFixed_t * Dar_MmFixedStart( int nEntrySize, int nEntriesMax )
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_MmFixedStop( Dar_MmFixed_t * p, int fVerbose )
+void Aig_MmFixedStop( Aig_MmFixed_t * p, int fVerbose )
 {
     int i;
     if ( p == NULL )
@@ -161,7 +157,7 @@ void Dar_MmFixedStop( Dar_MmFixed_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-char * Dar_MmFixedEntryFetch( Dar_MmFixed_t * p )
+char * Aig_MmFixedEntryFetch( Aig_MmFixed_t * p )
 {
     char * pTemp;
     int i;
@@ -212,7 +208,7 @@ char * Dar_MmFixedEntryFetch( Dar_MmFixed_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_MmFixedEntryRecycle( Dar_MmFixed_t * p, char * pEntry )
+void Aig_MmFixedEntryRecycle( Aig_MmFixed_t * p, char * pEntry )
 {
     // decrement the counter of used entries
     p->nEntriesUsed--;
@@ -232,7 +228,7 @@ void Dar_MmFixedEntryRecycle( Dar_MmFixed_t * p, char * pEntry )
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_MmFixedRestart( Dar_MmFixed_t * p )
+void Aig_MmFixedRestart( Aig_MmFixed_t * p )
 {
     int i;
     char * pTemp;
@@ -270,7 +266,7 @@ void Dar_MmFixedRestart( Dar_MmFixed_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Dar_MmFixedReadMemUsage( Dar_MmFixed_t * p )
+int Aig_MmFixedReadMemUsage( Aig_MmFixed_t * p )
 {
     return p->nMemoryAlloc;
 }
@@ -286,7 +282,7 @@ int Dar_MmFixedReadMemUsage( Dar_MmFixed_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Dar_MmFixedReadMaxEntriesUsed( Dar_MmFixed_t * p )
+int Aig_MmFixedReadMaxEntriesUsed( Aig_MmFixed_t * p )
 {
     return p->nEntriesMax;
 }
@@ -304,12 +300,12 @@ int Dar_MmFixedReadMaxEntriesUsed( Dar_MmFixed_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Dar_MmFlex_t * Dar_MmFlexStart()
+Aig_MmFlex_t * Aig_MmFlexStart()
 {
-    Dar_MmFlex_t * p;
+    Aig_MmFlex_t * p;
 
-    p = ALLOC( Dar_MmFlex_t, 1 );
-    memset( p, 0, sizeof(Dar_MmFlex_t) );
+    p = ALLOC( Aig_MmFlex_t, 1 );
+    memset( p, 0, sizeof(Aig_MmFlex_t) );
 
     p->nEntriesUsed  = 0;
     p->pCurrent      = NULL;
@@ -336,7 +332,7 @@ Dar_MmFlex_t * Dar_MmFlexStart()
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_MmFlexStop( Dar_MmFlex_t * p, int fVerbose )
+void Aig_MmFlexStop( Aig_MmFlex_t * p, int fVerbose )
 {
     int i;
     if ( p == NULL )
@@ -365,7 +361,7 @@ void Dar_MmFlexStop( Dar_MmFlex_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-char * Dar_MmFlexEntryFetch( Dar_MmFlex_t * p, int nBytes )
+char * Aig_MmFlexEntryFetch( Aig_MmFlex_t * p, int nBytes )
 {
     char * pTemp;
     // check if there are still free entries
@@ -410,7 +406,7 @@ char * Dar_MmFlexEntryFetch( Dar_MmFlex_t * p, int nBytes )
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_MmFlexRestart( Dar_MmFlex_t * p )
+void Aig_MmFlexRestart( Aig_MmFlex_t * p )
 {
     int i;
     if ( p->nChunks == 0 )
@@ -438,7 +434,7 @@ void Dar_MmFlexRestart( Dar_MmFlex_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Dar_MmFlexReadMemUsage( Dar_MmFlex_t * p )
+int Aig_MmFlexReadMemUsage( Aig_MmFlex_t * p )
 {
     return p->nMemoryUsed;
 }
@@ -467,20 +463,20 @@ int Dar_MmFlexReadMemUsage( Dar_MmFlex_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Dar_MmStep_t * Dar_MmStepStart( int nSteps )
+Aig_MmStep_t * Aig_MmStepStart( int nSteps )
 {
-    Dar_MmStep_t * p;
+    Aig_MmStep_t * p;
     int i, k;
-    p = ALLOC( Dar_MmStep_t, 1 );
-    memset( p, 0, sizeof(Dar_MmStep_t) );
+    p = ALLOC( Aig_MmStep_t, 1 );
+    memset( p, 0, sizeof(Aig_MmStep_t) );
     p->nMems = nSteps;
     // start the fixed memory managers
-    p->pMems = ALLOC( Dar_MmFixed_t *, p->nMems );
+    p->pMems = ALLOC( Aig_MmFixed_t *, p->nMems );
     for ( i = 0; i < p->nMems; i++ )
-        p->pMems[i] = Dar_MmFixedStart( (8<<i), (1<<13) );
+        p->pMems[i] = Aig_MmFixedStart( (8<<i), (1<<13) );
     // set up the mapping of the required memory size into the corresponding manager
     p->nMapSize = (4<<p->nMems);
-    p->pMap = ALLOC( Dar_MmFixed_t *, p->nMapSize+1 );
+    p->pMap = ALLOC( Aig_MmFixed_t *, p->nMapSize+1 );
     p->pMap[0] = NULL;
     for ( k = 1; k <= 4; k++ )
         p->pMap[k] = p->pMems[0];
@@ -503,11 +499,11 @@ Dar_MmStep_t * Dar_MmStepStart( int nSteps )
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_MmStepStop( Dar_MmStep_t * p, int fVerbose )
+void Aig_MmStepStop( Aig_MmStep_t * p, int fVerbose )
 {
     int i;
     for ( i = 0; i < p->nMems; i++ )
-        Dar_MmFixedStop( p->pMems[i], fVerbose );
+        Aig_MmFixedStop( p->pMems[i], fVerbose );
 //    if ( p->pLargeChunks ) 
 //    {
 //      for ( i = 0; i < p->nLargeChunks; i++ )
@@ -530,7 +526,7 @@ void Dar_MmStepStop( Dar_MmStep_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-char * Dar_MmStepEntryFetch( Dar_MmStep_t * p, int nBytes )
+char * Aig_MmStepEntryFetch( Aig_MmStep_t * p, int nBytes )
 {
     if ( nBytes == 0 )
         return NULL;
@@ -550,7 +546,7 @@ char * Dar_MmStepEntryFetch( Dar_MmStep_t * p, int nBytes )
 */
         return ALLOC( char, nBytes );
     }
-    return Dar_MmFixedEntryFetch( p->pMap[nBytes] );
+    return Aig_MmFixedEntryFetch( p->pMap[nBytes] );
 }
 
 
@@ -565,7 +561,7 @@ char * Dar_MmStepEntryFetch( Dar_MmStep_t * p, int nBytes )
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_MmStepEntryRecycle( Dar_MmStep_t * p, char * pEntry, int nBytes )
+void Aig_MmStepEntryRecycle( Aig_MmStep_t * p, char * pEntry, int nBytes )
 {
     if ( nBytes == 0 )
         return;
@@ -574,7 +570,7 @@ void Dar_MmStepEntryRecycle( Dar_MmStep_t * p, char * pEntry, int nBytes )
         free( pEntry );
         return;
     }
-    Dar_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
+    Aig_MmFixedEntryRecycle( p->pMap[nBytes], pEntry );
 }
 
 /**Function*************************************************************
@@ -588,7 +584,7 @@ void Dar_MmStepEntryRecycle( Dar_MmStep_t * p, char * pEntry, int nBytes )
   SeeAlso     []
 
 ***********************************************************************/
-int Dar_MmStepReadMemUsage( Dar_MmStep_t * p )
+int Aig_MmStepReadMemUsage( Aig_MmStep_t * p )
 {
     int i, nMemTotal = 0;
     for ( i = 0; i < p->nMems; i++ )

src/aig/dar/darTable.c → src/aig/aig/aigTable.c

 /**CFile****************************************************************
 
-  FileName    [darTable.c]
+  FileName    [aigTable.c]
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [DAG-aware AIG rewriting.]
+  PackageName [AIG package.]
 
   Synopsis    [Structural hashing table.]
 
@@ -14,48 +14,48 @@
 
   Date        [Ver. 1.0. Started - April 28, 2007.]
 
-  Revision    [$Id: darTable.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+  Revision    [$Id: aigTable.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
 
-#include "dar.h"
+#include "aig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
 // hashing the node
-static unsigned long Dar_Hash( Dar_Obj_t * pObj, int TableSize ) 
+static unsigned long Aig_Hash( Aig_Obj_t * pObj, int TableSize ) 
 {
-    unsigned long Key = Dar_ObjIsExor(pObj) * 1699;
-    Key ^= (long)Dar_ObjFanin0(pObj) * 7937;
-    Key ^= (long)Dar_ObjFanin1(pObj) * 2971;
-    Key ^= Dar_ObjFaninC0(pObj) * 911;
-    Key ^= Dar_ObjFaninC1(pObj) * 353;
+    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 Dar_Obj_t ** Dar_TableFind( Dar_Man_t * p, Dar_Obj_t * pObj )
+static Aig_Obj_t ** Aig_TableFind( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
-    Dar_Obj_t ** ppEntry;
-    if ( Dar_ObjIsLatch(pObj) )
+    Aig_Obj_t ** ppEntry;
+    if ( Aig_ObjIsLatch(pObj) )
     {
-        assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) == NULL );
+        assert( Aig_ObjChild0(pObj) && Aig_ObjChild1(pObj) == NULL );
     }
     else
     {
-        assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) );
-        assert( Dar_ObjFanin0(pObj)->Id < Dar_ObjFanin1(pObj)->Id );
+        assert( Aig_ObjChild0(pObj) && Aig_ObjChild1(pObj) );
+        assert( Aig_ObjFanin0(pObj)->Id < Aig_ObjFanin1(pObj)->Id );
     }
-    for ( ppEntry = p->pTable + Dar_Hash(pObj, p->nTableSize); *ppEntry; ppEntry = &(*ppEntry)->pNext )
+    for ( ppEntry = p->pTable + Aig_Hash(pObj, p->nTableSize); *ppEntry; ppEntry = &(*ppEntry)->pNext )
         if ( *ppEntry == pObj )
             return ppEntry;
     assert( *ppEntry == NULL );
     return ppEntry;
 }
 
-static void         Dar_TableResize( Dar_Man_t * p );
+static void         Aig_TableResize( Aig_Man_t * p );
 static unsigned int Cudd_PrimeAig( unsigned int  p );
 
 ////////////////////////////////////////////////////////////////////////
@@ -73,29 +73,29 @@ static unsigned int Cudd_PrimeAig( unsigned int  p );
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Obj_t * Dar_TableLookup( Dar_Man_t * p, Dar_Obj_t * pGhost )
+Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost )
 {
-    Dar_Obj_t * pEntry;
-    assert( !Dar_IsComplement(pGhost) );
-    if ( pGhost->Type == DAR_AIG_LATCH )
+    Aig_Obj_t * pEntry;
+    assert( !Aig_IsComplement(pGhost) );
+    if ( pGhost->Type == AIG_OBJ_LATCH )
     {
-        assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) == NULL );
-        if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) )
+        assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) == NULL );
+        if ( !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) )
             return NULL;
     }
     else
     {
-        assert( pGhost->Type == DAR_AIG_AND );
-        assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) );
-        assert( Dar_ObjFanin0(pGhost)->Id < Dar_ObjFanin1(pGhost)->Id );
-        if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) || !Dar_ObjRefs(Dar_ObjFanin1(pGhost)) )
+        assert( pGhost->Type == AIG_OBJ_AND );
+        assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) );
+        assert( Aig_ObjFanin0(pGhost)->Id < Aig_ObjFanin1(pGhost)->Id );
+        if ( !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) || !Aig_ObjRefs(Aig_ObjFanin1(pGhost)) )
             return NULL;
     }
-    for ( pEntry = p->pTable[Dar_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext )
+    for ( pEntry = p->pTable[Aig_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext )
     {
-        if ( Dar_ObjChild0(pEntry) == Dar_ObjChild0(pGhost) && 
-             Dar_ObjChild1(pEntry) == Dar_ObjChild1(pGhost) && 
-             Dar_ObjType(pEntry) == Dar_ObjType(pGhost) )
+        if ( Aig_ObjChild0(pEntry) == Aig_ObjChild0(pGhost) && 
+             Aig_ObjChild1(pEntry) == Aig_ObjChild1(pGhost) && 
+             Aig_ObjType(pEntry) == Aig_ObjType(pGhost) )
             return pEntry;
     }
     return NULL;
@@ -112,14 +112,14 @@ Dar_Obj_t * Dar_TableLookup( Dar_Man_t * p, Dar_Obj_t * pGhost )
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_TableInsert( Dar_Man_t * p, Dar_Obj_t * pObj )
+void Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
-    Dar_Obj_t ** ppPlace;
-    assert( !Dar_IsComplement(pObj) );
-    assert( Dar_TableLookup(p, pObj) == NULL );
-    if ( (pObj->Id & 0xFF) == 0 && 2 * p->nTableSize < Dar_ManNodeNum(p) )
-        Dar_TableResize( p );
-    ppPlace = Dar_TableFind( p, pObj );
+    Aig_Obj_t ** ppPlace;
+    assert( !Aig_IsComplement(pObj) );
+    assert( Aig_TableLookup(p, pObj) == NULL );
+    if ( (pObj->Id & 0xFF) == 0 && 2 * p->nTableSize < Aig_ManNodeNum(p) )
+        Aig_TableResize( p );
+    ppPlace = Aig_TableFind( p, pObj );
     assert( *ppPlace == NULL );
     *ppPlace = pObj;
 }
@@ -135,11 +135,11 @@ void Dar_TableInsert( Dar_Man_t * p, Dar_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_TableDelete( Dar_Man_t * p, Dar_Obj_t * pObj )
+void Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
-    Dar_Obj_t ** ppPlace;
-    assert( !Dar_IsComplement(pObj) );
-    ppPlace = Dar_TableFind( p, pObj );
+    Aig_Obj_t ** ppPlace;
+    assert( !Aig_IsComplement(pObj) );
+    ppPlace = Aig_TableFind( p, pObj );
     assert( *ppPlace == pObj ); // node should be in the table
     // remove the node
     *ppPlace = pObj->pNext;
@@ -157,9 +157,9 @@ void Dar_TableDelete( Dar_Man_t * p, Dar_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Dar_TableCountEntries( Dar_Man_t * p )
+int Aig_TableCountEntries( Aig_Man_t * p )
 {
-    Dar_Obj_t * pEntry;
+    Aig_Obj_t * pEntry;
     int i, Counter = 0;
     for ( i = 0; i < p->nTableSize; i++ )
         for ( pEntry = p->pTable[i]; pEntry; pEntry = pEntry->pNext )
@@ -178,33 +178,33 @@ int Dar_TableCountEntries( Dar_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_TableResize( Dar_Man_t * p )
+void Aig_TableResize( Aig_Man_t * p )
 {
-    Dar_Obj_t * pEntry, * pNext;
-    Dar_Obj_t ** pTableOld, ** ppPlace;
+    Aig_Obj_t * pEntry, * pNext;
+    Aig_Obj_t ** pTableOld, ** ppPlace;
     int nTableSizeOld, Counter, nEntries, i, clk;
 clk = clock();
     // save the old table
     pTableOld = p->pTable;
     nTableSizeOld = p->nTableSize;
     // get the new table
-    p->nTableSize = Cudd_PrimeAig( 2 * Dar_ManNodeNum(p) ); 
-    p->pTable = ALLOC( Dar_Obj_t *, p->nTableSize );
-    memset( p->pTable, 0, sizeof(Dar_Obj_t *) * p->nTableSize );
+    p->nTableSize = Cudd_PrimeAig( 2 * 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 ( i = 0; i < nTableSizeOld; i++ )
     for ( pEntry = pTableOld[i], pNext = pEntry? pEntry->pNext : NULL; pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL )
     {
         // get the place where this entry goes in the table 
-        ppPlace = Dar_TableFind( p, pEntry );
+        ppPlace = Aig_TableFind( p, pEntry );
         assert( *ppPlace == NULL ); // should not be there
         // add the entry to the list
         *ppPlace = pEntry;
         pEntry->pNext = NULL;
         Counter++;
     }
-    nEntries = Dar_ManNodeNum(p);
+    nEntries = Aig_ManNodeNum(p);
     assert( Counter == nEntries );
     printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
     PRT( "Time", clock() - clk );
@@ -223,9 +223,9 @@ clk = clock();
   SeeAlso     []
 
 ******************************************************************************/
-void Dar_TableProfile( Dar_Man_t * p )
+void Aig_TableProfile( Aig_Man_t * p )
 {
-    Dar_Obj_t * pEntry;
+    Aig_Obj_t * pEntry;
     int i, Counter;
     for ( i = 0; i < p->nTableSize; i++ )
     {

src/aig/aig/aig_.c

+/**CFile****************************************************************
+
+  FileName    [aig_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aig_.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/aig/module.make

+SRC +=    src/aig/aig/aigCheck.c \
+    src/aig/aig/aigDfs.c \
+    src/aig/aig/aigMan.c \
+    src/aig/aig/aigMem.c \
+    src/aig/aig/aigObj.c \
+    src/aig/aig/aigOper.c \
+    src/aig/aig/aigSeq.c \
+    src/aig/aig/aigTable.c \
+    src/aig/aig/aigUtil.c 

src/aig/bdc/module.make

+SRC +=  src/aig/bdc/bdcCore.c \
+    src/aig/bdc/bdcDec.c \
+    src/aig/bdc/bdcTable.c
+

src/aig/cnf/cnf.h

@@ -36,7 +36,8 @@ extern "C" {
 #include <time.h>
 
 #include "vec.h"
-#include "dar.h"
+#include "aig.h"
+#include "darInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -53,7 +54,7 @@ typedef struct Cnf_Cut_t_            Cnf_Cut_t;
 // the CNF asserting outputs of AIG to be 1
 struct Cnf_Dat_t_
 {
-    Dar_Man_t *     pMan;            // the AIG manager, for which CNF is computed
+    Aig_Man_t *     pMan;            // the AIG manager, for which CNF is computed
     int             nVars;           // the number of variables
     int             nLiterals;       // the number of CNF literals
     int             nClauses;        // the number of CNF clauses
@@ -74,11 +75,11 @@ struct Cnf_Cut_t_
 // the CNF computation manager
 struct Cnf_Man_t_
 {
-    Dar_Man_t *     pManAig;         // the underlying AIG manager
+    Aig_Man_t *     pManAig;         // the underlying AIG manager
     char *          pSopSizes;       // sizes of SOPs for 4-variable functions
     char **         pSops;           // the SOPs for 4-variable functions
     int             aArea;           // the area of the mapping
-    Dar_MmFlex_t *  pMemCuts;        // memory manager for cuts
+    Aig_MmFlex_t *  pMemCuts;        // memory manager for cuts
     int             nMergeLimit;     // the limit on the size of merged cut
     unsigned *      pTruths[4];      // temporary truth tables
     Vec_Int_t *     vMemory;         // memory for intermediate ISOP representation
@@ -88,8 +89,8 @@ static inline int          Cnf_CutLeaveNum( Cnf_Cut_t * pCut )    { return pCut-
 static inline int *        Cnf_CutLeaves( Cnf_Cut_t * pCut )      { return pCut->pFanins;                               }
 static inline unsigned *   Cnf_CutTruth( Cnf_Cut_t * pCut )       { return (unsigned *)(pCut->pFanins + pCut->nFanins); }
 
-static inline Cnf_Cut_t *  Cnf_ObjBestCut( Dar_Obj_t * pObj )                       { return pObj->pData;  }
-static inline void         Cnf_ObjSetBestCut( Dar_Obj_t * pObj, Cnf_Cut_t * pCut )  { pObj->pData = pCut;  }
+static inline Cnf_Cut_t *  Cnf_ObjBestCut( Aig_Obj_t * pObj )                       { return pObj->pData;  }
+static inline void         Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut )  { pObj->pData = pCut;  }
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
@@ -101,16 +102,16 @@ static inline void         Cnf_ObjSetBestCut( Dar_Obj_t * pObj, Cnf_Cut_t * pCut
 
 // iterator over leaves of the cut
 #define Cnf_CutForEachLeaf( p, pCut, pLeaf, i )                         \
-    for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Dar_ManObj(p, (pCut)->pFanins[i])); i++ )
+    for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== cnfCore.c ========================================================*/
-extern Cnf_Dat_t *     Cnf_Derive( Cnf_Man_t * p, Dar_Man_t * pAig );
+extern Cnf_Dat_t *     Cnf_Derive( Cnf_Man_t * p, Aig_Man_t * pAig );
 /*=== cnfCut.c ========================================================*/
-extern Cnf_Cut_t *     Cnf_CutCreate( Cnf_Man_t * p, Dar_Obj_t * pObj );
+extern Cnf_Cut_t *     Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj );
 extern void            Cnf_CutPrint( Cnf_Cut_t * pCut );
 extern void            Cnf_CutFree( Cnf_Cut_t * pCut );
 extern void            Cnf_CutUpdateRefs( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, Cnf_Cut_t * pCutRes );
@@ -130,7 +131,7 @@ extern void            Cnf_ManTransferCuts( Cnf_Man_t * p );
 extern void            Cnf_ManFreeCuts( Cnf_Man_t * p );
 extern void            Cnf_ManPostprocess( Cnf_Man_t * p );
 /*=== cnfUtil.c ========================================================*/
-extern Vec_Ptr_t *     Dar_ManScanMapping( Cnf_Man_t * p, int fCollect );
+extern Vec_Ptr_t *     Aig_ManScanMapping( Cnf_Man_t * p, int fCollect );
 extern Vec_Ptr_t *     Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect );
 /*=== cnfWrite.c ========================================================*/
 extern void            Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );

src/aig/cnf/cnfCore.c

@@ -39,20 +39,20 @@
   SeeAlso     []
 
 ***********************************************************************/
-Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Dar_Man_t * pAig )
+Cnf_Dat_t * Cnf_Derive( Cnf_Man_t * p, Aig_Man_t * pAig )
 {
+    Aig_MmFixed_t * pMemCuts;
     Cnf_Dat_t * pCnf = NULL;
     Vec_Ptr_t * vMapped;
     int nIters = 2;
     int clk;
 
     // connect the managers
-    pAig->pManCnf = p;
     p->pManAig = pAig;
 
     // generate cuts for all nodes, assign cost, and find best cuts
 clk = clock();
-    Dar_ManComputeCuts( pAig );
+    pMemCuts = Dar_ManComputeCuts( pAig );
 PRT( "Cuts", clock() - clk );
 /*
     // iteratively improve area flow
@@ -65,7 +65,7 @@ PRT( "iter ", clock() - clk );
     }
 */
     // write the file
-    vMapped = Dar_ManScanMapping( p, 1 );
+    vMapped = Aig_ManScanMapping( p, 1 );
     Vec_PtrFree( vMapped );
 
 clk = clock();
@@ -91,6 +91,7 @@ PRT( "Ext ", clock() - clk );
     Dar_ManCutsFree( pAig );
     return pCnf;
 */
+    Aig_MmFixedStop( pMemCuts, 0 );
     return NULL;
 }
 

src/aig/cnf/cnfCut.c

@@ -43,10 +43,10 @@
 Cnf_Cut_t * Cnf_CutAlloc( Cnf_Man_t * p, int nLeaves )
 {
     Cnf_Cut_t * pCut;
-    int nSize = sizeof(Cnf_Cut_t) + sizeof(int) * nLeaves + sizeof(unsigned) * Dar_TruthWordNum(nLeaves);
-    pCut = (Cnf_Cut_t *)Dar_MmFlexEntryFetch( p->pMemCuts, nSize );
+    int nSize = sizeof(Cnf_Cut_t) + sizeof(int) * nLeaves + sizeof(unsigned) * Aig_TruthWordNum(nLeaves);
+    pCut = (Cnf_Cut_t *)Aig_MmFlexEntryFetch( p->pMemCuts, nSize );
     pCut->nFanins = nLeaves;
-    pCut->nWords = Dar_TruthWordNum(nLeaves);
+    pCut->nWords = Aig_TruthWordNum(nLeaves);
     pCut->vIsop[0] = pCut->vIsop[1] = NULL;
     return pCut;
 }
@@ -81,13 +81,14 @@ void Cnf_CutFree( Cnf_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Dar_Obj_t * pObj )
+Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj )
 {
     Dar_Cut_t * pCutBest;
     Cnf_Cut_t * pCut;
     unsigned * pTruth;
-    assert( Dar_ObjIsNode(pObj) );
-    pCutBest = Dar_ObjBestCut( pObj );
+    assert( Aig_ObjIsNode(pObj) );
+//    pCutBest = Aig_ObjBestCut( pObj );
+        pCutBest = NULL;
     assert( pCutBest != NULL );
     assert( pCutBest->nLeaves <= 4 );
     pCut = Cnf_CutAlloc( p, pCutBest->nLeaves );
@@ -131,7 +132,7 @@ void Cnf_CutPrint( Cnf_Cut_t * pCut )
 ***********************************************************************/
 void Cnf_CutDeref( Cnf_Man_t * p, Cnf_Cut_t * pCut )
 {
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i;
     Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
     {
@@ -153,7 +154,7 @@ void Cnf_CutDeref( Cnf_Man_t * p, Cnf_Cut_t * pCut )
 ***********************************************************************/
 void Cnf_CutRef( Cnf_Man_t * p, Cnf_Cut_t * pCut )
 {
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i;
     Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i )
     {

src/aig/cnf/cnfData.c

@@ -4614,7 +4614,7 @@ void Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops )
   SeeAlso     []
 
 ***********************************************************************/
-int Dar_ManDeriveCnfTest()
+int Aig_ManDeriveCnfTest()
 {
     int i, k, Lit;
     printf( "\n" );
@@ -4644,7 +4644,7 @@ int Dar_ManDeriveCnfTest()
   SeeAlso     []
 
 ***********************************************************************/
-int Dar_ManDeriveCnfTest2()
+int Aig_ManDeriveCnfTest2()
 {
     char s_Data3[81] = "!#&()*+,-.0123456789:;<=>?ABCDEFGHIJKLMNOPQRSTUVWXYZ[]abcdefghijklmnopqrstuvwxyz|";
 

src/aig/cnf/cnfMan.c

@@ -52,12 +52,12 @@ Cnf_Man_t * Cnf_ManStart()
     // derive internal data structures
     Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
     // allocate memory manager for cuts
-    p->pMemCuts = Dar_MmFlexStart();
+    p->pMemCuts = Aig_MmFlexStart();
     p->nMergeLimit = 10;
     // allocate temporary truth tables
-    p->pTruths[0] = ALLOC( unsigned, 4 * Dar_TruthWordNum(p->nMergeLimit) );
+    p->pTruths[0] = ALLOC( unsigned, 4 * Aig_TruthWordNum(p->nMergeLimit) );
     for ( i = 1; i < 4; i++ )
-        p->pTruths[i] = p->pTruths[i-1] + Dar_TruthWordNum(p->nMergeLimit);
+        p->pTruths[i] = p->pTruths[i-1] + Aig_TruthWordNum(p->nMergeLimit);
     p->vMemory = Vec_IntAlloc( 1 << 18 );
     return p;
 }
@@ -77,7 +77,7 @@ void Cnf_ManStop( Cnf_Man_t * p )
 {
     Vec_IntFree( p->vMemory );
     free( p->pTruths[0] );
-    Dar_MmFlexStop( p->pMemCuts, 0 );
+    Aig_MmFlexStop( p->pMemCuts, 0 );
     free( p->pSopSizes );
     free( p->pSops[1] );
     free( p->pSops );

src/aig/cnf/cnfMap.c

@@ -28,6 +28,8 @@
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#if 0
+
 /**Function*************************************************************
 
   Synopsis    [Computes area of the first level.]
@@ -39,16 +41,16 @@
   SeeAlso     []
  
 ***********************************************************************/
-void Dar_CutDeref( Dar_Man_t * p, Dar_Cut_t * pCut )
+void Aig_CutDeref( Aig_Man_t * p, Dar_Cut_t * pCut )
 { 
-    Dar_Obj_t * pLeaf;
+    Aig_Obj_t * pLeaf;
     int i;
     Dar_CutForEachLeaf( p, pCut, pLeaf, i )
     {
         assert( pLeaf->nRefs > 0 );
-        if ( --pLeaf->nRefs > 0 || !Dar_ObjIsAnd(pLeaf) )
+        if ( --pLeaf->nRefs > 0 || !Aig_ObjIsAnd(pLeaf) )
             continue;
-        Dar_CutDeref( p, Dar_ObjBestCut(pLeaf) );
+        Aig_CutDeref( p, Aig_ObjBestCut(pLeaf) );
     }
 }
 
@@ -63,16 +65,16 @@ void Dar_CutDeref( Dar_Man_t * p, Dar_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-int Dar_CutRef( Dar_Man_t * p, Dar_Cut_t * pCut )
+int Aig_CutRef( Aig_Man_t * p, Dar_Cut_t * pCut )
 {
-    Dar_Obj_t * pLeaf;
-    int i, Area = pCut->Cost;
+    Aig_Obj_t * pLeaf;
+    int i, Area = pCut->Value;
     Dar_CutForEachLeaf( p, pCut, pLeaf, i )
     {
         assert( pLeaf->nRefs >= 0 );
-        if ( pLeaf->nRefs++ > 0 || !Dar_ObjIsAnd(pLeaf) )
+        if ( pLeaf->nRefs++ > 0 || !Aig_ObjIsAnd(pLeaf) )
             continue;
-        Area += Dar_CutRef( p, Dar_ObjBestCut(pLeaf) );
+        Area += Aig_CutRef( p, Aig_ObjBestCut(pLeaf) );
     }
     return Area;
 }
@@ -88,11 +90,11 @@ int Dar_CutRef( Dar_Man_t * p, Dar_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-int Cnf_CutArea( Dar_Man_t * p, Dar_Cut_t * pCut )
+int Cnf_CutArea( Aig_Man_t * p, Dar_Cut_t * pCut )
 {
     int Area;
-    Area = Dar_CutRef( p, pCut );
-    Dar_CutDeref( p, pCut );
+    Area = Aig_CutRef( p, pCut );
+    Aig_CutDeref( p, pCut );
     return Area;
 }
 
@@ -136,7 +138,7 @@ static inline int Cnf_CutCompare( Dar_Cut_t * pC0, Dar_Cut_t * pC1 )
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Cut_t * Cnf_ObjFindBestCut( Dar_Obj_t * pObj )
+Dar_Cut_t * Cnf_ObjFindBestCut( Aig_Obj_t * pObj )
 {
     Dar_Cut_t * pCut, * pCutBest;
     int i;
@@ -160,7 +162,7 @@ Dar_Cut_t * Cnf_ObjFindBestCut( Dar_Obj_t * pObj )
 ***********************************************************************/
 void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut )
 {
-    Dar_Obj_t * pLeaf;
+    Aig_Obj_t * pLeaf;
     int i;
     pCut->Cost    = p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth];
     pCut->Area    = (float)pCut->Cost;
@@ -168,16 +170,16 @@ void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut )
     pCut->FanRefs = 0;
     Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i )
     {
-        if ( !Dar_ObjIsNode(pLeaf) )
+        if ( !Aig_ObjIsNode(pLeaf) )
             continue;
         if ( pLeaf->nRefs == 0 )
         {
-            pCut->Area += Dar_ObjBestCut(pLeaf)->Area;
+            pCut->Area += Aig_ObjBestCut(pLeaf)->Area;
             pCut->NoRefs++;
         }
         else
         {
-            pCut->Area += Dar_ObjBestCut(pLeaf)->Area / pLeaf->nRefs;
+            pCut->Area += Aig_ObjBestCut(pLeaf)->Area / pLeaf->nRefs;
             if ( pCut->FanRefs + pLeaf->nRefs > 15 )
                 pCut->FanRefs = 15;
             else
@@ -199,18 +201,18 @@ void Cnf_CutAssignAreaFlow( Cnf_Man_t * p, Dar_Cut_t * pCut )
 ***********************************************************************/
 void Cnf_CutAssignArea( Cnf_Man_t * p, Dar_Cut_t * pCut )
 {
-    Dar_Obj_t * pLeaf;
+    Aig_Obj_t * pLeaf;
     int i;
     pCut->Area    = (float)pCut->Cost;
     pCut->NoRefs  = 0;
     pCut->FanRefs = 0;
     Dar_CutForEachLeaf( p->pManAig, pCut, pLeaf, i )
     {
-        if ( !Dar_ObjIsNode(pLeaf) )
+        if ( !Aig_ObjIsNode(pLeaf) )
             continue;
         if ( pLeaf->nRefs == 0 )
         {
-            pCut->Area += Dar_ObjBestCut(pLeaf)->Cost;
+            pCut->Area += Aig_ObjBestCut(pLeaf)->Cost;
             pCut->NoRefs++;
         }
         else
@@ -236,18 +238,18 @@ void Cnf_CutAssignArea( Cnf_Man_t * p, Dar_Cut_t * pCut )
 ***********************************************************************/
 int Cnf_ManMapForCnf( Cnf_Man_t * p )
 {
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     Dar_Cut_t * pCut, * pCutBest;
     int i, k;
     // visit the nodes in the topological order and update their best cuts
-    Dar_ManForEachNode( p->pManAig, pObj, i )
+    Aig_ManForEachNode( p->pManAig, pObj, i )
     {
         // find the old best cut
-        pCutBest = Dar_ObjBestCut(pObj);
+        pCutBest = Aig_ObjBestCut(pObj);
         Dar_ObjClearBestCut(pCutBest);
         // if the node is used, dereference its cut
         if ( pObj->nRefs )
-            Dar_CutDeref( p->pManAig, pCutBest );
+            Aig_CutDeref( p->pManAig, pCutBest );
 
         // evaluate the cuts of this node
         Dar_ObjForEachCut( pObj, pCut, k )
@@ -259,11 +261,13 @@ int Cnf_ManMapForCnf( Cnf_Man_t * p )
         Dar_ObjSetBestCut( pCutBest );
         // if the node is used, reference its cut
         if ( pObj->nRefs )
-            Dar_CutRef( p->pManAig, pCutBest );
+            Aig_CutRef( p->pManAig, pCutBest );
     }
     return 1;
 }
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/cnf/cnfPost.c

@@ -41,27 +41,30 @@
 ***********************************************************************/
 void Cnf_ManPostprocess_old( Cnf_Man_t * p )
 {
-    extern int Dar_ManLargeCutEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCutR, Dar_Cut_t * pCutL, int Leaf );
+//    extern int Aig_ManLargeCutEval( Aig_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCutR, Dar_Cut_t * pCutL, int Leaf );
     int nNew, Gain, nGain = 0, nVars = 0;
 
-    Dar_Obj_t * pObj, * pFan;
+    Aig_Obj_t * pObj, * pFan;
     Dar_Cut_t * pCutBest, * pCut;
     int i, k;//, a, b, Counter;
-    Dar_ManForEachObj( p->pManAig, pObj, i )
+    Aig_ManForEachObj( p->pManAig, pObj, i )
     {
-        if ( !Dar_ObjIsNode(pObj) )
+        if ( !Aig_ObjIsNode(pObj) )
             continue;
         if ( pObj->nRefs == 0 )
             continue;
-        pCutBest = Dar_ObjBestCut(pObj);
+//        pCutBest = Aig_ObjBestCut(pObj);
+        pCutBest = NULL;
+
         Dar_CutForEachLeaf( p->pManAig, pCutBest, pFan, k )
         {
-            if ( !Dar_ObjIsNode(pFan) )
+            if ( !Aig_ObjIsNode(pFan) )
                 continue;
             assert( pFan->nRefs != 0 );
             if ( pFan->nRefs != 1 )
                 continue;
-            pCut = Dar_ObjBestCut(pFan);
+//            pCut = Aig_ObjBestCut(pFan);
+            pCut = NULL;
 /*
             // find how many common variable they have
             Counter = 0;
@@ -77,11 +80,16 @@ void Cnf_ManPostprocess_old( Cnf_Man_t * p )
             printf( "%d ", Counter );
 */
             // find the new truth table after collapsing these two cuts
-            nNew = Dar_ManLargeCutEval( p->pManAig, pObj, pCutBest, pCut, pFan->Id );
+
+
+//            nNew = Aig_ManLargeCutEval( p->pManAig, pObj, pCutBest, pCut, pFan->Id );
+            nNew = 0;
+
+
 //            printf( "%d+%d=%d:%d(%d) ", pCutBest->Cost, pCut->Cost, 
 //                pCutBest->Cost+pCut->Cost, nNew, pCutBest->Cost+pCut->Cost-nNew );
 
-            Gain = pCutBest->Cost+pCut->Cost-nNew;
+            Gain = pCutBest->Value + pCut->Value - nNew;
             if ( Gain > 0 )
             {
                 nGain += Gain;
@@ -105,12 +113,12 @@ void Cnf_ManPostprocess_old( Cnf_Man_t * p )
 ***********************************************************************/
 void Cnf_ManTransferCuts( Cnf_Man_t * p )
 {
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i;
-    Dar_MmFlexRestart( p->pMemCuts );
-    Dar_ManForEachObj( p->pManAig, pObj, i )
+    Aig_MmFlexRestart( p->pMemCuts );
+    Aig_ManForEachObj( p->pManAig, pObj, i )
     {
-        if ( Dar_ObjIsNode(pObj) && pObj->nRefs > 0 )
+        if ( Aig_ObjIsNode(pObj) && pObj->nRefs > 0 )
             pObj->pData = Cnf_CutCreate( p, pObj );
         else
             pObj->pData = NULL;
@@ -130,9 +138,9 @@ void Cnf_ManTransferCuts( Cnf_Man_t * p )
 ***********************************************************************/
 void Cnf_ManFreeCuts( Cnf_Man_t * p )
 {
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i;
-    Dar_ManForEachObj( p->pManAig, pObj, i )
+    Aig_ManForEachObj( p->pManAig, pObj, i )
         if ( pObj->pData )
         {
             Cnf_CutFree( pObj->pData );
@@ -154,10 +162,10 @@ void Cnf_ManFreeCuts( Cnf_Man_t * p )
 void Cnf_ManPostprocess( Cnf_Man_t * p )
 {
     Cnf_Cut_t * pCut, * pCutFan, * pCutRes;
-    Dar_Obj_t * pObj, * pFan;
+    Aig_Obj_t * pObj, * pFan;
     int Order[16], Costs[16];
     int i, k, fChanges;
-    Dar_ManForEachNode( p->pManAig, pObj, i )
+    Aig_ManForEachNode( p->pManAig, pObj, i )
     {
         if ( pObj->nRefs == 0 )
             continue;
@@ -167,7 +175,7 @@ void Cnf_ManPostprocess( Cnf_Man_t * p )
         Cnf_CutForEachLeaf( p->pManAig, pCut, pFan, k )
         {
             Order[k] = k;
-            Costs[k] = Dar_ObjIsNode(pFan)? Cnf_ObjBestCut(pFan)->Cost : 0;
+            Costs[k] = Aig_ObjIsNode(pFan)? Cnf_ObjBestCut(pFan)->Cost : 0;
         }
         // sort the cuts by Weight
         do {
@@ -186,9 +194,9 @@ void Cnf_ManPostprocess( Cnf_Man_t * p )
 
 
 //        Cnf_CutForEachLeaf( p->pManAig, pCut, pFan, k )
-        for ( k = 0; (k < (int)(pCut)->nFanins) && ((pFan) = Dar_ManObj(p->pManAig, (pCut)->pFanins[Order[k]])); k++ )
+        for ( k = 0; (k < (int)(pCut)->nFanins) && ((pFan) = Aig_ManObj(p->pManAig, (pCut)->pFanins[Order[k]])); k++ )
         {
-            if ( !Dar_ObjIsNode(pFan) )
+            if ( !Aig_ObjIsNode(pFan) )
                 continue;
             assert( pFan->nRefs != 0 );
             if ( pFan->nRefs != 1 )

src/aig/cnf/cnfUtil.c

@@ -39,22 +39,23 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Dar_ManScanMapping_rec( Cnf_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped )
+int Aig_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped )
 {
-    Dar_Obj_t * pLeaf;
+    Aig_Obj_t * pLeaf;
     Dar_Cut_t * pCutBest;
     int aArea, i;
-    if ( pObj->nRefs++ || Dar_ObjIsPi(pObj) || Dar_ObjIsConst1(pObj) )
+    if ( pObj->nRefs++ || Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
         return 0;
-    assert( Dar_ObjIsAnd(pObj) );
+    assert( Aig_ObjIsAnd(pObj) );
     // collect the node first to derive pre-order
     if ( vMapped )
         Vec_PtrPush( vMapped, pObj );
     // visit the transitive fanin of the selected cut
-    pCutBest = Dar_ObjBestCut(pObj);
-    aArea = pCutBest->Cost;
+//    pCutBest = Aig_ObjBestCut(pObj);
+        pCutBest = NULL;
+    aArea = pCutBest->Value;
     Dar_CutForEachLeaf( p->pManAig, pCutBest, pLeaf, i )
-        aArea += Dar_ManScanMapping_rec( p, pLeaf, vMapped );
+        aArea += Aig_ManScanMapping_rec( p, pLeaf, vMapped );
     return aArea;
 }
 
@@ -69,21 +70,21 @@ int Dar_ManScanMapping_rec( Cnf_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Dar_ManScanMapping( Cnf_Man_t * p, int fCollect )
+Vec_Ptr_t * Aig_ManScanMapping( Cnf_Man_t * p, int fCollect )
 {
     Vec_Ptr_t * vMapped = NULL;
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i;
     // clean all references
-    Dar_ManForEachObj( p->pManAig, pObj, i )
+    Aig_ManForEachObj( p->pManAig, pObj, i )
         pObj->nRefs = 0;
     // allocate the array
     if ( fCollect )
         vMapped = Vec_PtrAlloc( 1000 );
     // collect nodes reachable from POs in the DFS order through the best cuts
     p->aArea = 0;
-    Dar_ManForEachPo( p->pManAig, pObj, i )
-        p->aArea += Dar_ManScanMapping_rec( p, Dar_ObjFanin0(pObj), vMapped );
+    Aig_ManForEachPo( p->pManAig, pObj, i )
+        p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
     printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
     return vMapped;
 }
@@ -99,14 +100,14 @@ Vec_Ptr_t * Dar_ManScanMapping( Cnf_Man_t * p, int fCollect )
   SeeAlso     []
 
 ***********************************************************************/
-int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped )
+int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vMapped )
 {
-    Dar_Obj_t * pLeaf;
+    Aig_Obj_t * pLeaf;
     Cnf_Cut_t * pCutBest;
     int aArea, i;
-    if ( pObj->nRefs++ || Dar_ObjIsPi(pObj) || Dar_ObjIsConst1(pObj) )
+    if ( pObj->nRefs++ || Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) )
         return 0;
-    assert( Dar_ObjIsAnd(pObj) );
+    assert( Aig_ObjIsAnd(pObj) );
     assert( pObj->pData != NULL );
     // visit the transitive fanin of the selected cut
     pCutBest = pObj->pData;
@@ -134,18 +135,18 @@ int Cnf_ManScanMapping_rec( Cnf_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vMapped
 Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect )
 {
     Vec_Ptr_t * vMapped = NULL;
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i;
     // clean all references
-    Dar_ManForEachObj( p->pManAig, pObj, i )
+    Aig_ManForEachObj( p->pManAig, pObj, i )
         pObj->nRefs = 0;
     // allocate the array
     if ( fCollect )
         vMapped = Vec_PtrAlloc( 1000 );
     // collect nodes reachable from POs in the DFS order through the best cuts
     p->aArea = 0;
-    Dar_ManForEachPo( p->pManAig, pObj, i )
-        p->aArea += Cnf_ManScanMapping_rec( p, Dar_ObjFanin0(pObj), vMapped );
+    Aig_ManForEachPo( p->pManAig, pObj, i )
+        p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
     printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) : 0, p->aArea );
     return vMapped;
 }

src/aig/cnf/cnfWrite.c

@@ -183,7 +183,7 @@ int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int fCompl, int * pLite
 ***********************************************************************/
 Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
 {
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     Cnf_Dat_t * pCnf;
     Cnf_Cut_t * pCut;
     int OutVar, pVars[32], * pLits, ** pClas;
@@ -191,11 +191,11 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
     int i, k, nLiterals, nClauses, nCubes, Cube, Number;
 
     // count the number of literals and clauses
-    nLiterals = 1 + Dar_ManPoNum( p->pManAig );
-    nClauses = 1 + Dar_ManPoNum( p->pManAig );
+    nLiterals = 1 + Aig_ManPoNum( p->pManAig );
+    nClauses = 1 + Aig_ManPoNum( p->pManAig );
     Vec_PtrForEachEntry( vMapped, pObj, i )
     {
-        assert( Dar_ObjIsNode(pObj) );
+        assert( Aig_ObjIsNode(pObj) );
         pCut = Cnf_ObjBestCut( pObj );
 
         // positive polarity of the cut
@@ -224,7 +224,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
             nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
             nClauses += Vec_IntSize(pCut->vIsop[0]);
         }
-//printf( "%d ", nClauses-(1 + Dar_ManPoNum( p->pManAig )) );
+//printf( "%d ", nClauses-(1 + Aig_ManPoNum( p->pManAig )) );
     }
 //printf( "\n" );
 
@@ -239,13 +239,13 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
 
     // set variable numbers
     Number = 0;
-    pCnf->pVarNums = ALLOC( int, 1+Dar_ManObjIdMax(p->pManAig) );
-    memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Dar_ManObjIdMax(p->pManAig)) );
+    pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p->pManAig) );
+    memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p->pManAig)) );
     Vec_PtrForEachEntry( vMapped, pObj, i )
         pCnf->pVarNums[pObj->Id] = Number++;
-    Dar_ManForEachPi( p->pManAig, pObj, i )
+    Aig_ManForEachPi( p->pManAig, pObj, i )
         pCnf->pVarNums[pObj->Id] = Number++;
-    pCnf->pVarNums[Dar_ManConst1(p->pManAig)->Id] = Number++;
+    pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number++;
     pCnf->nVars = Number;
 
     // assign the clauses
@@ -260,7 +260,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
         for ( k = 0; k < (int)pCut->nFanins; k++ )
         {
             pVars[k] = pCnf->pVarNums[ pCut->pFanins[k] ];
-            assert( pVars[k] <= Dar_ManObjIdMax(p->pManAig) );
+            assert( pVars[k] <= Aig_ManObjIdMax(p->pManAig) );
         }
 
         // positive polarity of the cut
@@ -310,17 +310,17 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped )
     }
 
     // write the constant literal
-    OutVar = pCnf->pVarNums[ Dar_ManConst1(p->pManAig)->Id ];
-    assert( OutVar <= Dar_ManObjIdMax(p->pManAig) );
+    OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ];
+    assert( OutVar <= Aig_ManObjIdMax(p->pManAig) );
     *pClas++ = pLits;
     *pLits++ = 2 * OutVar; 
 
     // write the output literals
-    Dar_ManForEachPo( p->pManAig, pObj, i )
+    Aig_ManForEachPo( p->pManAig, pObj, i )
     {
-        OutVar = pCnf->pVarNums[ Dar_ObjFanin0(pObj)->Id ];
+        OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
         *pClas++ = pLits;
-        *pLits++ = 2 * OutVar + Dar_ObjFaninC0(pObj); 
+        *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
     }
 
     // verify that the correct number of literals and clauses was written

src/aig/csw/csw.h

@@ -51,7 +51,7 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 /*=== cnfCore.c ========================================================*/
-extern Dar_Man_t *     Csw_Sweep( Dar_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
+extern Aig_Man_t *     Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
 
 #ifdef __cplusplus
 }

src/aig/csw/cswCore.c

@@ -39,34 +39,48 @@
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Man_t * Csw_Sweep( Dar_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose )
+Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose )
 {
     Csw_Man_t * p;
-    Dar_Man_t * pRes;
-    Dar_Obj_t * pObj, * pObjNew, * pObjRes;
-    int i;
+    Aig_Man_t * pRes;
+    Aig_Obj_t * pObj, * pObjNew, * pObjRes;
+    int i, clk;
+clk = clock();
     // start the manager
     p = Csw_ManStart( pAig, nCutsMax, nLeafMax, fVerbose );
     // set elementary cuts at the PIs
-    Dar_ManForEachPi( p->pManRes, pObj, i )
+    Aig_ManForEachPi( p->pManRes, pObj, i )
+    {
         Csw_ObjPrepareCuts( p, pObj, 1 );
+        Csw_ObjAddRefs( p, pObj, Aig_ManPi(p->pManAig,i)->nRefs );
+    }
     // process the nodes
-    Dar_ManForEachNode( pAig, pObj, i )
+    Aig_ManForEachNode( pAig, pObj, i )
     {
         // create the new node
-        pObjNew = Dar_And( p->pManRes, Csw_ObjChild0Equiv(p, pObj), Csw_ObjChild1Equiv(p, pObj) );
+        pObjNew = Aig_And( p->pManRes, Csw_ObjChild0Equiv(p, pObj), Csw_ObjChild1Equiv(p, pObj) );
         // check if this node can be represented using another node
-        pObjRes = Csw_ObjSweep( p, Dar_Regular(pObjNew), pObj->nRefs > 1 );
-        pObjRes = Dar_NotCond( pObjRes, Dar_IsComplement(pObjNew) );
-        // set the resulting node
+//        pObjRes = Csw_ObjSweep( p, Aig_Regular(pObjNew), pObj->nRefs > 1 );
+//        pObjRes = Aig_NotCond( pObjRes, Aig_IsComplement(pObjNew) );
+        // try recursively if resubsitution is used
+        do {
+            pObjRes = Csw_ObjSweep( p, Aig_Regular(pObjNew), pObj->nRefs > 1 );
+            pObjRes = Aig_NotCond( pObjRes, Aig_IsComplement(pObjNew) );        
+            pObjNew = pObjRes;
+        } while ( Csw_ObjCuts(p, Aig_Regular(pObjNew)) == NULL && !Aig_ObjIsConst1(Aig_Regular(pObjNew)) );
+        // save the resulting node
         Csw_ObjSetEquiv( p, pObj, pObjRes );
+        // add to the reference counter
+        Csw_ObjAddRefs( p, Aig_Regular(pObjRes), pObj->nRefs );
     }
     // add the POs
-    Dar_ManForEachPo( pAig, pObj, i )
-        Dar_ObjCreatePo( p->pManRes, Csw_ObjChild0Equiv(p, pObj) );
+    Aig_ManForEachPo( pAig, pObj, i )
+        Aig_ObjCreatePo( p->pManRes, Csw_ObjChild0Equiv(p, pObj) );
     // remove dangling nodes 
-    Dar_ManCleanup( p->pManRes );
+    Aig_ManCleanup( p->pManRes );
     // return the resulting manager
+p->timeTotal = clock() - clk;
+p->timeOther = p->timeTotal - p->timeCuts - p->timeHash;
     pRes = p->pManRes;
     Csw_ManStop( p );
     return pRes;

src/aig/csw/cswInt.h

@@ -35,6 +35,7 @@ extern "C" {
 #include <assert.h>
 #include <time.h>
 
+#include "aig.h"
 #include "dar.h"
 #include "kit.h"
 #include "csw.h"
@@ -55,9 +56,12 @@ struct Csw_Cut_t_
 {
     Csw_Cut_t *     pNext;           // the next cut in the table 
     int             Cost;            // the cost of the cut
+//    float           Cost;            // the cost of the cut
     unsigned        uSign;           // cut signature
     int             iNode;           // the node, for which it is the cut
-    int             nFanins;         // the number of words in truth table
+    short           nCutSize;        // the number of bytes in the cut
+    char            nLeafMax;        // the maximum number of fanins
+    char            nFanins;         // the current number of fanins
     int             pFanins[0];      // the fanins (followed by the truth table)
 };
 
@@ -65,10 +69,11 @@ struct Csw_Cut_t_
 struct Csw_Man_t_
 {
     // AIG manager
-    Dar_Man_t *     pManAig;         // the input AIG manager
-    Dar_Man_t *     pManRes;         // the output AIG manager
-    Dar_Obj_t **    pEquiv;          // the equivalent nodes in the resulting manager
+    Aig_Man_t *     pManAig;         // the input AIG manager
+    Aig_Man_t *     pManRes;         // the output AIG manager
+    Aig_Obj_t **    pEquiv;          // the equivalent nodes in the resulting manager
     Csw_Cut_t **    pCuts;           // the cuts for each node in the output manager
+    int *           pnRefs;          // the number of references of each new node
     // hash table for cuts
     Csw_Cut_t **    pTable;          // the table composed of cuts 
     int             nTableSize;      // the size of hash table
@@ -79,25 +84,36 @@ struct Csw_Man_t_
     // internal variables
     int             nCutSize;        // the number of bytes needed to store one cut
     int             nTruthWords;     // the number of truth table words
-    Dar_MmFixed_t * pMemCuts;        // memory manager for cuts
+    Aig_MmFixed_t * pMemCuts;        // memory manager for cuts
     unsigned *      puTemp[4];       // used for the truth table computation
+    // statistics
+    int             nNodesTriv0;     // the number of trivial nodes
+    int             nNodesTriv1;     // the number of trivial nodes
+    int             nNodesTriv2;     // the number of trivial nodes
+    int             nNodesCuts;      // the number of rewritten nodes
+    int             nNodesTried;     // the number of nodes tried
+    int             timeCuts;        // time to compute the cut and its truth table
+    int             timeHash;        // time for hashing cuts
+    int             timeOther;       // other time
+    int             timeTotal;       // total time
 };
 
-static inline unsigned     Csw_ObjCutSign( unsigned ObjId )                 { return (1 << (ObjId % 31));                         }
+static inline int          Csw_CutLeaveNum( Csw_Cut_t * pCut )          { return pCut->nFanins;                                   }
+static inline int *        Csw_CutLeaves( Csw_Cut_t * pCut )            { return pCut->pFanins;                                   }
+static inline unsigned *   Csw_CutTruth( Csw_Cut_t * pCut )             { return (unsigned *)(pCut->pFanins + pCut->nLeafMax);    }
+static inline Csw_Cut_t *  Csw_CutNext( Csw_Cut_t * pCut )              { return (Csw_Cut_t *)(((char *)pCut) + pCut->nCutSize);  }
 
-static inline int          Csw_CutLeaveNum( Csw_Cut_t * pCut )              { return pCut->nFanins;                               }
-static inline int *        Csw_CutLeaves( Csw_Cut_t * pCut )                { return pCut->pFanins;                               }
-static inline unsigned *   Csw_CutTruth( Csw_Cut_t * pCut )                 { return (unsigned *)(pCut->pFanins + pCut->nFanins); }
-static inline Csw_Cut_t *  Csw_CutNext( Csw_Man_t * p, Csw_Cut_t * pCut )   { return (Csw_Cut_t *)(((char *)pCut) + p->nCutSize); }
+static inline int          Csw_ObjRefs( Csw_Man_t * p, Aig_Obj_t * pObj )                         { return p->pnRefs[pObj->Id];   }
+static inline void         Csw_ObjAddRefs( Csw_Man_t * p, Aig_Obj_t * pObj, int nRefs )           { p->pnRefs[pObj->Id] += nRefs; }
 
-static inline Csw_Cut_t *  Csw_ObjCuts( Csw_Man_t * p, Dar_Obj_t * pObj )                         { return p->pCuts[pObj->Id];    }
-static inline void         Csw_ObjSetCuts( Csw_Man_t * p, Dar_Obj_t * pObj, Csw_Cut_t * pCuts )   { p->pCuts[pObj->Id] = pCuts;   }
+static inline Csw_Cut_t *  Csw_ObjCuts( Csw_Man_t * p, Aig_Obj_t * pObj )                         { return p->pCuts[pObj->Id];    }
+static inline void         Csw_ObjSetCuts( Csw_Man_t * p, Aig_Obj_t * pObj, Csw_Cut_t * pCuts )   { p->pCuts[pObj->Id] = pCuts;   }
 
-static inline Dar_Obj_t *  Csw_ObjEquiv( Csw_Man_t * p, Dar_Obj_t * pObj )                        { return p->pEquiv[pObj->Id];   }
-static inline void         Csw_ObjSetEquiv( Csw_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pEquiv ) { p->pEquiv[pObj->Id] = pEquiv; }
+static inline Aig_Obj_t *  Csw_ObjEquiv( Csw_Man_t * p, Aig_Obj_t * pObj )                        { return p->pEquiv[pObj->Id];   }
+static inline void         Csw_ObjSetEquiv( Csw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pEquiv ) { p->pEquiv[pObj->Id] = pEquiv; }
 
-static inline Dar_Obj_t *  Csw_ObjChild0Equiv( Csw_Man_t * p, Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond(Csw_ObjEquiv(p, Dar_ObjFanin0(pObj)), Dar_ObjFaninC0(pObj)) : NULL;  }
-static inline Dar_Obj_t *  Csw_ObjChild1Equiv( Csw_Man_t * p, Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond(Csw_ObjEquiv(p, Dar_ObjFanin1(pObj)), Dar_ObjFaninC1(pObj)) : NULL;  }
+static inline Aig_Obj_t *  Csw_ObjChild0Equiv( Csw_Man_t * p, Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Csw_ObjEquiv(p, Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL;  }
+static inline Aig_Obj_t *  Csw_ObjChild1Equiv( Csw_Man_t * p, Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Csw_ObjEquiv(p, Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL;  }
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
@@ -109,25 +125,25 @@ static inline Dar_Obj_t *  Csw_ObjChild1Equiv( Csw_Man_t * p, Dar_Obj_t * pObj )
 
 // iterator over cuts of the node
 #define Csw_ObjForEachCut( p, pObj, pCut, i )                           \
-    for ( i = 0, pCut = Csw_ObjCuts(p, pObj); i < p->nCutsMax; i++, pCut = Csw_CutNext(p, pCut) ) 
+    for ( i = 0, pCut = Csw_ObjCuts(p, pObj); i < p->nCutsMax; i++, pCut = Csw_CutNext(pCut) ) 
 // iterator over leaves of the cut
 #define Csw_CutForEachLeaf( p, pCut, pLeaf, i )                         \
-    for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Dar_ManObj(p, (pCut)->pFanins[i])); i++ )
+    for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== cnfCut.c ========================================================*/
-extern Csw_Cut_t *    Csw_ObjPrepareCuts( Csw_Man_t * p, Dar_Obj_t * pObj, int fTriv );
-extern Dar_Obj_t *    Csw_ObjSweep( Csw_Man_t * p, Dar_Obj_t * pObj, int fTriv );
+extern Csw_Cut_t *    Csw_ObjPrepareCuts( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv );
+extern Aig_Obj_t *    Csw_ObjSweep( Csw_Man_t * p, Aig_Obj_t * pObj, int fTriv );
 /*=== cnfMan.c ========================================================*/
-extern Csw_Man_t *    Csw_ManStart( Dar_Man_t * pMan, int nCutsMax, int nLeafMax, int fVerbose );
+extern Csw_Man_t *    Csw_ManStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, int fVerbose );
 extern void           Csw_ManStop( Csw_Man_t * p );
 /*=== cnfTable.c ========================================================*/
+extern int            Csw_TableCountCuts( Csw_Man_t * p );
 extern void           Csw_TableCutInsert( Csw_Man_t * p, Csw_Cut_t * pCut );
-extern Dar_Obj_t *    Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut );
-extern unsigned int   Cudd_PrimeCws( unsigned int p );
+extern Aig_Obj_t *    Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut );
 
 #ifdef __cplusplus
 }

src/aig/csw/cswMan.c

@@ -39,10 +39,10 @@
   SeeAlso     []
 
 ***********************************************************************/
-Csw_Man_t * Csw_ManStart( Dar_Man_t * pMan, int nCutsMax, int nLeafMax, int fVerbose )
+Csw_Man_t * Csw_ManStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, int fVerbose )
 {
     Csw_Man_t * p;
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i;
     assert( nCutsMax >= 2  );
     assert( nLeafMax <= 16 );
@@ -54,24 +54,26 @@ Csw_Man_t * Csw_ManStart( Dar_Man_t * pMan, int nCutsMax, int nLeafMax, int fVer
     p->fVerbose = fVerbose;
     p->pManAig  = pMan;
     // create the new manager
-    p->pManRes  = Dar_ManStartFrom( pMan );
-    assert( Dar_ManPiNum(p->pManAig) == Dar_ManPiNum(p->pManRes) );
+    p->pManRes  = Aig_ManStartFrom( pMan );
+    assert( Aig_ManPiNum(p->pManAig) == Aig_ManPiNum(p->pManRes) );
     // allocate room for cuts and equivalent nodes
-    p->pEquiv   = ALLOC( Dar_Obj_t *, Dar_ManObjIdMax(pMan) + 1 );
-    p->pCuts    = ALLOC( Csw_Cut_t *, Dar_ManObjIdMax(pMan) + 1 );
-    memset( p->pCuts, 0, sizeof(Dar_Obj_t *) * (Dar_ManObjIdMax(pMan) + 1) );
+    p->pnRefs   = ALLOC( int, Aig_ManObjIdMax(pMan) + 1 );
+    p->pEquiv   = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(pMan) + 1 );
+    p->pCuts    = ALLOC( Csw_Cut_t *, Aig_ManObjIdMax(pMan) + 1 );
+    memset( p->pCuts, 0, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(pMan) + 1) );
+    memset( p->pnRefs, 0, sizeof(int) * (Aig_ManObjIdMax(pMan) + 1) );
     // allocate memory manager
-    p->nTruthWords = Dar_TruthWordNum(nLeafMax);
+    p->nTruthWords = Aig_TruthWordNum(nLeafMax);
     p->nCutSize = sizeof(Csw_Cut_t) + sizeof(int) * nLeafMax + sizeof(unsigned) * p->nTruthWords;
-    p->pMemCuts = Dar_MmFixedStart( p->nCutSize * p->nCutsMax, 512 );
+    p->pMemCuts = Aig_MmFixedStart( p->nCutSize * p->nCutsMax, 512 );
     // allocate hash table for cuts
-    p->nTableSize = Cudd_PrimeCws( Dar_ManNodeNum(pMan) * p->nCutsMax / 2 );
+    p->nTableSize = Aig_PrimeCudd( Aig_ManNodeNum(pMan) * p->nCutsMax / 2 );
     p->pTable = ALLOC( Csw_Cut_t *, p->nTableSize );
-    memset( p->pTable, 0, sizeof(Dar_Obj_t *) * p->nTableSize );
+    memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize );
     // set the pointers to the available fraig nodes
-    Csw_ObjSetEquiv( p, Dar_ManConst1(p->pManAig), Dar_ManConst1(p->pManRes) );
-    Dar_ManForEachPi( p->pManAig, pObj, i )
-        Csw_ObjSetEquiv( p, pObj, Dar_ManPi(p->pManRes, i) );
+    Csw_ObjSetEquiv( p, Aig_ManConst1(p->pManAig), Aig_ManConst1(p->pManRes) );
+    Aig_ManForEachPi( p->pManAig, pObj, i )
+        Csw_ObjSetEquiv( p, pObj, Aig_ManPi(p->pManRes, i) );
     // room for temporary truth tables
     p->puTemp[0] = ALLOC( unsigned, 4 * p->nTruthWords );
     p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
@@ -93,8 +95,23 @@ Csw_Man_t * Csw_ManStart( Dar_Man_t * pMan, int nCutsMax, int nLeafMax, int fVer
 ***********************************************************************/
 void Csw_ManStop( Csw_Man_t * p )
 {
+    if ( p->fVerbose )
+    {
+        int nNodesBeg = Aig_ManNodeNum(p->pManAig);
+        int nNodesEnd = Aig_ManNodeNum(p->pManRes);
+        printf( "Beg = %7d.  End = %7d.  (%6.2f %%)  Try = %7d.  Cuts = %8d.\n", 
+            nNodesBeg, nNodesEnd, 100.0*(nNodesBeg-nNodesEnd)/nNodesBeg,
+            p->nNodesTried, Csw_TableCountCuts( p ) );
+        printf( "Triv0 = %6d.  Triv1 = %6d.  Triv2 = %6d.  Cut-replace = %6d.\n", 
+            p->nNodesTriv0, p->nNodesTriv1, p->nNodesTriv2, p->nNodesCuts );
+        PRTP( "Cuts    ", p->timeCuts,     p->timeTotal );
+        PRTP( "Hashing ", p->timeHash,     p->timeTotal );
+        PRTP( "Other   ", p->timeOther,    p->timeTotal );
+        PRTP( "TOTAL   ", p->timeTotal,    p->timeTotal );
+    }
     free( p->puTemp[0] );
-    Dar_MmFixedStop( p->pMemCuts, 0 );
+    Aig_MmFixedStop( p->pMemCuts, 0 );
+    free( p->pnRefs );
     free( p->pEquiv );
     free( p->pCuts );
     free( p->pTable );

src/aig/csw/cswTable.c

@@ -65,41 +65,26 @@ unsigned Csw_CutHash( Csw_Cut_t * pCut )
     return uHash;
 }
 
-/**Function********************************************************************
-
-  Synopsis    [Returns the next prime >= p.]
+/**Function*************************************************************
 
-  Description [Copied from CUDD, for stand-aloneness.]
+  Synopsis    [Returns the total number of cuts in the table.]
 
-  SideEffects [None]
+  Description []
+               
+  SideEffects []
 
   SeeAlso     []
 
-******************************************************************************/
-unsigned int Cudd_PrimeCws( unsigned int p )
+***********************************************************************/
+int Csw_TableCountCuts( Csw_Man_t * 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 */
+    Csw_Cut_t * pEnt;
+    int i, Counter = 0;
+    for ( i = 0; i < p->nTableSize; i++ )
+        for ( pEnt = p->pTable[i]; pEnt; pEnt = pEnt->pNext )
+            Counter++;
+    return Counter;
+}
 
 /**Function*************************************************************
 
@@ -130,9 +115,9 @@ void Csw_TableCutInsert( Csw_Man_t * p, Csw_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Obj_t * Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut )
+Aig_Obj_t * Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut )
 {
-    Dar_Obj_t * pRes = NULL;
+    Aig_Obj_t * pRes = NULL;
     Csw_Cut_t * pEnt;
     unsigned * pTruthNew, * pTruthOld;
     int iEntry = Csw_CutHash(pCut) % p->nTableSize;
@@ -150,8 +135,8 @@ Dar_Obj_t * Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut )
         {
             if ( Kit_TruthIsEqual( pTruthOld, pTruthNew, pCut->nFanins ) )
             {
-                pRes = Dar_ManObj( p->pManRes, pEnt->iNode );
-                assert( pRes->fPhase == Dar_ManObj( p->pManRes, pCut->iNode )->fPhase );
+                pRes = Aig_ManObj( p->pManRes, pEnt->iNode );
+                assert( pRes->fPhase == Aig_ManObj( p->pManRes, pCut->iNode )->fPhase );
                 break;
             }
         }
@@ -159,8 +144,8 @@ Dar_Obj_t * Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut )
         {
             if ( Kit_TruthIsOpposite( pTruthOld, pTruthNew, pCut->nFanins ) )
             {
-                pRes = Dar_Not( Dar_ManObj( p->pManRes, pEnt->iNode ) );
-                assert( Dar_Regular(pRes)->fPhase != Dar_ManObj( p->pManRes, pCut->iNode )->fPhase );
+                pRes = Aig_Not( Aig_ManObj( p->pManRes, pEnt->iNode ) );
+                assert( Aig_Regular(pRes)->fPhase != Aig_ManObj( p->pManRes, pCut->iNode )->fPhase );
                 break;
             }
         }

src/aig/dar/darCore.c

@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "dar.h"
+#include "darInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -30,6 +30,28 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the structure with default assignment of parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ManDefaultParams( Dar_Par_t * pPars )
+{
+    memset( pPars, 0, sizeof(Dar_Par_t) );
+    pPars->nCutsMax     = 8;
+    pPars->nSubgMax     = 4;
+    pPars->fUpdateLevel = 0;
+    pPars->fUseZeros    = 0;
+    pPars->fVerbose     = 0;
+    pPars->fVeryVerbose = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -39,89 +61,107 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Dar_ManRewrite( Dar_Man_t * p )
+int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars )
 {
+    Dar_Man_t * p;
     ProgressBar * pProgress;
-    Dar_Cut_t * pCutSet;
-    Dar_Obj_t * pObj, * pObjNew;
+    Dar_Cut_t * pCut;
+    Aig_Obj_t * pObj, * pObjNew;
     int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
     int clk = 0, clkStart;
+    // create rewriting manager
+    p = Dar_ManStart( pAig, pPars );
     // remove dangling nodes
-    Dar_ManCleanup( p );
+    Aig_ManCleanup( pAig );
     // set elementary cuts for the PIs
-    Dar_ManSetupPis( p );
+//    Dar_ManSetupPis( p );
+    Aig_ManCleanData( pAig );
+    Dar_ObjPrepareCuts( p, Aig_ManConst1(pAig) );
+    Aig_ManForEachPi( pAig, pObj, i )
+        Dar_ObjPrepareCuts( p, pObj );
 //    if ( p->pPars->fUpdateLevel )
-//        Dar_NtkStartReverseLevels( p );
+//        Aig_NtkStartReverseLevels( p );
     // resynthesize each node once
     clkStart = clock();
-    p->nNodesInit = Dar_ManNodeNum(p);
-    nNodesOld = Vec_PtrSize( p->vObjs );
+    p->nNodesInit = Aig_ManNodeNum(pAig);
+    nNodesOld = Vec_PtrSize( pAig->vObjs );
     pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
-    Dar_ManForEachObj( p, pObj, i )
+    Aig_ManForEachObj( pAig, pObj, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
-        if ( !Dar_ObjIsNode(pObj) )
+        if ( !Aig_ObjIsNode(pObj) )
             continue;
         if ( i > nNodesOld )
             break;
         // compute cuts for the node
 clk = clock();
-        pCutSet = Dar_ObjComputeCuts_rec( p, pObj );
+        Dar_ObjComputeCuts_rec( p, pObj );
 p->timeCuts += clock() - clk;
-        // go through the cuts of this node
-        Required = 1000000;
-        p->GainBest = -1;
-        for ( k = 1; k < (int)pObj->nCuts; k++ )
+
+        // check if there is a trivial cut
+        Dar_ObjForEachCut( pObj, pCut, k )
+            if ( pCut->nLeaves == 0 || (pCut->nLeaves == 1 && pCut->pLeaves[0] != pObj->Id) )
+                break;
+        if ( k < (int)pObj->nCuts )
         {
-/*
-            if ( pObj->Id == 654 )
+            assert( pCut->nLeaves < 2 );
+            if ( pCut->nLeaves == 0 ) // replace by constant
             {
-                int m;
-                for ( m = 0; m < 4; m++ )
-                    printf( "%d ", pCutSet[k].pLeaves[m] );
-                printf( "\n" );
+                assert( pCut->uTruth == 0 || pCut->uTruth == 0xFFFF );
+                pObjNew = Aig_NotCond( Aig_ManConst1(p->pAig), pCut->uTruth==0 );
             }
-*/
-            Dar_LibEval( p, pObj, pCutSet + k, Required );
+            else
+            {
+                assert( pCut->uTruth == 0xAAAA || pCut->uTruth == 0x5555 );
+                pObjNew = Aig_NotCond( Aig_ManObj(p->pAig, pCut->pLeaves[0]), pCut->uTruth==0x5555 );
+            }
+            // replace the node
+            Aig_ObjReplace( pAig, pObj, pObjNew, 1 );
+            // remove the old cuts
+            Dar_ObjSetCuts( pObj, NULL );
+            continue;
         }
+
+        // evaluate the cuts
+        p->GainBest = -1;
+        Required = 1000000;
+        Dar_ObjForEachCut( pObj, pCut, k )
+            Dar_LibEval( p, pObj, pCut, Required );
         // check the best gain
         if ( !(p->GainBest > 0 || p->GainBest == 0 && p->pPars->fUseZeros) )
             continue;
         // if we end up here, a rewriting step is accepted
-        nNodeBefore = Dar_ManNodeNum( p );
+        nNodeBefore = Aig_ManNodeNum( pAig );
         pObjNew = Dar_LibBuildBest( p );
-        pObjNew = Dar_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase );
-        assert( (int)Dar_Regular(pObjNew)->Level <= Required );
+        pObjNew = Aig_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase );
+        assert( (int)Aig_Regular(pObjNew)->Level <= Required );
         // replace the node
-        Dar_ObjReplace( p, pObj, pObjNew, 1 );
+        Aig_ObjReplace( pAig, pObj, pObjNew, 1 );
         // remove the old cuts
-        pObj->pData = NULL;
+        Dar_ObjSetCuts( pObj, NULL );
         // compare the gains
-        nNodeAfter = Dar_ManNodeNum( p );
+        nNodeAfter = Aig_ManNodeNum( pAig );
         assert( p->GainBest <= nNodeBefore - nNodeAfter );
         // count gains of this class
         p->ClassGains[p->ClassBest] += nNodeBefore - nNodeAfter;
-
-//        if ( p->ClassBest == 29 )
-//            printf( "%d ", p->OutNumBest );
-
     }
 p->timeTotal = clock() - clkStart;
 p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
 
     Extra_ProgressBarStop( pProgress );
-    p->nCutMemUsed = Dar_MmFlexReadMemUsage(p->pMemCuts)/(1<<20);
+    p->nCutMemUsed = Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20);
     Dar_ManCutsFree( p );
+    // stop the rewriting manager
+    Dar_ManStop( p );
     // put the nodes into the DFS order and reassign their IDs
-//    Dar_NtkReassignIds( p );
-
+//    Aig_NtkReassignIds( p );
     // fix the levels
 //    if ( p->pPars->fUpdateLevel )
-//        Dar_NtkStopReverseLevels( p );
+//        Aig_NtkStopReverseLevels( p );
     // check
-    if ( !Dar_ManCheck( p ) )
+    if ( !Aig_ManCheck( pAig ) )
     {
-        printf( "Dar_ManRewrite: The network check has failed.\n" );
+        printf( "Aig_ManRewrite: The network check has failed.\n" );
         return 0;
     }
     return 1;
@@ -138,32 +178,37 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
   SeeAlso     []
 
 ***********************************************************************/
-int Dar_ManComputeCuts( Dar_Man_t * p )
+Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig )
 {
-    Dar_Obj_t * pObj;
+    Dar_Man_t * p;
+    Aig_Obj_t * pObj;
+    Aig_MmFixed_t * pMemCuts;
     int i, clk = 0, clkStart = clock();
     int nCutsMax = 0, nCutsTotal = 0;
+    // create rewriting manager
+    p = Dar_ManStart( pAig, NULL );
     // remove dangling nodes
-    Dar_ManCleanup( p );
+    Aig_ManCleanup( pAig );
     // set elementary cuts for the PIs
-    Dar_ManSetupPis( p );
+//    Dar_ManSetupPis( p );
+    Aig_ManForEachPi( pAig, pObj, i )
+        Dar_ObjPrepareCuts( p, pObj );
     // compute cuts for each nodes in the topological order
-    Dar_ManForEachObj( p, pObj, i )
+    Aig_ManForEachObj( pAig, pObj, i )
     {
-        if ( !Dar_ObjIsNode(pObj) )
+        if ( !Aig_ObjIsNode(pObj) )
             continue;
         Dar_ObjComputeCuts( p, pObj );
         nCutsTotal += pObj->nCuts - 1;
-        nCutsMax = DAR_MAX( nCutsMax, (int)pObj->nCuts - 1 );
+        nCutsMax = AIG_MAX( nCutsMax, (int)pObj->nCuts - 1 );
     }
-    // print statistics on the number of non-trivial cuts
-    printf( "Node = %6d. Cut = %8d. Max = %3d. Ave = %.2f.  Filter = %8d. Created = %8d.\n", 
-        Dar_ManNodeNum(p), nCutsTotal, nCutsMax, (float)nCutsTotal/Dar_ManNodeNum(p), 
-        p->nCutsFiltered, p->nCutsFiltered+nCutsTotal+Dar_ManNodeNum(p)+Dar_ManPiNum(p) );
-    PRT( "Time", clock() - clkStart );
     // free the cuts
+    pMemCuts = p->pMemCuts;
+    p->pMemCuts = NULL;
 //    Dar_ManCutsFree( p );
-    return 1;
+    // stop the rewriting manager
+    Dar_ManStop( p );
+    return pMemCuts;
 }
 
 

src/aig/dar/darInt.h

+/**CFile****************************************************************
+
+  FileName    [darInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: darInt.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef __DAR_INT_H__
+#define __DAR_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+
+#include "vec.h"
+#include "aig.h"
+#include "dar.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Dar_Man_t_            Dar_Man_t;
+typedef struct Dar_Cut_t_            Dar_Cut_t;
+
+// the AIG 4-cut
+struct Dar_Cut_t_  // 6 words
+{
+    unsigned         uSign;          // cut signature
+    unsigned         uTruth  : 16;   // the truth table of the cut function
+    unsigned         Value   : 12;   // the value of the cut 
+    unsigned         fUsed   :  1;   // marks the cut currently in use
+    unsigned         nLeaves :  3;   // the number of leaves
+    int              pLeaves[4];     // the array of leaves
+};
+
+// the AIG manager
+struct Dar_Man_t_
+{
+    // input data;
+    Dar_Par_t *      pPars;          // rewriting parameters
+    Aig_Man_t *      pAig;           // AIG manager 
+    // various data members
+    Aig_MmFixed_t *  pMemCuts;       // memory manager for cuts
+    void *           pManCnf;        // CNF managers
+    // current rewriting step
+    Vec_Ptr_t *      vLeavesBest;    // the best set of leaves
+    int              OutBest;        // the best output (in the library)
+    int              OutNumBest;     // the best number of the output
+    int              GainBest;       // the best gain
+    int              LevelBest;      // the level of node with the best gain
+    int              ClassBest;      // the equivalence class of the best replacement
+    // function statistics
+    int              nTotalSubgs;    // the total number of subgraphs tried
+    int              ClassTimes[222];// the runtimes for each class
+    int              ClassGains[222];// the gains for each class
+    int              ClassSubgs[222];// the graphs for each class
+    int              nCutMemUsed;    // memory used for cuts
+    // rewriting statistics
+    int              nNodesInit;     // the original number of nodes
+    int              nCutsAll;       // all cut pairs
+    int              nCutsTried;     // computed cuts
+    int              nCutsUsed;      // used cuts
+    int              nCutsBad;       // bad cuts due to absent fanin
+    int              nCutsGood;      // good cuts
+    int              nCutsSkipped;   // skipped bad cuts
+    // timing statistics
+    int              timeCuts;
+    int              timeEval;
+    int              timeOther;
+    int              timeTotal;
+    int              time1;
+    int              time2;
+};
+
+static inline Dar_Cut_t *  Dar_ObjCuts( Aig_Obj_t * pObj )                         { return pObj->pData;    }
+static inline void         Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts )   { pObj->pData = pCuts;   }
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                          ITERATORS                               ///
+////////////////////////////////////////////////////////////////////////
+
+// iterator over all cuts of the node
+#define Dar_ObjForEachCutAll( pObj, pCut, i )                                   \
+    for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ ) 
+#define Dar_ObjForEachCut( pObj, pCut, i )                                      \
+    for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ ) if ( (pCut)->fUsed==0 ) {} else
+// iterator over leaves of the cut
+#define Dar_CutForEachLeaf( p, pCut, pLeaf, i )                                 \
+    for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pLeaf) = Aig_ManObj(p, (pCut)->pLeaves[i])), 1); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== darBalance.c ========================================================*/
+extern Aig_Man_t *     Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
+/*=== darCore.c ========================================================*/
+/*=== darCut.c ========================================================*/
+extern Dar_Cut_t *     Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
+extern void            Dar_ManCutsFree( Dar_Man_t * p );
+extern Dar_Cut_t *     Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj );
+extern Dar_Cut_t *     Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
+/*=== darData.c ========================================================*/
+extern Vec_Int_t *     Dar_LibReadNodes();
+extern Vec_Int_t *     Dar_LibReadOuts();
+extern Vec_Int_t *     Dar_LibReadPrios();
+/*=== darLib.c ==========================================================*/
+extern void            Dar_LibStart();
+extern void            Dar_LibStop();
+extern void            Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
+extern Aig_Obj_t *     Dar_LibBuildBest( Dar_Man_t * p );
+/*=== darMan.c ==========================================================*/
+extern Dar_Man_t *     Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars );
+extern void            Dar_ManStop( Dar_Man_t * p );
+extern void            Dar_ManPrintStats( Dar_Man_t * p );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+

src/aig/dar/darMan.c

@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "dar.h"
+#include "darInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -30,48 +30,25 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Starts the AIG manager.]
+  Synopsis    [Starts the rewriting manager.]
 
-  Description [The argument of this procedure is a soft limit on the
-  the number of nodes, or 0 if the limit is unknown.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Man_t * Dar_ManStart( int nNodesMax )
+Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars )
 {
     Dar_Man_t * p;
-    int i;
-    if ( nNodesMax <= 0 )
-        nNodesMax = 10007;
     // start the manager
     p = ALLOC( Dar_Man_t, 1 );
     memset( p, 0, sizeof(Dar_Man_t) );
-    // perform initializations
-    p->nTravIds = 1;
-    p->fCatchExor = 0;
-    // allocate arrays for nodes
-    p->vPis = Vec_PtrAlloc( 100 );
-    p->vPos = Vec_PtrAlloc( 100 );
-    p->vObjs = Vec_PtrAlloc( 1000 );
+    p->pPars = pPars;
+    p->pAig  = pAig;
     // prepare the internal memory manager
-    p->pMemObjs = Dar_MmFixedStart( sizeof(Dar_Obj_t), nNodesMax );
-    p->pMemCuts = Dar_MmFlexStart();
-    // prepare storage for cuts
-    p->nBaseCuts = DAR_CUT_BASE;
-    for ( i = 0; i < p->nBaseCuts; i++ )
-        p->pBaseCuts[i] = p->BaseCuts + i;
-    // create the constant node
-    p->pConst1 = Dar_ManFetchMemory( p );
-    p->pConst1->Type = DAR_AIG_CONST1;
-    p->pConst1->fPhase = 1;
-    p->nObjs[DAR_AIG_CONST1]++;
-    // start the table
-    p->nTableSize = nNodesMax;
-    p->pTable = ALLOC( Dar_Obj_t *, p->nTableSize );
-    memset( p->pTable, 0, sizeof(Dar_Obj_t *) * p->nTableSize );
+    p->pMemCuts = Aig_MmFixedStart( p->pPars->nCutsMax * sizeof(Dar_Cut_t), 512 );
     // other data
     p->vLeavesBest = Vec_PtrAlloc( 4 );
     return p;
@@ -79,69 +56,7 @@ Dar_Man_t * Dar_ManStart( int nNodesMax )
 
 /**Function*************************************************************
 
-  Synopsis    [Duplicates the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dar_Man_t * Dar_ManStartFrom( Dar_Man_t * p )
-{
-    Dar_Man_t * pNew;
-    Dar_Obj_t * pObj;
-    int i;
-    // create the new manager
-    pNew = Dar_ManStart( Dar_ManObjIdMax(p) + 1 );
-    // create the PIs
-    Dar_ManConst1(p)->pData = Dar_ManConst1(pNew);
-    Dar_ManForEachPi( p, pObj, i )
-        pObj->pData = Dar_ObjCreatePi(pNew);
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Dar_Man_t * Dar_ManDup( Dar_Man_t * p )
-{
-    Dar_Man_t * pNew;
-    Dar_Obj_t * pObj;
-    int i;
-    // create the new manager
-    pNew = Dar_ManStart( Dar_ManObjIdMax(p) + 1 );
-    // create the PIs
-    Dar_ManConst1(p)->pData = Dar_ManConst1(pNew);
-    Dar_ManForEachPi( p, pObj, i )
-        pObj->pData = Dar_ObjCreatePi(pNew);
-    // duplicate internal nodes
-    Dar_ManForEachObj( p, pObj, i )
-        if ( Dar_ObjIsBuf(pObj) )
-            pObj->pData = Dar_ObjChild0Copy(pObj);
-        else if ( Dar_ObjIsNode(pObj) )
-            pObj->pData = Dar_And( pNew, Dar_ObjChild0Copy(pObj), Dar_ObjChild1Copy(pObj) );
-    // add the POs
-    Dar_ManForEachPo( p, pObj, i )
-        Dar_ObjCreatePo( pNew, Dar_ObjChild0Copy(pObj) );
-    // check the resulting network
-    if ( !Dar_ManCheck(pNew) )
-        printf( "Dar_ManDup(): The check has failed.\n" );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the AIG manager.]
+  Synopsis    [Stops the rewriting manager.]
 
   Description []
                
@@ -152,57 +67,17 @@ Dar_Man_t * Dar_ManDup( Dar_Man_t * p )
 ***********************************************************************/
 void Dar_ManStop( Dar_Man_t * p )
 {
-    Dar_Obj_t * pObj;
-    int i;
-    // make sure the nodes have clean marks
-    Dar_ManForEachObj( p, pObj, i )
-        assert( !pObj->fMarkA && !pObj->fMarkB );
-    // print time
-    if ( p->time1 ) { PRT( "time1", p->time1 ); }
-    if ( p->time2 ) { PRT( "time2", p->time2 ); }
-//    Dar_TableProfile( p );
-    Dar_MmFixedStop( p->pMemObjs, 0 );
-    Dar_MmFlexStop( p->pMemCuts, 0 );
-    if ( p->vPis )        Vec_PtrFree( p->vPis );
-    if ( p->vPos )        Vec_PtrFree( p->vPos );
-    if ( p->vObjs )       Vec_PtrFree( p->vObjs );
-    if ( p->vRequired )   Vec_IntFree( p->vRequired );
-    if ( p->vLeavesBest ) Vec_PtrFree( p->vLeavesBest );
-    free( p->pTable );
+    if ( p->pPars->fVerbose )
+        Dar_ManPrintStats( p );
+    if ( p->pMemCuts )
+        Aig_MmFixedStop( p->pMemCuts, 0 );
+    if ( p->vLeavesBest ) 
+        Vec_PtrFree( p->vLeavesBest );
     free( p );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the number of dangling nodes removed.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Dar_ManCleanup( Dar_Man_t * p )
-{
-    Vec_Ptr_t * vObjs;
-    Dar_Obj_t * pNode;
-    int i, nNodesOld;
-    nNodesOld = Dar_ManNodeNum(p);
-    // collect roots of dangling nodes
-    vObjs = Vec_PtrAlloc( 100 );
-    Dar_ManForEachObj( p, pNode, i )
-        if ( Dar_ObjIsNode(pNode) && Dar_ObjRefs(pNode) == 0 )
-            Vec_PtrPush( vObjs, pNode );
-    // recursively remove dangling nodes
-    Vec_PtrForEachEntry( vObjs, pNode, i )
-        Dar_ObjDelete_rec( p, pNode, 1 );
-    Vec_PtrFree( vObjs );
-    return nNodesOld - Dar_ManNodeNum(p);
-}
-
-/**Function*************************************************************
-
   Synopsis    [Stops the AIG manager.]
 
   Description []
@@ -214,39 +89,18 @@ int Dar_ManCleanup( Dar_Man_t * p )
 ***********************************************************************/
 void Dar_ManPrintStats( Dar_Man_t * p )
 {
-    printf( "PI/PO/Lat = %5d/%5d/%5d   ", Dar_ManPiNum(p), Dar_ManPoNum(p), Dar_ManLatchNum(p) );
-    printf( "A = %6d. ",    Dar_ManAndNum(p) );
-    if ( Dar_ManExorNum(p) )
-        printf( "X = %5d. ",    Dar_ManExorNum(p) );
-    if ( Dar_ManBufNum(p) )
-        printf( "B = %3d. ",    Dar_ManBufNum(p) );
-    printf( "Cre = %6d. ",  p->nCreated );
-    printf( "Del = %6d. ",  p->nDeleted );
-//    printf( "Lev = %3d. ",  Dar_ManCountLevels(p) );
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Dar_ManPrintRuntime( Dar_Man_t * p )
-{
     int i, Gain;
-    printf( "Good cuts = %d. Bad cuts = %d.  Cut mem = %d Mb\n", 
-        p->nCutsGood, p->nCutsBad, p->nCutMemUsed );
+    Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig);
+    printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%).  Cut mem = %d Mb\n", 
+        p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit, p->nCutMemUsed );
+    printf( "Cuts = %8d. Tried = %8d. Used = %8d. Bad = %5d. Skipped = %5d. Ave = %.2f.\n", 
+        p->nCutsAll, p->nCutsTried, p->nCutsUsed, p->nCutsBad, p->nCutsSkipped,
+        (float)p->nCutsUsed/Aig_ManNodeNum(p->pAig) );
     PRT( "Cuts  ", p->timeCuts );
     PRT( "Eval  ", p->timeEval );
     PRT( "Other ", p->timeOther );
     PRT( "TOTAL ", p->timeTotal );
-    Gain = p->nNodesInit - Dar_ManNodeNum(p);
+/*
     for ( i = 0; i < 222; i++ )
     {
         if ( p->ClassGains[i] == 0 && p->ClassTimes[i] == 0 )
@@ -257,6 +111,7 @@ void Dar_ManPrintRuntime( Dar_Man_t * p )
         printf( "R = %7d  ", p->ClassGains[i]? p->ClassSubgs[i]/p->ClassGains[i] : 9999999 );
         PRTP( "T", p->ClassTimes[i], p->timeEval );
     }
+*/
 }
 
 

src/aig/dar/module.make

 SRC +=    src/aig/dar/darBalance.c \
-    src/aig/dar/darCheck.c \
     src/aig/dar/darCore.c \
     src/aig/dar/darCut.c \
     src/aig/dar/darData.c \
-    src/aig/dar/darDfs.c \
     src/aig/dar/darLib.c \
     src/aig/dar/darMan.c \
-    src/aig/dar/darMem.c \
-    src/aig/dar/darObj.c \
-    src/aig/dar/darOper.c \
-    src/aig/dar/darSeq.c \
-    src/aig/dar/darTable.c \
-    src/aig/dar/darTruth.c \
-    src/aig/dar/darUtil.c 
+    src/aig/dar/darTruth.c

src/aig/fra/fra.h

@@ -36,6 +36,7 @@ extern "C" {
 #include <time.h>
 
 #include "vec.h"
+#include "aig.h"
 #include "dar.h"
 #include "satSolver.h"
 
@@ -73,8 +74,8 @@ struct Fra_Man_t_
     // high-level data    
     Fra_Par_t *      pPars;             // parameters governing fraiging
     // AIG managers
-    Dar_Man_t *      pManAig;           // the starting AIG manager
-    Dar_Man_t *      pManFraig;         // the final AIG manager
+    Aig_Man_t *      pManAig;           // the starting AIG manager
+    Aig_Man_t *      pManFraig;         // the final AIG manager
     // simulation info
     unsigned *       pSimWords;         // memory for simulation information
     int              nSimWords;         // the number of simulation words
@@ -86,8 +87,8 @@ struct Fra_Man_t_
     Vec_Ptr_t *      vClasses;          // equivalence classes
     Vec_Ptr_t *      vClasses1;         // equivalence class of Const1 node
     Vec_Ptr_t *      vClassesTemp;      // temporary storage for new classes
-    Dar_Obj_t **     pMemClasses;       // memory allocated for equivalence classes
-    Dar_Obj_t **     pMemClassesFree;   // memory allocated for equivalence classes to be used
+    Aig_Obj_t **     pMemClasses;       // memory allocated for equivalence classes
+    Aig_Obj_t **     pMemClassesFree;   // memory allocated for equivalence classes to be used
     Vec_Ptr_t *      vClassOld;         // old equivalence class after splitting
     Vec_Ptr_t *      vClassNew;         // new equivalence class(es) after splitting
     int              nPairs;            // the number of pairs of nodes
@@ -98,8 +99,8 @@ struct Fra_Man_t_
     sint64           nBTLimitGlobal;    // resource limit
     sint64           nInsLimitGlobal;   // resource limit
     // various data members
-    Dar_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
-    Dar_Obj_t **     pMemRepr;          // memory allocated for points to the node representatives
+    Aig_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
+    Aig_Obj_t **     pMemRepr;          // memory allocated for points to the node representatives
     Vec_Ptr_t **     pMemFanins;        // the arrays of fanins
     int *            pMemSatNums;       // the array of SAT numbers
     int              nSizeAlloc;        // allocated size of the arrays
@@ -135,21 +136,21 @@ struct Fra_Man_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline unsigned *   Fra_ObjSim( Dar_Obj_t * pObj )   { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id;  }
+static inline unsigned *   Fra_ObjSim( Aig_Obj_t * pObj )   { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id;  }
 static inline unsigned     Fra_ObjRandomSim()               { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
 
-static inline Dar_Obj_t *  Fra_ObjFraig( Dar_Obj_t * pObj )                              { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id];       }
-static inline Dar_Obj_t *  Fra_ObjRepr( Dar_Obj_t * pObj )                               { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id];        }
-static inline Vec_Ptr_t *  Fra_ObjFaninVec( Dar_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];      }
-static inline int          Fra_ObjSatNum( Dar_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];     }
+static inline Aig_Obj_t *  Fra_ObjFraig( Aig_Obj_t * pObj )                              { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id];       }
+static inline Aig_Obj_t *  Fra_ObjRepr( Aig_Obj_t * pObj )                               { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id];        }
+static inline Vec_Ptr_t *  Fra_ObjFaninVec( Aig_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];      }
+static inline int          Fra_ObjSatNum( Aig_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];     }
 
-static inline void         Fra_ObjSetFraig( Dar_Obj_t * pObj, Dar_Obj_t * pNode )        { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]   = pNode;    }
-static inline void         Fra_ObjSetRepr( Dar_Obj_t * pObj, Dar_Obj_t * pNode )         { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]    = pNode;    }
-static inline void         Fra_ObjSetFaninVec( Dar_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]  = vFanins;  }
-static inline void         Fra_ObjSetSatNum( Dar_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;      }
+static inline void         Fra_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode )        { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]   = pNode;    }
+static inline void         Fra_ObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode )         { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]    = pNode;    }
+static inline void         Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]  = vFanins;  }
+static inline void         Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;      }
 
-static inline Dar_Obj_t *  Fra_ObjChild0Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin0(pObj)), Dar_ObjFaninC0(pObj)) : NULL;  }
-static inline Dar_Obj_t *  Fra_ObjChild1Fra( Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond(Fra_ObjFraig(Dar_ObjFanin1(pObj)), Dar_ObjFaninC1(pObj)) : NULL;  }
+static inline Aig_Obj_t *  Fra_ObjChild0Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL;  }
+static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL;  }
 
 ////////////////////////////////////////////////////////////////////////
 ///                         ITERATORS                                ///
@@ -167,21 +168,21 @@ extern void                Fra_CreateClasses( Fra_Man_t * p );
 extern int                 Fra_RefineClasses( Fra_Man_t * p );
 extern int                 Fra_RefineClasses1( Fra_Man_t * p );
 /*=== fraCnf.c ========================================================*/
-extern void                Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
+extern void                Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== fraCore.c ========================================================*/
-extern Dar_Man_t *         Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pParams );
+extern Aig_Man_t *         Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pParams );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
-extern Fra_Man_t *         Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pParams );
+extern Fra_Man_t *         Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
 extern void                Fra_ManPrepare( Fra_Man_t * p );
 extern void                Fra_ManStop( Fra_Man_t * p );
 extern void                Fra_ManPrint( Fra_Man_t * p );
 /*=== fraSat.c ========================================================*/
-extern int                 Fra_NodesAreEquiv( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
-extern int                 Fra_NodeIsConst( Fra_Man_t * p, Dar_Obj_t * pNew );
+extern int                 Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
+extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
 /*=== fraSim.c ========================================================*/
-extern int                 Fra_NodeHasZeroSim( Fra_Man_t * p, Dar_Obj_t * pObj );
-extern int                 Fra_NodeCompareSims( Fra_Man_t * p, Dar_Obj_t * pObj0, Dar_Obj_t * pObj1 );
+extern int                 Fra_NodeHasZeroSim( Fra_Man_t * p, Aig_Obj_t * pObj );
+extern int                 Fra_NodeCompareSims( Fra_Man_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
 extern void                Fra_SavePattern( Fra_Man_t * p );
 extern void                Fra_Simulate( Fra_Man_t * p );
 extern void                Fra_Resimulate( Fra_Man_t * p );

src/aig/fra/fraAnd.c

@@ -40,48 +40,48 @@
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
+Aig_Obj_t * Fra_And( Fra_Man_t * p, Aig_Obj_t * pObjOld )
 { 
-    Dar_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig;
+    Aig_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig;
     int RetValue;
-    assert( !Dar_IsComplement(pObjOld) );
-    assert( Dar_ObjIsNode(pObjOld) );
+    assert( !Aig_IsComplement(pObjOld) );
+    assert( Aig_ObjIsNode(pObjOld) );
     // get the fraiged fanins
     pFanin0Fraig = Fra_ObjChild0Fra(pObjOld);
     pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
     // get the fraiged node
-    pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
-    if ( Dar_ObjIsConst1(Dar_Regular(pObjFraig)) )
+    pObjFraig = Aig_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
+    if ( Aig_ObjIsConst1(Aig_Regular(pObjFraig)) )
         return pObjFraig;
-    Dar_Regular(pObjFraig)->pData = p;
+    Aig_Regular(pObjFraig)->pData = p;
     // get representative of this class
     pObjOldRepr = Fra_ObjRepr(pObjOld);
     if ( pObjOldRepr == NULL || // this is a unique node
-       (!p->pPars->fDoSparse && pObjOldRepr == Dar_ManConst1(p->pManAig)) ) // this is a sparse node
+       (!p->pPars->fDoSparse && pObjOldRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node
     {
-        assert( Dar_Regular(pFanin0Fraig) != Dar_Regular(pFanin1Fraig) );
-        assert( Dar_Regular(pObjFraig) != Dar_Regular(pFanin0Fraig) );
-        assert( Dar_Regular(pObjFraig) != Dar_Regular(pFanin1Fraig) );
+        assert( Aig_Regular(pFanin0Fraig) != Aig_Regular(pFanin1Fraig) );
+        assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin0Fraig) );
+        assert( Aig_Regular(pObjFraig) != Aig_Regular(pFanin1Fraig) );
         return pObjFraig;
     }
     // get the fraiged representative
     pObjOldReprFraig = Fra_ObjFraig(pObjOldRepr);
     // if the fraiged nodes are the same, return
-    if ( Dar_Regular(pObjFraig) == Dar_Regular(pObjOldReprFraig) )
+    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjOldReprFraig) )
         return pObjFraig;
-    assert( Dar_Regular(pObjFraig) != Dar_ManConst1(p->pManFraig) );
+    assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
 //    printf( "Node = %d. Repr = %d.\n", pObjOld->Id, pObjOldRepr->Id );
 
     // if they are proved different, the c-ex will be in p->pPatWords
-    RetValue = Fra_NodesAreEquiv( p, Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) );
+    RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) );
     if ( RetValue == 1 )  // proved equivalent
     {
 //        pObjOld->fMarkA = 1;
-        return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
+        return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
     }
     if ( RetValue == -1 ) // failed
     {
-        Dar_Obj_t * ppNodes[2] = { Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) };
+        Aig_Obj_t * ppNodes[2] = { Aig_Regular(pObjOldReprFraig), Aig_Regular(pObjFraig) };
         Vec_Ptr_t * vNodes;
 
         if ( !p->pPars->fSpeculate )
@@ -90,11 +90,11 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
 //        pObjOld->fMarkB = 1;
         p->nSpeculs++;
 
-        vNodes = Dar_ManDfsNodes( p->pManFraig, ppNodes, 2 );
+        vNodes = Aig_ManDfsNodes( p->pManFraig, ppNodes, 2 );
         printf( "%d ", Vec_PtrSize(vNodes) );
         Vec_PtrFree( vNodes );
 
-        return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
+        return Aig_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
     }
 //    printf( "Disproved %d and %d.\n", pObjOldRepr->Id, pObjOld->Id );
     // simulate the counter-example and return the Fraig node
@@ -118,18 +118,18 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
 ***********************************************************************/
 void Fra_Sweep( Fra_Man_t * p )
 {
-    Dar_Obj_t * pObj, * pObjNew;
+    Aig_Obj_t * pObj, * pObjNew;
     int i, k = 0;
 p->nClassesZero = Vec_PtrSize(p->vClasses1);
 p->nClassesBeg  = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
     // duplicate internal nodes
-//    p->pProgress = Extra_ProgressBarStart( stdout, Dar_ManNodeNum(p->pManAig) );
-    Dar_ManForEachNode( p->pManAig, pObj, i )
+//    p->pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p->pManAig) );
+    Aig_ManForEachNode( p->pManAig, pObj, i )
     {
 //        Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
         // default to simple strashing if simulation detected a counter-example for a PO
         if ( p->pManFraig->pData )
-            pObjNew = Dar_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
+            pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
         else
             pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented
         Fra_ObjSetFraig( pObj, pObjNew );
@@ -138,15 +138,15 @@ p->nClassesBeg  = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0
 //    Extra_ProgressBarStop( p->pProgress );
 p->nClassesEnd = Vec_PtrSize(p->vClasses) + (int)(Vec_PtrSize(p->vClasses1) > 0);
     // try to prove the outputs of the miter
-    p->nNodesMiter = Dar_ManNodeNum(p->pManFraig);
+    p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
 //    Fra_MiterStatus( p->pManFraig );
 //    if ( p->pPars->fProve && p->pManFraig->pData == NULL )
 //        Fra_MiterProve( p );
     // add the POs
-    Dar_ManForEachPo( p->pManAig, pObj, i )
-        Dar_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) );
+    Aig_ManForEachPo( p->pManAig, pObj, i )
+        Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) );
     // remove dangling nodes 
-    Dar_ManCleanup( p->pManFraig );
+    Aig_ManCleanup( p->pManFraig );
 }
 
 ////////////////////////////////////////////////////////////////////////

src/aig/fra/fraClass.c

@@ -36,8 +36,8 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline Dar_Obj_t *  Fra_ObjNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pObj )                       { return ppNexts[pObj->Id];  }
-static inline void         Fra_ObjSetNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pObj, Dar_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
+static inline Aig_Obj_t *  Fra_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj )                       { return ppNexts[pObj->Id];  }
+static inline void         Fra_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -54,9 +54,9 @@ static inline void         Fra_ObjSetNext( Dar_Obj_t ** ppNexts, Dar_Obj_t * pOb
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_PrintClass( Dar_Obj_t ** pClass )
+void Fra_PrintClass( Aig_Obj_t ** pClass )
 {
-    Dar_Obj_t * pTemp;
+    Aig_Obj_t * pTemp;
     int i;
     printf( "{ " );
     for ( i = 0; pTemp = pClass[i]; i++ )
@@ -75,9 +75,9 @@ void Fra_PrintClass( Dar_Obj_t ** pClass )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_CountClass( Dar_Obj_t ** pClass )
+int Fra_CountClass( Aig_Obj_t ** pClass )
 {
-    Dar_Obj_t * pTemp;
+    Aig_Obj_t * pTemp;
     int i;
     for ( i = 0; pTemp = pClass[i]; i++ );
     return i;
@@ -96,7 +96,7 @@ int Fra_CountClass( Dar_Obj_t ** pClass )
 ***********************************************************************/
 int Fra_CountPairsClasses( Fra_Man_t * p )
 {
-    Dar_Obj_t ** pClass;
+    Aig_Obj_t ** pClass;
     int i, nNodes, nPairs = 0;
     Vec_PtrForEachEntry( p->vClasses, pClass, i )
     {
@@ -120,7 +120,7 @@ int Fra_CountPairsClasses( Fra_Man_t * p )
 ***********************************************************************/
 void Fra_PrintClasses( Fra_Man_t * p )
 {
-    Dar_Obj_t ** pClass;
+    Aig_Obj_t ** pClass;
     int i;
     printf( "Total classes = %d. Total pairs = %d.\n", Vec_PtrSize(p->vClasses), Fra_CountPairsClasses(p) );
     Vec_PtrForEachEntry( p->vClasses, pClass, i )
@@ -142,7 +142,7 @@ void Fra_PrintClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned Fra_NodeHash( Fra_Man_t * p, Dar_Obj_t * pObj )
+unsigned Fra_NodeHash( Fra_Man_t * p, Aig_Obj_t * pObj )
 {
     static int s_FPrimes[128] = { 
         1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
@@ -220,21 +220,21 @@ unsigned int Cudd_PrimeFra( unsigned int p )
 ***********************************************************************/
 void Fra_CreateClasses( Fra_Man_t * p )
 {
-    Dar_Obj_t ** ppTable, ** ppNexts;
-    Dar_Obj_t * pObj, * pTemp;
+    Aig_Obj_t ** ppTable, ** ppNexts;
+    Aig_Obj_t * pObj, * pTemp;
     int i, k, nTableSize, nEntries, nNodes, iEntry;
 
     // allocate the hash table hashing simulation info into nodes
-    nTableSize = Cudd_PrimeFra( Dar_ManObjIdMax(p->pManAig) + 1 );
-    ppTable = ALLOC( Dar_Obj_t *, nTableSize ); 
-    ppNexts = ALLOC( Dar_Obj_t *, nTableSize ); 
-    memset( ppTable, 0, sizeof(Dar_Obj_t *) * nTableSize );
+    nTableSize = Cudd_PrimeFra( Aig_ManObjIdMax(p->pManAig) + 1 );
+    ppTable = ALLOC( Aig_Obj_t *, nTableSize ); 
+    ppNexts = ALLOC( Aig_Obj_t *, nTableSize ); 
+    memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
 
     // add all the nodes to the hash table
     Vec_PtrClear( p->vClasses1 );
-    Dar_ManForEachObj( p->pManAig, pObj, i )
+    Aig_ManForEachObj( p->pManAig, pObj, i )
     {
-        if ( !Dar_ObjIsNode(pObj) && !Dar_ObjIsPi(pObj) )
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
             continue;
         // hash the node by its simulation info
         iEntry = Fra_NodeHash( p, pObj ) % nTableSize;
@@ -242,7 +242,7 @@ void Fra_CreateClasses( Fra_Man_t * p )
         if ( iEntry == 0 && Fra_NodeHasZeroSim( p, pObj ) )
         {
             Vec_PtrPush( p->vClasses1, pObj );
-            Fra_ObjSetRepr( pObj, Dar_ManConst1(p->pManAig) );
+            Fra_ObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
             continue;
         }
         // add the node to the class
@@ -275,15 +275,15 @@ void Fra_CreateClasses( Fra_Man_t * p )
         }
 
     // allocate room for classes
-    p->pMemClasses = ALLOC( Dar_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
+    p->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
     p->pMemClassesFree = p->pMemClasses + 2*nEntries;
 
     // copy the entries into storage in the topological order
     Vec_PtrClear( p->vClasses );
     nEntries = 0;
-    Dar_ManForEachObj( p->pManAig, pObj, i )
+    Aig_ManForEachObj( p->pManAig, pObj, i )
     {
-        if ( !Dar_ObjIsNode(pObj) && !Dar_ObjIsPi(pObj) )
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
             continue;
         // skip the nodes that are not representatives of non-trivial classes
         if ( pObj->fMarkA == 0 )
@@ -307,7 +307,7 @@ void Fra_CreateClasses( Fra_Man_t * p )
             Fra_ObjSetRepr( pTemp, pObj );
         }
         // add as many empty entries
-//        memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Dar_Obj_t *) * nNodes );
+//        memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Aig_Obj_t *) * nNodes );
         p->pMemClasses[2*nEntries + nNodes] = NULL;
         // increment the number of entries
         nEntries += k;
@@ -329,9 +329,9 @@ void Fra_CreateClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass )
+Aig_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Aig_Obj_t ** ppClass )
 {
-    Dar_Obj_t * pObj, ** ppThis;
+    Aig_Obj_t * pObj, ** ppThis;
     int i;
     assert( ppClass[0] != NULL && ppClass[1] != NULL );
 
@@ -390,7 +390,7 @@ Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass )
 ***********************************************************************/
 int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses )
 {
-    Dar_Obj_t ** pClass, ** pClass2;
+    Aig_Obj_t ** pClass, ** pClass2;
     int nRefis;
     pClass = Vec_PtrEntryLast( vClasses );
     for ( nRefis = 0; pClass2 = Fra_RefineClassOne( p, pClass ); nRefis++ )
@@ -426,7 +426,7 @@ int Fra_RefineClassLastIter( Fra_Man_t * p, Vec_Ptr_t * vClasses )
 int Fra_RefineClasses( Fra_Man_t * p )
 {
     Vec_Ptr_t * vTemp;
-    Dar_Obj_t ** pClass;
+    Aig_Obj_t ** pClass;
     int clk, i, nRefis;
     // check if some outputs already became non-constant
     // this is a special case when computation can be stopped!!!
@@ -466,14 +466,14 @@ p->timeRef += clock() - clk;
 ***********************************************************************/
 int Fra_RefineClasses1( Fra_Man_t * p )
 {
-    Dar_Obj_t * pObj, ** ppClass;
+    Aig_Obj_t * pObj, ** ppClass;
     int i, k, nRefis, clk;
     // check if there is anything to refine
     if ( Vec_PtrSize(p->vClasses1) == 0 )
         return 0;
 clk = clock();
     // make sure constant 1 class contains only non-constant nodes
-    assert( Vec_PtrEntry(p->vClasses1,0) != Dar_ManConst1(p->pManAig) );
+    assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pManAig) );
     // collect all the nodes to be refined
     k = 0;
     Vec_PtrClear( p->vClassNew );

src/aig/fra/fraCnf.c

@@ -40,23 +40,23 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_AddClausesMux( Fra_Man_t * p, Dar_Obj_t * pNode )
+void Fra_AddClausesMux( Fra_Man_t * p, Aig_Obj_t * pNode )
 {
-    Dar_Obj_t * pNodeI, * pNodeT, * pNodeE;
+    Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
     int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
 
-    assert( !Dar_IsComplement( pNode ) );
-    assert( Dar_ObjIsMuxType( pNode ) );
+    assert( !Aig_IsComplement( pNode ) );
+    assert( Aig_ObjIsMuxType( pNode ) );
     // get nodes (I = if, T = then, E = else)
-    pNodeI = Dar_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
+    pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
     // get the variable numbers
     VarF = Fra_ObjSatNum(pNode);
     VarI = Fra_ObjSatNum(pNodeI);
-    VarT = Fra_ObjSatNum(Dar_Regular(pNodeT));
-    VarE = Fra_ObjSatNum(Dar_Regular(pNodeE));
+    VarT = Fra_ObjSatNum(Aig_Regular(pNodeT));
+    VarE = Fra_ObjSatNum(Aig_Regular(pNodeE));
     // get the complementation flags
-    fCompT = Dar_IsComplement(pNodeT);
-    fCompE = Dar_IsComplement(pNodeE);
+    fCompT = Aig_IsComplement(pNodeT);
+    fCompE = Aig_IsComplement(pNodeE);
 
     // f = ITE(i, t, e)
 
@@ -123,12 +123,12 @@ void Fra_AddClausesMux( Fra_Man_t * p, Dar_Obj_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_AddClausesSuper( Fra_Man_t * p, Dar_Obj_t * pNode, Vec_Ptr_t * vSuper )
+void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
 {
-    Dar_Obj_t * pFanin;
+    Aig_Obj_t * pFanin;
     int * pLits, nLits, RetValue, i;
-    assert( !Dar_IsComplement(pNode) );
-    assert( Dar_ObjIsNode( pNode ) );
+    assert( !Aig_IsComplement(pNode) );
+    assert( Aig_ObjIsNode( pNode ) );
     // create storage for literals
     nLits = Vec_PtrSize(vSuper) + 1;
     pLits = ALLOC( int, nLits );
@@ -136,14 +136,14 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Dar_Obj_t * pNode, Vec_Ptr_t * vSuper )
     // add !A => !C   or   A + !C
     Vec_PtrForEachEntry( vSuper, pFanin, i )
     {
-        pLits[0] = toLitCond(Fra_ObjSatNum(Dar_Regular(pFanin)), Dar_IsComplement(pFanin));
+        pLits[0] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
         pLits[1] = toLitCond(Fra_ObjSatNum(pNode), 1);
         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
         assert( RetValue );
     }
     // add A & B => C   or   !A + !B + C
     Vec_PtrForEachEntry( vSuper, pFanin, i )
-        pLits[i] = toLitCond(Fra_ObjSatNum(Dar_Regular(pFanin)), !Dar_IsComplement(pFanin));
+        pLits[i] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
     pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0);
     RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
     assert( RetValue );
@@ -161,18 +161,18 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Dar_Obj_t * pNode, Vec_Ptr_t * vSuper )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_CollectSuper_rec( Dar_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
+void Fra_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
 {
     // if the new node is complemented or a PI, another gate begins
-    if ( Dar_IsComplement(pObj) || Dar_ObjIsPi(pObj) || (!fFirst && Dar_ObjRefs(pObj) > 1) || 
-         (fUseMuxes && Dar_ObjIsMuxType(pObj)) )
+    if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || 
+         (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
     {
         Vec_PtrPushUnique( vSuper, pObj );
         return;
     }
     // go through the branches
-    Fra_CollectSuper_rec( Dar_ObjChild0(pObj), vSuper, 0, fUseMuxes );
-    Fra_CollectSuper_rec( Dar_ObjChild1(pObj), vSuper, 0, fUseMuxes );
+    Fra_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
+    Fra_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
 }
 
 /**Function*************************************************************
@@ -186,11 +186,11 @@ void Fra_CollectSuper_rec( Dar_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Fra_CollectSuper( Dar_Obj_t * pObj, int fUseMuxes )
+Vec_Ptr_t * Fra_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes )
 {
     Vec_Ptr_t * vSuper;
-    assert( !Dar_IsComplement(pObj) );
-    assert( !Dar_ObjIsPi(pObj) );
+    assert( !Aig_IsComplement(pObj) );
+    assert( !Aig_ObjIsPi(pObj) );
     vSuper = Vec_PtrAlloc( 4 );
     Fra_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
     return vSuper;
@@ -207,19 +207,19 @@ Vec_Ptr_t * Fra_CollectSuper( Dar_Obj_t * pObj, int fUseMuxes )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_ObjAddToFrontier( Fra_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+void Fra_ObjAddToFrontier( Fra_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
 {
     Fra_Man_t * pTemp = pObj->pData;
-    assert( !Dar_IsComplement(pObj) );
+    assert( !Aig_IsComplement(pObj) );
     if ( Fra_ObjSatNum(pObj) )
         return;
     assert( Fra_ObjSatNum(pObj) == 0 );
     assert( Fra_ObjFaninVec(pObj) == NULL );
-    if ( Dar_ObjIsConst1(pObj) )
+    if ( Aig_ObjIsConst1(pObj) )
         return;
 //printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars );
     Fra_ObjSetSatNum( pObj, p->nSatVars++ );
-    if ( Dar_ObjIsNode(pObj) )
+    if ( Aig_ObjIsNode(pObj) )
         Vec_PtrPush( vFrontier, pObj );
 }
 
@@ -234,10 +234,10 @@ void Fra_ObjAddToFrontier( Fra_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vFrontie
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
+void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 { 
     Vec_Ptr_t * vFrontier, * vFanins;
-    Dar_Obj_t * pNode, * pFanin;
+    Aig_Obj_t * pNode, * pFanin;
     int i, k, fUseMuxes = 1;
     assert( pOld || pNew );
     // quit if CNF is ready
@@ -253,22 +253,22 @@ void Fra_NodeAddToSolver( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
         // create the supergate
         assert( Fra_ObjSatNum(pNode) );
         assert( Fra_ObjFaninVec(pNode) == NULL );
-        if ( fUseMuxes && Dar_ObjIsMuxType(pNode) )
+        if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
         {
             vFanins = Vec_PtrAlloc( 4 );
-            Vec_PtrPushUnique( vFanins, Dar_ObjFanin0( Dar_ObjFanin0(pNode) ) );
-            Vec_PtrPushUnique( vFanins, Dar_ObjFanin0( Dar_ObjFanin1(pNode) ) );
-            Vec_PtrPushUnique( vFanins, Dar_ObjFanin1( Dar_ObjFanin0(pNode) ) );
-            Vec_PtrPushUnique( vFanins, Dar_ObjFanin1( Dar_ObjFanin1(pNode) ) );
+            Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
+            Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
+            Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
+            Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
             Vec_PtrForEachEntry( vFanins, pFanin, k )
-                Fra_ObjAddToFrontier( p, Dar_Regular(pFanin), vFrontier );
+                Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
             Fra_AddClausesMux( p, pNode );
         }
         else
         {
             vFanins = Fra_CollectSuper( pNode, fUseMuxes );
             Vec_PtrForEachEntry( vFanins, pFanin, k )
-                Fra_ObjAddToFrontier( p, Dar_Regular(pFanin), vFrontier );
+                Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
             Fra_AddClausesSuper( p, pNode, vFanins );
         }
         assert( Vec_PtrSize(vFanins) > 1 );

src/aig/fra/fraCore.c

@@ -39,15 +39,15 @@
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Man_t * Fra_Perform( Dar_Man_t * pManAig, Fra_Par_t * pPars )
+Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
 {
     Fra_Man_t * p;
-    Dar_Man_t * pManAigNew;
+    Aig_Man_t * pManAigNew;
     int clk;
-    if ( Dar_ManNodeNum(pManAig) == 0 )
-        return Dar_ManDup(pManAig);
+    if ( Aig_ManNodeNum(pManAig) == 0 )
+        return Aig_ManDup(pManAig);
 clk = clock();
-    assert( Dar_ManLatchNum(pManAig) == 0 );
+    assert( Aig_ManLatchNum(pManAig) == 0 );
     p = Fra_ManStart( pManAig, pPars );
     Fra_Simulate( p );
     Fra_Sweep( p );

src/aig/fra/fraMan.c

@@ -66,7 +66,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
+Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
 {
     Fra_Man_t * p;
     // allocate the fraiging manager
@@ -74,15 +74,15 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
     memset( p, 0, sizeof(Fra_Man_t) );
     p->pPars      = pPars;
     p->pManAig    = pManAig;
-    p->pManFraig  = Dar_ManStartFrom( pManAig );
-    assert( Dar_ManPiNum(p->pManAig) == Dar_ManPiNum(p->pManFraig) );
+    p->pManFraig  = Aig_ManStartFrom( pManAig );
+    assert( Aig_ManPiNum(p->pManAig) == Aig_ManPiNum(p->pManFraig) );
     // allocate simulation info
     p->nSimWords  = pPars->nSimWords;
-    p->pSimWords  = ALLOC( unsigned, (Dar_ManObjIdMax(pManAig) + 1) * p->nSimWords );
+    p->pSimWords  = ALLOC( unsigned, (Aig_ManObjIdMax(pManAig) + 1) * p->nSimWords );
     // clean simulation info of the constant node
-    memset( p->pSimWords, 0, sizeof(unsigned) * ((Dar_ManPiNum(pManAig) + 1) * p->nSimWords) );
+    memset( p->pSimWords, 0, sizeof(unsigned) * ((Aig_ManPiNum(pManAig) + 1) * p->nSimWords) );
     // allocate storage for sim pattern
-    p->nPatWords  = Dar_BitWordNum( Dar_ManPiNum(pManAig) );
+    p->nPatWords  = Aig_BitWordNum( Aig_ManPiNum(pManAig) );
     p->pPatWords  = ALLOC( unsigned, p->nPatWords ); 
     p->pPatScores = ALLOC( int, 32 * p->nSimWords ); 
     p->vPiVars    = Vec_PtrAlloc( 100 );
@@ -92,11 +92,11 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
     p->vClassNew  = Vec_PtrAlloc( 100 );
     p->vClassesTemp = Vec_PtrAlloc( 100 );
     // allocate other members
-    p->nSizeAlloc = Dar_ManObjIdMax(pManAig) + 1;
-    p->pMemFraig  = ALLOC( Dar_Obj_t *, p->nSizeAlloc );
-    memset( p->pMemFraig, 0, p->nSizeAlloc * sizeof(Dar_Obj_t *) );
-    p->pMemRepr  = ALLOC( Dar_Obj_t *, p->nSizeAlloc );
-    memset( p->pMemRepr, 0, p->nSizeAlloc * sizeof(Dar_Obj_t *) );
+    p->nSizeAlloc = Aig_ManObjIdMax(pManAig) + 1;
+    p->pMemFraig  = ALLOC( Aig_Obj_t *, p->nSizeAlloc );
+    memset( p->pMemFraig, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
+    p->pMemRepr  = ALLOC( Aig_Obj_t *, p->nSizeAlloc );
+    memset( p->pMemRepr, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
     p->pMemFanins  = ALLOC( Vec_Ptr_t *, p->nSizeAlloc );
     memset( p->pMemFanins, 0, p->nSizeAlloc * sizeof(Vec_Ptr_t *) );
     p->pMemSatNums  = ALLOC( int, p->nSizeAlloc );
@@ -123,18 +123,18 @@ Fra_Man_t * Fra_ManStart( Dar_Man_t * pManAig, Fra_Par_t * pPars )
 ***********************************************************************/
 void Fra_ManPrepare( Fra_Man_t * p )
 {
-    Dar_Obj_t * pObj;
+    Aig_Obj_t * pObj;
     int i;
     // set the pointers to the manager
-    Dar_ManForEachObj( p->pManFraig, pObj, i )
+    Aig_ManForEachObj( p->pManFraig, pObj, i )
         pObj->pData = p;
     // set the pointer to the manager
-    Dar_ManForEachObj( p->pManAig, pObj, i )
+    Aig_ManForEachObj( p->pManAig, pObj, i )
         pObj->pData = p;
     // set the pointers to the available fraig nodes
-    Fra_ObjSetFraig( Dar_ManConst1(p->pManAig), Dar_ManConst1(p->pManFraig) );
-    Dar_ManForEachPi( p->pManAig, pObj, i )
-        Fra_ObjSetFraig( pObj, Dar_ManPi(p->pManFraig, i) );
+    Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), Aig_ManConst1(p->pManFraig) );
+    Aig_ManForEachPi( p->pManAig, pObj, i )
+        Fra_ObjSetFraig( pObj, Aig_ManPi(p->pManFraig, i) );
 }
 
 /**Function*************************************************************
@@ -187,14 +187,14 @@ void Fra_ManStop( Fra_Man_t * p )
 ***********************************************************************/
 void Fra_ManPrint( Fra_Man_t * p )
 {
-    double nMemory = 1.0*Dar_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
+    double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
     printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb.  ", p->nSimWords, p->nSimRounds, nMemory );
     printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
     printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pPars->nBTLimitNode, p->pPars->nBTLimitMiter );
     printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 
         p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
     printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", 
-        Dar_ManNodeNum(p->pManFraig), p->nNodesMiter, Dar_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
+        Aig_ManNodeNum(p->pManFraig), p->nNodesMiter, Aig_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
     if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
     PRT( "AIG simulation  ", p->timeSim  );
     PRT( "AIG traversal   ", p->timeTrav  );

src/aig/fra/fraSat.c

@@ -24,7 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew );
+static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -41,13 +41,13 @@ static int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t *
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_NodesAreEquiv( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
+int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
     int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
 
     // make sure the nodes are not complemented
-    assert( !Dar_IsComplement(pNew) );
-    assert( !Dar_IsComplement(pOld) );
+    assert( !Aig_IsComplement(pNew) );
+    assert( !Aig_IsComplement(pOld) );
     assert( pNew != pOld );
 
     // if at least one of the nodes is a failed node, perform adjustments:
@@ -189,12 +189,12 @@ p->timeSatFail += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_NodeIsConst( Fra_Man_t * p, Dar_Obj_t * pNew )
+int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
 {
     int pLits[2], RetValue1, RetValue, clk;
 
     // make sure the nodes are not complemented
-    assert( !Dar_IsComplement(pNew) );
+    assert( !Aig_IsComplement(pNew) );
     assert( pNew != p->pManFraig->pConst1 );
     p->nSatCalls++;
 
@@ -261,19 +261,19 @@ p->timeSatFail += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_SetActivityFactors_rec( Fra_Man_t * p, Dar_Obj_t * pObj, int LevelMin, int LevelMax )
+int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, int LevelMax )
 {
     Vec_Ptr_t * vFanins;
-    Dar_Obj_t * pFanin;
+    Aig_Obj_t * pFanin;
     int i, Counter = 0;
-    assert( !Dar_IsComplement(pObj) );
+    assert( !Aig_IsComplement(pObj) );
     assert( Fra_ObjSatNum(pObj) );
     // skip visited variables
-    if ( Dar_ObjIsTravIdCurrent(p->pManFraig, pObj) )
+    if ( Aig_ObjIsTravIdCurrent(p->pManFraig, pObj) )
         return 0;
-    Dar_ObjSetTravIdCurrent(p->pManFraig, pObj);
+    Aig_ObjSetTravIdCurrent(p->pManFraig, pObj);
     // add the PI to the list
-    if ( pObj->Level <= (unsigned)LevelMin || Dar_ObjIsPi(pObj) )
+    if ( pObj->Level <= (unsigned)LevelMin || Aig_ObjIsPi(pObj) )
         return 0;
     // set the factor of this variable
     // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump
@@ -282,7 +282,7 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Dar_Obj_t * pObj, int LevelMin, i
     // explore the fanins
     vFanins = Fra_ObjFaninVec( pObj );
     Vec_PtrForEachEntry( vFanins, pFanin, i )
-        Counter += Fra_SetActivityFactors_rec( p, Dar_Regular(pFanin), LevelMin, LevelMax );
+        Counter += Fra_SetActivityFactors_rec( p, Aig_Regular(pFanin), LevelMin, LevelMax );
     return 1 + Counter;
 }
 
@@ -297,7 +297,7 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Dar_Obj_t * pObj, int LevelMin, i
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_SetActivityFactors( Fra_Man_t * p, Dar_Obj_t * pOld, Dar_Obj_t * pNew )
+int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
     int clk, LevelMin, LevelMax;
     assert( pOld || pNew );
@@ -305,15 +305,15 @@ clk = clock();
     // reset the active variables
     veci_resize(&p->pSat->act_vars, 0);
     // prepare for traversal
-    Dar_ManIncrementTravId( p->pManFraig );
+    Aig_ManIncrementTravId( p->pManFraig );
     // determine the min and max level to visit
     assert( p->pPars->dActConeRatio > 0 && p->pPars->dActConeRatio < 1 );
-    LevelMax = DAR_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
+    LevelMax = AIG_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
     LevelMin = (int)(LevelMax * (1.0 - p->pPars->dActConeRatio));
     // traverse
-    if ( pOld && !Dar_ObjIsConst1(pOld) )
+    if ( pOld && !Aig_ObjIsConst1(pOld) )
         Fra_SetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
-    if ( pNew && !Dar_ObjIsConst1(pNew) )
+    if ( pNew && !Aig_ObjIsConst1(pNew) )
         Fra_SetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
 //Fra_PrintActivity( p );
 p->timeTrav += clock() - clk;

src/aig/kit/module.make

+SRC +=  src/aig/kit/kitBdd.c \
+    src/aig/kit/kitDsd.c \
+    src/aig/kit/kitFactor.c \
+    src/aig/kit/kitGraph.c \
+    src/aig/kit/kitHop.c \
+    src/aig/kit/kitIsop.c \
+    src/aig/kit/kitSop.c \
+    src/aig/kit/kitTruth.c

src/base/abci/abc.c

@@ -27,6 +27,8 @@
 #include "if.h"
 #include "res.h"
 #include "lpk.h"
+#include "aig.h"
+#include "dar.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -108,6 +110,7 @@ static int Abc_CommandQuaReach       ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandIStrash        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandICut           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIRewrite       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDRewrite       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIRewriteSeq    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIResyn         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandISat           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -265,6 +268,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "istrash",       Abc_CommandIStrash,          1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "icut",          Abc_CommandICut,             0 );
     Cmd_CommandAdd( pAbc, "New AIG",      "irw",           Abc_CommandIRewrite,         1 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "drw",           Abc_CommandDRewrite,         1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "irws",          Abc_CommandIRewriteSeq,      1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "iresyn",        Abc_CommandIResyn,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "isat",          Abc_CommandISat,             1 );
@@ -337,7 +341,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
     {
         extern void Dar_LibStart();
-//        Dar_LibStart();
+        Dar_LibStart();
     }
 } 
 
@@ -354,13 +358,16 @@ void Abc_Init( Abc_Frame_t * pAbc )
 ***********************************************************************/
 void Abc_End()
 {
+//    Dar_LibDumpPriorities();
+
     {
         extern void Dar_LibStop();
-//        Dar_LibStop();
+        Dar_LibStop();
     }
 
     Abc_NtkFraigStoreClean();
 //    Rwt_Man4ExplorePrint();
+
 }
 
 /**Function*************************************************************
@@ -6081,14 +6088,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    Abc_Ntk4VarTable( pNtk );
 //    Dar_NtkGenerateArrays( pNtk );
 //    Dar_ManDeriveCnfTest2();
-/*
+
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         fprintf( pErr, "Network should be strashed. Command has failed.\n" );
         return 1;
     }
-*/
-//    pNtkRes = Abc_NtkDar( pNtk );
+    pNtkRes = Abc_NtkDar( pNtk );
 //    pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" );
     pNtkRes = NULL;
     if ( pNtkRes == NULL )
@@ -6609,6 +6615,105 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    Dar_Par_t Pars, * pPars = &Pars;
+    int c;
+
+    extern Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_Par_t * pPars );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Dar_ManDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CNlzvwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nCutsMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nCutsMax < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nSubgMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nSubgMax < 0 ) 
+                goto usage;
+            break;
+        case 'l':
+            pPars->fUpdateLevel ^= 1;
+            break;
+        case 'z':
+            pPars->fUseZeros ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'w':
+            pPars->fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    pNtkRes = Abc_NtkDRewrite( pNtk, pPars );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: drw [-C num] [-N num] [-lzvwh]\n" );
+    fprintf( pErr, "\t         perform combinational AIG rewriting\n" );
+    fprintf( pErr, "\t-C num : limit on the number of cuts at a node [default = %d]\n", pPars->nCutsMax );
+    fprintf( pErr, "\t-N num : limit on the number of subgraphs tried [default = %d]\n", pPars->nSubgMax );
+    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", pPars->fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", pPars->fUseZeros? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-w     : toggle very verbose printout [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandIRewriteSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -7023,7 +7128,7 @@ int Abc_CommandCSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     nCutsMax  =  8;  
-    nLeafMax  =  8;
+    nLeafMax  =  6;
     fVerbose  =  0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "CKvh" ) ) != EOF )
@@ -7067,6 +7172,18 @@ int Abc_CommandCSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    if ( nCutsMax < 2 )
+    {
+        fprintf( pErr, "The number of cuts cannot be less than 2.\n" );
+        return 1;
+    }
+
+    if ( nLeafMax < 3 || nLeafMax > 16 )
+    {
+        fprintf( pErr, "The number of leaves is infeasible.\n" );
+        return 1;
+    }
+
     pNtkRes = Abc_NtkCSweep( pNtk, nCutsMax, nLeafMax, fVerbose );
     if ( pNtkRes == NULL )
     {
@@ -7080,8 +7197,8 @@ int Abc_CommandCSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: csweep [-C num] [-K num] [-vh]\n" );
     fprintf( pErr, "\t         performs cut sweeping using a new method\n" );
-    fprintf( pErr, "\t-C num : limit on the number of cuts [default = %d]\n", nCutsMax );
-    fprintf( pErr, "\t-K num : limit on the cut size [default = %d]\n", nLeafMax );
+    fprintf( pErr, "\t-C num : limit on the number of cuts (C >= 2) [default = %d]\n", nCutsMax );
+    fprintf( pErr, "\t-K num : limit on the cut size (3 <= K <= 16) [default = %d]\n", nLeafMax );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;

src/map/if/ifCut.c

@@ -76,6 +76,7 @@ static inline int If_CutCheckEquality( If_Cut_t * pDom, If_Cut_t * pCut )
             return 0;
     return 1;
 }
+
 /**Function*************************************************************
 
   Synopsis    [Returns 1 if the cut is contained.]

src/opt/bdc/module.make

-SRC +=  src/opt/res/resCore.c \
-    src/opt/res/resDivs.c \
-    src/opt/res/resFilter.c \
-    src/opt/res/resSat.c \
-    src/opt/res/resSim.c \
-    src/opt/res/resStrash.c \
-    src/opt/res/resUpdate.c \
-    src/opt/res/resWin.c

src/opt/kit/module.make

-SRC +=  src/opt/kit/kitBdd.c \
-    src/opt/kit/kitDsd.c \
-    src/opt/kit/kitFactor.c \
-    src/opt/kit/kitGraph.c \
-    src/opt/kit/kitHop.c \
-    src/opt/kit/kitIsop.c \
-    src/opt/kit/kitSop.c \
-    src/opt/kit/kitTruth.c

src/opt/rwr/rwrEva.c

@@ -56,13 +56,13 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
 {
     int fVeryVerbose = 0;
     Dec_Graph_t * pGraph;
-    Cut_Cut_t * pCut;
+    Cut_Cut_t * pCut;//, * pTemp;
     Abc_Obj_t * pFanin;
     unsigned uPhase, uTruthBest, uTruth;
     char * pPerm;
     int Required, nNodesSaved, nNodesSaveCur;
     int i, GainCur, GainBest = -1;
-    int clk, clk2;
+    int clk, clk2;//, Counter;
 
     p->nNodesConsidered++;
     // get the required times
@@ -75,7 +75,12 @@ clk = clock();
 p->timeCut += clock() - clk;
 
 //printf( " %d", Rwr_CutCountNumNodes(pNode, pCut) );
-
+/*
+    Counter = 0;
+    for ( pTemp = pCut->pNext; pTemp; pTemp = pTemp->pNext )
+        Counter++;
+    printf( "%d ", Counter );
+*/
     // go through the cuts
 clk = clock();
     for ( pCut = pCut->pNext; pCut; pCut = pCut->pNext )