diff --git a/src/aig/aig/aigShow.c b/src/aig/aig/aigShow.c index e3d89942a..7612d02b1 100644 --- a/src/aig/aig/aigShow.c +++ b/src/aig/aig/aigShow.c @@ -344,7 +344,7 @@ void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold ) char FileNameDot[200]; FILE * pFile; // create the file name - sprintf( FileNameDot, "%s", Extra_FileNameGenericAppend(pMan->pName, ".dot") ); + sprintf( FileNameDot, "%s", Extra_FileNameGenericAppend(pMan->pName ? pMan->pName : (char *)"unknown", ".dot") ); // check that the file can be opened if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) { diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c index 33fd5276d..7de1283e4 100644 --- a/src/aig/gia/giaResub.c +++ b/src/aig/gia/giaResub.c @@ -23,6 +23,7 @@ #include "misc/vec/vecQue.h" #include "misc/vec/vecHsh.h" #include "misc/util/utilTruth.h" +#include "base/io/ioResub.h" ABC_NAMESPACE_IMPL_START @@ -2048,10 +2049,109 @@ Vec_Int_t * Gia_ManDeriveSubset( Gia_Man_t * p, Vec_Wrd_t * vFuncs, Vec_Int_t * return vRes; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManResubFindUsed( Vec_Int_t * vRes, int nDivs, int nNodes, Vec_Int_t * vSupp ) +{ + int i, k, iLit, Counter = 1; + Vec_Int_t * vUsed = Vec_IntStartFull( nDivs ); + Vec_Int_t * vRes2 = Vec_IntDup( vRes ); + Vec_IntWriteEntry( vUsed, 0, 0 ); + assert( Vec_IntSize(vRes) % 2 == 1 ); + Vec_IntSort( vRes2, 0 ); + Vec_IntForEachEntry( vRes2, iLit, k ) + { + int iVar = Abc_Lit2Var(iLit); + if ( iVar > 0 && iVar < nDivs && Vec_IntEntry(vUsed, iVar) == -1 ) { + Vec_IntWriteEntry( vUsed, iVar, Counter++ ); + Vec_IntPush( vSupp, iVar-2 ); + } + } + Vec_IntFree( vRes2 ); + for ( i = nDivs; i < nDivs + nNodes; i++ ) + Vec_IntPush( vUsed, Counter++ ); + return vUsed; +} +Vec_Int_t * Gia_ManResubRemapSolution( Vec_Int_t * vRes, Vec_Int_t * vUsed ) +{ + int i, iLit; + Vec_Int_t * vResNew = Vec_IntAlloc( Vec_IntSize(vRes) ); + Vec_IntForEachEntry( vRes, iLit, i ) + Vec_IntPush( vResNew, Abc_Lit2LitV(Vec_IntArray(vUsed), iLit) ); + return vResNew; +} +void Gia_ManResubRecordSolution( char * pFileName, Vec_Int_t * vRes, int nDivs ) +{ + FILE * pFile = fopen( pFileName, "ab" ); + if ( pFile == NULL ) { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return; + } + Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); + Vec_Int_t * vUsed = Gia_ManResubFindUsed( vRes, nDivs, Vec_IntSize(vRes)/2, vSupp ); + Vec_Int_t * vResN = Gia_ManResubRemapSolution( vRes, vUsed ); + + int i, Temp; + fprintf( pFile, "\n.s" ); + Vec_IntForEachEntry( vSupp, Temp, i ) + fprintf( pFile, " %d", Temp ); + fprintf( pFile, "\n.a" ); + Vec_IntForEachEntry( vResN, Temp, i ) + fprintf( pFile, " %d", Temp ); + fprintf( pFile, "\n" ); + fclose( pFile ); + + Vec_IntFree( vUsed ); + Vec_IntFree( vSupp ); + Vec_IntFree( vResN ); +} +Gia_Man_t * Gia_ManResubUnateOne( char * pFileName, int nLimit, int nDivMax, int fWriteSol, int fVerbose ) +{ + Gia_Man_t * pNew = NULL; + Abc_RData_t * p = Abc_ReadPla( pFileName ); assert( p->nOuts == 1 ); + Vec_Ptr_t * vDivs = Vec_PtrAlloc( 2+p->nIns ); + Vec_Int_t * vRes = Vec_IntAlloc( 100 ); + Vec_PtrPush( vDivs, Vec_WrdEntryP(p->vSimsOut, 0*p->nSimWords) ); + Vec_PtrPush( vDivs, Vec_WrdEntryP(p->vSimsOut, 1*p->nSimWords) ); + int i, k, ArraySize, * pArray; + for ( i = 0; i < p->nIns; i++ ) + Vec_PtrPush( vDivs, Vec_WrdEntryP(p->vSimsIn, i*p->nSimWords) ); + Abc_ResubPrepareManager( p->nSimWords ); + if ( fVerbose ) + printf( "The problem has %d divisors and %d outputs.\n", p->nIns, p->nOuts ); + ArraySize = Abc_ResubComputeFunction( (void **)Vec_PtrArray(vDivs), Vec_PtrSize(vDivs), p->nSimWords, nLimit, nDivMax, 0, 0, 1, fVerbose, &pArray ); + for ( k = 0; k < ArraySize; k++ ) + Vec_IntPush( vRes, pArray[k] ); + if ( ArraySize ) { + //printf( "Divisors = %d. Solution: ", Vec_PtrSize(vDivs) ), Vec_IntPrint( vRes ); + Vec_Wec_t * vGates = Vec_WecStart(1); + Vec_IntAppend( Vec_WecEntry(vGates, 0), vRes ); + pNew = Gia_ManConstructFromGates( vGates, Vec_PtrSize(vDivs) ); + Vec_WecFree( vGates ); + if ( fVerbose ) + printf( "The solution has %d inputs and %d nodes.\n", Gia_ManCiNum(pNew), Gia_ManAndNum(pNew) ); + } + if ( fWriteSol && ArraySize ) + Gia_ManResubRecordSolution( pFileName, vRes, Vec_PtrSize(vDivs) ); + Abc_ResubPrepareManager( 0 ); + Vec_IntFree( vRes ); + Vec_PtrFree( vDivs ); + Abc_RDataStop( p ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// - ABC_NAMESPACE_IMPL_END diff --git a/src/aig/gia/giaResub6.c b/src/aig/gia/giaResub6.c index 3203a6996..02bb26963 100644 --- a/src/aig/gia/giaResub6.c +++ b/src/aig/gia/giaResub6.c @@ -20,6 +20,7 @@ #include "gia.h" #include "misc/util/utilTruth.h" +#include "base/io/ioResub.h" ABC_NAMESPACE_IMPL_START @@ -45,6 +46,7 @@ struct Res6_Man_t_ Vec_Int_t vSol; // current solution Vec_Int_t vSolBest; // best solution Vec_Int_t vTempBest;// current best solution + Vec_Int_t vSupp; // support }; extern void Dau_DsdPrintFromTruth2( word * pTruth, int nVarsInit ); @@ -95,11 +97,47 @@ static inline void Res6_ManStop( Res6_Man_t * p ) Vec_IntErase( &p->vSol ); Vec_IntErase( &p->vSolBest ); Vec_IntErase( &p->vTempBest ); + Vec_IntErase( &p->vSupp ); ABC_FREE( p->ppLits ); ABC_FREE( p->ppSets ); ABC_FREE( p ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Res6_Man_t * Res6_ManReadPla( char * pFileName ) +{ + int i, n; + Abc_RData_t * pData = Abc_ReadPla( pFileName ); assert( pData->nOuts == 1 ); + Res6_Man_t * p = pData ? Res6_ManStart( 0, pData->nIns, pData->nOuts, pData->nPats ) : NULL; + if ( p == NULL ) return NULL; + assert( pData->nSimWords == p->nWords ); + for ( i = 1; i < p->nDivs; i++ ) + for ( n = 0; n < 2; n++ ) + Abc_TtCopy( p->ppLits[2*i+n], Vec_WrdEntryP(pData->vSimsIn, (i-1)*pData->nSimWords), pData->nSimWords, n ); + for ( i = 0; i < (1 << p->nOuts); i++ ) + Abc_TtCopy( p->ppSets[i], Vec_WrdEntryP(pData->vSimsOut, i*pData->nSimWords), pData->nSimWords, 0 ); + if ( pData->vDivs ) + Vec_IntForEachEntry( pData->vDivs, n, i ) + Vec_IntPush( &p->vSupp, 1+n ); + if ( pData->vSol ) { + Vec_IntForEachEntry( pData->vSol, n, i ) + Vec_IntPush( &p->vSol, n ); + Vec_IntPush( &p->vSol, Vec_IntEntryLast(&p->vSol) ); + } + Abc_RDataStop( pData ); + return p; +} + /**Function************************************************************* Synopsis [] @@ -197,7 +235,7 @@ void Res6_ManWrite( char * pFileName, Res6_Man_t * p ) void Res6_ManPrintProblem( Res6_Man_t * p, int fVerbose ) { int i, nInputs = (p->nIns && p->nIns < 6) ? p->nIns : 6; - printf( "Problem: In = %d Div = %d Out = %d Pattern = %d\n", p->nIns, p->nDivs - p->nIns - 1, p->nOuts, p->nPats ); + printf( "Problem: In = %d Div = %d Out = %d Pat = %d\n", p->nIns, p->nDivs - p->nIns - 1, p->nOuts, p->nPats ); if ( !fVerbose ) return; printf( "%02d : %s\n", 0, "const0" ); @@ -426,6 +464,7 @@ void Res6_ManResubCheck( char * pFileNameRes, char * pFileNameSol, int fVerbose { Res6_Man_t * p = Res6_ManRead( pFileNameRes ); Vec_Int_t * vSol = Res6_ManReadSol( FileNameSol ); + //Vec_IntPrint( vSol ); if ( p == NULL || vSol == NULL ) return; if ( fVerbose ) @@ -440,6 +479,80 @@ void Res6_ManResubCheck( char * pFileNameRes, char * pFileNameSol, int fVerbose } } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Res6_FindBestEvalPla( Res6_Man_t * p, Vec_Int_t * vSol ) +{ + int i, n, iObj, iLit0, iLit1, iOffset = 2*(1+Vec_IntSize(&p->vSupp)); + assert( Vec_IntSize(vSol) % 2 == 0 ); + Vec_IntForEachEntry( &p->vSupp, iObj, i ) + for ( n = 0; n < 2; n++ ) + Abc_TtCopy( p->ppLits[2*(1+i)+n], p->ppLits[2*iObj+n], p->nWords, 0 ); + Vec_IntForEachEntryDouble( vSol, iLit0, iLit1, i ) + { + if ( iLit0 > iLit1 ) + { + Abc_TtXor( p->ppLits[iOffset+i+0], p->ppLits[iLit0], p->ppLits[iLit1], p->nWords, 0 ); + Abc_TtXor( p->ppLits[iOffset+i+1], p->ppLits[iLit0], p->ppLits[iLit1], p->nWords, 1 ); + } + else + { + Abc_TtAnd( p->ppLits[iOffset+i+0], p->ppLits[iLit0], p->ppLits[iLit1], p->nWords, 0 ); + Abc_TtOr ( p->ppLits[iOffset+i+1], p->ppLits[iLit0^1], p->ppLits[iLit1^1], p->nWords ); + } + } + return Res6_FindGetCost( p, Vec_IntEntryLast(vSol) ); +} +void Res6_ManResubVerifyPla( Res6_Man_t * p, Vec_Int_t * vSol ) +{ + int Cost = Res6_FindBestEvalPla( p, vSol ); + if ( Cost == 0 ) + printf( "Verification successful.\n" ); + else + printf( "Verification FAILED with %d errors on %d patterns.\n", Cost, p->nPats ); +} +void Res6_PrintSolutionPla( Vec_Int_t * vSol, int nSuppSize, int nDivs ) +{ + int iNode, nNodes = Vec_IntSize(vSol)/2-1; + assert( Vec_IntSize(vSol) % 2 == 0 ); + printf( "Solution: In = %d Div = %d Node = %d Out = %d\n", nSuppSize, nDivs-1, nNodes, 1 ); + for ( iNode = 0; iNode <= nNodes; iNode++ ) + { + int * pLits = Vec_IntEntryP( vSol, 2*iNode ); + printf( "x%-2d = ", 1+nSuppSize+iNode ); + Res6_LitPrint( pLits[0], 1+nSuppSize ); + if ( pLits[0] != pLits[1] ) + { + printf( " %c ", pLits[0] < pLits[1] ? '&' : '^' ); + Res6_LitPrint( pLits[1], 1+nSuppSize ); + } + printf( "\n" ); + } +} +void Res6_ManResubCheckPla( char * pFileName, int fVerbose ) +{ + Res6_Man_t * p = Res6_ManReadPla( pFileName ); + if ( p == NULL ) return; + //Vec_IntPrint( &p->vSupp ); + //Vec_IntPrint( &p->vSol ); + if ( fVerbose ) + Res6_ManPrintProblem( p, 0 ); + if ( fVerbose ) + Res6_PrintSolutionPla( &p->vSol, Vec_IntSize(&p->vSupp), p->nDivs ); + //if ( fVerbose ) + // Res6_PrintSuppSims( vSol, p->ppLits, p->nWords, p->nDivs ); + Res6_ManResubVerifyPla( p, &p->vSol ); + Res6_ManStop( p ); +} //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c index c3a211849..6a25cfd89 100644 --- a/src/aig/gia/giaShow.c +++ b/src/aig/gia/giaShow.c @@ -1129,7 +1129,7 @@ void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds, char FileNameDot[200]; FILE * pFile; Vec_Int_t * vXors = NULL, * vAdds = fAdders ? Ree_ManComputeCuts( pMan, &vXors, 0 ) : NULL; - sprintf( FileNameDot, "%s", Extra_FileNameGenericAppend(pMan->pName, ".dot") ); + sprintf( FileNameDot, "%s", Extra_FileNameGenericAppend(pMan->pName ? pMan->pName : (char *)"unknown", ".dot") ); // check that the file can be opened if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) { diff --git a/src/aig/gia/giaSupps.c b/src/aig/gia/giaSupps.c index 0d95997b8..2d2f202de 100644 --- a/src/aig/gia/giaSupps.c +++ b/src/aig/gia/giaSupps.c @@ -818,6 +818,53 @@ void Supp_DeriveDumpSol( Vec_Int_t * vSet, Vec_Int_t * vRes, int nDivs ) printf( "Dumped solution info file \"%s\".\n", Buffer ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Supp_DeriveDumpProb2( Vec_Wrd_t * vIsfs, Vec_Wrd_t * vDivs, int nWords, Vec_Int_t * vSupp, Vec_Int_t * vRes ) +{ + char Buffer[100]; int i, k, Temp, nDivs = Vec_WrdSize(vDivs)/nWords; + int RetValue = sprintf( Buffer, "%02d.pla", s_Counter ); + FILE * pFile = fopen( Buffer, "wb" ); + if ( pFile == NULL ) + printf( "Cannot open output file.\n" ); +// fprintf( pFile, "resyn %d %d %d %d\n", 0, nDivs, 1, 64*nWords ); + fprintf( pFile, ".i %d\n", nDivs ); + fprintf( pFile, ".o %d\n", 1 ); + fprintf( pFile, ".p %d\n", 64*nWords ); + for ( i = 0; i < 64*nWords; i++ ) { + for ( k = 0; k < nDivs; k++ ) + fprintf( pFile, "%d", Abc_TtGetBit(Vec_WrdEntryP(vDivs, k*nWords), i) ); +// fprintf( pFile, " %d\n", Abc_TtGetBit(Vec_WrdEntryP(vIsfs, 1*nWords), i) ); + if ( Abc_TtGetBit(Vec_WrdEntryP(vIsfs, 0*nWords), i) ) + fprintf( pFile, " 0\n" ); + else if ( Abc_TtGetBit(Vec_WrdEntryP(vIsfs, 1*nWords), i) ) + fprintf( pFile, " 1\n" ); + else + fprintf( pFile, " -\n" ); + } + fprintf( pFile, ".e\n" ); + + fprintf( pFile, "\n.s" ); + Vec_IntForEachEntryStart( vSupp, Temp, i, 2 ) + fprintf( pFile, " %d", Temp ); + fprintf( pFile, "\n.a" ); + Vec_IntForEachEntry( vRes, Temp, i ) + fprintf( pFile, " %d", Temp ); + fprintf( pFile, "\n" ); + fclose ( pFile ); + RetValue = 0; +} + + /**Function************************************************************* Synopsis [] @@ -857,6 +904,7 @@ Vec_Int_t * Supp_ManFindBestSolution( Supp_Man_t * p, Vec_Wec_t * vSols, int fVe } if ( iSolBest > 0 && (CostBest >> 2) < 50 ) { + Vec_Int_t * vDivs2 = Vec_IntAlloc( 100 ); Vec_Int_t * vSet = Hsh_VecReadEntry( p->pHash, iSolBest ); int i, iObj; vRes = Gia_ManDeriveSolutionOne( p->pGia, p->vSims, p->vIsfs, p->vCands, vSet, p->nWords, CostBest & 3 ); assert( !vRes || Vec_IntSize(vRes) == 2*(CostBest >> 2)+1 ); @@ -864,13 +912,18 @@ Vec_Int_t * Supp_ManFindBestSolution( Supp_Man_t * p, Vec_Wec_t * vSols, int fVe { Vec_IntClear( *pvDivs ); Vec_IntPushTwo( *pvDivs, -1, -1 ); - Vec_IntForEachEntry( vSet, iObj, i ) + Vec_IntPushTwo( vDivs2, -1, -1 ); + Vec_IntForEachEntry( vSet, iObj, i ) { Vec_IntPush( *pvDivs, Vec_IntEntry(p->vCands, iObj) ); + Vec_IntPush( vDivs2, iObj ); + } } //Supp_DeriveDumpProbC( p->vIsfs, p->vDivsC, p->nWords ); //Supp_DeriveDumpProb( p->vIsfs, p->vDivs[1], p->nWords ); //Supp_DeriveDumpSol( vSet, vRes, Vec_WrdSize(p->vDivs[1])/p->nWords ); - //s_Counter++; + //Supp_DeriveDumpProb2( p->vIsfs, p->vDivs[1], p->nWords, vDivs2, vRes ); + Vec_IntFree( vDivs2 ); + s_Counter++; } return vRes; } @@ -1013,6 +1066,35 @@ void Supp_ManComputeTest( Gia_Man_t * p ) Vec_IntFree( vRes ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Supp_RecordSolution( char * pFileName, Vec_Int_t * vDivs, Vec_Int_t * vRes ) +{ + FILE * pFile = fopen( pFileName, "ab" ); + if ( pFile == NULL ) { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return; + } + int i, Temp; + fprintf( pFile, "\n.s" ); + Vec_IntForEachEntryStart( vDivs, Temp, i, 2 ) + fprintf( pFile, " %d", Temp ); + fprintf( pFile, "\n.a" ); + Vec_IntForEachEntry( vRes, Temp, i ) + fprintf( pFile, " %d", Temp-2 ); + fprintf( pFile, "\n" ); + fclose( pFile ); +} + /**Function************************************************************* Synopsis [] @@ -1044,14 +1126,17 @@ Gia_Man_t * Supp_GenerateGia( Vec_Int_t * vRes, Vec_Int_t * vDivs ) Gia_ManAppendCo(pNew, iTopLit-nAddOn); return pNew; } -Gia_Man_t * Supp_ManSolveOne( char * pFileName, int nIters, int nRounds, int fVerbose ) +Gia_Man_t * Supp_ManSolveOne( char * pFileName, int nIters, int nRounds, int fWriteSol, int fVerbose ) { + //Abc_Random(1); Abc_RData_t * p = Abc_ReadPla( pFileName ); assert( p->nOuts == 1 ); Vec_Int_t * vDivs = Vec_IntAlloc( 100 ); Vec_Int_t * vRes = Supp_ManCompute( p->vSimsOut, NULL, NULL, p->vSimsIn, NULL, p->nSimWords, NULL, &vDivs, nIters, nRounds, fVerbose ); if ( fVerbose && vDivs ) printf( "Divisors: " ), Vec_IntPrint( vDivs ); if ( fVerbose && vRes ) printf( "Solution: " ), Vec_IntPrint( vRes ); Gia_Man_t * pNew = vRes ? Supp_GenerateGia( vRes, vDivs ) : NULL; + if ( fWriteSol && vDivs && vRes ) + Supp_RecordSolution( pFileName, vDivs, vRes ); Vec_IntFreeP( &vRes ); Vec_IntFreeP( &vDivs ); Abc_RDataStop( p ); diff --git a/src/aig/gia/giaTranStoch.c b/src/aig/gia/giaTranStoch.c index aa600c0c0..f7b300c0d 100644 --- a/src/aig/gia/giaTranStoch.c +++ b/src/aig/gia/giaTranStoch.c @@ -423,6 +423,10 @@ Gia_Man_t * Gia_ManTranStoch( Gia_Man_t * pGia, int nRestarts, int nHops, int nS if ( nVerbose ) printf( "best: %d\n", Gia_ManAndNum( pBest ) ); Vec_PtrFree( vpStarts ); + ABC_FREE( pBest->pName ); + ABC_FREE( pBest->pSpec ); + pBest->pName = Abc_UtilStrsav( pGia->pName ); + pBest->pSpec = Abc_UtilStrsav( pGia->pSpec ); return pBest; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 353609973..a260f0bd7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -148,8 +148,9 @@ static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRestructure ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandResubstitute ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandResubCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandResubUnate ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandResubCore ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandResubCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRr ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCascade ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandExtract ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -934,8 +935,9 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 ); // Cmd_CommandAdd( pAbc, "Synthesis", "restructure", Abc_CommandRestructure, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "resub", Abc_CommandResubstitute, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "resub_unate", Abc_CommandResubUnate, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "resub_core", Abc_CommandResubCore, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "resub_check", Abc_CommandResubCheck, 0 ); - Cmd_CommandAdd( pAbc, "Synthesis", "resub_core", Abc_CommandResubCore, 0 ); // Cmd_CommandAdd( pAbc, "Synthesis", "rr", Abc_CommandRr, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "cascade", Abc_CommandCascade, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "extract", Abc_CommandExtract, 1 ); @@ -8358,6 +8360,182 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandResubUnate( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManResubUnateOne( char * pFileName, int nLimit, int nDivMax, int fWriteSol, int fVerbose ); + Gia_Man_t * pTemp; + int nLimit = 16; + int nDivMax = 50; + int fWriteSol = 0; + int fVerbose = 0, c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "LDsvh" ) ) != EOF ) + { + switch ( c ) + { + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + nLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLimit < 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + nDivMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nDivMax < 0 ) + goto usage; + break; + case 's': + fWriteSol ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 1 ) + { + Abc_Print( -1, "Input file should be given on the command line.\n" ); + return 1; + } + pTemp = Gia_ManResubUnateOne( argv[globalUtilOptind], nLimit, nDivMax, fWriteSol, fVerbose ); + if ( pTemp ) + { + Aig_Man_t * pMan = Gia_ManToAig( pTemp, 0 ); + Abc_Ntk_t * pNtk = Abc_NtkFromAigPhase( pMan ); + Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); + Aig_ManStop( pMan ); + Gia_ManStop( pTemp ); + return 0; + } + Abc_Print( 0, "The networks is not generated.\n" ); + return 0; + +usage: + Abc_Print( -2, "usage: resub_unate [-LD ] [-svh] \n" ); + Abc_Print( -2, "\t solves one instance of the resub problem\n" ); + Abc_Print( -2, "\t-L num : the limit on the number of nodes [default = %d]\n", nLimit ); + Abc_Print( -2, "\t-D num : the maximum number of binate divisors to consider [default = %d]\n", nDivMax ); + Abc_Print( -2, "\t-s : toggle saving the result in the input file [default = %s]\n", fWriteSol? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t : resub problem file name\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandResubCore( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Supp_ManSolveOne( char * pFileName, int nIters, int nRounds, int fWriteSol, int fVerbose ); + Gia_Man_t * pTemp; + int nIters = 1; + int nRounds = 1; + int fWriteSol = 0; + int fVerbose = 0, c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "IRsvh" ) ) != EOF ) + { + switch ( c ) + { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nIters < 0 ) + goto usage; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + nRounds = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nRounds < 0 ) + goto usage; + break; + case 's': + fWriteSol ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 1 ) + { + Abc_Print( -1, "Input file should be given on the command line.\n" ); + return 1; + } + pTemp = Supp_ManSolveOne( argv[globalUtilOptind], nIters, nRounds, fWriteSol, fVerbose ); + if ( pTemp ) + { + Aig_Man_t * pMan = Gia_ManToAig( pTemp, 0 ); + Abc_Ntk_t * pNtk = Abc_NtkFromAigPhase( pMan ); + Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); + Aig_ManStop( pMan ); + Gia_ManStop( pTemp ); + return 0; + } + Abc_Print( 0, "The networks is not generated.\n" ); + return 0; + +usage: + Abc_Print( -2, "usage: resub_core [-IR ] [-svh] \n" ); + Abc_Print( -2, "\t solves one instance of the resub problem\n" ); + Abc_Print( -2, "\t-I num : the number of iterations [default = %d]\n", nIters ); + Abc_Print( -2, "\t-R num : the number of rounds in each iteration [default = %d]\n", nRounds ); + Abc_Print( -2, "\t-s : toggle saving the result in the input file [default = %s]\n", fWriteSol? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t : resub problem file name\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -8372,6 +8550,7 @@ usage: int Abc_CommandResubCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Res6_ManResubCheck( char * pFileNameRes, char * pFileNameSol, int fVerbose ); + extern void Res6_ManResubCheckPla( char * pFileName, int fVerbose ); char * pFileR = NULL, * pFileS = NULL; int fVerbose = 0, c; Extra_UtilGetoptReset(); @@ -8403,7 +8582,10 @@ int Abc_CommandResubCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Incorrect number of command line arguments.\n" ); return 1; } - Res6_ManResubCheck( pFileR, pFileS, fVerbose ); + if ( !strcmp(pFileR + strlen(pFileR) - 3, "pla") ) + Res6_ManResubCheckPla( pFileR, fVerbose ); + else + Res6_ManResubCheck( pFileR, pFileS, fVerbose ); return 0; usage: @@ -8416,91 +8598,6 @@ usage: return 1; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_CommandResubCore( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - extern Gia_Man_t * Supp_ManSolveOne( char * pFileName, int nIters, int nRounds, int fVerbose ); - Gia_Man_t * pTemp; - int nIters = 1; - int nRounds = 1; - int fVerbose = 0, c; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "IRvh" ) ) != EOF ) - { - switch ( c ) - { - case 'I': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); - goto usage; - } - nIters = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( nIters < 0 ) - goto usage; - break; - case 'R': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); - goto usage; - } - nRounds = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( nRounds < 0 ) - goto usage; - break; - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( argc != globalUtilOptind + 1 ) - { - Abc_Print( -1, "Input file should be given on the command line.\n" ); - return 1; - } - pTemp = Supp_ManSolveOne( argv[globalUtilOptind], nIters, nRounds, fVerbose ); - if ( pTemp ) - { - Aig_Man_t * pMan = Gia_ManToAig( pTemp, 0 ); - Abc_Ntk_t * pNtk = Abc_NtkFromAigPhase( pMan ); - Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); - Aig_ManStop( pMan ); - Gia_ManStop( pTemp ); - return 0; - } - Abc_Print( 0, "The networks is not generated.\n" ); - return 0; - -usage: - Abc_Print( -2, "usage: resub_core [-IR ] [-vh] \n" ); - Abc_Print( -2, "\t solves one instance of the resub problem\n" ); - Abc_Print( -2, "\t-I num : the number of iterations [default = %d]\n", nIters ); - Abc_Print( -2, "\t-R num : the number of rounds in each iteration [default = %d]\n", nRounds ); - Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-h : print the command usage\n"); - Abc_Print( -2, "\t : resub problem file name\n"); - return 1; -} - - - /**Function************************************************************* Synopsis [] @@ -53171,10 +53268,10 @@ int Abc_CommandAbc9Window( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: &window [-vh] ... \n" ); - Abc_Print( -2, "\t generates window supported by the given nodes\n" ); - Abc_Print( -2, "\t-v : toggles printing verbose information [default = %d]\n", fVerbose ? "yes": "no" ); + Abc_Print( -2, "\t generates a logic window supported by the given nodes\n" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); - Abc_Print( -2, "\t : the list of input nodes\n"); + Abc_Print( -2, "\t : the list of window inputs\n"); return 1; } diff --git a/src/base/io/ioResub.h b/src/base/io/ioResub.h index f78d6f8cd..bd5175fbe 100644 --- a/src/base/io/ioResub.h +++ b/src/base/io/ioResub.h @@ -46,6 +46,8 @@ struct Abc_RData_t_ int nSimWords; // the number of words needed to store the patterns Vec_Wrd_t * vSimsIn; // input simulation signatures Vec_Wrd_t * vSimsOut; // output simulation signatures + Vec_Int_t * vDivs; // divisors + Vec_Int_t * vSol; // solution }; //////////////////////////////////////////////////////////////////////// @@ -83,11 +85,15 @@ static inline Abc_RData_t * Abc_RDataStart( int nIns, int nOuts, int nPats ) p->nPats = nPats; p->nSimWords = Abc_Bit6WordNum(nPats); p->vSimsIn = Vec_WrdStart( p->nIns * p->nSimWords ); - p->vSimsOut = Vec_WrdStart( 2*p->nOuts * p->nSimWords ); + p->vSimsOut = Vec_WrdStart( 2*p->nOuts * p->nSimWords ); + p->vDivs = Vec_IntAlloc( 16 ); + p->vSol = Vec_IntAlloc( 16 ); return p; } static inline void Abc_RDataStop( Abc_RData_t * p ) { + Vec_IntFree( p->vSol ); + Vec_IntFree( p->vDivs ); Vec_WrdFree( p->vSimsIn ); Vec_WrdFree( p->vSimsOut ); ABC_FREE( p ); @@ -99,9 +105,10 @@ static inline int Abc_ReadPlaResubParams( char * pFileName, int * pnIns, int * p printf( "Cannot open file \"%s\" for reading.\n", pFileName ); return 0; } - char pBuffer[100]; int iLine = 0; + int nLineSize = 1000000, iLine = 0; + char * pBuffer = ABC_ALLOC( char, nLineSize ); *pnIns = *pnOuts = *pnPats = 0; - while ( fgets( pBuffer, 100, pFile ) != NULL ) { + while ( fgets( pBuffer, nLineSize, pFile ) != NULL ) { iLine += (pBuffer[0] == '0' || pBuffer[0] == '1' || pBuffer[0] == '-'); if ( pBuffer[0] != '.' ) continue; @@ -119,6 +126,7 @@ static inline int Abc_ReadPlaResubParams( char * pFileName, int * pnIns, int * p else if ( *pnPats != iLine ) printf( "The number of lines in the file (%d) does not match the number listed in .p (%d).\n", iLine, *pnPats ); fclose(pFile); + free( pBuffer ); return 1; } static inline int Abc_ReadPlaResubData( Abc_RData_t * p, char * pFileName ) @@ -143,16 +151,24 @@ static inline int Abc_ReadPlaResubData( Abc_RData_t * p, char * pFileName ) Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+0)*p->nSimWords), iLine ); else if ( *pTemp == '1' ) Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+1)*p->nSimWords), iLine ); - else if ( *pTemp == '-' ) { - Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+0)*p->nSimWords), iLine ); - Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+1)*p->nSimWords), iLine ); - } + //else if ( *pTemp == '-' ) { + // Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+0)*p->nSimWords), iLine ); + // Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+1)*p->nSimWords), iLine ); + //} } i += (*pTemp == '0' || *pTemp == '1' || *pTemp == '-'); } assert( i == p->nIns + p->nOuts ); iLine++; } + if ( pBuffer[0] == '.' && (pBuffer[1] == 's' || pBuffer[1] == 'a') ) { + Vec_Int_t * vArray = pBuffer[1] == 'a' ? p->vSol : p->vDivs; + if ( Vec_IntSize(vArray) > 0 ) + continue; + char * pTemp = strtok( pBuffer+2, " \r\n\t" ); + do Vec_IntPush( vArray, atoi(pTemp) ); + while ( (pTemp = strtok( NULL, " \r\n\t" )) ); + } } if ( nDashes ) printf( "Several (%d) don't-care literals in the input part are replaced by zeros \"%s\" \n", nDashes, pFileName );