From c64f9278283546e2f58512526d943d9be30a72b6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 19 May 2024 14:47:18 -0700 Subject: [PATCH] Various changes and bug fixes. --- src/aig/gia/giaCut.c | 8 +++++++- src/aig/gia/giaDup.c | 4 +++- src/aig/gia/giaQbf.c | 7 ++++--- src/aig/gia/giaResub.c | 6 ++++-- src/aig/gia/giaResub6.c | 2 +- src/aig/gia/giaSupps.c | 4 +++- src/base/abci/abc.c | 5 ++++- src/sat/bmc/bmcMaj.c | 24 ++++++++++++------------ 8 files changed, 38 insertions(+), 22 deletions(-) diff --git a/src/aig/gia/giaCut.c b/src/aig/gia/giaCut.c index 19e2d8fc9f..45f1de71d1 100644 --- a/src/aig/gia/giaCut.c +++ b/src/aig/gia/giaCut.c @@ -986,10 +986,16 @@ Vec_Wec_t * Gia_ManExploreCuts( Gia_Man_t * pGia, int nCutSize0, int nCuts0, int Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart ); } vCutsSel = Gia_ManFilterCuts( pGia, p->vCuts, nCutSize0, nCuts0 ); - Gia_ManConsiderCuts( pGia, vCutsSel ); + //Gia_ManConsiderCuts( pGia, vCutsSel ); Gia_StoFree( p ); return vCutsSel; } +void Gia_ManExploreCutsTest( Gia_Man_t * pGia, int nCutSize0, int nCuts0, int fVerbose0 ) +{ + Vec_Wec_t * vCutSel = Gia_ManExploreCuts( pGia, nCutSize0, nCuts0, fVerbose0 ); + Vec_WecPrint( vCutSel, 0 ); + Vec_WecFree( vCutSel ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 35bc543944..64e7a16c9a 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -5952,7 +5952,9 @@ Gia_Man_t * Gia_ManDupWindow( Gia_Man_t * p, Vec_Int_t * vCut ) pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); Gia_ManForEachObjVec( vOuts, p, pObj, i ) pObj->Value = Gia_ManAppendCo( pNew, pObj->Value ); - printf( "Derived window with %d inputs, %d internal nodes, and %d outputs: ", Vec_IntSize(vCut), Vec_IntSize(vInner), Vec_IntSize(vOuts) ); + printf( "Derived window with %d inputs, %d internal nodes, and %d outputs.\n", Vec_IntSize(vCut), Vec_IntSize(vInner), Vec_IntSize(vOuts) ); + printf( "Outputs: " ); + Vec_IntPrint( vOuts ); Vec_IntFree( vInner ); Vec_IntFree( vOuts ); return pNew; diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index 2c2dbde36e..a4b21b5c3d 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -1011,8 +1011,6 @@ Vec_Int_t * Gia_ManGenCombs( Gia_Man_t * p, Vec_Int_t * vInsOuts, int fVerbose ) Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); return vRes; } - - void Gia_ManGenRel( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, char * pFileName, int fVerbose ) { Vec_Int_t * vRes = Gia_ManGenCombs( pGia, vInsOuts, fVerbose ); int i, k, Mask; @@ -1020,7 +1018,7 @@ void Gia_ManGenRel( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, char * pFi printf( "Enumerating solutions did not succeed.\n" ); return; } - Abc_RData_t * p = Abc_RDataStart( nIns, Vec_IntSize(vInsOuts)-nIns, Vec_IntSize(vRes) ); + Abc_RData_t * p2, * p = Abc_RDataStart( nIns, Vec_IntSize(vInsOuts)-nIns, Vec_IntSize(vRes) ); Vec_IntForEachEntry( vRes, Mask, i ) { for ( k = 0; k < Vec_IntSize(vInsOuts); k++ ) if ( (Mask >> (Vec_IntSize(vInsOuts)-1-k)) & 1 ) { // the bit is 1 @@ -1035,6 +1033,9 @@ void Gia_ManGenRel( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, char * pFi } } Abc_WritePla( p, pFileName, 0 ); + p2 = Abc_RData2Rel( p ); + Abc_WritePla( p2, Extra_FileNameGenericAppend(pFileName, "_rel.pla"), 1 ); + Abc_RDataStop( p2 ); Abc_RDataStop( p ); Vec_IntFree( vRes ); } diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c index 7de1283e40..fc6fd7bf02 100644 --- a/src/aig/gia/giaResub.c +++ b/src/aig/gia/giaResub.c @@ -2117,7 +2117,9 @@ void Gia_ManResubRecordSolution( char * pFileName, Vec_Int_t * vRes, int nDivs ) 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 ); + Abc_RData_t * p = Abc_ReadPla( pFileName ); + if ( p == NULL ) return NULL; + 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) ); @@ -2132,7 +2134,7 @@ Gia_Man_t * Gia_ManResubUnateOne( char * pFileName, int nLimit, int nDivMax, int for ( k = 0; k < ArraySize; k++ ) Vec_IntPush( vRes, pArray[k] ); if ( ArraySize ) { - //printf( "Divisors = %d. Solution: ", Vec_PtrSize(vDivs) ), Vec_IntPrint( vRes ); + //Vec_IntPrint( vRes ); Vec_Wec_t * vGates = Vec_WecStart(1); Vec_IntAppend( Vec_WecEntry(vGates, 0), vRes ); pNew = Gia_ManConstructFromGates( vGates, Vec_PtrSize(vDivs) ); diff --git a/src/aig/gia/giaResub6.c b/src/aig/gia/giaResub6.c index 02bb269634..85d5bb094a 100644 --- a/src/aig/gia/giaResub6.c +++ b/src/aig/gia/giaResub6.c @@ -235,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 Pat = %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" ); diff --git a/src/aig/gia/giaSupps.c b/src/aig/gia/giaSupps.c index 2d2f202de4..558411eda2 100644 --- a/src/aig/gia/giaSupps.c +++ b/src/aig/gia/giaSupps.c @@ -1129,7 +1129,9 @@ Gia_Man_t * Supp_GenerateGia( Vec_Int_t * vRes, Vec_Int_t * vDivs ) 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 ); + if ( p == NULL ) return NULL; + 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 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a260f0bd74..4251f69d7b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -53250,7 +53250,10 @@ int Abc_CommandAbc9Window( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( argc == globalUtilOptind ) { - Abc_Print( -1, "Abc_CommandAbc9Window(): Node IDs should be given on the command line.\n" ); + int nCutSize = 6, nCuts = 30; + extern void Gia_ManExploreCutsTest( Gia_Man_t * pGia, int nCutSize, int nCuts, int fVerbose ); + printf( "Here are %d the most frequently appearing %d-cuts:\n", nCutSize, nCuts ); + Gia_ManExploreCutsTest( pAbc->pGia, nCutSize, nCuts, fVerbose ); return 0; } if ( argc-globalUtilOptind < 1 ) diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index 6c2e29b1d7..3b31de0ded 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -3420,7 +3420,7 @@ void Exa6_ManGenMint( Exa6_Man_t * p, int iMint, int fOnlyAnd, int fFancy ) assert( t ); if ( ~t ) { - Abc_Tt6IsopCover( t, t, p->nOuts, pCover, &nCubes ); + Abc_Tt6IsopCover( ~t, ~t, p->nOuts, pCover, &nCubes ); for ( c = 0; c < nCubes; c++ ) { int nLits = 0; @@ -3664,7 +3664,7 @@ Vec_Wrd_t * Exa6_ManTransformOutputs( Vec_Wrd_t * vOuts, int nOuts ) Vec_Wrd_t * Exa6_ManTransformInputs( Vec_Wrd_t * vIns ) { Vec_Wrd_t * vRes = Vec_WrdAlloc( Vec_WrdSize(vIns) ); - int i, Polar = Vec_WrdEntry( vIns, 0 ); word Entry; + int i; word Entry, Polar = Vec_WrdEntry( vIns, 0 ); Vec_WrdForEachEntry( vIns, Entry, i ) Vec_WrdPush( vRes, Entry ^ Polar ); return vRes; @@ -3679,7 +3679,7 @@ void Exa_ManExactPrint( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut, int nDivs, i Abc_TtPrintBits( &Entry, 1 << nOuts ); printf( "\n" ); } -Mini_Aig_t * Exa_ManExactSynthesis6Int( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut, int nVars, int nDivs, int nOuts, int nNodes, int fOnlyAnd, int fVerbose ) +Mini_Aig_t * Exa_ManExactSynthesis6Int( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut, int nVars, int nDivs, int nOuts, int nNodes, int fOnlyAnd, int fVerbose, char * pFileName ) { Mini_Aig_t * pTemp, * pMini; Vec_Wrd_t * vSimsDiv2, * vSimsOut2; @@ -3701,10 +3701,10 @@ Mini_Aig_t * Exa_ManExactSynthesis6Int( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsO pMini = Mini_AigDupCompl( pTemp = pMini, DivCompl, OutCompl ); Mini_AigStop( pTemp ); } - Mini_AigerWrite( "exa6.aig", pMini, 1 ); - if ( nVars <= 6 ) - Exa_ManMiniVerify( pMini, vSimsDiv, vSimsOut ); - printf( "\n" ); + Mini_AigerWrite( Extra_FileNameGenericAppend(pFileName, "_twoexact.aig"), pMini, 1 ); + //if ( nVars <= 6 ) + // Exa_ManMiniVerify( pMini, vSimsDiv, vSimsOut ); + //printf( "\n" ); //Mini_AigStop( pMini ); } Vec_WrdFreeP( &vSimsDiv2 ); @@ -3725,14 +3725,14 @@ void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName ) nDivs = 0; nOuts = p->nOuts; nVars = p->nIns; - vSimsDiv = Vec_WrdStart( p->nPats ); + vSimsDiv = Vec_WrdStart( p2->nPats ); for ( k = 0; k < p->nIns; k++ ) - for ( i = 0; i < p->nPats; i++ ) + for ( i = 0; i < p2->nPats; i++ ) if ( Abc_RDataGetIn(p2, k, i) ) Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsDiv, i), 1+k); - vSimsOut = Vec_WrdStart( 1 << p->nOuts ); + vSimsOut = Vec_WrdStart( p2->nPats ); for ( k = 0; k < (1 << p->nOuts); k++ ) - for ( i = 0; i < p->nPats; i++ ) + for ( i = 0; i < p2->nPats; i++ ) if ( Abc_RDataGetOut(p2, k, i) ) Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsOut, i), k); Abc_RDataStop( p ); @@ -3745,7 +3745,7 @@ void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName ) //Vec_WrdPrintBin( vSimsDiv, 1 ); //Vec_WrdPrintBin( vSimsOut, 1 ); Exa6_SortSims( vSimsDiv, vSimsOut ); - pMini = Exa_ManExactSynthesis6Int( vSimsDiv, vSimsOut, nVars, nDivs, nOuts, pPars->nNodes, pPars->fOnlyAnd, pPars->fVerbose ); + pMini = Exa_ManExactSynthesis6Int( vSimsDiv, vSimsOut, nVars, nDivs, nOuts, pPars->nNodes, pPars->fOnlyAnd, pPars->fVerbose, pFileName ); Vec_WrdFreeP( &vSimsDiv ); Vec_WrdFreeP( &vSimsOut ); if ( pMini ) Mini_AigStop( pMini );