Added recording of AIG subgraphs.

3 files changed, 22 insertions, 22 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ac0f26dd..daf92b1b 100644
--- a/src/base/abci/abc.c
+++ b/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    []
diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c
index 47380da1..33fd9e82 100644
--- a/src/base/abci/abcRec.c
+++ b/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 );
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index b0223330..965e0258 100644
--- a/src/base/abci/module.make
+++ b/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 \