summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2022-06-10 14:06:23 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2022-06-10 14:06:23 -0700
commitae0f03f4a953a98540d67bc64846a492c568c70d (patch)
treefd4b0f3a15bb49a84307a7903481e903750d0250 /src
parent3241a595bab1601a26a10d6452dbd205b2c1480f (diff)
downloadabc-ae0f03f4a953a98540d67bc64846a492c568c70d.tar.gz
abc-ae0f03f4a953a98540d67bc64846a492c568c70d.tar.bz2
abc-ae0f03f4a953a98540d67bc64846a492c568c70d.zip
Adding command to check resub problem solution.
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaResub6.c403
-rw-r--r--src/aig/gia/giaSupps.c104
-rw-r--r--src/aig/gia/module.make1
-rw-r--r--src/base/abci/abc.c60
4 files changed, 568 insertions, 0 deletions
diff --git a/src/aig/gia/giaResub6.c b/src/aig/gia/giaResub6.c
new file mode 100644
index 00000000..567bf30b
--- /dev/null
+++ b/src/aig/gia/giaResub6.c
@@ -0,0 +1,403 @@
+/**CFile****************************************************************
+
+ FileName [giaResub6.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis [Resubstitution.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: giaResub6.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define MAX_NODE 100
+
+typedef struct Res6_Man_t_ Res6_Man_t;
+struct Res6_Man_t_
+{
+ int nIns; // inputs
+ int nDivs; // divisors
+ int nDivsA; // divisors alloc
+ int nOuts; // outputs
+ int nPats; // patterns
+ int nWords; // words
+ Vec_Wrd_t vIns; // input sim data
+ Vec_Wrd_t vOuts; // input sim data
+ word ** ppLits; // literal sim info
+ word ** ppSets; // set sim info
+ Vec_Int_t vSol; // current solution
+ Vec_Int_t vSolBest; // best solution
+ Vec_Int_t vTempBest;// current best solution
+};
+
+extern void Dau_DsdPrintFromTruth2( word * pTruth, int nVarsInit );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Res6_Man_t * Res6_ManStart( int nIns, int nNodes, int nOuts, int nPats )
+{
+ Res6_Man_t * p; int i;
+ p = ABC_CALLOC( Res6_Man_t, 1 );
+ p->nIns = nIns;
+ p->nDivs = 1 + nIns + nNodes;
+ p->nDivsA = p->nDivs + MAX_NODE;
+ p->nOuts = nOuts;
+ p->nPats = nPats;
+ p->nWords =(nPats + 63)/64;
+ Vec_WrdFill( &p->vIns, 2*p->nDivsA*p->nWords, 0 );
+ Vec_WrdFill( &p->vOuts, (1 << nOuts)*p->nWords, 0 );
+ p->ppLits = ABC_CALLOC( word *, 2*p->nDivsA );
+ p->ppSets = ABC_CALLOC( word *, 1 << nOuts );
+ for ( i = 0; i < 2*p->nDivsA; i++ )
+ p->ppLits[i] = Vec_WrdEntryP( &p->vIns, i*p->nWords );
+ for ( i = 0; i < (1 << nOuts); i++ )
+ p->ppSets[i] = Vec_WrdEntryP( &p->vOuts, i*p->nWords );
+ Abc_TtFill( p->ppLits[1], p->nWords );
+ Vec_IntGrow( &p->vSol, 2*MAX_NODE+nOuts );
+ Vec_IntGrow( &p->vSolBest, 2*MAX_NODE+nOuts );
+ Vec_IntGrow( &p->vTempBest, 2*MAX_NODE+nOuts );
+ return p;
+}
+static inline void Res6_ManStop( Res6_Man_t * p )
+{
+ Vec_WrdErase( &p->vIns );
+ Vec_WrdErase( &p->vOuts );
+ Vec_IntErase( &p->vSol );
+ Vec_IntErase( &p->vSolBest );
+ Vec_IntErase( &p->vTempBest );
+ ABC_FREE( p->ppLits );
+ ABC_FREE( p->ppSets );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Res6_Man_t * Res6_ManRead( char * pFileName )
+{
+ Res6_Man_t * p = NULL;
+ FILE * pFile = fopen( pFileName, "rb" );
+ if ( pFile == NULL )
+ printf( "Cannot open input file \"%s\".\n", pFileName );
+ else
+ {
+ int i, k, nIns, nNodes, nOuts, nPats, iLit = 0;
+ char Temp[100], Buffer[100];
+ char * pLine = fgets( Buffer, 100, pFile );
+ if ( pLine == NULL )
+ {
+ printf( "Cannot read the header line of input file \"%s\".\n", pFileName );
+ return NULL;
+ }
+ if ( 5 != sscanf(pLine, "%s %d %d %d %d", Temp, &nIns, &nNodes, &nOuts, &nPats) )
+ {
+ printf( "Cannot read the parameters from the header of input file \"%s\".\n", pFileName );
+ return NULL;
+ }
+ p = Res6_ManStart( nIns, nNodes, nOuts, nPats );
+ pLine = ABC_ALLOC( char, nPats + 100 );
+ for ( i = 1; i < p->nDivs; i++ )
+ {
+ char * pNext = fgets( pLine, nPats + 100, pFile );
+ if ( pNext == NULL )
+ {
+ printf( "Cannot read line %d of input file \"%s\".\n", i, pFileName );
+ Res6_ManStop( p );
+ ABC_FREE( pLine );
+ fclose( pFile );
+ return NULL;
+ }
+ for ( k = 0; k < p->nPats; k++ )
+ if ( pNext[k] == '0' )
+ Abc_TtSetBit( p->ppLits[2*i+1], k );
+ else if ( pNext[k] == '1' )
+ Abc_TtSetBit( p->ppLits[2*i], k );
+ }
+ for ( i = 0; i < (1 << p->nOuts); i++ )
+ {
+ char * pNext = fgets( pLine, nPats + 100, pFile );
+ if ( pNext == NULL )
+ {
+ printf( "Cannot read line %d of input file \"%s\".\n", i, pFileName );
+ Res6_ManStop( p );
+ ABC_FREE( pLine );
+ fclose( pFile );
+ return NULL;
+ }
+ for ( k = 0; k < p->nPats; k++ )
+ if ( pNext[k] == '1' )
+ Abc_TtSetBit( p->ppSets[i], k );
+ }
+ ABC_FREE( pLine );
+ fclose( pFile );
+ }
+ return p;
+}
+void Res6_ManWrite( char * pFileName, Res6_Man_t * p )
+{
+ FILE * pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL )
+ printf( "Cannot open output file \"%s\".\n", pFileName );
+ else
+ {
+ int i, k;
+ fprintf( pFile, "resyn %d %d %d %d\n", p->nIns, p->nDivs - p->nIns - 1, p->nOuts, p->nPats );
+ for ( i = 1; i < p->nDivs; i++, fputc('\n', pFile) )
+ for ( k = 0; k < p->nPats; k++ )
+ if ( Abc_TtGetBit(p->ppLits[2*i+1], k) )
+ fputc( '0', pFile );
+ else if ( Abc_TtGetBit(p->ppLits[2*i], k) )
+ fputc( '1', pFile );
+ else
+ fputc( '-', pFile );
+ for ( i = 0; i < (1 << p->nOuts); i++, fputc('\n', pFile) )
+ for ( k = 0; k < p->nPats; k++ )
+ fputc( '0' + Abc_TtGetBit(p->ppSets[i], k), pFile );
+ fclose( pFile );
+ }
+}
+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 );
+ if ( !fVerbose )
+ return;
+ printf( "%02d : %s\n", 0, "const0" );
+ printf( "%02d : %s\n", 1, "const1" );
+ for ( i = 1; i < p->nDivs; i++ )
+ {
+ if ( nInputs < 6 )
+ {
+ *p->ppLits[2*i+0] = Abc_Tt6Stretch( *p->ppLits[2*i+0], nInputs );
+ *p->ppLits[2*i+1] = Abc_Tt6Stretch( *p->ppLits[2*i+1], nInputs );
+ }
+ printf("%02d : ", 2*i+0), Dau_DsdPrintFromTruth2(p->ppLits[2*i+0], nInputs), printf( "\n" );
+ printf("%02d : ", 2*i+1), Dau_DsdPrintFromTruth2(p->ppLits[2*i+1], nInputs), printf( "\n" );
+ }
+ for ( i = 0; i < (1 << p->nOuts); i++ )
+ {
+ if ( nInputs < 6 )
+ *p->ppSets[i] = Abc_Tt6Stretch( *p->ppSets[i], nInputs );
+ printf("%02d : ", i), Dau_DsdPrintFromTruth2(p->ppSets[i], nInputs), printf( "\n" );
+ }
+}
+static inline Vec_Int_t * Res6_ManReadSol( char * pFileName )
+{
+ Vec_Int_t * vRes = NULL; int Num;
+ FILE * pFile = fopen( pFileName, "rb" );
+ if ( pFile == NULL )
+ printf( "Cannot open input file \"%s\".\n", pFileName );
+ else
+ {
+ while ( fgetc(pFile) != '\n' );
+ vRes = Vec_IntAlloc( 10 );
+ while ( fscanf(pFile, "%d", &Num) == 1 )
+ Vec_IntPush( vRes, Num );
+ fclose ( pFile );
+ }
+ return vRes;
+}
+static inline void Res6_ManWriteSol( char * pFileName, Vec_Int_t * p )
+{
+ FILE * pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL )
+ printf( "Cannot open output file \"%s\".\n", pFileName );
+ else
+ {
+ int i, iLit;
+ Vec_IntForEachEntry( p, iLit, i )
+ fprintf( pFile, "%d ", iLit );
+ fclose ( pFile );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Res6_LitSign( int iLit )
+{
+ return Abc_LitIsCompl(iLit) ? '~' : ' ';
+}
+static inline int Res6_LitChar( int iLit, int nDivs )
+{
+ return Abc_Lit2Var(iLit) < nDivs ? (nDivs < 28 ? 'a'+Abc_Lit2Var(iLit)-1 : 'd') : 'x';
+}
+static inline void Res6_LitPrint( int iLit, int nDivs )
+{
+ if ( iLit < 2 )
+ printf( "%d", iLit );
+ else
+ {
+ printf( "%c%c", Res6_LitSign(iLit), Res6_LitChar(iLit, nDivs) );
+ if ( Abc_Lit2Var(iLit) >= nDivs || nDivs >= 28 )
+ printf( "%d", Abc_Lit2Var(iLit) );
+ }
+}
+void Res6_PrintSolution( Vec_Int_t * vSol, int nDivs )
+{
+ int iNode, nNodes = Vec_IntSize(vSol)/2-1;
+ assert( Vec_IntSize(vSol) % 2 == 0 );
+ printf( "Solution: In+Div = %d Node = %d Out = %d\n", nDivs-1, nNodes, 1 );
+ for ( iNode = 0; iNode <= nNodes; iNode++ )
+ {
+ int * pLits = Vec_IntEntryP( vSol, 2*iNode );
+ printf( "x%-2d = ", nDivs + iNode );
+ Res6_LitPrint( pLits[0], nDivs );
+ if ( pLits[0] != pLits[1] )
+ {
+ printf( " %c ", pLits[0] < pLits[1] ? '&' : '^' );
+ Res6_LitPrint( pLits[1], nDivs );
+ }
+ printf( "\n" );
+ }
+}
+int Res6_FindGetCost( Res6_Man_t * p, int iDiv )
+{
+ int w, Cost = 0;
+ //printf( "DivLit = %d\n", iDiv );
+ //Abc_TtPrintBinary1( stdout, p->ppLits[iDiv], p->nIns ); printf( "\n" );
+ //printf( "Set0\n" );
+ //Abc_TtPrintBinary1( stdout, p->ppSets[0], p->nIns ); printf( "\n" );
+ //printf( "Set1\n" );
+ //Abc_TtPrintBinary1( stdout, p->ppSets[1], p->nIns ); printf( "\n" );
+ for ( w = 0; w < p->nWords; w++ )
+ Cost += Abc_TtCountOnes( (p->ppLits[iDiv][w] & p->ppSets[0][w]) | (p->ppLits[iDiv^1][w] & p->ppSets[1][w]) );
+ return Cost;
+}
+int Res6_FindBestDiv( Res6_Man_t * p, int * pCost )
+{
+ int d, dBest = -1, CostBest = ABC_INFINITY;
+ for ( d = 0; d < 2*p->nDivs; d++ )
+ {
+ int Cost = Res6_FindGetCost( p, d );
+ printf( "Div = %d Cost = %d\n", d, Cost );
+ if ( CostBest >= Cost )
+ CostBest = Cost, dBest = d;
+ }
+ if ( pCost )
+ *pCost = CostBest;
+ return dBest;
+}
+int Res6_FindBestEval( Res6_Man_t * p, Vec_Int_t * vSol, int Start )
+{
+ int i, iLit0, iLit1;
+ assert( Vec_IntSize(vSol) % 2 == 0 );
+ Vec_IntForEachEntryDoubleStart( vSol, iLit0, iLit1, i, 2*Start )
+ {
+ if ( iLit0 > iLit1 )
+ {
+ Abc_TtXor( p->ppLits[2*p->nDivs+i+0], p->ppLits[iLit0], p->ppLits[iLit1], p->nWords, 0 );
+ Abc_TtXor( p->ppLits[2*p->nDivs+i+1], p->ppLits[iLit0], p->ppLits[iLit1], p->nWords, 1 );
+ }
+ else
+ {
+ Abc_TtAnd( p->ppLits[2*p->nDivs+i+0], p->ppLits[iLit0], p->ppLits[iLit1], p->nWords, 0 );
+ Abc_TtOr ( p->ppLits[2*p->nDivs+i+1], p->ppLits[iLit0^1], p->ppLits[iLit1^1], p->nWords );
+ }
+
+ //printf( "Node %d\n", i/2 );
+ //Abc_TtPrintBinary1( stdout, p->ppLits[2*p->nDivs+i+0], 6 ); printf( "\n" );
+ //Abc_TtPrintBinary1( stdout, p->ppLits[2*p->nDivs+i+1], 6 ); printf( "\n" );
+ }
+ return Res6_FindGetCost( p, Vec_IntEntryLast(vSol) );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res6_ManResubVerify( Res6_Man_t * p, Vec_Int_t * vSol )
+{
+ int Cost = Res6_FindBestEval( p, vSol, 0 );
+ if ( Cost == 0 )
+ printf( "Verification successful.\n" );
+ else
+ printf( "Verification FAILED with %d errors on %d patterns.\n", Cost, p->nPats );
+}
+void Res6_ManResubCheck( char * pFileNameRes, char * pFileNameSol, int fVerbose )
+{
+ char FileNameSol[1000];
+ if ( pFileNameSol )
+ strcpy( FileNameSol, pFileNameSol );
+ else
+ {
+ strcpy( FileNameSol, pFileNameRes );
+ strcpy( FileNameSol + strlen(FileNameSol) - strlen(".resub"), ".sol" );
+ }
+ {
+ Res6_Man_t * p = Res6_ManRead( pFileNameRes );
+ Vec_Int_t * vSol = Res6_ManReadSol( FileNameSol );
+ if ( p == NULL || vSol == NULL )
+ return;
+ if ( fVerbose )
+ Res6_ManPrintProblem( p, 0 );
+ if ( fVerbose )
+ Res6_PrintSolution( vSol, p->nDivs );
+ Res6_ManResubVerify( p, vSol );
+ Vec_IntFree( vSol );
+ Res6_ManStop( p );
+ }
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaSupps.c b/src/aig/gia/giaSupps.c
index f95d815d..f9f5b5e6 100644
--- a/src/aig/gia/giaSupps.c
+++ b/src/aig/gia/giaSupps.c
@@ -138,6 +138,7 @@ int Supp_DeriveLines( Supp_Man_t * p )
{
int n, i, iObj, nWords = p->nWords;
int nDivWords = Abc_Bit6WordNum( Vec_IntSize(p->vCands) );
+ //Vec_IntPrint( p->vCands );
for ( n = 0; n < 2; n++ )
{
p->vDivs[n] = Vec_WrdStart( 64*nWords*nDivWords );
@@ -656,6 +657,79 @@ int Supp_ManReconstruct( Supp_Man_t * p, int fVerbose )
return Supp_ManRandomSolution( p, iSet, fVerbose );
}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static int s_Counter = 0;
+
+void Supp_DeriveDumpSims( FILE * pFile, Vec_Wrd_t * vDivs, int nWords )
+{
+ int i, k, nDivs = Vec_WrdSize(vDivs)/nWords;
+ for ( i = 0; i < nDivs; i++ )
+ {
+ word * pSim = Vec_WrdEntryP(vDivs, i*nWords);
+ for ( k = 0; k < 64*nWords; k++ )
+ fprintf( pFile, "%c", '0'+Abc_TtGetBit(pSim, k) );
+ fprintf( pFile, "\n" );
+ }
+}
+void Supp_DeriveDumpProb( Vec_Wrd_t * vIsfs, Vec_Wrd_t * vDivs, int nWords )
+{
+ char Buffer[100]; int nDivs = Vec_WrdSize(vDivs)/nWords;
+ int RetValue = sprintf( Buffer, "case01_%02d.resub", 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, "%d %d %d %d\n", 0, nDivs, 1, 64*nWords );
+ Supp_DeriveDumpSims( pFile, vDivs, nWords );
+ Supp_DeriveDumpSims( pFile, vIsfs, nWords );
+ fclose ( pFile );
+ RetValue = 0;
+}
+void Supp_DeriveDumpSol( Vec_Int_t * vSet, Vec_Int_t * vRes, int nDivs )
+{
+ char Buffer[100];
+ int RetValue = sprintf( Buffer, "case01_%02d.sol", s_Counter );
+ int i, iLit, iLitRes = -1, nSupp = Vec_IntSize(vSet);
+ FILE * pFile = fopen( Buffer, "wb" );
+ if ( pFile == NULL )
+ printf( "Cannot open output file.\n" );
+ fprintf( pFile, "sol name aig %d\n", Vec_IntSize(vRes)/2 );
+ //Vec_IntPrint( vSet );
+ //Vec_IntPrint( vRes );
+ Vec_IntForEachEntry( vRes, iLit, i )
+ {
+ assert( iLit != 2 && iLit != 3 );
+ if ( iLit < 2 )
+ iLitRes = iLit;
+ else if ( iLit-4 < 2*nSupp )
+ {
+ int iDiv = Vec_IntEntry(vSet, Abc_Lit2Var(iLit-4));
+ assert( iDiv >= 0 && iDiv < nDivs );
+ iLitRes = Abc_Var2Lit(1+iDiv, Abc_LitIsCompl(iLit));
+ }
+ else
+ iLitRes = iLit + 2*((nDivs+1)-(nSupp+2));
+ fprintf( pFile, "%d ", iLitRes );
+ }
+ if ( Vec_IntSize(vRes) & 1 )
+ fprintf( pFile, "%d ", iLitRes );
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+ RetValue = 0;
+ printf( "Dumped solution info file \"%s\".\n", Buffer );
+}
+
/**Function*************************************************************
Synopsis []
@@ -705,6 +779,7 @@ Vec_Int_t * Supp_ManFindBestSolution( Supp_Man_t * p, Vec_Wec_t * vSols, int fVe
Vec_IntForEachEntry( vSet, iObj, i )
Vec_IntPush( *pvDivs, Vec_IntEntry(p->vCands, iObj) );
}
+ //Supp_DeriveDumpSol( vSet, vRes, Vec_WrdSize(p->vDivs[1])/p->nWords );
}
return vRes;
}
@@ -802,11 +877,40 @@ Vec_Int_t * Supp_ManCompute( Vec_Wrd_t * vIsfs, Vec_Int_t * vCands, Vec_Int_t *
Supp_PrintOne( p, iBest );
}
vRes = Supp_ManFindBestSolution( p, p->vSolutions, fVerbose, pvDivs );
+ //Supp_DeriveDumpProb( vIsfs, p->vDivs[1], p->nWords );
+ s_Counter++;
+ //Vec_IntPrint( vRes );
Supp_ManDelete( p );
// if ( vRes && Vec_IntSize(vRes) == 0 )
// Vec_IntFreeP( &vRes );
return vRes;
}
+void Supp_ManComputeTest( Gia_Man_t * p )
+{
+ Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
+ Vec_Wrd_t * vSims = Gia_ManSimPatSimOut( p, vSimsPi, 0 );
+ int i, iPoId, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p);
+ Vec_Wrd_t * vIsfs = Vec_WrdStart( 2*nWords );
+ Vec_Int_t * vCands = Vec_IntAlloc( 4 );
+ Vec_Int_t * vRes;
+
+// for ( i = 0; i < Gia_ManCiNum(p)+5; i++ )
+ for ( i = 0; i < Gia_ManCiNum(p); i++ )
+ Vec_IntPush( vCands, 1+i );
+
+ iPoId = Gia_ObjId(p, Gia_ManPo(p, 0));
+ Abc_TtCopy( Vec_WrdEntryP(vIsfs, 0*nWords), Vec_WrdEntryP(vSims, iPoId*nWords), nWords, 1 );
+ Abc_TtCopy( Vec_WrdEntryP(vIsfs, 1*nWords), Vec_WrdEntryP(vSims, iPoId*nWords), nWords, 0 );
+
+ vRes = Supp_ManCompute( vIsfs, vCands, NULL, vSims, NULL, nWords, p, NULL, 1, 1, 0 );
+ Vec_IntPrint( vRes );
+
+ Vec_WrdFree( vSimsPi );
+ Vec_WrdFree( vSims );
+ Vec_WrdFree( vIsfs );
+ Vec_IntFree( vCands );
+ Vec_IntFree( vRes );
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 1cb7331c..35fcb4df 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -69,6 +69,7 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaResub.c \
src/aig/gia/giaResub2.c \
src/aig/gia/giaResub3.c \
+ src/aig/gia/giaResub6.c \
src/aig/gia/giaRetime.c \
src/aig/gia/giaRex.c \
src/aig/gia/giaSatEdge.c \
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 71f8cad5..0b60baca 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -146,6 +146,7 @@ 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_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 );
@@ -894,6 +895,7 @@ 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_check", Abc_CommandResubCheck, 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 );
@@ -7802,6 +7804,64 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandResubCheck( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern void Res6_ManResubCheck( char * pFileNameRes, char * pFileNameSol, int fVerbose );
+ char * pFileR = NULL, * pFileS = NULL;
+ int fVerbose = 0, c;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( argc == globalUtilOptind + 2 )
+ {
+ pFileR = argv[globalUtilOptind];
+ pFileS = argv[globalUtilOptind+1];
+ }
+ else if ( argc == globalUtilOptind + 1 )
+ {
+ pFileR = argv[globalUtilOptind];
+ pFileS = NULL;
+ }
+ else
+ {
+ Abc_Print( -1, "Incorrect number of command line arguments.\n" );
+ return 1;
+ }
+ Res6_ManResubCheck( pFileR, pFileS, fVerbose );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: resub_check [-vh] <file1> <file2>\n" );
+ Abc_Print( -2, "\t checks solution to a resub problem\n" );
+ Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t<file1> : resub problem file name\n");
+ Abc_Print( -2, "\t<file2> : (optional) solution file name\n");
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandRr( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);