From e7dd9151b1020a8c0612d769abe7096b362ee689 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 18 Mar 2025 17:51:40 -0700 Subject: [PATCH] Adding structural guidance. --- src/aig/gia/giaSatLut.c | 53 ++++++++++++++++++++++++++++++++++++---- src/aig/gia/giaSimBase.c | 4 +-- src/base/abci/abc.c | 34 ++++++++++++++++++++------ src/sat/bmc/bmc.h | 1 + src/sat/bmc/bmcMaj.c | 33 +++++++++++++++++++------ 5 files changed, 103 insertions(+), 22 deletions(-) diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c index df92030b9..cc6068a96 100644 --- a/src/aig/gia/giaSatLut.c +++ b/src/aig/gia/giaSatLut.c @@ -1683,12 +1683,54 @@ int Gia_KSatFindFan( int * pMap, int i, int f, Vec_Int_t * vRes ) return -1; } -Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound, int fMultiLevel ) +Vec_Int_t * Gia_ManKSatGenLevels( char * pGuide, int nIns, int nNodes ) +{ + Vec_Int_t * vRes; + int i, k, Count = 0; + for ( i = 0; pGuide[i]; i++ ) + Count += pGuide[i] - '0'; + if ( Count != nNodes ) { + printf( "Guidance %s has %d nodes while the problem has %d nodes.\n", pGuide, Count, nNodes ); + return NULL; + } + int FirstPrev = 0; + int FirstThis = nIns; + int FirstNext = FirstThis; + vRes = Vec_IntStartFull( 2*nIns ); + for ( i = 0; pGuide[i]; i++ ) { + FirstNext += pGuide[i] - '0'; + for ( k = FirstThis; k < FirstNext; k++ ) + Vec_IntPushTwo( vRes, FirstPrev, FirstThis ); + FirstPrev = FirstThis; + FirstThis = FirstNext; + } + assert( Vec_IntSize(vRes) == 2*(nIns + nNodes) ); + Count = 0; + //int Start, Stop; + //Vec_IntForEachEntryDouble(vRes, Start, Stop, i) + // printf( "%2d : Start %2d Stop %2d\n", Count++, Start, Stop ); + return vRes; +} + +Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound, int fMultiLevel, char * pGuide ) { Vec_Str_t * vStr = Vec_StrAlloc( 10000 ); - int i, j, m, n, f, c, a, nLits = 0, pLits[256] = {0}; + Vec_Int_t * vRes = pGuide ? Gia_ManKSatGenLevels( pGuide, nIns, nNodes ) : NULL; + int i, j, m, n, f, c, a, Start, Stop, nLits = 0, pLits[256] = {0}; Gia_SatDumpLiteral( vStr, 1 ); - Gia_SatDumpLiteral( vStr, 2 ); + Gia_SatDumpLiteral( vStr, 2 ); + if ( vRes ) { + n = nIns; + Vec_IntForEachEntryDoubleStart( vRes, Start, Stop, i, 2*nIns ) { + for ( j = 0; j < Start; j++ ) + Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, j), 1 ) ); + for ( f = 0; f < 2; f++ ) + for ( j = Stop; j < n; j++ ) + Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, j), 1 ) ); + n++; + } + assert( n == nIns + nNodes ); + } // fanins are connected once for ( n = nIns; n < nIns+nNodes; n++ ) for ( f = 0; f < 2; f++ ) { @@ -1854,6 +1896,7 @@ Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound, int fM Gia_SatDumpClause( vStr, pLits, nLits ); } Vec_StrPush( vStr, '\0' ); + Vec_IntFreeP( &vRes ); return vStr; } @@ -2005,7 +2048,7 @@ word Gia_ManGetTruth( Gia_Man_t * p ) return Const[Gia_ObjFaninC0(pObj)] ^ pFuncs[Gia_ObjFaninId0p(p, pObj)]; } -Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int Seed, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv ) +Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int Seed, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv, char * pGuide ) { abctime clkStart = Abc_Clock(); Gia_Man_t * pNew = NULL; @@ -2014,7 +2057,7 @@ Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, in char pFileNameI[32]; sprintf( pFileNameI, "_%06x_.cnf", Rand ); char pFileNameO[32]; sprintf( pFileNameO, "_%06x_.out", Rand ); int nVars = 0, * pMap = Gia_KSatMapInit( nIns, nNodes, Truth, &nVars ); - Vec_Str_t * vStr = Gia_ManKSatCnf( pMap, nIns, nNodes, nBound/2, fMultiLevel ); + Vec_Str_t * vStr = Gia_ManKSatCnf( pMap, nIns, nNodes, nBound/2, fMultiLevel, pGuide ); if ( !Gia_ManDumpCnf(pFileNameI, vStr, nVars) ) { Vec_StrFree( vStr ); return NULL; diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index e5cf77dcb..b5c3c0802 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -3199,7 +3199,7 @@ Vec_Int_t * Gia_ManRelDeriveSimple( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts, Vec_Int_t * vRel, Vec_Int_t * vDivs ) { - extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard ); + extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard, char * pGuide ); int i, m, iObj, Entry, iMint = 0, nMints = Vec_IntSize(vRel) - Vec_IntCountEntry(vRel, -1); Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints ); @@ -3232,7 +3232,7 @@ void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_In } assert( iMint == nMints ); printf( "Created %d minterms.\n", iMint ); - Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 0, 1, 0 ); + Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 0, 1, 0, NULL ); Vec_WrdFree( vSimsIn ); Vec_WrdFree( vSimsOut ); } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0e898d63c..faaa6f639 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -10061,7 +10061,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INTGabdconugklmvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INTGSabdconugklmvh" ) ) != EOF ) { switch ( c ) { @@ -10109,6 +10109,15 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( GateSize < 0 ) goto usage; break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by a file name.\n" ); + goto usage; + } + pPars->pGuide = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'a': pPars->fOnlyAnd ^= 1; break; @@ -10193,12 +10202,13 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: twoexact [-INTG ] [-abdconugklmvh] \n" ); + Abc_Print( -2, "usage: twoexact [-INTG ] [-S str] [-abdconugklmvh] \n" ); Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" ); Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-N : the number of two-input nodes [default = %d]\n", pPars->nNodes ); Abc_Print( -2, "\t-T : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); Abc_Print( -2, "\t-G : the largest allowed gate size (NANDs only) [default = %d]\n", GateSize ); + Abc_Print( -2, "\t-S : structural guidance from the user [default = %s]\n", pPars->pGuide ? pPars->pGuide : "unknown" ); Abc_Print( -2, "\t-a : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); Abc_Print( -2, "\t-b : toggle using only NAND-gates [default = %s]\n", fUseNands ? "yes" : "no" ); Abc_Print( -2, "\t-d : toggle using dynamic constraint addition [default = %s]\n", pPars->fDynConstr ? "yes" : "no" ); @@ -44559,11 +44569,11 @@ usage: int Abc_CommandAbc9Exmap( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Mio_IntallSimpleLibrary2(); - extern Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int Seed, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv ); - Gia_Man_t * pTemp = NULL; char * pTruth = NULL; word Truth = 0; + extern Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int Seed, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv, char * pGuide ); + Gia_Man_t * pTemp = NULL; char * pTruth = NULL, * pGuide = NULL; word Truth = 0; int c, nVars = 0, nNodes = 0, nVars2, Seed = 0, nBTLimit = 0, nBound = 0, fMultiLevel = 0, nTimeout = 0, fKeepFile = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NBRCTmfvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "NBRCTSmfvh" ) ) != EOF ) { switch ( c ) { @@ -44627,6 +44637,15 @@ int Abc_CommandAbc9Exmap( Abc_Frame_t * pAbc, int argc, char ** argv ) nTimeout = atoi(argv[globalUtilOptind]); globalUtilOptind++; break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by a file name.\n" ); + goto usage; + } + pGuide = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'm': fMultiLevel ^= 1; break; @@ -44665,7 +44684,7 @@ int Abc_CommandAbc9Exmap( Abc_Frame_t * pAbc, int argc, char ** argv ) } nVars2 = Abc_TtReadHex( &Truth, pTruth ); assert( nVars2 == nVars ); - pTemp = Gia_ManKSatMapping( Truth, nVars, nNodes, nBound, Seed, fMultiLevel, nBTLimit, nTimeout, fVerbose, fKeepFile, argc, argv ); + pTemp = Gia_ManKSatMapping( Truth, nVars, nNodes, nBound, Seed, fMultiLevel, nBTLimit, nTimeout, fVerbose, fKeepFile, argc, argv, pGuide ); if ( pTemp ) { //Mio_IntallSimpleLibrary2(); Abc_FrameUpdateGia( pAbc, pTemp ); @@ -44673,13 +44692,14 @@ int Abc_CommandAbc9Exmap( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &exmap [-NBRCT num] [-mfvh] \n" ); + Abc_Print( -2, "usage: &exmap [-NBRCT num] [-S str] [-mfvh] \n" ); Abc_Print( -2, "\t performs simple mapping of the truth table\n" ); Abc_Print( -2, "\t-N num : the number of nodes [default = %d]\n", nNodes ); Abc_Print( -2, "\t-B num : the bound on the solution size [default = %d]\n", nBound ); Abc_Print( -2, "\t-R num : random number generator seed [default = %d]\n", Seed ); Abc_Print( -2, "\t-C num : the conflict limit [default = %d]\n", nBTLimit ); Abc_Print( -2, "\t-T num : runtime limit in seconds [default = %d]\n", nTimeout ); + Abc_Print( -2, "\t-S str : structural guidance from the user [default = %s]\n", pGuide ? pGuide : "unknown" ); Abc_Print( -2, "\t-m : toggles using multi-level primitives [default = %s]\n", fMultiLevel? "yes": "no" ); Abc_Print( -2, "\t-f : toggles keeping the intermediate CNF file [default = %s]\n", fKeepFile? "yes": "no" ); Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 320a85886..233930178 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -70,6 +70,7 @@ struct Bmc_EsPar_t_ int fVerbose; char * pTtStr; char * pSymStr; + char * pGuide; }; static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars ) diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index ca11102bf..3440ac514 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -1941,9 +1941,25 @@ static inline int Exa4_ManAddClause4( Exa4_Man_t * p, int Lit0, int Lit1, int Li int pLits[4] = { Lit0, Lit1, Lit2, Lit3 }; return Exa4_ManAddClause( p, pLits, 4 ); } -int Exa4_ManGenStart( Exa4_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard ) +int Exa4_ManGenStart( Exa4_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard, char * pGuide ) { - int pLits[2*MAJ_NOBJS], i, j, k, n, m, nLits; + extern Vec_Int_t * Gia_ManKSatGenLevels( char * pGuide, int nIns, int nNodes ); + Vec_Int_t * vRes = pGuide ? Gia_ManKSatGenLevels( pGuide, p->nDivs, p->nNodes ) : NULL; + int pLits[2*MAJ_NOBJS], i, j, k, n, m, nLits, Start, Stop; + if ( vRes ) { + n = p->nDivs; + Vec_IntForEachEntryDoubleStart( vRes, Start, Stop, i, 2*p->nDivs ) { + for ( j = 0; j < Start; j++ ) + if ( p->VarMarks[n][0][j] ) + Exa4_ManAddClause4( p, Abc_Var2Lit( p->VarMarks[n][0][j], 1 ), 0, 0, 0 ); + for ( k = 0; k < 2; k++ ) + for ( j = Stop; j < n; j++ ) + if ( p->VarMarks[n][k][j] ) + Exa4_ManAddClause4( p, Abc_Var2Lit( p->VarMarks[n][k][j], 1 ), 0, 0, 0 ); + n++; + } + assert( n == p->nDivs + p->nNodes ); + } for ( i = p->nDivs; i < p->nDivs + p->nNodes; i++ ) { int iVarStart = 1 + 5*(i - p->nDivs);// @@ -2023,6 +2039,7 @@ int Exa4_ManGenStart( Exa4_Man_t * p, int fOnlyAnd, int fFancy, int fOrderNodes, for ( m = n+1; m < nLits; m++ ) Exa4_ManAddClause4( p, Abc_LitNot(pLits[n]), Abc_LitNot(pLits[m]), 0, 0 ); } + Vec_IntFreeP( &vRes ); return 1; } void Exa4_ManGenMint( Exa4_Man_t * p, int iMint, int fOnlyAnd, int fFancy ) @@ -2104,13 +2121,13 @@ void Exa4_ManGenMint( Exa4_Man_t * p, int iMint, int fOnlyAnd, int fFancy ) Exa4_ManAddClause4( p, Abc_Var2Lit(p->VarMarks[i][0][j], 1), Abc_LitNotCond(VarVals[j], n), Abc_LitNotCond(VarVals[i], !n), 0); } } -void Exa4_ManGenCnf( Exa4_Man_t * p, char * pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard ) +void Exa4_ManGenCnf( Exa4_Man_t * p, char * pFileName, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fCard, char * pGuide ) { int m; assert( p->pFile == NULL ); p->pFile = fopen( pFileName, "wb" ); fputs( "p cnf \n", p->pFile ); - Exa4_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard ); + Exa4_ManGenStart( p, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard, pGuide ); for ( m = 1; m < Vec_WrdSize(p->vSimsIn); m++ ) Exa4_ManGenMint( p, m, fOnlyAnd, fFancy ); rewind( p->pFile ); @@ -2278,7 +2295,7 @@ Mini_Aig_t * Exa4_ManMiniAig( Exa4_Man_t * p, Vec_Int_t * vValues, int fFancy ) SeeAlso [] ***********************************************************************/ -Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard ) +Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard, char * pGuide ) { extern Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int Seed, int nBTLimit, int TimeOut, int fVerbose, int * pStatus ); Mini_Aig_t * pMini = NULL; @@ -2290,7 +2307,7 @@ Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIn char pFileNameOut[32]; sprintf( pFileNameOut, "_%05x_.out", Rand ); Exa4_Man_t * p = Exa4_ManAlloc( vSimsIn, vSimsOut, nIns, nDivs, nOuts, nNodes, fVerbose ); Exa_ManIsNormalized( vSimsIn, vSimsOut ); - Exa4_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard ); + Exa4_ManGenCnf( p, pFileNameIn, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fCard, pGuide ); if ( fVerbose ) printf( "Timeout = %d. OnlyAnd = %d. Fancy = %d. OrderNodes = %d. UniqueFans = %d. Verbose = %d.\n", TimeOut, fOnlyAnd, fFancy, fOrderNodes, fUniqFans, fVerbose ); if ( fVerbose ) @@ -2327,7 +2344,7 @@ void Exa_ManExactSynthesis4_( Bmc_EsPar_t * pPars ) if ( (m >> i) & 1 ) Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i ); } - pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, 3, 4, 2, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, 0 ); + pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, 3, 4, 2, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, 0, pPars->pGuide ); if ( pMini ) Mini_AigStop( pMini ); Vec_WrdFree( vSimsIn ); Vec_WrdFree( vSimsOut ); @@ -2349,7 +2366,7 @@ void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars ) Abc_TtSetBit( Vec_WrdEntryP(vSimsIn, m), 1+i ); } assert( Vec_WrdSize(vSimsIn) == (1 << pPars->nVars) ); - pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, pPars->nVars, 1+pPars->nVars, 1, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, pPars->fCard ); + pMini = Exa4_ManGenTest( vSimsIn, vSimsOut, pPars->nVars, 1+pPars->nVars, 1, pPars->nNodes, pPars->RuntimeLim, pPars->fOnlyAnd, pPars->fFewerVars, pPars->fOrderNodes, pPars->fUniqFans, pPars->fVerbose, pPars->fCard, pPars->pGuide ); if ( pMini ) Mini_AigStop( pMini ); if ( fCompl ) printf( "The resulting circuit, if computed, will be complemented.\n" ); Vec_WrdFree( vSimsIn );