diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-12-06 12:42:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-12-06 12:42:00 -0800 |
commit | 360c705fc41eaacf1e891ecce5e948a091f0b293 (patch) | |
tree | e8ba53c215255ed86b5fd240ea261debbf3d2258 | |
parent | b4a46eb688d30c72b69256b93b73ec71d3fb0dab (diff) | |
download | abc-360c705fc41eaacf1e891ecce5e948a091f0b293.tar.gz abc-360c705fc41eaacf1e891ecce5e948a091f0b293.tar.bz2 abc-360c705fc41eaacf1e891ecce5e948a091f0b293.zip |
Added recording of AIG subgraphs.
-rw-r--r-- | src/aig/kit/kitTruth.c | 19 | ||||
-rw-r--r-- | src/base/abci/abc.c | 25 | ||||
-rw-r--r-- | src/base/abci/abcRec.c | 18 | ||||
-rw-r--r-- | src/base/abci/module.make | 1 |
4 files changed, 31 insertions, 32 deletions
diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c index 56f10ac0..5b467c00 100644 --- a/src/aig/kit/kitTruth.c +++ b/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; 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 \ |