Added recording of AIG subgraphs.

src/aig/kit/kitTruth.c

@@ -1658,20 +1658,20 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
 {
 //    short pStore2[32];
     unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
-//    int nWords = Kit_TruthWordNum( nVars );
-    int i, Temp, fChange, Counter;//, nOnes;//, k, j, w, Limit;
+    int nWords = Kit_TruthWordNum( nVars );
+    int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
     unsigned uCanonPhase;
 
     // canonicize output
     uCanonPhase = 0;
-/*
+
     nOnes = Kit_TruthCountOnes(pIn, nVars);
     if ( (nOnes > nWords * 16) )//|| ((nOnes == nWords * 16) && (pIn[0] & 1)) )
     {
         uCanonPhase |= (1 << nVars);
         Kit_TruthNot( pIn, pIn, nVars );
     }
-*/
+
     // collect the minterm counts
     Kit_TruthCountOnesInCofs( pIn, nVars, pStore );
 /*
@@ -1698,7 +1698,6 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
 
     // permute
     Counter = 0;
-
     do {
         fChange = 0;
         for ( i = 0; i < nVars-1; i++ )
@@ -1721,11 +1720,11 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
             pStore[2*(i+1)+1] = Temp;
 
             // if the polarity of variables is different, swap them
-//            if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
-//            {
-//                uCanonPhase ^= (1 << i);
-//                uCanonPhase ^= (1 << (i+1));
-//            }
+            if ( ((uCanonPhase & (1 << i)) > 0) != ((uCanonPhase & (1 << (i+1))) > 0) )
+            {
+                uCanonPhase ^= (1 << i);
+                uCanonPhase ^= (1 << (i+1));
+            }
 
             Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
             pTemp = pIn; pIn = pOut; pOut = pTemp;

src/base/abci/abc.c

@@ -206,11 +206,11 @@ static int Abc_CommandFraigDress             ( Abc_Frame_t * pAbc, int argc, cha
 //static int Abc_CommandHaigStop               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandHaigUse                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
-//static int Abc_CommandRecStart               ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandRecStop                ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandRecAdd                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandRecPs                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandRecUse                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecStart               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecStop                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecAdd                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecPs                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecUse                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandMap                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAmap                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -662,11 +662,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
 //    Cmd_CommandAdd( pAbc, "Choicing",     "haig_stop",     Abc_CommandHaigStop,         0 );
 //    Cmd_CommandAdd( pAbc, "Choicing",     "haig_use",      Abc_CommandHaigUse,          1 );
 
-//    Cmd_CommandAdd( pAbc, "Choicing",     "rec_start",     Abc_CommandRecStart,         0 );
-//    Cmd_CommandAdd( pAbc, "Choicing",     "rec_stop",      Abc_CommandRecStop,          0 );
-//    Cmd_CommandAdd( pAbc, "Choicing",     "rec_add",       Abc_CommandRecAdd,           0 );
-//    Cmd_CommandAdd( pAbc, "Choicing",     "rec_ps",        Abc_CommandRecPs,            0 );
-//    Cmd_CommandAdd( pAbc, "Choicing",     "rec_use",       Abc_CommandRecUse,           1 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_start",     Abc_CommandRecStart,         0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_stop",      Abc_CommandRecStop,          0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_add",       Abc_CommandRecAdd,           0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_ps",        Abc_CommandRecPs,            0 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_use",       Abc_CommandRecUse,           1 );
 
     Cmd_CommandAdd( pAbc, "SC mapping",   "map",           Abc_CommandMap,              1 );
     Cmd_CommandAdd( pAbc, "SC mapping",   "amap",          Abc_CommandAmap,             1 );
@@ -11887,6 +11887,7 @@ usage:
     return 1;
 }
 
+#endif
 
 
 /**Function*************************************************************
@@ -11909,7 +11910,7 @@ int Abc_CommandRecStart( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     pNtk = Abc_FrameReadNtk(pAbc);
     // set defaults
-    nVars = 4;
+    nVars = 6;
     nCuts = 8;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "KCh" ) ) != EOF )
@@ -12155,8 +12156,6 @@ usage:
     return 1;
 }
 
-#endif
-
 /**Function*************************************************************
 
   Synopsis    []

src/base/abci/abcRec.c

@@ -237,7 +237,7 @@ p->timeTruth += clock() - clk;
 
         // add the resulting truth table to the hash table 
         ppSpot = Abc_NtkRecTableLookup( p, pTruth, p->nVars );
-        assert( pObj->pEquiv == NULL );
+        assert( pObj->pData == NULL );
         assert( pObj->pCopy == NULL );
         if ( *ppSpot == NULL )
         {
@@ -246,8 +246,8 @@ p->timeTruth += clock() - clk;
         }
         else
         {
-            pObj->pEquiv = (*ppSpot)->pEquiv;
-            (*ppSpot)->pEquiv = (Hop_Obj_t *)pObj;
+            pObj->pData = (*ppSpot)->pData;
+            (*ppSpot)->pData = (Hop_Obj_t *)pObj;
             if ( !Abc_NtkRecAddCutCheckCycle_rec(*ppSpot, pObj) )
                 printf( "Loop!\n" );
         }
@@ -362,7 +362,7 @@ void Abc_NtkRecPs()
     {
         Counters[ Abc_ObjGetMax(pEntry) ]++;
         Counter++;
-        for ( pTemp = pEntry; pTemp; pTemp = (Abc_Obj_t *)pTemp->pEquiv )
+        for ( pTemp = pEntry; pTemp; pTemp = (Abc_Obj_t *)pTemp->pData )
         {
             assert( Abc_ObjGetMax(pTemp) == Abc_ObjGetMax(pEntry) );
             CountersS[ Abc_ObjGetMax(pTemp) ]++;
@@ -935,7 +935,7 @@ s_pMan->timeCanon += clock() - clk;
 
     // add the resulting truth table to the hash table 
     ppSpot = Abc_NtkRecTableLookup( s_pMan, pTruth, nInputs );
-    assert( pObj->pEquiv == NULL );
+    assert( pObj->pData == NULL );
     assert( pObj->pCopy == NULL );
     if ( *ppSpot == NULL )
     {
@@ -944,8 +944,8 @@ s_pMan->timeCanon += clock() - clk;
     }
     else
     {
-        pObj->pEquiv = (*ppSpot)->pEquiv;
-        (*ppSpot)->pEquiv = (Hop_Obj_t *)pObj;
+        pObj->pData = (*ppSpot)->pData;
+        (*ppSpot)->pData = pObj;
         if ( !Abc_NtkRecAddCutCheckCycle_rec(*ppSpot, pObj) )
             printf( "Loop!\n" );
     }
@@ -1104,7 +1104,7 @@ int Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTru
     }
 
     // go through the candidates - and recursively label them
-    for ( pCand = *ppSpot; pCand; pCand = (Abc_Obj_t *)pCand->pEquiv )
+    for ( pCand = *ppSpot; pCand; pCand = (Abc_Obj_t *)pCand->pData )
         Abc_NtkRecStrashNodeLabel_rec( pNtkNew, pCand, 0, s_pMan->vLabels );
 
 
@@ -1120,7 +1120,7 @@ int Abc_NtkRecStrashNode( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, unsigned * pTru
     // find the best subgraph
     CostMin = ABC_INFINITY;
     pCandMin = NULL;
-    for ( pCand = *ppSpot; pCand; pCand = (Abc_Obj_t *)pCand->pEquiv )
+    for ( pCand = *ppSpot; pCand; pCand = (Abc_Obj_t *)pCand->pData )
     {
         // label the leaves
         Abc_NtkIncrementTravId( pAig );

src/base/abci/module.make

@@ -42,6 +42,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcProve.c \
     src/base/abci/abcQbf.c \
     src/base/abci/abcQuant.c \
+    src/base/abci/abcRec.c \
     src/base/abci/abcReconv.c \
     src/base/abci/abcReach.c \
     src/base/abci/abcRefactor.c \