luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

New command "resub_unate" and various changes.

This commit is contained in:
Alan Mishchenko 2024-05-17 02:56:33 -07:00
parent 9a89447de4
commit 3616fd8fb5
8 changed files with 520 additions and 105 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/aig/aigShow.c
View File

@ -344,7 +344,7 @@ void Aig_ManShow( Aig_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )
char FileNameDot[200]; char FileNameDot[200];
FILE * pFile; FILE * pFile;
// create the file name // 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 // check that the file can be opened
if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
{ {

102
src/aig/gia/giaResub.c
View File

@ -23,6 +23,7 @@
#include "misc/vec/vecQue.h" #include "misc/vec/vecQue.h"
#include "misc/vec/vecHsh.h" #include "misc/vec/vecHsh.h"
#include "misc/util/utilTruth.h" #include "misc/util/utilTruth.h"
#include "base/io/ioResub.h"
ABC_NAMESPACE_IMPL_START 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; 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 /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_END

115
src/aig/gia/giaResub6.c
View File

@ -20,6 +20,7 @@
#include "gia.h" #include "gia.h"
#include "misc/util/utilTruth.h" #include "misc/util/utilTruth.h"
#include "base/io/ioResub.h"
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
@ -45,6 +46,7 @@ struct Res6_Man_t_
Vec_Int_t vSol; // current solution Vec_Int_t vSol; // current solution
Vec_Int_t vSolBest; // best solution Vec_Int_t vSolBest; // best solution
Vec_Int_t vTempBest;// current best solution Vec_Int_t vTempBest;// current best solution
Vec_Int_t vSupp; // support
}; };
extern void Dau_DsdPrintFromTruth2( word * pTruth, int nVarsInit ); 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->vSol );
Vec_IntErase( &p->vSolBest ); Vec_IntErase( &p->vSolBest );
Vec_IntErase( &p->vTempBest ); Vec_IntErase( &p->vTempBest );
Vec_IntErase( &p->vSupp );
ABC_FREE( p->ppLits ); ABC_FREE( p->ppLits );
ABC_FREE( p->ppSets ); ABC_FREE( p->ppSets );
ABC_FREE( p ); 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************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
@ -197,7 +235,7 @@ void Res6_ManWrite( char * pFileName, Res6_Man_t * p )
void Res6_ManPrintProblem( Res6_Man_t * p, int fVerbose ) void Res6_ManPrintProblem( Res6_Man_t * p, int fVerbose )
{ {
int i, nInputs = (p->nIns && p->nIns < 6) ? p->nIns : 6; 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 ) if ( !fVerbose )
return; return;
printf( "%02d : %s\n", 0, "const0" ); 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 ); Res6_Man_t * p = Res6_ManRead( pFileNameRes );
Vec_Int_t * vSol = Res6_ManReadSol( FileNameSol ); Vec_Int_t * vSol = Res6_ManReadSol( FileNameSol );
//Vec_IntPrint( vSol );
if ( p == NULL || vSol == NULL ) if ( p == NULL || vSol == NULL )
return; return;
if ( fVerbose ) 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 );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

2
src/aig/gia/giaShow.c
View File

