diff --git a/src/aig/gia/giaGen.c b/src/aig/gia/giaGen.c index 426409c70..edd3a28af 100644 --- a/src/aig/gia/giaGen.c +++ b/src/aig/gia/giaGen.c @@ -1446,23 +1446,76 @@ void Gia_ManGenPrefix( Gia_Man_t * pNew, int * p, int * g, int p2, int g2 ) *g = Gia_ManHashOr(pNew, *g, Gia_ManHashAnd(pNew, *p, g2)); *p = Gia_ManHashAnd(pNew, *p, p2); } -Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries, int fVerbose ) +static int Gia_ManGenAdderMaj( Gia_Man_t * p, int a, int b, int c ) +{ + int ab = Gia_ManHashAnd( p, a, b ); + int ac = Gia_ManHashAnd( p, a, c ); + int bc = Gia_ManHashAnd( p, b, c ); + return Gia_ManHashOr( p, ab, Gia_ManHashOr( p, ac, bc ) ); +} +static int Gia_ManGenAdderFloorPow2( int n ) +{ + int r = 1; + assert( n > 0 ); + while ( r <= n / 2 ) + r *= 2; + return r; +} +static void Gia_ManGenAdderMMRange( Gia_Man_t * p, int nVars, int * pLitsI, int * pM0, int * pM1, int i, int k ) +{ + int Index = i * nVars + k; + int nRange, nLeft, j; + assert( 0 <= i && i <= k && k < nVars ); + if ( pM0[Index] >= 0 ) + return; + if ( i == k ) + { + pM0[Index] = pLitsI[2*i]; + pM1[Index] = pLitsI[2*i+1]; + return; + } + nRange = k - i + 1; + nLeft = Gia_ManGenAdderFloorPow2( nRange - 1 ); + j = i + nLeft - 1; + Gia_ManGenAdderMMRange( p, nVars, pLitsI, pM0, pM1, i, j ); + Gia_ManGenAdderMMRange( p, nVars, pLitsI, pM0, pM1, j+1, k ); + pM0[Index] = Gia_ManGenAdderMaj( p, pM0[(j+1)*nVars+k], pM1[(j+1)*nVars+k], pM0[i*nVars+j] ); + pM1[Index] = Gia_ManGenAdderMaj( p, pM0[(j+1)*nVars+k], pM1[(j+1)*nVars+k], pM1[i*nVars+j] ); +} +static int Gia_ManGenAdderMMCarry( Gia_Man_t * p, int nVars, int * pLitsI, int * pM0, int * pM1, int * pCarries, int iCarry ) +{ + int nBase, iBeg; + assert( 0 <= iCarry && iCarry <= nVars ); + if ( pCarries[iCarry] >= 0 ) + return pCarries[iCarry]; + nBase = Gia_ManGenAdderFloorPow2( iCarry ); + iBeg = nBase - 1; + Gia_ManGenAdderMMRange( p, nVars, pLitsI, pM0, pM1, iBeg, iCarry-1 ); + pCarries[iCarry] = Gia_ManGenAdderMaj( p, pM0[iBeg*nVars+iCarry-1], pM1[iBeg*nVars+iCarry-1], Gia_ManGenAdderMMCarry( p, nVars, pLitsI, pM0, pM1, pCarries, iBeg ) ); + return pCarries[iCarry]; +} +Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fMM, int fCarries, int fVerbose ) { extern void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps ); int i, k, nBits = Abc_Base2Log(nVars), nVarsAlloc = (1 << nBits) + 2; - int ** pStore = (int **)Extra_ArrayAlloc( nVarsAlloc, nVarsAlloc, 4 ); + int ** pStore = fMM ? NULL : (int **)Extra_ArrayAlloc( nVarsAlloc, nVarsAlloc, 4 ); printf( "Generating %d-bit ", nVars ); - Gia_ManGenPrep( nVars+2, pStore ); - if ( fSK ) - Gia_ManGenSK( nVars, pStore ), printf("Sklansky "); - else if ( fBK ) - Gia_ManGenBK( nVars, pStore ), printf("Brent-Kung "); - else if ( fHC ) - Gia_ManGenHC( nVars, pStore ), printf("Huan-Carlsson "); + if ( fMM ) + printf("M/M "); else - Gia_ManGenRca( nVars, pStore ), printf("ripple-carry "); + { + Gia_ManGenPrep( nVars+2, pStore ); + if ( fSK ) + Gia_ManGenSK( nVars, pStore ), printf("Sklansky "); + else if ( fBK ) + Gia_ManGenBK( nVars, pStore ), printf("Brent-Kung "); + else if ( fHC ) + Gia_ManGenHC( nVars, pStore ), printf("Huan-Carlsson "); + else + Gia_ManGenRca( nVars, pStore ), printf("ripple-carry "); + } printf( "adder with%s carry-in and carry-out\n", fCarries ? "":"out" ); - if ( fVerbose ) Gia_ManGenPrint( nVars, pStore ); + if ( fVerbose && !fMM ) Gia_ManGenPrint( nVars, pStore ); Gia_Man_t * p = Gia_ManStart( 1000 ), * pTemp; p->pName = Abc_UtilStrsav( "adder" ); int * pLitsI = ABC_CALLOC( int, 2*nVars+10 ); @@ -1472,6 +1525,33 @@ Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries, pLitsI[2*k+1] = Gia_ManAppendCi(p); int Carry = fCarries ? Gia_ManAppendCi(p) : 0; Gia_ManHashStart( p ); + if ( fMM ) + { + int nPairs = nVars * nVars; + int * pM0 = ABC_ALLOC( int, nPairs ); + int * pM1 = ABC_ALLOC( int, nPairs ); + int * pCarries = ABC_ALLOC( int, nVars + 1 ); + int * pProps = ABC_ALLOC( int, nVars ); + for ( k = 0; k < nPairs; k++ ) + pM0[k] = pM1[k] = -1; + for ( k = 0; k <= nVars; k++ ) + pCarries[k] = -1; + pCarries[0] = Carry; + for ( k = 0; k < nVars; k++ ) + pProps[k] = Gia_ManHashXor( p, pLitsI[2*k], pLitsI[2*k+1] ); + if ( fCarries ) + Gia_ManAppendCo( p, Gia_ManGenAdderMMCarry( p, nVars, pLitsI, pM0, pM1, pCarries, nVars ) ); + for ( k = 0; k < nVars; k++ ) + Gia_ManAppendCo( p, Gia_ManHashXor( p, pProps[k], Gia_ManGenAdderMMCarry( p, nVars, pLitsI, pM0, pM1, pCarries, k ) ) ); + ABC_FREE( pM0 ); + ABC_FREE( pM1 ); + ABC_FREE( pCarries ); + ABC_FREE( pProps ); + ABC_FREE( pLitsI ); + p = Gia_ManCleanup( pTemp = p ); + Gia_ManStop( pTemp ); + return p; + } for ( k = 0; k < nVars; k++ ) Wlc_BlastFullAdder( p, pLitsI[2*k], pLitsI[2*k+1], k ? 0 : Carry, &pLitsI[2*k+1], &pLitsI[2*k] ); int * pLits = ABC_CALLOC( int, 2*nVars+10 ); @@ -1498,4 +1578,3 @@ Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries, ABC_NAMESPACE_IMPL_END - diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dc249282c..9a4e638df 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -10603,19 +10603,391 @@ usage: SeeAlso [] ***********************************************************************/ +static int Abc_TwoExactPermAddFanin( int * pFans, int iNode, int iFanin ) +{ + int * pNode = pFans + 2 * iNode; + if ( pNode[0] == iFanin || pNode[1] == iFanin ) + return 0; + if ( pNode[0] == -1 && pNode[1] == -1 ) + pNode[Abc_Random(0) & 1] = iFanin; + else if ( pNode[0] == -1 ) + pNode[0] = iFanin; + else if ( pNode[1] == -1 ) + pNode[1] = iFanin; + else + return 0; + return 1; +} +static int Abc_TwoExactPermAddRequired( int * pFans, int nVars, int nNodes, int iFanin ) +{ + int iNodeStart = (iFanin + 1 > nVars) ? iFanin + 1 - nVars : 0; + int i, nChoices = 0, iChoice = -1; + for ( i = iNodeStart; i < nNodes; i++ ) + { + int * pNode = pFans + 2 * i; + if ( pNode[0] == iFanin || pNode[1] == iFanin ) + continue; + if ( pNode[0] != -1 && pNode[1] != -1 ) + continue; + if ( Abc_Random(0) % ++nChoices == 0 ) + iChoice = i; + } + return iChoice >= 0 && Abc_TwoExactPermAddFanin( pFans, iChoice, iFanin ); +} +static int Abc_TwoExactPermCountDistinct( int * pFans, int nVars, int iNode ) +{ + int iPrevObj = nVars + iNode - 1; + int pVals[4], nVals = 0, i, k; + assert( iNode > 0 ); + for ( i = iNode - 1; i <= iNode; i++ ) + for ( k = 0; k < 2; k++ ) + { + int v = pFans[2 * i + k]; + int j, fSeen = 0; + if ( v == iPrevObj ) + continue; + for ( j = 0; j < nVals; j++ ) + fSeen |= pVals[j] == v; + if ( !fSeen ) + pVals[nVals++] = v; + } + return nVals; +} +static int Abc_TwoExactPermCheck( int * pFans, int nVars, int nNodes, int fStrict ) +{ + int nObjs = nVars + nNodes; + int * pUsed = ABC_CALLOC( int, nObjs ); + int i, RetValue = 1; + for ( i = 0; i < nNodes; i++ ) + { + if ( pFans[2*i] < 0 || pFans[2*i+1] < 0 || pFans[2*i] >= nVars + i || pFans[2*i+1] >= nVars + i || pFans[2*i] == pFans[2*i+1] ) + RetValue = 0; + if ( fStrict && i > 0 && Abc_TwoExactPermCountDistinct(pFans, nVars, i) < 3 ) + RetValue = 0; + if ( !RetValue ) + break; + pUsed[pFans[2*i]]++; + pUsed[pFans[2*i+1]]++; + } + if ( RetValue ) + for ( i = 0; i < nObjs - 1; i++ ) + if ( pUsed[i] == 0 ) + { + RetValue = 0; + break; + } + ABC_FREE( pUsed ); + return RetValue; +} +static char * Abc_TwoExactPermEncode( int * pFans, int nVars, int nNodes ) +{ + char * pPerm = ABC_ALLOC( char, 3 * nNodes ); + int i, k, Pos = 0; + for ( i = 0; i < nNodes; i++ ) + { + if ( i ) + pPerm[Pos++] = '_'; + for ( k = 0; k < 2; k++ ) + pPerm[Pos++] = pFans[2*i+k] >= 0 && pFans[2*i+k] < nVars ? 'a' + pFans[2*i+k] : '*'; + } + pPerm[Pos] = 0; + return pPerm; +} +static char * Abc_TwoExactObjName( int iObj, int nVars, char * pBuffer ) +{ + if ( iObj < 0 ) + sprintf( pBuffer, "*" ); + else if ( iObj < nVars ) + sprintf( pBuffer, "%c", 'a' + iObj ); + else if ( iObj - nVars < 26 ) + sprintf( pBuffer, "%c", 'A' + iObj - nVars ); + else + sprintf( pBuffer, "N%d", iObj - nVars ); + return pBuffer; +} +static char * Abc_TwoExactPermEncodeFull( int * pFans, int nVars, int nNodes ) +{ + int nSize = 8 * (nNodes + 1); + char * pPerm = ABC_ALLOC( char, nSize ); + int i, k, Pos = 0; + char Name[16]; + for ( i = 0; i < nNodes; i++ ) + { + if ( i ) + pPerm[Pos++] = '_'; + for ( k = 0; k < 2; k++ ) + Pos += sprintf( pPerm + Pos, "%s", Abc_TwoExactObjName(pFans[2*i+k], nVars, Name) ); + } + pPerm[Pos] = 0; + return pPerm; +} +static int Abc_TwoExactPermParseObj( char ** ppToken, int nVars, int nNodes, int * pObj ) +{ + char * pToken = *ppToken; + if ( *pToken == '*' ) + { + *pObj = -1; + *ppToken = pToken + 1; + return 1; + } + if ( *pToken >= 'a' && *pToken < 'a' + nVars ) + { + *pObj = *pToken - 'a'; + *ppToken = pToken + 1; + return 1; + } + if ( *pToken >= 'A' && *pToken <= 'Z' ) + { + *pObj = nVars + *pToken - 'A'; + *ppToken = pToken + 1; + return *pObj < nVars + nNodes; + } + if ( *pToken == 'N' ) + { + char * pNext = pToken + 1; + int Num = 0; + if ( *pNext < '0' || *pNext > '9' ) + return 0; + while ( *pNext >= '0' && *pNext <= '9' ) + Num = 10 * Num + *pNext++ - '0'; + *pObj = nVars + Num; + *ppToken = pNext; + return *pObj < nVars + nNodes; + } + return 0; +} +static int Abc_TwoExactPermAddDcs( int * pFans, int nVars, int nNodes, int nDcs, int nSkip, int fAll ) +{ + int i, k, nLetters = 0; + if ( nDcs == 0 ) + return 1; + for ( i = nSkip; i < 2 * nNodes; i++ ) + nLetters += pFans[i] >= 0 && (fAll || pFans[i] < nVars); + if ( nDcs > nLetters ) + return 0; + for ( k = 0; k < nDcs; k++ ) + { + int iChoice = -1, nChoices = 0; + for ( i = nSkip; i < 2 * nNodes; i++ ) + if ( pFans[i] >= 0 && (fAll || pFans[i] < nVars) && Abc_Random(0) % ++nChoices == 0 ) + iChoice = i; + assert( iChoice >= 0 ); + pFans[iChoice] = -1; + } + return 1; +} +static int * Abc_TwoExactPermRandom( int nVars, int nNodes, int nDcs ) +{ + int nObjs = nVars + nNodes; + int Attempt, i, k; + for ( Attempt = 0; Attempt < 200; Attempt++ ) + { + int * pFans = ABC_ALLOC( int, 2 * nNodes ); + int fOk = 1; + for ( i = 0; i < 2 * nNodes; i++ ) + pFans[i] = -1; + for ( i = nObjs - 2; i >= nVars && fOk; i-- ) + fOk = Abc_TwoExactPermAddRequired( pFans, nVars, nNodes, i ); + for ( i = 0; i < nVars && fOk; i++ ) + fOk = Abc_TwoExactPermAddRequired( pFans, nVars, nNodes, i ); + for ( i = 0; i < nNodes && fOk; i++ ) + { + int Limit = nVars + i; + for ( k = 0; k < 2; k++ ) + { + int Try; + if ( pFans[2*i+k] != -1 ) + continue; + for ( Try = 0; Try < 100; Try++ ) + if ( Abc_TwoExactPermAddFanin( pFans, i, Abc_Random(0) % Limit ) ) + break; + if ( Try == 100 ) + fOk = 0; + } + if ( pFans[2*i] > pFans[2*i+1] ) + ABC_SWAP( int, pFans[2*i], pFans[2*i+1] ); + } + if ( fOk && Abc_TwoExactPermCheck(pFans, nVars, nNodes, 1) && Abc_TwoExactPermAddDcs(pFans, nVars, nNodes, nDcs, 0, 0) ) + return pFans; + ABC_FREE( pFans ); + } + return NULL; +} +static int * Abc_TwoExactPermRandomSeeded( int nVars, int nNodes, int nDcs, Vec_Int_t * vSeedPairs, int nSeeds ) +{ + int nObjs = nVars + nNodes; + int Attempt, i, k; + nSeeds = Abc_MinInt( nSeeds, Vec_IntSize(vSeedPairs) ); + for ( Attempt = 0; Attempt < 200; Attempt++ ) + { + int * pFans = ABC_ALLOC( int, 2 * nNodes ); + int * pUsed = ABC_CALLOC( int, Vec_IntSize(vSeedPairs) ); + int fOk = 1; + for ( i = 0; i < 2 * nNodes; i++ ) + pFans[i] = -1; + for ( i = 0; i < nSeeds; i++ ) + { + int s, iSeed = -1, nChoices = 0; + for ( s = 0; s < Vec_IntSize(vSeedPairs); s++ ) + if ( !pUsed[s] && Abc_Random(0) % ++nChoices == 0 ) + iSeed = s; + assert( iSeed >= 0 ); + pUsed[iSeed] = 1; + int Pair = Vec_IntEntry( vSeedPairs, iSeed ); + pFans[2*i] = Pair / nVars; + pFans[2*i+1] = Pair % nVars; + } + for ( i = nObjs - 2; i >= nVars && fOk; i-- ) + fOk = Abc_TwoExactPermAddRequired( pFans, nVars, nNodes, i ); + for ( i = 0; i < nVars && fOk; i++ ) + fOk = Abc_TwoExactPermAddRequired( pFans, nVars, nNodes, i ); + for ( i = 0; i < nNodes && fOk; i++ ) + { + int Limit = nVars + i; + for ( k = 0; k < 2; k++ ) + { + int Try; + if ( pFans[2*i+k] != -1 ) + continue; + for ( Try = 0; Try < 100; Try++ ) + if ( Abc_TwoExactPermAddFanin( pFans, i, Abc_Random(0) % Limit ) ) + break; + if ( Try == 100 ) + fOk = 0; + } + if ( pFans[2*i] > pFans[2*i+1] ) + ABC_SWAP( int, pFans[2*i], pFans[2*i+1] ); + } + if ( fOk && Abc_TwoExactPermCheck(pFans, nVars, nNodes, 0) && Abc_TwoExactPermAddDcs(pFans, nVars, nNodes, nDcs, 2*nSeeds, 1) ) + { + ABC_FREE( pUsed ); + return pFans; + } + ABC_FREE( pUsed ); + ABC_FREE( pFans ); + } + return NULL; +} +static char * Abc_TwoExactCofactorHex( char * pHex, int nVars, int iVar, int Value ) +{ + word pTruth[64], pCof[64]; + int nCofVars = nVars - 1; + int nMints = 1 << nCofVars; + char * pRes = ABC_ALLOC( char, (nCofVars >= 2 ? (1 << (nCofVars-2)) : 1) + 10 ); + int m; + memset( pTruth, 0, sizeof(word) * 64 ); + memset( pCof, 0, sizeof(word) * 64 ); + Abc_TtReadHex( pTruth, pHex ); + for ( m = 0; m < nMints; m++ ) + { + int Low = m & ((1 << iVar) - 1); + int High = m >> iVar; + int Mint = Low | (Value << iVar) | (High << (iVar + 1)); + if ( Abc_TtGetBit(pTruth, Mint) ) + Abc_TtSetBit( pCof, m ); + } + Extra_PrintHexadecimalString( pRes, (unsigned *)pCof, nCofVars ); + return pRes; +} +static int Abc_TwoExactRun( Bmc_EsPar_t * pPars ) +{ + extern int Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ); + extern int Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ); + return pPars->fGlucose ? Exa_ManExactSynthesis( pPars ) : Exa_ManExactSynthesis2( pPars ); +} +static int Abc_TwoExactRunMin( Bmc_EsPar_t * pPars, int nNodeMax ) +{ + int n, nNodeBeg = pPars->nVars + 1; + int fFound = 0; + for ( n = nNodeBeg; n <= nNodeMax; n++ ) + { + if ( !pPars->fSilent ) + printf( "\nTrying N = %d:\n", n ); + pPars->nNodes = n; + ABC_FREE( pPars->pSolFans ); + fFound = Abc_TwoExactRun( pPars ); + if ( fFound ) + return n; + } + return 0; +} +static Vec_Int_t * Abc_TwoExactCofactorSeeds( Bmc_EsPar_t * pPars, int nNodeMax ) +{ + int Counts[16][16]; + int v, c, i, k, nPairs = 0; + Vec_Int_t * vPairs = Vec_IntAlloc( 16 ); + memset( Counts, 0, sizeof(Counts) ); + if ( pPars->nVars > 16 ) + return vPairs; + for ( v = 0; v < pPars->nVars; v++ ) + for ( c = 0; c < 2; c++ ) + { + Bmc_EsPar_t CofPars, * pCof = &CofPars; + char * pCofHex = Abc_TwoExactCofactorHex( pPars->pTtStr, pPars->nVars, v, c ); + int nFound; + Bmc_EsParSetDefault( pCof ); + pCof->nVars = pPars->nVars - 1; + pCof->nNodes = nNodeMax; + pCof->pTtStr = pCofHex; + pCof->fOnlyAnd = pPars->fOnlyAnd; + pCof->fGlucose = pPars->fGlucose; + pCof->RuntimeLim = pPars->RuntimeLim ? pPars->RuntimeLim : 1; + pCof->fSilent = 1; + nFound = Abc_TwoExactRunMin( pCof, nNodeMax ); + if ( nFound ) + { + printf( "Cofactor %c=%d: minimum N = %d, truth = %s\n", 'a' + v, c, nFound, pCofHex ); + for ( i = 0; i < nFound; i++ ) + { + int Fan0 = pCof->pSolFans[2*i]; + int Fan1 = pCof->pSolFans[2*i+1]; + if ( Fan0 >= pCof->nVars || Fan1 >= pCof->nVars ) + continue; + Fan0 += Fan0 >= v; + Fan1 += Fan1 >= v; + if ( Fan0 > Fan1 ) + ABC_SWAP( int, Fan0, Fan1 ); + Counts[Fan0][Fan1]++; + } + } + else + printf( "Cofactor %c=%d: no solution up to N = %d, truth = %s\n", 'a' + v, c, nNodeMax, pCofHex ); + ABC_FREE( pCof->pSolFans ); + ABC_FREE( pCofHex ); + } + for ( k = pPars->nVars * pPars->nVars; k > 0; k-- ) + { + int BestI = -1, BestJ = -1, Best = 0; + for ( i = 0; i < pPars->nVars; i++ ) + for ( v = i + 1; v < pPars->nVars; v++ ) + if ( Counts[i][v] > Best ) + { + Best = Counts[i][v]; + BestI = i; + BestJ = v; + } + if ( Best == 0 ) + break; + printf( "Frequent seed %d: %c%c appears %d time%s.\n", ++nPairs, 'a' + BestI, 'a' + BestJ, Best, Best == 1 ? "" : "s" ); + for ( v = 0; v < Best; v++ ) + Vec_IntPush( vPairs, BestI * pPars->nVars + BestJ ); + Counts[BestI][BestJ] = 0; + } + return vPairs; +} int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ); - extern void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ); + extern int Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ); + extern int Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ); extern void Exa_ManExactSynthesis4( Bmc_EsPar_t * pPars ); extern void Exa_ManExactSynthesis5( Bmc_EsPar_t * pPars ); extern void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName ); extern void Exa_ManExactSynthesis7( Bmc_EsPar_t * pPars, int GateSize ); - int c, fKissat = 0, fKissat2 = 0, fUseNands = 0, GateSize = 0; + int c, fKissat = 0, fKissat2 = 0, fUseNands = 0, GateSize = 0, nCandPerms = 0, nPermDcs = 0, fTryMin = 0, fSmartGen = 0, nSeedNodes = 0; Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INTGSabdconugklmvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INTGSPCDEabdconugklmtxvh" ) ) != EOF ) { switch ( c ) { @@ -10672,6 +11044,48 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->pGuide = argv[globalUtilOptind]; globalUtilOptind++; break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by a variable permutation.\n" ); + goto usage; + } + pPars->pPermStr = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nCandPerms = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nCandPerms < 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; + } + nPermDcs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nPermDcs < 0 ) + goto usage; + break; + case 'E': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-E\" should be followed by an integer.\n" ); + goto usage; + } + nSeedNodes = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nSeedNodes < 0 ) + goto usage; + break; case 'a': pPars->fOnlyAnd ^= 1; break; @@ -10705,6 +11119,12 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'm': pPars->fCard ^= 1; break; + case 't': + fTryMin ^= 1; + break; + case 'x': + fSmartGen ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -10718,6 +11138,11 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) { if ( strstr(argv[globalUtilOptind], ".") ) { + if ( pPars->pPermStr || nCandPerms ) + { + Abc_Print( -1, "Permutation options -P and -C are not supported when reading the function from a file.\n" ); + return 1; + } Exa_ManExactSynthesis6( pPars, argv[globalUtilOptind] ); return 0; } @@ -10743,6 +11168,147 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Function should not have more than 10 inputs.\n" ); return 1; } + if ( nPermDcs && nCandPerms == 0 ) + { + Abc_Print( -1, "Command line switch \"-D\" can only be used together with \"-C\".\n" ); + return 1; + } + if ( fSmartGen && nCandPerms == 0 ) + { + Abc_Print( -1, "Command line switch \"-x\" can only be used together with \"-C\".\n" ); + return 1; + } + if ( nSeedNodes && !fSmartGen ) + { + Abc_Print( -1, "Command line switch \"-E\" can only be used together with \"-x\".\n" ); + return 1; + } + if ( nCandPerms && pPars->pPermStr ) + { + Abc_Print( -1, "Command line switch \"-C\" cannot be used together with \"-P\".\n" ); + return 1; + } + if ( fTryMin && nCandPerms ) + { + Abc_Print( -1, "Command line switch \"-t\" cannot be used together with \"-C\".\n" ); + return 1; + } + if ( nPermDcs > 2 * pPars->nNodes ) + { + Abc_Print( -1, "The number of don't-care positions should not exceed %d.\n", 2 * pPars->nNodes ); + return 1; + } + if ( pPars->pPermStr ) + { + char * pToken = pPars->pPermStr; + int nEntries = 0; + while ( *pToken ) + { + int iObj = -1; + if ( *pToken == '_' ) + { + pToken++; + continue; + } + if ( !Abc_TwoExactPermParseObj(&pToken, pPars->nVars, pPars->nNodes, &iObj) ) + { + Abc_Print( -1, "Permutation should use '*', '_', input variables 'a' through '%c', or internal nodes 'A' through '%c'.\n", 'a' + pPars->nVars - 1, 'A' + Abc_MinInt(pPars->nNodes, 26) - 1 ); + return 1; + } + nEntries++; + } + if ( nEntries != 2 * pPars->nNodes ) + { + Abc_Print( -1, "Permutation should contain %d non-separator symbols (instead of %d).\n", 2 * pPars->nNodes, nEntries ); + return 1; + } + if ( fUseNands || fKissat || fKissat2 || pPars->fCard ) + { + Abc_Print( -1, "Permutation option -P is currently supported by the default and Glucose (-g) twoexact engines.\n" ); + return 1; + } + } + if ( nCandPerms ) + { + int i, fFound = 0, nGenerated = 0, nFailed = 0, fSilentSave = pPars->fSilent; + Vec_Int_t * vSeedPairs = NULL; + abctime clk = Abc_Clock(); + if ( fUseNands || fKissat || fKissat2 || pPars->fCard ) + { + Abc_Print( -1, "Candidate generation with -C is currently supported by the default and Glucose (-g) twoexact engines.\n" ); + return 1; + } + Abc_Random( 1 ); + if ( fSmartGen ) + { + printf( "Deriving frequent seed nodes from cofactors.\n" ); + vSeedPairs = Abc_TwoExactCofactorSeeds( pPars, pPars->nNodes ); + nSeedNodes = Abc_MinInt( nSeedNodes, Vec_IntSize(vSeedPairs) ); + printf( "Trying %d smart candidate input assignments with %d frozen seed node%s and %d randomized don't-care position%s.\n", nCandPerms, nSeedNodes, nSeedNodes == 1 ? "" : "s", nPermDcs, nPermDcs == 1 ? "" : "s" ); + } + else + printf( "Trying %d random candidate input assignments with %d randomized don't-care position%s.\n", nCandPerms, nPermDcs, nPermDcs == 1 ? "" : "s" ); + pPars->fSilent = 1; + for ( i = 0; i < nCandPerms; i++ ) + { + int * pFans = fSmartGen ? Abc_TwoExactPermRandomSeeded( pPars->nVars, pPars->nNodes, nPermDcs, vSeedPairs, nSeedNodes ) : Abc_TwoExactPermRandom( pPars->nVars, pPars->nNodes, nPermDcs ); + char * pPerm, * pStruct; + if ( pFans == NULL ) + { + nFailed++; + continue; + } + pPerm = Abc_TwoExactPermEncode( pFans, pPars->nVars, pPars->nNodes ); + pStruct = Abc_TwoExactPermEncodeFull( pFans, pPars->nVars, pPars->nNodes ); + nGenerated++; + pPars->pPermFans = pFans; + pPars->pPermStr = pPerm; + if ( nGenerated == 1 || nGenerated % 10000 == 0 ) + printf( "Trying candidate %d/%d: %s\n", nGenerated, nCandPerms, pStruct ); + fFound = pPars->fGlucose ? Exa_ManExactSynthesis( pPars ) : Exa_ManExactSynthesis2( pPars ); + if ( fFound ) + { + pPars->fSilent = fSilentSave; + Abc_TwoExactRun( pPars ); + printf( "Found solution using candidate %d: %s\n", nGenerated, pStruct ); + ABC_FREE( pStruct ); + ABC_FREE( pPerm ); + ABC_FREE( pFans ); + break; + } + ABC_FREE( pStruct ); + ABC_FREE( pPerm ); + ABC_FREE( pFans ); + pPars->pPermStr = NULL; + pPars->pPermFans = NULL; + } + pPars->pPermStr = NULL; + pPars->pPermFans = NULL; + pPars->fSilent = fSilentSave; + Vec_IntFreeP( &vSeedPairs ); + ABC_FREE( pPars->pSolFans ); + if ( !fFound ) + printf( "No solution found after trying %d generated candidate%s (%d generation failure%s).\n", nGenerated, nGenerated == 1 ? "" : "s", nFailed, nFailed == 1 ? "" : "s" ); + Abc_PrintTime( 1, "Total candidate-search runtime", Abc_Clock() - clk ); + return 0; + } + if ( fTryMin ) + { + if ( fUseNands || fKissat || fKissat2 || pPars->fCard ) + { + Abc_Print( -1, "Minimum-node enumeration with -t is currently supported by the default and Glucose (-g) twoexact engines.\n" ); + return 1; + } + if ( pPars->nNodes < pPars->nVars + 1 ) + { + Abc_Print( -1, "Command line switch \"-t\" expects \"-N \" to be at least %d.\n", pPars->nVars + 1 ); + return 1; + } + if ( !Abc_TwoExactRunMin(pPars, pPars->nNodes) ) + printf( "No solution found from N = %d through N = %d.\n", pPars->nVars + 1, pPars->nNodes ); + ABC_FREE( pPars->pSolFans ); + return 0; + } if ( fUseNands ) Exa_ManExactSynthesis7( pPars, GateSize ); else if ( fKissat || pPars->fCard ) @@ -10753,16 +11319,21 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Exa_ManExactSynthesis( pPars ); else Exa_ManExactSynthesis2( pPars ); + ABC_FREE( pPars->pSolFans ); return 0; usage: - Abc_Print( -2, "usage: twoexact [-INTG ] [-S str] [-abdconugklmvh] \n" ); + Abc_Print( -2, "usage: twoexact [-INTGCDE ] [-S str] [-P str] [-abdconugklmtxvh] \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-P : fixed input permutation; '_' separates gates, '*' leaves fanin free [default = %s]\n", pPars->pPermStr ? pPars->pPermStr : "none" ); + Abc_Print( -2, "\t-C : number of random candidate permutations to try [default = %d]\n", nCandPerms ); + Abc_Print( -2, "\t-D : number of fixed variable positions randomized to '*' in each candidate [default = %d]\n", nPermDcs ); + Abc_Print( -2, "\t-E : number of frequent cofactor seed nodes used with -x [default = %d]\n", nSeedNodes ); 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" ); @@ -10774,6 +11345,8 @@ usage: Abc_Print( -2, "\t-k : toggle using Kissat by Armin Biere [default = %s]\n", fKissat ? "yes" : "no" ); Abc_Print( -2, "\t-l : toggle using Kissat by Armin Biere [default = %s]\n", fKissat2 ? "yes" : "no" ); Abc_Print( -2, "\t-m : toggle using CaDiCaL by Armin Biere [default = %s]\n", pPars->fCard ? "yes" : "no" ); + Abc_Print( -2, "\t-t : toggle trying increasing node counts up to \"-N \" [default = %s]\n", fTryMin ? "yes" : "no" ); + Abc_Print( -2, "\t-x : toggle smart candidate generation using cofactor seed nodes [default = %s]\n", fSmartGen ? "yes" : "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" ); Abc_Print( -2, "\t-h : print the command usage\n" ); Abc_Print( -2, "\t : truth table in hex notation\n" ); @@ -30698,7 +31271,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Saig_ParBmcSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursgvzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursgvzhc" ) ) != EOF ) { switch ( c ) { @@ -30873,6 +31446,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'g': pPars->fUseGlucose ^= 1; break; + case 'c': + pPars->fUseCadical ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -30967,6 +31543,7 @@ usage: Abc_Print( -2, "\t-r : toggle disabling periodic restarts [default = %s]\n", pPars->fNoRestarts? "yes": "no" ); Abc_Print( -2, "\t-s : toggle using Satoko by Bruno Schmitt [default = %s]\n", pPars->fUseSatoko? "yes": "no" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n",pPars->fUseGlucose? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle using CaDiCaL by Armin Biere, University of Freiburg [default = %s]\n",pPars->fUseCadical? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -42705,6 +43282,105 @@ static Gia_Man_t * Abc_GiaReorderInputsByName( Gia_Man_t * pFirst, Gia_Man_t * p return pNew; } +static Gia_Man_t * Abc_GiaDupPermOutputs( Gia_Man_t * p, Vec_Int_t * vPoPerm ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + assert( Vec_IntSize(vPoPerm) == Gia_ManPoNum(p) ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + { + if ( Gia_ObjIsBuf(pObj) ) + pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) ); + else + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + Gia_ManForEachPo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p, Vec_IntEntry(vPoPerm, i))) ); + Gia_ManForEachRi( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + +static Gia_Man_t * Abc_GiaReorderOutputsByName( Gia_Man_t * pFirst, Gia_Man_t * pSecond ) +{ + Vec_Int_t * vPoPerm; + Gia_Man_t * pNew; + char * pName1, * pName2; + int * pUsed; + int i, k, nPos, fDiff = 0; + if ( pFirst == NULL || pSecond == NULL || pFirst->vNamesOut == NULL || pSecond->vNamesOut == NULL ) + return NULL; + nPos = Gia_ManPoNum( pFirst ); + if ( nPos != Gia_ManPoNum(pSecond) ) + return NULL; + if ( Vec_PtrSize(pFirst->vNamesOut) < nPos || Vec_PtrSize(pSecond->vNamesOut) < nPos ) + return NULL; + vPoPerm = Vec_IntAlloc( nPos ); + pUsed = ABC_CALLOC( int, nPos ); + for ( i = 0; i < nPos; i++ ) + { + pName1 = (char *)Vec_PtrEntry( pFirst->vNamesOut, i ); + if ( pName1 == NULL ) + break; + for ( k = 0; k < nPos; k++ ) + { + pName2 = (char *)Vec_PtrEntry( pSecond->vNamesOut, k ); + if ( pName2 && !pUsed[k] && !strcmp(pName1, pName2) ) + break; + } + if ( k == nPos ) + break; + pUsed[k] = 1; + Vec_IntPush( vPoPerm, k ); + fDiff |= (k != i); + } + ABC_FREE( pUsed ); + if ( i < nPos || !fDiff ) + { + Vec_IntFree( vPoPerm ); + return NULL; + } + pNew = Abc_GiaDupPermOutputs( pSecond, vPoPerm ); + Vec_IntFree( vPoPerm ); + pNew->vNamesIn = Abc_GiaDupNameVec( pSecond->vNamesIn ); + pNew->vNamesOut = Vec_PtrAlloc( Vec_PtrSize(pSecond->vNamesOut) ); + for ( i = 0; i < nPos; i++ ) + { + pName1 = (char *)Vec_PtrEntry( pFirst->vNamesOut, i ); + Vec_PtrPush( pNew->vNamesOut, pName1 ? Abc_UtilStrsav(pName1) : NULL ); + } + for ( i = nPos; i < Vec_PtrSize(pSecond->vNamesOut); i++ ) + { + pName2 = (char *)Vec_PtrEntry( pSecond->vNamesOut, i ); + Vec_PtrPush( pNew->vNamesOut, pName2 ? Abc_UtilStrsav(pName2) : NULL ); + } + return pNew; +} + +static void Abc_GiaTransferNamesIfMatch( Gia_Man_t * pGia, Gia_Man_t * pGiaNames ) +{ + if ( pGia == NULL || pGiaNames == NULL ) + return; + if ( pGia->vNamesIn == NULL && pGiaNames->vNamesIn != NULL && Gia_ManCiNum(pGia) == Vec_PtrSize(pGiaNames->vNamesIn) ) + { + pGia->vNamesIn = pGiaNames->vNamesIn; + pGiaNames->vNamesIn = NULL; + } + if ( pGia->vNamesOut == NULL && pGiaNames->vNamesOut != NULL && Gia_ManCoNum(pGia) == Vec_PtrSize(pGiaNames->vNamesOut) ) + { + pGia->vNamesOut = pGiaNames->vNamesOut; + pGiaNames->vNamesOut = NULL; + } +} + /**Function************************************************************* Synopsis [] @@ -42722,6 +43398,7 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam Gia_Man_t * pGia; char * pTemp; char * pOrigFileName = NULL; + char * pFileTemp = NULL; int fVerilog, fSystemVerilog; *pAbc_ReadAigerOrVerilogFileStatus = 0; @@ -42750,17 +43427,24 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); Aig_Man_t * pAig = NULL; char pCommand[2000]; + char * pFileBase; int RetValue; int fSystemVerilog2 = pFileName2 && Extra_FileIsType( pFileName2, ".sv", NULL, NULL ); // Save the original filename before changing it pOrigFileName = pFileName; + pFileBase = pTopModule ? Abc_UtilStrsav(pTopModule) : + Extra_FileNameGeneric( Extra_FileNameWithoutPath(pFileName) ); + pFileTemp = ABC_ALLOC( char, strlen(pFileBase) + 5 ); + sprintf( pFileTemp, "%s.aig", pFileBase ); + ABC_FREE( pFileBase ); snprintf( pCommand, sizeof(pCommand), - "yosys -qp \"read_verilog %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols _temp_.aig\"", + "yosys -qp \"read_verilog %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"", pDefines ? "-D" : "", pDefines ? pDefines : "", (fSystemVerilog || fSystemVerilog2) ? "-sv " : "", pFileName, pFileName2 ? " " : "", pFileName2 ? pFileName2 : "", pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "", - pFileName2 ? "delete t:\\$scopeinfo; " : "" ); + pFileName2 ? "delete t:\\$scopeinfo; " : "", + pFileTemp ); #if defined(__wasm) RetValue = 1; #else @@ -42769,14 +43453,17 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam if ( RetValue != 0 ) { Abc_Print( -1, "Yosys command failed: \"%s\".\n", pCommand ); + ABC_FREE( pFileTemp ); return NULL; } if ( pFileName2 ) { - Abc_Ntk_t * pNtk = Io_Read( "_temp_.aig", IO_FILE_AIGER, 1, 0 ); + Gia_Man_t * pGiaNames = NULL; + Abc_Ntk_t * pNtk = Io_Read( pFileTemp, IO_FILE_AIGER, 1, 0 ); if ( pNtk == NULL ) { - Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", "_temp_.aig" ); + Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileTemp ); + ABC_FREE( pFileTemp ); return NULL; } pAig = Abc_NtkToDar( pNtk, 0, 1 ); @@ -42784,14 +43471,19 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam if ( pAig == NULL ) { Abc_Print( -1, "Converting the AIGER network into an internal AIG has failed.\n" ); + ABC_FREE( pFileTemp ); return NULL; } pGia = Gia_ManFromAig( pAig ); Aig_ManStop( pAig ); + pGiaNames = Gia_AigerRead( pFileTemp, 0, 1, 0 ); + Abc_GiaTransferNamesIfMatch( pGia, pGiaNames ); + if ( pGiaNames ) + Gia_ManStop( pGiaNames ); } else { - pFileName = "_temp_.aig"; + pFileName = pFileTemp; pGia = Gia_AigerRead( pFileName, 0, 0, 0 ); } } @@ -42800,6 +43492,7 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam if ( pGia == NULL ) { Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileName ); + ABC_FREE( pFileTemp ); return NULL; } @@ -42810,6 +43503,7 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam pGia->pSpec = Abc_UtilStrsav( pOrigFileName ); } + ABC_FREE( pFileTemp ); return pGia; } @@ -43069,6 +43763,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ManStop( pGias[1] ); pGias[1] = pTemp; } + pTemp = Abc_GiaReorderOutputsByName( pGias[0], pGias[1] ); + if ( pTemp ) + { + if ( pPars->fVerbose ) + Abc_Print( 1, "Reordered primary outputs of the second network using output names.\n" ); + if ( pGias[1] != pAbc->pGia && pGias[1] != pAbc->pGiaSaved ) + Gia_ManStop( pGias[1] ); + pGias[1] = pTemp; + } } pPars->pNameSpec = pGias[0] ? (pGias[0]->pSpec ? pGias[0]->pSpec : pGias[0]->pName) : NULL; pPars->pNameImpl = pGias[1] ? (pGias[1]->pSpec ? pGias[1]->pSpec : pGias[1]->pName) : NULL; @@ -51747,12 +52450,12 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: &sprove [-PTUW num] [-C str] [-R file] [-usvwh]\n" ); - Abc_Print( -2, "\t proves CEC problem by case-splitting\n" ); + Abc_Print( -2, "\t concurrent sequential model checker\n" ); Abc_Print( -2, "\t-P num : the number of concurrent processes (1 <= num <= 6) [default = %d]\n", nProcs ); - Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut ); - Abc_Print( -2, "\t-U num : second-stage timeout in seconds [default = %d]\n", nTimeOut2 ); + Abc_Print( -2, "\t-T num : first-stage timeout for proving original and scnew reduction [default = %d]\n", nTimeOut ); + Abc_Print( -2, "\t-U num : second-stage proving timeout on optimized miter [default = %d]\n", nTimeOut2 ); + Abc_Print( -2, "\t-W num : late-stage timeout for optimization and final proving [default = %d]\n", nTimeOut3 ); Abc_Print( -2, "\t-C str : with -u, pass this option string to internal %%ufar\n" ); - Abc_Print( -2, "\t-W num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut3 ); Abc_Print( -2, "\t-R str : dump replay/trace file for later execution by &sprove2\n" ); Abc_Print( -2, "\t-u : enable concurrent UFAR on word-level design (uses internal %%blast + &miter -x)\n" ); Abc_Print( -2, "\t-s : enable silent computation (no reporting) [default = %s]\n", fSilent? "yes": "no" ); @@ -58745,11 +59448,11 @@ usage: ***********************************************************************/ int Abc_CommandAbc9GenAdder( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries, int fVerbose ); + extern Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fMM, int fCarries, int fVerbose ); Gia_Man_t * pTemp = NULL; - int c, nBits = 0, fSK = 0, fBK = 0, fHC = 0, fCarries = 0, fVerbose = 0; + int c, nBits = 0, fSK = 0, fBK = 0, fHC = 0, fMM = 0, fCarries = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Nsbhcv" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Nsbhmcv" ) ) != EOF ) { switch ( c ) { @@ -58773,6 +59476,9 @@ int Abc_CommandAbc9GenAdder( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'h': fHC ^= 1; break; + case 'm': + fMM ^= 1; + break; case 'c': fCarries ^= 1; break; @@ -58788,17 +59494,18 @@ int Abc_CommandAbc9GenAdder( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9GenAdder(): The number of inputs should be defined on the command line \"-N num\".\n" ); return 0; } - pTemp = Gia_ManGenAdder( nBits, fSK, fBK, fHC, fCarries, fVerbose ); + pTemp = Gia_ManGenAdder( nBits, fSK, fBK, fHC, fMM, fCarries, fVerbose ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &genadder [-N ] [-sbhcv]\n" ); + Abc_Print( -2, "usage: &genadder [-N ] [-sbhmcv]\n" ); Abc_Print( -2, "\t generates a prefix adder (by default, the ripple carry adder)\n" ); Abc_Print( -2, "\t-N num : the bit-width of the adder [default = undefined]\n" ); Abc_Print( -2, "\t-s : toggles using Sklansky adder [default = %s]\n", fSK ? "yes": "no" ); Abc_Print( -2, "\t-b : toggles using Brent-Kung adder [default = %s]\n", fBK ? "yes": "no" ); Abc_Print( -2, "\t-h : toggles using Huan-Carlsson adder [default = %s]\n", fHC ? "yes": "no" ); + Abc_Print( -2, "\t-m : toggles using majority-based M/M adder [default = %s]\n", fMM ? "yes": "no" ); Abc_Print( -2, "\t-c : toggles using carry-in and carry-out [default = %s]\n", fCarries ? "yes": "no" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" ); return 1; @@ -60470,7 +61177,7 @@ int Abc_CommandAbc9elSLIM( Abc_Frame_t * pAbc, int argc, char ** argv ) { seteSLIMParams(¶ms); Extra_UtilGetoptReset(); params.subcircuit_max_size = 4; - while ( ( c = Extra_UtilGetopt( argc, argv, "CDGIPRSTVWXZfhist" ) ) != EOF ) { + while ( ( c = Extra_UtilGetopt( argc, argv, "CDGIPRSTVWXZcfhist" ) ) != EOF ) { switch ( c ) { case 'C': if ( globalUtilOptind >= argc ) diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c index 654d246f0..5db012cfe 100644 --- a/src/base/main/mainUtils.c +++ b/src/base/main/mainUtils.c @@ -18,6 +18,12 @@ ***********************************************************************/ +#ifdef WIN32 +#include +#else +#include +#endif + #include "base/abc/abc.h" #include "mainInt.h" @@ -91,7 +97,13 @@ char * Abc_UtilsGetUsersInput( Abc_Frame_t * pAbc ) { char * pRetValue; fprintf( pAbc->Out, "%s", Prompt ); + fflush( pAbc->Out ); pRetValue = fgets( Prompt, 5000, stdin ); + if ( pRetValue == NULL ) { exit(0); } + if ( !isatty( fileno(stdin) ) ) { + fputs( Prompt, pAbc->Out ); + fflush( pAbc->Out ); + } return Prompt; } #endif diff --git a/src/base/wln/wlnCom.c b/src/base/wln/wlnCom.c index 2436932cd..e471bc877 100644 --- a/src/base/wln/wlnCom.c +++ b/src/base/wln/wlnCom.c @@ -92,13 +92,16 @@ void Wln_End( Abc_Frame_t * pAbc ) ******************************************************************************/ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose ); - extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ); - extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose ); + extern Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose ); + extern Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ); + extern Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fCollapse, int fVerbose ); FILE * pFile; char * pFileName = NULL; char * pFileName2= NULL; + char ** ppFileNames = NULL; + int nFileNames = 0; + int fFileNamesAlloc = 0; char * pTopModule= NULL; char * pDefines = NULL; char * pLibrary = NULL; @@ -194,48 +197,64 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( argc != globalUtilOptind + 1 ) + nFileNames = argc - globalUtilOptind; + if ( nFileNames < 1 ) { - printf( "Abc_CommandReadWlc(): Input file name should be given on the command line.\n" ); + printf( "Abc_CommandReadWlc(): Input file name(s) should be given on the command line.\n" ); return 0; } - // get the file name - pFileName = argv[globalUtilOptind]; - if ( (pFile = fopen( pFileName, "r" )) == NULL ) - { - Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName ); - if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".sv", NULL, NULL, NULL )) ) - Abc_Print( 1, "Did you mean \"%s\"?", pFileName ); - Abc_Print( 1, "\n" ); - return 0; - } - fclose( pFile ); + ppFileNames = pFileName2 ? ABC_ALLOC( char *, nFileNames + 1 ) : argv + globalUtilOptind; + fFileNamesAlloc = pFileName2 != NULL; if ( pFileName2 ) { - if ( (pFile = fopen( pFileName2, "r" )) == NULL ) + int i; + for ( i = 0; i < nFileNames; i++ ) + ppFileNames[i] = argv[globalUtilOptind + i]; + ppFileNames[nFileNames++] = pFileName2; + } + pFileName = ppFileNames[0]; + for ( c = 0; c < nFileNames; c++ ) + { + if ( (pFile = fopen( ppFileNames[c], "r" )) == NULL ) { - Abc_Print( 1, "Cannot open input file \"%s\".\n", pFileName2 ); + Abc_Print( 1, "Cannot open input file \"%s\". ", ppFileNames[c] ); + if ( (pFileName = Extra_FileGetSimilarName( ppFileNames[c], ".v", ".sv", NULL, NULL, NULL )) ) + Abc_Print( 1, "Did you mean \"%s\"?", pFileName ); + Abc_Print( 1, "\n" ); + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); return 0; } fclose( pFile ); } - - // perform reading - if ( pLibrary ) + pFileName = ppFileNames[0]; + if ( nFileNames > 1 ) { - if ( pFileName2 ) + int i, fAllVerilog = 1; + for ( i = 0; i < nFileNames; i++ ) + fAllVerilog &= Extra_FileIsType( ppFileNames[i], ".v", ".sv", NULL ); + if ( !fAllVerilog ) { - Abc_Print( 1, "Command line switch \"-F\" only applies in the default bit-blasting path.\n" ); + Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" ); + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); return 0; } + } + + // perform reading + if ( pLibrary ) + { Abc_Ntk_t * pNtk = NULL; if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) - pNtk = Wln_ReadMappedSystemVerilog( pFileName, pTopModule, pDefines, pLibrary, fVerbose ); + pNtk = Wln_ReadMappedSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, pLibrary, fVerbose ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) ) - pNtk = Wln_ReadMappedSystemVerilog( pFileName, pTopModule, pDefines, pLibrary, fVerbose ); + pNtk = Wln_ReadMappedSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, pLibrary, fVerbose ); else { printf( "Abc_CommandYosys(): Unknown file extension.\n" ); + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); return 0; } Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); @@ -244,55 +263,67 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pNew = NULL; if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) - pNew = Wln_BlastSystemVerilog( pFileName, pFileName2, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); + pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) ) - pNew = Wln_BlastSystemVerilog( pFileName, pFileName2, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); + pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) ) { - if ( pFileName2 ) + if ( nFileNames > 1 ) { - Abc_Print( 1, "Command line switch \"-F\" is only supported when the main input is Verilog/SystemVerilog.\n" ); + Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" ); + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); return 0; } - pNew = Wln_BlastSystemVerilog( pFileName, NULL, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); + pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose ); } else { printf( "Abc_CommandYosys(): Unknown file extension.\n" ); + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); return 0; } Abc_FrameUpdateGia( pAbc, pNew ); } else { - if ( pFileName2 ) - { - Abc_Print( 1, "Command line switch \"-F\" only applies in the default bit-blasting path.\n" ); - return 0; - } Rtl_Lib_t * pLib = NULL; if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) - pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose ); + pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) ) - pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose ); + pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose ); else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) ) - pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose ); + { + if ( nFileNames > 1 ) + { + Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" ); + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); + return 0; + } + pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose ); + } else { printf( "Abc_CommandYosys(): Unknown file extension.\n" ); + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); return 0; } Wln_AbcUpdateRtl( pAbc, pLib ); } + if ( fFileNamesAlloc ) + ABC_FREE( ppFileNames ); return 0; usage: - Abc_Print( -2, "usage: %%yosys [-TM ] [-D ] [-L ] [-F ] [-bdisumlcvh] \n" ); + Abc_Print( -2, "usage: %%yosys [-TM ] [-D ] [-L ] [-F ] [-bdisumlcvh] [file_name...]\n" ); Abc_Print( -2, "\t reads Verilog or SystemVerilog using Yosys\n" ); Abc_Print( -2, "\t-T : specify the top module name (default uses \"-auto-top\")\n" ); Abc_Print( -2, "\t-M : specify the top module name (default uses \"-auto-top\") (equivalent to \"-T\")\n" ); Abc_Print( -2, "\t-D : specify defines to be used by Yosys (default \"not used\")\n" ); Abc_Print( -2, "\t-L : specify the Liberty library to read a mapped design (default \"not used\")\n" ); - Abc_Print( -2, "\t-F : specify a second Verilog/SystemVerilog file for the default bit-blasting flow (default \"not used\")\n" ); + Abc_Print( -2, "\t-F : specify an additional Verilog/SystemVerilog file (default \"not used\")\n" ); Abc_Print( -2, "\t-b : toggle bit-blasting the design into an AIG using Yosys (this switch has no effect)\n" ); Abc_Print( -2, "\t-d : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", !fDontBlast? "yes": "no" ); Abc_Print( -2, "\t-i : toggle inverting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" ); diff --git a/src/base/wln/wlnRtl.c b/src/base/wln/wlnRtl.c index ffe8e457d..6c92cffbc 100644 --- a/src/base/wln/wlnRtl.c +++ b/src/base/wln/wlnRtl.c @@ -122,6 +122,45 @@ char * Wln_GetYosysName() #endif return pYosysName; } +static char * Wln_FileNamesJoin( char ** ppFileNames, int nFileNames ) +{ + char * pFileNames; + int i, nChars = 1; + for ( i = 0; i < nFileNames; i++ ) + nChars += strlen( ppFileNames[i] ) + 1; + pFileNames = ABC_ALLOC( char, nChars ); + pFileNames[0] = 0; + for ( i = 0; i < nFileNames; i++ ) + { + if ( i ) + strcat( pFileNames, " " ); + strcat( pFileNames, ppFileNames[i] ); + } + return pFileNames; +} +static int Wln_FileNamesHasSv( char ** ppFileNames, int nFileNames ) +{ + int i; + for ( i = 0; i < nFileNames; i++ ) + if ( strstr( ppFileNames[i], ".sv" ) != NULL ) + return 1; + return 0; +} +static void Wln_GiaTransferNamesIfMatch( Gia_Man_t * pGia, Gia_Man_t * pGiaNames ) +{ + if ( pGia == NULL || pGiaNames == NULL ) + return; + if ( pGia->vNamesIn == NULL && pGiaNames->vNamesIn != NULL && Gia_ManCiNum(pGia) == Vec_PtrSize(pGiaNames->vNamesIn) ) + { + pGia->vNamesIn = pGiaNames->vNamesIn; + pGiaNames->vNamesIn = NULL; + } + if ( pGia->vNamesOut == NULL && pGiaNames->vNamesOut != NULL && Gia_ManCoNum(pGia) == Vec_PtrSize(pGiaNames->vNamesOut) ) + { + pGia->vNamesOut = pGiaNames->vNamesOut; + pGiaNames->vNamesOut = NULL; + } +} int Wln_ConvertToRtl( char * pCommand, char * pFileTemp ) { #if defined(__wasm) @@ -142,29 +181,39 @@ int Wln_ConvertToRtl( char * pCommand, char * pFileTemp ) return 1; #endif } -Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose ) +Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fCollapse, int fVerbose ) { Rtl_Lib_t * pNtk = NULL; - char Command[1000]; + char * pFileNames, * pCommand; char * pFileTemp = "_temp_.rtlil"; - int fSVlog = strstr(pFileName, ".sv") != NULL; - if ( strstr(pFileName, ".rtl") ) - return Rtl_LibReadFile( pFileName, pFileName ); - sprintf( Command, "%s -qp \"read_verilog %s%s %s%s; hierarchy %s%s; %sproc; memory -nomap; memory_map; write_rtlil %s\"", + int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames); + int nCommand; + if ( nFileNames == 1 && strstr(ppFileNames[0], ".rtl") ) + return Rtl_LibReadFile( ppFileNames[0], ppFileNames[0] ); + pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames ); + nCommand = strlen(Wln_GetYosysName()) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 200; + pCommand = ABC_ALLOC( char, nCommand ); + sprintf( pCommand, "%s -qp \"read_verilog %s%s %s%s; hierarchy %s%s; %sproc; memory -nomap; memory_map; write_rtlil %s\"", Wln_GetYosysName(), pDefines ? "-D" : "", pDefines ? pDefines : "", fSVlog ? "-sv " : "", - pFileName, + pFileNames, pTopModule ? "-top " : "", pTopModule ? pTopModule : "", fCollapse ? "flatten; ": "", pFileTemp ); if ( fVerbose ) - printf( "%s\n", Command ); - if ( !Wln_ConvertToRtl(Command, pFileTemp) ) + printf( "%s\n", pCommand ); + if ( !Wln_ConvertToRtl(pCommand, pFileTemp) ) + { + ABC_FREE( pCommand ); + ABC_FREE( pFileNames ); return NULL; - pNtk = Rtl_LibReadFile( pFileTemp, pFileName ); + } + ABC_FREE( pCommand ); + ABC_FREE( pFileNames ); + pNtk = Rtl_LibReadFile( pFileTemp, ppFileNames[0] ); if ( pNtk == NULL ) { printf( "Dumped the design into file \"%s\".\n", pFileTemp ); @@ -174,40 +223,56 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * p unlink( pFileTemp ); return pNtk; } -Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ) +Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose ) { Gia_Man_t * pGia = NULL; - char Command[1000]; - char * pFileTemp = "_temp_.aig"; - int fRtlil = strstr(pFileName, ".rtl") != NULL; - int fSVlog = strstr(pFileName, ".sv") != NULL || (pFileName2 && strstr(pFileName2, ".sv") != NULL); - sprintf( Command, "%s -qp \"%s %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; %s%smemory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"", + char * pFileNames, * pCommand; + char * pFileTemp, * pFileBase; + int fRtlil = nFileNames == 1 && strstr(ppFileNames[0], ".rtl") != NULL; + int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames); + int nCommand; + pFileBase = pTopModule ? Abc_UtilStrsav(pTopModule) : + Extra_FileNameGeneric( Extra_FileNameWithoutPath(ppFileNames[0]) ); + pFileTemp = ABC_ALLOC( char, strlen(pFileBase) + 5 ); + sprintf( pFileTemp, "%s.aig", pFileBase ); + ABC_FREE( pFileBase ); + pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames ); + nCommand = strlen(Wln_GetYosysName()) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 500; + pCommand = ABC_ALLOC( char, nCommand ); + sprintf( pCommand, "%s -qp \"%s %s%s %s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; %s%smemory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"", Wln_GetYosysName(), fRtlil ? "read_rtlil" : "read_verilog", pDefines ? "-D" : "", pDefines ? pDefines : "", fSVlog ? "-sv " : "", - pFileName, - pFileName2 ? " " : "", - pFileName2 ? pFileName2 : "", + pFileNames, pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "", fTechMap ? (fLibInDir ? "techmap -map techmap.v; " : "techmap; ") : "", fSetUndef ? "setundef -init -zero; " : "", - pFileName2 ? "delete t:\\$scopeinfo; " : "", + nFileNames > 1 ? "delete t:\\$scopeinfo; " : "", pFileTemp ); if ( fVerbose ) - printf( "%s\n", Command ); - if ( !Wln_ConvertToRtl(Command, pFileTemp) ) + printf( "%s\n", pCommand ); + if ( !Wln_ConvertToRtl(pCommand, pFileTemp) ) + { + ABC_FREE( pCommand ); + ABC_FREE( pFileNames ); + ABC_FREE( pFileTemp ); return NULL; - if ( pFileName2 ) + } + ABC_FREE( pCommand ); + ABC_FREE( pFileNames ); + if ( nFileNames > 1 ) { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); Aig_Man_t * pAig = NULL; + Gia_Man_t * pGiaNames = NULL; Abc_Ntk_t * pNtk = Io_Read( pFileTemp, IO_FILE_AIGER, 1, 0 ); if ( pNtk == NULL ) { printf( "Reading AIGER from file \"%s\" has failed.\n", pFileTemp ); + ABC_FREE( pFileTemp ); return NULL; } pAig = Abc_NtkToDar( pNtk, 0, 1 ); @@ -215,22 +280,29 @@ Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * if ( pAig == NULL ) { printf( "Converting the AIGER network into an internal AIG has failed.\n" ); + ABC_FREE( pFileTemp ); return NULL; } pGia = fSkipStrash ? Gia_ManFromAigSimple(pAig) : Gia_ManFromAig(pAig); Aig_ManStop( pAig ); + pGiaNames = Gia_AigerRead( pFileTemp, 0, 1, 0 ); + Wln_GiaTransferNamesIfMatch( pGia, pGiaNames ); + if ( pGiaNames ) + Gia_ManStop( pGiaNames ); } else pGia = Gia_AigerRead( pFileTemp, 0, fSkipStrash, 0 ); if ( pGia == NULL ) { printf( "Converting to AIG has failed.\n" ); + ABC_FREE( pFileTemp ); return NULL; } ABC_FREE( pGia->pName ); pGia->pName = pTopModule ? Abc_UtilStrsav(pTopModule) : - Extra_FileNameGeneric( Extra_FileNameWithoutPath(pFileName) ); + Extra_FileNameGeneric( Extra_FileNameWithoutPath(ppFileNames[0]) ); unlink( pFileTemp ); + ABC_FREE( pFileTemp ); // complement the outputs if ( fInvert ) { @@ -240,35 +312,48 @@ Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * } return pGia; } -Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose ) +Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose ) { Abc_Ntk_t * pNtk = NULL; - char Command[1000]; + char * pFileNames, * pCommand; char * pFileTemp = "_temp_.blif"; - int fSVlog = strstr(pFileName, ".sv") != NULL; - sprintf( Command, "%s -qp \"read_liberty -lib %s; read %s %s%s %s; hierarchy %s%s; flatten; proc; memory -nomap; memory_map; write_blif %s%s -impltf -gates %s\"", + int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames); + int nCommand; + pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames ); + nCommand = strlen(Wln_GetYosysName()) + strlen(pLibrary) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + 2 * (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 300; + pCommand = ABC_ALLOC( char, nCommand ); + sprintf( pCommand, "%s -qp \"read_liberty -lib %s; read %s %s%s %s; hierarchy %s%s; flatten; proc; memory -nomap; memory_map; write_blif %s%s -impltf -gates %s\"", Wln_GetYosysName(), pLibrary, fSVlog ? "-sv " : "-vlog95", pDefines ? "-D" : "", pDefines ? pDefines : "", - pFileName, + pFileNames, pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "", pTopModule ? "-top " : "", pTopModule ? pTopModule : "", pFileTemp ); if ( fVerbose ) - printf( "%s\n", Command ); - if ( !Wln_ConvertToRtl(Command, pFileTemp) ) - return NULL; - sprintf( Command, "read_lib %s", pLibrary ); - if ( Cmd_CommandExecute( Abc_FrameReadGlobalFrame(), Command ) ) + printf( "%s\n", pCommand ); + if ( !Wln_ConvertToRtl(pCommand, pFileTemp) ) { - fprintf( stdout, "Cannot execute ABC command \"%s\".\n", Command ); + ABC_FREE( pCommand ); + ABC_FREE( pFileNames ); + return NULL; + } + ABC_FREE( pCommand ); + ABC_FREE( pFileNames ); + pCommand = ABC_ALLOC( char, strlen(pLibrary) + 20 ); + sprintf( pCommand, "read_lib %s", pLibrary ); + if ( Cmd_CommandExecute( Abc_FrameReadGlobalFrame(), pCommand ) ) + { + fprintf( stdout, "Cannot execute ABC command \"%s\".\n", pCommand ); + ABC_FREE( pCommand ); unlink( pFileTemp ); return NULL; } + ABC_FREE( pCommand ); pNtk = Io_Read( pFileTemp, IO_FILE_BLIF, 1, 0 ); if ( pNtk == NULL ) { diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index f93b73edb..6a0148d4f 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -194,7 +194,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep pCut->Delay = If_CutSopBalanceEval( p, pCut, NULL ); else if ( p->pPars->fDsdBalance ) pCut->Delay = If_CutDsdBalanceEval( p, pCut, NULL ); - else if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell ) + else if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib ) { int iLeaf, Intrinsic[IF_MAX_LUTSIZE]; float Delay = -IF_FLOAT_LARGE; @@ -364,7 +364,7 @@ IfMapBestCutDone: for ( iLeaf = 0; iLeaf < p->nCutLeavesCur; iLeaf++ ) { If_Obj_t * pLeaf = If_CutLeaf( p, pCut, iLeaf ); - if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && pCut->nLeaves > 1 ) + if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib && pCut->nLeaves > 1 ) { If_Cut_t * pBestCut = If_ObjCutBest( pLeaf ); assert( pBestCut != NULL ); @@ -472,8 +472,10 @@ IfMapBestCutDone: pCut->Delay = If_CutSopBalanceEval( p, pCut, NULL ); else if ( p->pPars->fDsdBalance ) pCut->Delay = If_CutDsdBalanceEval( p, pCut, NULL ); - else if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell ) + else if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib ) { + int iLeaf, Intrinsic[IF_MAX_LUTSIZE]; + float Delay = -IF_FLOAT_LARGE; if ( pCut->nLeaves == 0 ) { pCut->Delay = 0.0; @@ -487,9 +489,16 @@ IfMapBestCutDone: pCut->fUseless = 0; goto IfMapCutEvalDone; } - assert( pCut->fUseless || p->fCutDelayCurValid ); assert( pCut->fUseless || pCut->Config != 0 ); - pCut->Delay = pCut->fUseless ? IF_FLOAT_LARGE : p->CutDelayCur; + if ( pCut->fUseless ) + pCut->Delay = IF_FLOAT_LARGE; + else + { + If_CutComputeIntrinsicJ( p, pCut->Config, pCut->nLeaves, Intrinsic ); + If_CutForEachLeaf( p, pCut, pLeaf, iLeaf ) + Delay = IF_MAX( Delay, If_ObjArrTime(pLeaf) + (float)Intrinsic[iLeaf] ); + pCut->Delay = Delay; + } IfMapCutEvalDone: ; } diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c index 81f88fd72..3126b75a7 100644 --- a/src/map/if/ifTime.c +++ b/src/map/if/ifTime.c @@ -131,7 +131,7 @@ float If_CutDelay( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut ) } else { - if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && p->pPars->pCellLib ) + if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib ) { int Intrinsic[IF_MAX_LUTSIZE]; if ( pCut->nLeaves == 0 ) @@ -233,7 +233,7 @@ void If_CutPropagateRequired( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut, fl } else { - if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && p->pPars->pCellLib ) + if ( p->pPars->fEnableCheck07 && p->pPars->pCellLib ) { int Intrinsic[IF_MAX_LUTSIZE]; if ( pCut->nLeaves == 0 ) @@ -338,7 +338,7 @@ float If_ManDelayMax( If_Man_t * p, int fSeq ) void If_ManComputeRequired( If_Man_t * p ) { If_Obj_t * pObj; - int i, Counter; + int i, iBox, Counter; float reqTime; // compute area, clean required times, collect nodes used in the mapping @@ -480,7 +480,7 @@ void If_ManComputeRequired( If_Man_t * p ) if ( p->pPars->pTimesReq ) { Counter = 0; - If_ManForEachCo( p, pObj, i ) + If_ManForEachPo( p, pObj, i ) { reqTime = p->pPars->pTimesReq[i]; if ( If_ObjArrTime(If_ObjFanin0(pObj)) > reqTime + p->fEpsilon ) @@ -551,6 +551,9 @@ void If_ManComputeRequired( If_Man_t * p ) { reqTime = pObj->Required; Tim_ManSetCiRequired( p->pManTim, pObj->IdPio, reqTime ); + iBox = Tim_ManBoxForCi( p->pManTim, pObj->IdPio ); + if ( iBox >= 0 ) + Tim_ManSetPreviousTravIdBoxInputs( p->pManTim, iBox ); } else if ( If_ObjIsCo(pObj) ) { diff --git a/src/opt/eslim/eSLIM.cpp b/src/opt/eslim/eSLIM.cpp index 670551568..764c822e1 100644 --- a/src/opt/eslim/eSLIM.cpp +++ b/src/opt/eslim/eSLIM.cpp @@ -603,6 +603,10 @@ Circuitrepresentation* runeSLIM(Circuitrepresentation * cir, const eSLIM_ParamSt Gia_Man_t* applyeSLIM(Gia_Man_t * pGia, const eSLIM_ParamStruct* params) { + if (Gia_ManHasDangling(pGia)) { + std::cout << "Warning: Circuit must not contain dangling nodes.\n"; + return pGia; + } return runeSLIM(pGia, params); } @@ -610,12 +614,6 @@ Abc_Ntk_t* applyelSLIM(Abc_Ntk_t * ntk, const eSLIM_ParamStruct* params) { return runeSLIM(ntk, params); } -Abc_Ntk_t* applyetSLIM(Abc_Ntk_t * ntk, const eSLIM_ParamStruct* params) { - return runeSLIM(ntk, params); -} - - - diff --git a/src/opt/eslim/eslimCirMan.cpp b/src/opt/eslim/eslimCirMan.cpp index 38e1635cd..5f9c5007d 100644 --- a/src/opt/eslim/eslimCirMan.cpp +++ b/src/opt/eslim/eslimCirMan.cpp @@ -79,6 +79,7 @@ namespace eSLIM { } eSLIMCirMan::eSLIMCirMan(Gia_Man_t * pGia) : eSLIMCirMan(Gia_ManObjNum(pGia)) { + assert (!Gia_ManHasDangling(pGia)); Gia_ManConst0(pGia)->Value = 0; Gia_Obj_t * pObj; int i; diff --git a/src/opt/eslim/relationSynthesiser.cpp b/src/opt/eslim/relationSynthesiser.cpp index 6e639fc04..70a488d83 100644 --- a/src/opt/eslim/relationSynthesiser.cpp +++ b/src/opt/eslim/relationSynthesiser.cpp @@ -27,8 +27,8 @@ ABC_NAMESPACE_IMPL_START namespace eSLIM { RelationSynthesiser::RelationSynthesiser(const Relation& relation, const Subcircuit& subcir, unsigned int max_size, const eSLIMConfig& cfg, eSLIMLog& log) - : relation(relation), subcir(subcir), - max_size(max_size), config(cfg), log(log) { + : subcir(subcir), max_size(max_size), + relation(relation), config(cfg), log(log) { setupEncoding(); } @@ -609,4 +609,4 @@ namespace eSLIM { } -ABC_NAMESPACE_IMPL_END \ No newline at end of file +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 1e6d51a24..83ddc810a 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -82,6 +82,8 @@ struct Bmc_EsPar_t_ char * pSymStr; char * pPermStr; char * pGuide; + int * pPermFans; + int * pSolFans; Vec_Wrd_t* vTruths; }; @@ -134,6 +136,7 @@ struct Saig_ParBmc_t_ int fNoRestarts; // disables periodic restarts int fUseSatoko; // enables using Satoko int fUseGlucose; // enables using Glucose 3.0 + int fUseCadical; // enables using CaDiCaL int nLearnedStart; // starting learned clause limit int nLearnedDelta; // delta of learned clause limit int nLearnedPerce; // ratio of learned clause limit diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 7e0a6cfdc..a6d5bc594 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -23,12 +23,21 @@ #include "sat/bsat/satStore.h" #include "sat/satoko/satoko.h" #include "sat/glucose/AbcGlucose.h" +#include "sat/cadical/cadicalSolver.h" +#include "sat/cadical/ccadical.h" #include "misc/vec/vecHsh.h" #include "misc/vec/vecWec.h" #include "bmc.h" ABC_NAMESPACE_IMPL_START +static inline void Bmc3_CadicalSetRuntimeLimit( cadical_solver * pSat4, abctime nSeconds ) +{ + if ( pSat4 == NULL || nSeconds <= 0 ) + return; + ccadical_limit( (CCaDiCaL *)pSat4->p, "seconds", nSeconds ); +} + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -64,6 +73,7 @@ struct Gia_ManBmc_t_ sat_solver * pSat; // SAT solver satoko_t * pSat2; // SAT solver bmcg_sat_solver * pSat3; // SAT solver + cadical_solver * pSat4; // SAT solver int nSatVars; // SAT variables int nObjNums; // SAT objects int nWordNum; // unsigned words for ternary simulation @@ -718,7 +728,7 @@ Vec_Int_t * Saig_ManBmcComputeMappingRefs( Aig_Man_t * p, Vec_Int_t * vMap ) SeeAlso [] ***********************************************************************/ -Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose ) +Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose, int fUseCadical ) { Gia_ManBmc_t * p; Aig_Obj_t * pObj; @@ -763,6 +773,11 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLi for ( i = 0; i < 1000; i++ ) bmcg_sat_solver_addvar( p->pSat3 ); } + else if ( fUseCadical ) + { + p->pSat4 = cadical_solver_new(); + cadical_solver_setnvars(p->pSat4, 1000); + } else { p->pSat = sat_solver_new(); @@ -806,9 +821,9 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) p->pSat ? p->pSat->nLearntDelta : 0, p->pSat ? p->pSat->nLearntRatio : 0, p->pSat ? p->pSat->nDBreduces : 0, - p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2), + p->pSat ? sat_solver_nvars(p->pSat) : p->pSat4 ? cadical_solver_nvars(p->pSat4) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2), nUsedVars, - 100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2)) ); + 100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : p->pSat4 ? cadical_solver_nvars(p->pSat4) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2)) ); Abc_Print( 1, "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. UniProps = %d.\n", p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nUniProps ); } @@ -830,6 +845,7 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) if ( p->pSat ) sat_solver_delete( p->pSat ); if ( p->pSat2 ) satoko_destroy( p->pSat2 ); if ( p->pSat3 ) bmcg_sat_solver_stop( p->pSat3 ); + if ( p->pSat4 ) cadical_solver_delete( p->pSat4 ); ABC_FREE( p->pTime4Outs ); Vec_IntFree( p->vData ); Hsh_IntManStop( p->vHash ); @@ -1029,6 +1045,11 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits if ( !bmcg_sat_solver_addclause( p->pSat3, ClaLits, nClaLits ) ) assert( 0 ); } + else if ( p->pSat4 ) + { + if ( !cadical_solver_addclause( p->pSat4, ClaLits, ClaLits+nClaLits ) ) + assert( 0 ); + } else { if ( !sat_solver_addclause( p->pSat, ClaLits, ClaLits+nClaLits ) ) @@ -1287,6 +1308,11 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame ) for ( i = bmcg_sat_solver_varnum(p->pSat3); i < p->nSatVars; i++ ) bmcg_sat_solver_addvar( p->pSat3 ); } + else if ( p->pSat4 ) + { + for ( i = cadical_solver_nvars(p->pSat4); i < p->nSatVars; i++ ) + cadical_solver_addvar( p->pSat4 ); + } else sat_solver_setnvars( p->pSat, p->nSatVars ); return Lit; @@ -1411,6 +1437,11 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i ) if ( iLit != ~0 && bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(iLit)) ) Abc_InfoSetBit( pCex->pData, iBit + k ); } + else if ( p->pSat4) + { + if ( iLit != ~0 && cadical_solver_get_var_value(p->pSat4, lit_var(iLit)) ) + Abc_InfoSetBit( pCex->pData, iBit + k ); + } else { if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) ) @@ -1445,6 +1476,10 @@ int Saig_ManCallSolver( Gia_ManBmc_t * p, int Lit ) bmcg_sat_solver_set_conflict_budget( p->pSat3, p->pPars->nConfLimit ); return bmcg_sat_solver_solve( p->pSat3, &Lit, 1 ); } + else if ( p->pSat4 ) + { + return cadical_solver_solve( p->pSat4, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + } else return sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); } @@ -1482,7 +1517,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0; nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG ); // create BMC manager - p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose ); + p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose, pPars->fUseCadical ); p->pPars = pPars; if ( p->pSat ) { @@ -1498,6 +1533,10 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) { // satoko_set_runid(p->pSat3, p->pPars->RunId); // satoko_set_stop_func(p->pSat3, p->pPars->pFuncStop); + } + else if ( p->pSat4 ) + { + } else { @@ -1522,6 +1561,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) satoko_set_runtime_limit( p->pSat2, nTimeToStop ); else if ( p->pSat3 ) bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop ); + else if ( p-> pSat4 ) + Bmc3_CadicalSetRuntimeLimit( p->pSat4, nTimeToStop ); else sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); } @@ -1659,6 +1700,8 @@ clkOther += Abc_Clock() - clk2; satoko_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() ); else if ( p->pSat3 ) bmcg_sat_solver_set_runtime_limit( p->pSat3, p->pTime4Outs[i] + Abc_Clock() ); + else if ( p-> pSat4 ) + Bmc3_CadicalSetRuntimeLimit( p->pSat4, p->pTime4Outs[i] + Abc_Clock() ); else sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() ); } @@ -1690,6 +1733,8 @@ nTimeUnsat += clkSatRun; status = satoko_add_clause( p->pSat2, &Lit, 1 ); else if ( p->pSat3 ) status = bmcg_sat_solver_addclause( p->pSat3, &Lit, 1 ); + else if ( p->pSat4 ) + status = cadical_solver_addclause( p->pSat4, &Lit, &Lit + 1 ); else status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); assert( status ); @@ -1721,12 +1766,12 @@ nTimeSat += clkSatRun; { Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" ); Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars ); - Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) ); - Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) ); + Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat4 ? cadical_solver_nclauses(p->pSat4) : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) ); + Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) ); // Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); // Abc_Print( 1, "Uni =%7.0f. ",(double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) ); // ABC_PRT( "Time", Abc_Clock() - clk ); - Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) ); + Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat4 ? cadical_solver_nlearned(p->pSat4) : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) ); Abc_Print( 1, "%4.0f MB", 4.25*(f+1)*p->nObjNums /(1<<20) ); Abc_Print( 1, "%4.0f MB", 1.0*(p->pSat ? sat_solver_memory(p->pSat) : 0)/(1<<20) ); Abc_Print( 1, "%9.2f sec ", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); @@ -1773,6 +1818,8 @@ nTimeSat += clkSatRun; satoko_set_runtime_limit( p->pSat2, nTimeToStop ); else if ( p->pSat3 ) bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop ); + else if ( p->pSat4 ) + Bmc3_CadicalSetRuntimeLimit ( p->pSat4, nTimeToStop ); else sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); } @@ -1798,6 +1845,11 @@ nTimeSat += clkSatRun; if ( bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(Lit)) == Abc_LitIsCompl(Lit) ) continue; } + else if (p->pSat4) + { + if ( cadical_solver_get_var_value(p->pSat4, lit_var(Lit)) == Abc_LitIsCompl(Lit) ) + continue; + } else { if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) ) @@ -1841,7 +1893,7 @@ nTimeUndec += clkSatRun; } if ( pPars->fVerbose ) { - if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 1 ) + if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 1 ) { fFirst = 0; // Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f ); @@ -1849,11 +1901,11 @@ nTimeUndec += clkSatRun; Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" ); Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars ); // Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) ); - Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) ); - Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) ); + Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat4 ? cadical_solver_nclauses(p->pSat4) : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) ); + Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : p->pSat4 ? cadical_solver_nconflicts(p->pSat4) : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) ); // Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); // Abc_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) ); - Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) ); + Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat4 ? cadical_solver_nlearned(p->pSat4) : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) ); if ( pPars->fSolveAll ) Abc_Print( 1, "CEX =%5d. ", pPars->nFailOuts ); if ( pPars->nTimeOutOne ) diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c index e342ff350..b5831e7ff 100644 --- a/src/sat/bmc/bmcMaj.c +++ b/src/sat/bmc/bmcMaj.c @@ -488,7 +488,8 @@ int Exa_ManMarkup( Exa_Man_t * p ) } } } - printf( "The number of parameter variables = %d.\n", p->iVar ); + if ( !p->pPars->fSilent ) + printf( "The number of parameter variables = %d.\n", p->iVar ); return p->iVar; // printout for ( i = p->nVars; i < p->nObjs; i++ ) @@ -569,6 +570,18 @@ static inline int Exa_ManFindFanin( Exa_Man_t * p, int i, int k ) assert( Count == 1 ); return iVar; } +static inline char * Exa_ManObjName( Exa_Man_t * p, int iObj, char * pBuffer ) +{ + if ( iObj < 0 ) + sprintf( pBuffer, "*" ); + else if ( iObj < p->nVars ) + sprintf( pBuffer, "%c", 'a' + iObj ); + else if ( iObj - p->nVars < 26 ) + sprintf( pBuffer, "%c", 'A' + iObj - p->nVars ); + else + sprintf( pBuffer, "N%d", iObj - p->nVars ); + return pBuffer; +} static inline int Exa_ManEval( Exa_Man_t * p ) { static int Flag = 0; @@ -637,20 +650,18 @@ void Exa_ManDumpBlif( Exa_Man_t * p, int fCompl ) int Val1 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart); int Val2 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+1); int Val3 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+2); + char Name[16]; fprintf( pFile, ".names" ); for ( k = 1; k >= 0; k-- ) { iVar = Exa_ManFindFanin( p, i, k ); - if ( iVar >= 0 && iVar < p->nVars ) - fprintf( pFile, " %c", 'a'+iVar ); - else - fprintf( pFile, " %02d", iVar ); + fprintf( pFile, " %s", Exa_ManObjName(p, iVar, Name) ); } if ( i == p->nObjs - 1 ) fprintf( pFile, " F\n" ); else - fprintf( pFile, " %02d\n", i ); + fprintf( pFile, " %s\n", Exa_ManObjName(p, i, Name) ); if ( i == p->nObjs - 1 && fCompl ) fprintf( pFile, "00 1\n" ); if ( (i == p->nObjs - 1 && fCompl) ^ Val1 ) @@ -668,6 +679,7 @@ void Exa_ManDumpBlif( Exa_Man_t * p, int fCompl ) void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl ) { int i, k, iVar; + char Name[16]; printf( "Realization of given %d-input function using %d two-input gates:\n", p->nVars, p->nNodes ); // for ( i = p->nVars + 2; i < p->nObjs; i++ ) for ( i = p->nObjs - 1; i >= p->nVars; i-- ) @@ -677,20 +689,107 @@ void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl ) int Val2 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+1); int Val3 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+2); if ( i == p->nObjs - 1 && fCompl ) - printf( "%02d = 4\'b%d%d%d1(", i, !Val3, !Val2, !Val1 ); + printf( "%s = 4\'b%d%d%d1(", Exa_ManObjName(p, i, Name), !Val3, !Val2, !Val1 ); else - printf( "%02d = 4\'b%d%d%d0(", i, Val3, Val2, Val1 ); + printf( "%s = 4\'b%d%d%d0(", Exa_ManObjName(p, i, Name), Val3, Val2, Val1 ); for ( k = 1; k >= 0; k-- ) { iVar = Exa_ManFindFanin( p, i, k ); - if ( iVar >= 0 && iVar < p->nVars ) - printf( " %c", 'a'+iVar ); - else - printf( " %02d", iVar ); + printf( " %s", Exa_ManObjName(p, iVar, Name) ); } printf( " )\n" ); } } +static inline int Exa_ManPermFanin( Exa_Man_t * p, int i, int k ) +{ + char * pPermStr = p->pPars->pPermStr; + int iTarget = 2 * (i - p->nVars) + (k ? 0 : 1); + int nSeen = 0; + char * pToken; + if ( p->pPars->pPermFans ) + return p->pPars->pPermFans[iTarget]; + assert( pPermStr != NULL ); + for ( pToken = pPermStr; *pToken; ) + { + int iObj = -2; + if ( *pToken == '_' ) + { + pToken++; + continue; + } + if ( *pToken == '*' ) + { + iObj = -1; + pToken++; + } + else if ( *pToken >= 'a' && *pToken < 'a' + p->nVars ) + iObj = *pToken++ - 'a'; + else if ( *pToken >= 'A' && *pToken <= 'Z' ) + iObj = p->nVars + (*pToken++ - 'A'); + else if ( *pToken == 'N' ) + { + char * pNext = pToken + 1; + int Num = 0; + assert( *pNext >= '0' && *pNext <= '9' ); + while ( *pNext >= '0' && *pNext <= '9' ) + Num = 10 * Num + *pNext++ - '0'; + iObj = p->nVars + Num; + pToken = pNext; + } + else + assert( 0 ); + if ( nSeen++ == iTarget ) + return iObj; + } + assert( 0 ); + return -1; +} +static void Exa_ManPrintPermFanin( Exa_Man_t * p, int iFanin ) +{ + char Name[16]; + printf( "%s ", Exa_ManObjName(p, iFanin, Name) ); +} +static void Exa_ManPrintFixedPerm( Exa_Man_t * p ) +{ + int i, k; + char Name[16]; + if ( (p->pPars->pPermStr == NULL && p->pPars->pPermFans == NULL) || p->pPars->fSilent ) + return; + printf( "Using fixed input assignment provided by the user %s:\n", p->pPars->pPermStr ? p->pPars->pPermStr : "" ); + for ( i = p->nObjs - 1; i >= p->nVars; i-- ) + { + printf( "%s : ", Exa_ManObjName(p, i, Name) ); + for ( k = 1; k >= 0; k-- ) + Exa_ManPrintPermFanin( p, Exa_ManPermFanin(p, i, k) ); + printf( "\n" ); + } +} +static void Exa_ManPrintPerm( Exa_Man_t * p ) +{ + int i, k, iVar; + char Name[16]; + printf( "The variable permutation is \"" ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + if ( i > p->nVars ) + printf( "_" ); + for ( k = 1; k >= 0; k-- ) + { + iVar = Exa_ManFindFanin( p, i, k ); + printf( "%s", Exa_ManObjName(p, iVar, Name) ); + } + } + printf( "\".\n" ); +} +static void Exa_ManSaveSolution( Exa_Man_t * p ) +{ + int i, k, Pos = 0; + ABC_FREE( p->pPars->pSolFans ); + p->pPars->pSolFans = ABC_ALLOC( int, 2 * p->nNodes ); + for ( i = p->nVars; i < p->nObjs; i++ ) + for ( k = 1; k >= 0; k-- ) + p->pPars->pSolFans[Pos++] = Exa_ManFindFanin( p, i, k ); +} /**Function************************************************************* @@ -716,6 +815,39 @@ static inline int Exa_ManAddClause( Exa_Man_t * p, int * pLits, int nLits ) } return bmcg_sat_solver_addclause( p->pSat, pLits, nLits ); } +static int Exa_ManAddPermConstr( Exa_Man_t * p ) +{ + int i, k, iVar, Lit; + char Name0[16], Name1[16]; + if ( p->pPars->pPermStr == NULL && p->pPars->pPermFans == NULL ) + return 1; + Exa_ManPrintFixedPerm( p ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + for ( k = 0; k < 2; k++ ) + { + iVar = Exa_ManPermFanin( p, i, k ); + if ( iVar == -1 ) + continue; + if ( iVar < 0 || iVar >= p->nVars || p->VarMarks[i][k][iVar] == 0 ) + { + if ( iVar >= p->nVars && iVar < i && p->VarMarks[i][k][iVar] ) + { + Lit = Abc_Var2Lit( p->VarMarks[i][k][iVar], 0 ); + if ( !Exa_ManAddClause( p, &Lit, 1 ) ) + return 0; + continue; + } + printf( "Cannot force node %s fanin %d to object %s because this connection is not available.\n", Exa_ManObjName(p, i, Name0), k, Exa_ManObjName(p, iVar, Name1) ); + return 0; + } + Lit = Abc_Var2Lit( p->VarMarks[i][k][iVar], 0 ); + if ( !Exa_ManAddClause( p, &Lit, 1 ) ) + return 0; + } + } + return 1; +} int Exa_ManAddCnfAdd( Exa_Man_t * p, int * pnAdded ) { int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m; @@ -794,6 +926,8 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd ) assert( n == p->nVars + p->nNodes ); Vec_IntFreeP( &vRes ); } + if ( !Exa_ManAddPermConstr(p) ) + return 0; // input constraints for ( i = p->nVars; i < p->nObjs; i++ ) { @@ -946,9 +1080,10 @@ int Exa_ManAddCnf( Exa_Man_t * p, int iMint ) p->iVar += 3*p->nNodes; return 1; } -void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ) +int Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ) { int i, status, iMint = 1; + int fFound = 0; abctime clkTotal = Abc_Clock(); Exa_Man_t * p; int fCompl = 0; word pTruth[64]; Abc_TtReadHex( pTruth, pPars->pTtStr ); @@ -956,8 +1091,13 @@ void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ) p = Exa_ManAlloc( pPars, pTruth ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); } status = Exa_ManAddCnfStart( p, pPars->fOnlyAnd ); - assert( status ); - printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes ); + if ( !status ) + { + Exa_ManFree( p ); + return 0; + } + if ( !pPars->fSilent ) + printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes ); for ( i = 0; iMint != -1; i++ ) { abctime clk = Abc_Clock(); @@ -978,23 +1118,33 @@ void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars ) } if ( status == GLUCOSE_UNSAT ) { - printf( "The problem has no solution.\n" ); + if ( !pPars->fSilent ) + printf( "The problem has no solution.\n" ); break; } if ( status == GLUCOSE_UNDEC ) { - printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim ); + if ( !pPars->fSilent ) + printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim ); break; } iMint = Exa_ManEval( p ); } if ( iMint == -1 ) { - Exa_ManPrintSolution( p, fCompl ); - Exa_ManDumpBlif( p, fCompl ); + Exa_ManSaveSolution( p ); + if ( !pPars->fSilent ) + { + Exa_ManPrintSolution( p, fCompl ); + Exa_ManPrintPerm( p ); + Exa_ManDumpBlif( p, fCompl ); + } + fFound = 1; } Exa_ManFree( p ); - Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); + if ( !pPars->fSilent ) + Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); + return fFound; } diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c index 761795d96..23ccb7217 100644 --- a/src/sat/bmc/bmcMaj2.c +++ b/src/sat/bmc/bmcMaj2.c @@ -577,7 +577,8 @@ static int Exa_ManMarkup( Exa_Man_t * p ) } } } - printf( "The number of parameter variables = %d.\n", p->iVar ); + if ( !p->pPars->fSilent ) + printf( "The number of parameter variables = %d.\n", p->iVar ); return p->iVar; // printout for ( i = p->nVars; i < p->nObjs; i++ ) @@ -640,6 +641,18 @@ static inline int Exa_ManFindFanin( Exa_Man_t * p, int i, int k ) assert( Count == 1 ); return iVar; } +static inline char * Exa_ManObjName( Exa_Man_t * p, int iObj, char * pBuffer ) +{ + if ( iObj < 0 ) + sprintf( pBuffer, "*" ); + else if ( iObj < p->nVars ) + sprintf( pBuffer, "%c", 'a' + iObj ); + else if ( iObj - p->nVars < 26 ) + sprintf( pBuffer, "%c", 'A' + iObj - p->nVars ); + else + sprintf( pBuffer, "N%d", iObj - p->nVars ); + return pBuffer; +} static inline int Exa_ManEval( Exa_Man_t * p ) { static int Flag = 0; @@ -681,6 +694,7 @@ static inline int Exa_ManEval( Exa_Man_t * p ) static void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl ) { int i, k, iVar; + char Name[16]; printf( "Realization of given %d-input function using %d two-input gates:\n", p->nVars, p->nNodes ); // for ( i = p->nVars + 2; i < p->nObjs; i++ ) for ( i = p->nObjs - 1; i >= p->nVars; i-- ) @@ -690,20 +704,140 @@ static void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl ) int Val2 = sat_solver_var_value(p->pSat, iVarStart+1); int Val3 = sat_solver_var_value(p->pSat, iVarStart+2); if ( i == p->nObjs - 1 && fCompl ) - printf( "%02d = 4\'b%d%d%d1(", i, !Val3, !Val2, !Val1 ); + printf( "%s = 4\'b%d%d%d1(", Exa_ManObjName(p, i, Name), !Val3, !Val2, !Val1 ); else - printf( "%02d = 4\'b%d%d%d0(", i, Val3, Val2, Val1 ); + printf( "%s = 4\'b%d%d%d0(", Exa_ManObjName(p, i, Name), Val3, Val2, Val1 ); for ( k = 1; k >= 0; k-- ) { iVar = Exa_ManFindFanin( p, i, k ); - if ( iVar >= 0 && iVar < p->nVars ) - printf( " %c", 'a'+iVar ); - else - printf( " %02d", iVar ); + printf( " %s", Exa_ManObjName(p, iVar, Name) ); } printf( " )\n" ); } } +static inline int Exa_ManPermFanin( Exa_Man_t * p, int i, int k ) +{ + char * pPermStr = p->pPars->pPermStr; + int iTarget = 2 * (i - p->nVars) + (k ? 0 : 1); + int nSeen = 0; + char * pToken; + if ( p->pPars->pPermFans ) + return p->pPars->pPermFans[iTarget]; + assert( pPermStr != NULL ); + for ( pToken = pPermStr; *pToken; ) + { + int iObj = -2; + if ( *pToken == '_' ) + { + pToken++; + continue; + } + if ( *pToken == '*' ) + { + iObj = -1; + pToken++; + } + else if ( *pToken >= 'a' && *pToken < 'a' + p->nVars ) + iObj = *pToken++ - 'a'; + else if ( *pToken >= 'A' && *pToken <= 'Z' ) + iObj = p->nVars + (*pToken++ - 'A'); + else if ( *pToken == 'N' ) + { + char * pNext = pToken + 1; + int Num = 0; + assert( *pNext >= '0' && *pNext <= '9' ); + while ( *pNext >= '0' && *pNext <= '9' ) + Num = 10 * Num + *pNext++ - '0'; + iObj = p->nVars + Num; + pToken = pNext; + } + else + assert( 0 ); + if ( nSeen++ == iTarget ) + return iObj; + } + assert( 0 ); + return -1; +} +static void Exa_ManPrintPermFanin( Exa_Man_t * p, int iFanin ) +{ + char Name[16]; + printf( "%s ", Exa_ManObjName(p, iFanin, Name) ); +} +static void Exa_ManPrintFixedPerm( Exa_Man_t * p ) +{ + int i, k; + char Name[16]; + if ( (p->pPars->pPermStr == NULL && p->pPars->pPermFans == NULL) || p->pPars->fSilent ) + return; + printf( "Using fixed input assignment provided by the user %s:\n", p->pPars->pPermStr ? p->pPars->pPermStr : "" ); + for ( i = p->nObjs - 1; i >= p->nVars; i-- ) + { + printf( "%s : ", Exa_ManObjName(p, i, Name) ); + for ( k = 1; k >= 0; k-- ) + Exa_ManPrintPermFanin( p, Exa_ManPermFanin(p, i, k) ); + printf( "\n" ); + } +} +static void Exa_ManPrintPerm( Exa_Man_t * p ) +{ + int i, k, iVar; + char Name[16]; + printf( "The variable permutation is \"" ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + if ( i > p->nVars ) + printf( "_" ); + for ( k = 1; k >= 0; k-- ) + { + iVar = Exa_ManFindFanin( p, i, k ); + printf( "%s", Exa_ManObjName(p, iVar, Name) ); + } + } + printf( "\".\n" ); +} +static void Exa_ManSaveSolution( Exa_Man_t * p ) +{ + int i, k, Pos = 0; + ABC_FREE( p->pPars->pSolFans ); + p->pPars->pSolFans = ABC_ALLOC( int, 2 * p->nNodes ); + for ( i = p->nVars; i < p->nObjs; i++ ) + for ( k = 1; k >= 0; k-- ) + p->pPars->pSolFans[Pos++] = Exa_ManFindFanin( p, i, k ); +} +static int Exa_ManAddPermConstr( Exa_Man_t * p ) +{ + int i, k, iVar, Lit; + char Name0[16], Name1[16]; + if ( p->pPars->pPermStr == NULL && p->pPars->pPermFans == NULL ) + return 1; + Exa_ManPrintFixedPerm( p ); + for ( i = p->nVars; i < p->nObjs; i++ ) + { + for ( k = 0; k < 2; k++ ) + { + iVar = Exa_ManPermFanin( p, i, k ); + if ( iVar == -1 ) + continue; + if ( iVar < 0 || iVar >= p->nVars || p->VarMarks[i][k][iVar] == 0 ) + { + if ( iVar >= p->nVars && iVar < i && p->VarMarks[i][k][iVar] ) + { + Lit = Abc_Var2Lit( p->VarMarks[i][k][iVar], 0 ); + if ( !sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ) ) + return 0; + continue; + } + printf( "Cannot force node %s fanin %d to object %s because this connection is not available.\n", Exa_ManObjName(p, i, Name0), k, Exa_ManObjName(p, iVar, Name1) ); + return 0; + } + Lit = Abc_Var2Lit( p->VarMarks[i][k][iVar], 0 ); + if ( !sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ) ) + return 0; + } + } + return 1; +} /**Function************************************************************* @@ -720,6 +854,8 @@ static void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl ) static int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd ) { int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m; + if ( !Exa_ManAddPermConstr(p) ) + return 0; // input constraints for ( i = p->nVars; i < p->nObjs; i++ ) { @@ -849,9 +985,10 @@ static int Exa_ManAddCnf( Exa_Man_t * p, int iMint ) p->iVar += 3*p->nNodes; return 1; } -void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ) +int Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ) { int i, status, iMint = 1; + int fFound = 0; abctime clkTotal = Abc_Clock(); Exa_Man_t * p; int fCompl = 0; word pTruth[64]; Abc_TtReadHex( pTruth, pPars->pTtStr ); @@ -859,8 +996,13 @@ void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ) p = Exa_ManAlloc( pPars, pTruth ); if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); } status = Exa_ManAddCnfStart( p, pPars->fOnlyAnd ); - assert( status ); - printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes ); + if ( !status ) + { + Exa_ManFree( p ); + return 0; + } + if ( !pPars->fSilent ) + printf( "Running exact synthesis for %d-input function with %d two-input gates...\n", p->nVars, p->nNodes ); for ( i = 0; iMint != -1; i++ ) { abctime clk = Abc_Clock(); @@ -878,15 +1020,26 @@ void Exa_ManExactSynthesis2( Bmc_EsPar_t * pPars ) } if ( status == l_False ) { - printf( "The problem has no solution.\n" ); + if ( !pPars->fSilent ) + printf( "The problem has no solution.\n" ); break; } iMint = Exa_ManEval( p ); } if ( iMint == -1 ) - Exa_ManPrintSolution( p, fCompl ); + { + Exa_ManSaveSolution( p ); + if ( !pPars->fSilent ) + { + Exa_ManPrintSolution( p, fCompl ); + Exa_ManPrintPerm( p ); + } + fFound = 1; + } Exa_ManFree( p ); - Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); + if ( !pPars->fSilent ) + Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); + return fFound; } diff --git a/src/sat/cadical/cadical.hpp b/src/sat/cadical/cadical.hpp index 7ceedcec4..4ef09e0c4 100644 --- a/src/sat/cadical/cadical.hpp +++ b/src/sat/cadical/cadical.hpp @@ -1058,6 +1058,7 @@ public: // Extra APIs int clauses (); int conflicts (); + int learned (); private: //==== start of state ==================================================== diff --git a/src/sat/cadical/cadicalSolver.c b/src/sat/cadical/cadicalSolver.c index f27fe19f9..30cd6c68c 100644 --- a/src/sat/cadical/cadicalSolver.c +++ b/src/sat/cadical/cadicalSolver.c @@ -297,6 +297,21 @@ int cadical_solver_nconflicts(cadical_solver* s) { return ccadical_conflicts((CCaDiCaL*)s->p); } +/**Function************************************************************* + + Synopsis [get number of learned clauses] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int cadical_solver_nlearned(cadical_solver* s) { + return ccadical_learned((CCaDiCaL*)s->p); +} + /**Function************************************************************* diff --git a/src/sat/cadical/cadicalSolver.h b/src/sat/cadical/cadicalSolver.h index 2aec06c2a..9e6394ff5 100644 --- a/src/sat/cadical/cadicalSolver.h +++ b/src/sat/cadical/cadicalSolver.h @@ -67,6 +67,7 @@ extern void cadical_solver_setnvars(cadical_solver* s,int n); extern int cadical_solver_get_var_value(cadical_solver* s, int v); extern int cadical_solver_nclauses(cadical_solver* s); extern int cadical_solver_nconflicts(cadical_solver* s); +extern int cadical_solver_nlearned(cadical_solver* s); extern Vec_Int_t * cadical_solve_cnf( Cnf_Dat_t * pCnf, char * pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose ); ABC_NAMESPACE_HEADER_END diff --git a/src/sat/cadical/cadical_ccadical.cpp b/src/sat/cadical/cadical_ccadical.cpp index 3b61a0373..a929a4743 100644 --- a/src/sat/cadical/cadical_ccadical.cpp +++ b/src/sat/cadical/cadical_ccadical.cpp @@ -228,4 +228,8 @@ int ccadical_conflicts(CCaDiCaL *ptr) { return ((Wrapper *) ptr)->solver->conflicts (); } +int ccadical_learned(CCaDiCaL *ptr) { + return ((Wrapper *) ptr)->solver->learned (); +} + ABC_NAMESPACE_IMPL_END diff --git a/src/sat/cadical/cadical_solver.cpp b/src/sat/cadical/cadical_solver.cpp index 7dd03e8be..0efeddaa8 100644 --- a/src/sat/cadical/cadical_solver.cpp +++ b/src/sat/cadical/cadical_solver.cpp @@ -1853,6 +1853,10 @@ int Solver::conflicts () { return internal->stats.conflicts; } +int Solver::learned () { + return internal->stats.learned.clauses; +} + } // namespace CaDiCaL ABC_NAMESPACE_IMPL_END diff --git a/src/sat/cadical/ccadical.h b/src/sat/cadical/ccadical.h index ef442e7a3..b4401305c 100644 --- a/src/sat/cadical/ccadical.h +++ b/src/sat/cadical/ccadical.h @@ -63,6 +63,7 @@ void ccadical_resize(CCaDiCaL *, int min_max_var); int ccadical_is_inconsistent(CCaDiCaL *); int ccadical_clauses(CCaDiCaL *); int ccadical_conflicts(CCaDiCaL *); +int ccadical_learned(CCaDiCaL *); /*------------------------------------------------------------------------*/