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

Imrpovements in "twoexact".

This commit is contained in:
Alan Mishchenko 2026-05-17 18:51:49 -07:00
parent 7bf1177d39
commit 07e38ef030
4 changed files with 823 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -10602,19 +10602,356 @@ 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_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 )
{
@ -10671,6 +11008,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;
@ -10704,6 +11083,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;
@ -10717,6 +11102,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;
}
@ -10742,6 +11132,143 @@ 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 )
{
int i, nEntries = 0;
for ( i = 0; pPars->pPermStr[i]; i++ )
{
char Sym = pPars->pPermStr[i];
if ( Sym == '_' )
continue;
if ( Sym != '*' && (Sym < 'a' || Sym >= 'a' + pPars->nVars) )
{
Abc_Print( -1, "Permutation symbol \"%c\" is not one of '*', '_' or input variables 'a' through '%c'.\n", Sym, 'a' + pPars->nVars - 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 <num>\" 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 )
@ -10752,16 +11279,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 <num>] [-S str] [-abdconugklmvh] <hex>\n" );
Abc_Print( -2, "usage: twoexact [-INTGCDE <num>] [-S str] [-P str] [-abdconugklmtxvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" );
Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars );
Abc_Print( -2, "\t-N <num> : the number of two-input nodes [default = %d]\n", pPars->nNodes );
Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim );
Abc_Print( -2, "\t-G <num> : the largest allowed gate size (NANDs only) [default = %d]\n", GateSize );
Abc_Print( -2, "\t-S <str> : structural guidance from the user [default = %s]\n", pPars->pGuide ? pPars->pGuide : "unknown" );
Abc_Print( -2, "\t-P <str> : fixed input permutation; '_' separates gates, '*' leaves fanin free [default = %s]\n", pPars->pPermStr ? pPars->pPermStr : "none" );
Abc_Print( -2, "\t-C <num> : number of random candidate permutations to try [default = %d]\n", nCandPerms );
Abc_Print( -2, "\t-D <num> : number of fixed variable positions randomized to '*' in each candidate [default = %d]\n", nPermDcs );
Abc_Print( -2, "\t-E <num> : 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" );
@ -10773,6 +11305,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 <num>\" [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<hex> : truth table in hex notation\n" );

2
src/sat/bmc/bmc.h
View File

@ -82,6 +82,8 @@ struct Bmc_EsPar_t_
char * pSymStr;
char * pPermStr;
char * pGuide;
int * pPermFans;
int * pSolFans;
Vec_Wrd_t* vTruths;
};

163
src/sat/bmc/bmcMaj.c
View File

@ -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,80 @@ 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, s;
if ( p->pPars->pPermFans )
return p->pPars->pPermFans[iTarget];
assert( pPermStr != NULL );
for ( s = 0; pPermStr[s]; s++ )
{
if ( pPermStr[s] == '_' )
continue;
if ( nSeen++ == iTarget )
return pPermStr[s] == '*' ? -1 : pPermStr[s] - 'a';
}
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;
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( "%c", iVar < p->nVars ? 'a' + iVar : '*' );
}
}
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 +788,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 +899,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 +1053,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 +1064,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 +1091,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;
}

152
src/sat/bmc/bmcMaj2.c
View File

@ -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,113 @@ 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, s;
if ( p->pPars->pPermFans )
return p->pPars->pPermFans[iTarget];
assert( pPermStr != NULL );
for ( s = 0; pPermStr[s]; s++ )
{
if ( pPermStr[s] == '_' )
continue;
if ( nSeen++ == iTarget )
return pPermStr[s] == '*' ? -1 : pPermStr[s] - 'a';
}
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;
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( "%c", iVar < p->nVars ? 'a' + iVar : '*' );
}
}
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 +827,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 +958,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 +969,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 +993,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;
}