@ -1129,7 +1129,7 @@ void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds,
char FileNameDot[200]; char FileNameDot[200];
FILE * pFile; FILE * pFile;
Vec_Int_t * vXors = NULL, * vAdds = fAdders ? Ree_ManComputeCuts( pMan, &vXors, 0 ) : NULL; 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 // check that the file can be opened
if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
{ {

91
src/aig/gia/giaSupps.c
View File

@ -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 ); 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************************************************************* /**Function*************************************************************
Synopsis [] 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 ) 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; 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 ); 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 ); 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_IntClear( *pvDivs );
Vec_IntPushTwo( *pvDivs, -1, -1 ); 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( *pvDivs, Vec_IntEntry(p->vCands, iObj) );
Vec_IntPush( vDivs2, iObj );
}
} }
//Supp_DeriveDumpProbC( p->vIsfs, p->vDivsC, p->nWords ); //Supp_DeriveDumpProbC( p->vIsfs, p->vDivsC, p->nWords );
//Supp_DeriveDumpProb( p->vIsfs, p->vDivs[1], p->nWords ); //Supp_DeriveDumpProb( p->vIsfs, p->vDivs[1], p->nWords );
//Supp_DeriveDumpSol( vSet, vRes, Vec_WrdSize(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; return vRes;
} }
@ -1013,6 +1066,35 @@ void Supp_ManComputeTest( Gia_Man_t * p )
Vec_IntFree( vRes ); 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************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
@ -1044,14 +1126,17 @@ Gia_Man_t * Supp_GenerateGia( Vec_Int_t * vRes, Vec_Int_t * vDivs )
Gia_ManAppendCo(pNew, iTopLit-nAddOn); Gia_ManAppendCo(pNew, iTopLit-nAddOn);
return pNew; 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 ); Abc_RData_t * p = Abc_ReadPla( pFileName ); assert( p->nOuts == 1 );
Vec_Int_t * vDivs = Vec_IntAlloc( 100 ); 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 ); 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 && vDivs ) printf( "Divisors: " ), Vec_IntPrint( vDivs );
if ( fVerbose && vRes ) printf( "Solution: " ), Vec_IntPrint( vRes ); if ( fVerbose && vRes ) printf( "Solution: " ), Vec_IntPrint( vRes );
Gia_Man_t * pNew = vRes ? Supp_GenerateGia( vRes, vDivs ) : NULL; Gia_Man_t * pNew = vRes ? Supp_GenerateGia( vRes, vDivs ) : NULL;
if ( fWriteSol && vDivs && vRes )
Supp_RecordSolution( pFileName, vDivs, vRes );
Vec_IntFreeP( &vRes ); Vec_IntFreeP( &vRes );
Vec_IntFreeP( &vDivs ); Vec_IntFreeP( &vDivs );
Abc_RDataStop( p ); Abc_RDataStop( p );

4
src/aig/gia/giaTranStoch.c
View File

@ -423,6 +423,10 @@ Gia_Man_t * Gia_ManTranStoch( Gia_Man_t * pGia, int nRestarts, int nHops, int nS
if ( nVerbose ) if ( nVerbose )
printf( "best: %d\n", Gia_ManAndNum( pBest ) ); printf( "best: %d\n", Gia_ManAndNum( pBest ) );
Vec_PtrFree( vpStarts ); 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; return pBest;
} }

279
src/base/abci/abc.c
View File

@ -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_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRestructure ( 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_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_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_CommandRr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCascade ( 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 ); 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", "refactor", Abc_CommandRefactor, 1 );
// Cmd_CommandAdd( pAbc, "Synthesis", "restructure", Abc_CommandRestructure, 1 ); // Cmd_CommandAdd( pAbc, "Synthesis", "restructure", Abc_CommandRestructure, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "resub", Abc_CommandResubstitute, 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_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", "rr", Abc_CommandRr, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "cascade", Abc_CommandCascade, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "cascade", Abc_CommandCascade, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "extract", Abc_CommandExtract, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "extract", Abc_CommandExtract, 1 );
@ -8358,6 +8360,182 @@ usage:
return 1; 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 <num>] [-svh] <file>\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<file> : 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 <num>] [-svh] <file>\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<file> : resub problem file name\n");
return 1;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
@ -8372,6 +8550,7 @@ usage:
int Abc_CommandResubCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandResubCheck( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
extern void Res6_ManResubCheck( char * pFileNameRes, char * pFileNameSol, int fVerbose ); extern void Res6_ManResubCheck( char * pFileNameRes, char * pFileNameSol, int fVerbose );
extern void Res6_ManResubCheckPla( char * pFileName, int fVerbose );
char * pFileR = NULL, * pFileS = NULL; char * pFileR = NULL, * pFileS = NULL;
int fVerbose = 0, c; int fVerbose = 0, c;
Extra_UtilGetoptReset(); 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" ); Abc_Print( -1, "Incorrect number of command line arguments.\n" );
return 1; 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; return 0;
usage: usage:
@ -8416,91 +8598,6 @@ usage:
return 1; 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 <num>] [-vh] <file>\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<file> : resub problem file name\n");
return 1;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis []
@ -53171,10 +53268,10 @@ int Abc_CommandAbc9Window( Abc_Frame_t * pAbc, int argc, char ** argv )
usage: usage:
Abc_Print( -2, "usage: &window [-vh] <node1> <node2> ... <nodeN>\n" ); Abc_Print( -2, "usage: &window [-vh] <node1> <node2> ... <nodeN>\n" );
Abc_Print( -2, "\t generates window supported by the given nodes\n" ); Abc_Print( -2, "\t generates a logic 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-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-h : print the command usage\n");
Abc_Print( -2, "\t<nodes> : the list of input nodes\n"); Abc_Print( -2, "\t<nodes> : the list of window inputs\n");
return 1; return 1;
} }

28
src/base/io/ioResub.h
View File

@ -46,6 +46,8 @@ struct Abc_RData_t_
int nSimWords; // the number of words needed to store the patterns int nSimWords; // the number of words needed to store the patterns
Vec_Wrd_t * vSimsIn; // input simulation signatures Vec_Wrd_t * vSimsIn; // input simulation signatures
Vec_Wrd_t * vSimsOut; // output simulation signatures Vec_Wrd_t * vSimsOut; // output simulation signatures
Vec_Int_t * vDivs; // divisors
Vec_Int_t * vSol; // solution
}; };
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
@ -84,10 +86,14 @@ static inline Abc_RData_t * Abc_RDataStart( int nIns, int nOuts, int nPats )
p->nSimWords = Abc_Bit6WordNum(nPats); p->nSimWords = Abc_Bit6WordNum(nPats);
p->vSimsIn = Vec_WrdStart( p->nIns * p->nSimWords ); 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; return p;
} }
static inline void Abc_RDataStop( Abc_RData_t * 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->vSimsIn );
Vec_WrdFree( p->vSimsOut ); Vec_WrdFree( p->vSimsOut );
ABC_FREE( p ); 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 ); printf( "Cannot open file \"%s\" for reading.\n", pFileName );
return 0; return 0;
} }
char pBuffer[100]; int iLine = 0; int nLineSize = 1000000, iLine = 0;
char * pBuffer = ABC_ALLOC( char, nLineSize );
*pnIns = *pnOuts = *pnPats = 0; *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] == '-'); iLine += (pBuffer[0] == '0' || pBuffer[0] == '1' || pBuffer[0] == '-');
if ( pBuffer[0] != '.' ) if ( pBuffer[0] != '.' )
continue; continue;
@ -119,6 +126,7 @@ static inline int Abc_ReadPlaResubParams( char * pFileName, int * pnIns, int * p
else if ( *pnPats != iLine ) 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 ); printf( "The number of lines in the file (%d) does not match the number listed in .p (%d).\n", iLine, *pnPats );
fclose(pFile); fclose(pFile);
free( pBuffer );
return 1; return 1;
} }
static inline int Abc_ReadPlaResubData( Abc_RData_t * p, char * pFileName ) 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 ); Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+0)*p->nSimWords), iLine );
else if ( *pTemp == '1' ) else if ( *pTemp == '1' )
Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+1)*p->nSimWords), iLine ); Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+1)*p->nSimWords), iLine );
else if ( *pTemp == '-' ) { //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)+0)*p->nSimWords), iLine );
Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+1)*p->nSimWords), iLine ); // Abc_InfoSetBit( (unsigned *)Vec_WrdEntryP(p->vSimsOut, (2*(i-p->nIns)+1)*p->nSimWords), iLine );
} //}
} }
i += (*pTemp == '0' || *pTemp == '1' || *pTemp == '-'); i += (*pTemp == '0' || *pTemp == '1' || *pTemp == '-');
} }
assert( i == p->nIns + p->nOuts ); assert( i == p->nIns + p->nOuts );
iLine++; 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 ) if ( nDashes )
printf( "Several (%d) don't-care literals in the input part are replaced by zeros \"%s\" \n", nDashes, pFileName ); printf( "Several (%d) don't-care literals in the input part are replaced by zeros \"%s\" \n", nDashes, pFileName );