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

Updating interface of "twoexaxct".

This commit is contained in:
Alan Mishchenko 2026-05-18 07:31:39 -07:00
parent ffb0ff63fc
commit f4d870e109
3 changed files with 110 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -10720,6 +10720,41 @@ static char * Abc_TwoExactPermEncodeFull( int * pFans, int nVars, int nNodes )
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;
@ -11164,15 +11199,19 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pPars->pPermStr )
{
int i, nEntries = 0;
for ( i = 0; pPars->pPermStr[i]; i++ )
char * pToken = pPars->pPermStr;
int nEntries = 0;
while ( *pToken )
{
char Sym = pPars->pPermStr[i];
if ( Sym == '_' )
continue;
if ( Sym != '*' && (Sym < 'a' || Sym >= 'a' + pPars->nVars) )
int iObj = -1;
if ( *pToken == '_' )
{
Abc_Print( -1, "Permutation symbol \"%c\" is not one of '*', '_' or input variables 'a' through '%c'.\n", Sym, 'a' + pPars->nVars - 1 );
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++;

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

@ -704,16 +704,42 @@ 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;
int nSeen = 0;
char * pToken;
if ( p->pPars->pPermFans )
return p->pPars->pPermFans[iTarget];
assert( pPermStr != NULL );
for ( s = 0; pPermStr[s]; s++ )
for ( pToken = pPermStr; *pToken; )
{
if ( pPermStr[s] == '_' )
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 pPermStr[s] == '*' ? -1 : pPermStr[s] - 'a';
return iObj;
}
assert( 0 );
return -1;
@ -741,6 +767,7 @@ static void Exa_ManPrintFixedPerm( Exa_Man_t * p )
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++ )
{
@ -749,7 +776,7 @@ static void Exa_ManPrintPerm( Exa_Man_t * p )
for ( k = 1; k >= 0; k-- )
{
iVar = Exa_ManFindFanin( p, i, k );
printf( "%c", iVar < p->nVars ? 'a' + iVar : '*' );
printf( "%s", Exa_ManObjName(p, iVar, Name) );
}
}
printf( "\".\n" );

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

@ -719,16 +719,42 @@ 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;
int nSeen = 0;
char * pToken;
if ( p->pPars->pPermFans )
return p->pPars->pPermFans[iTarget];
assert( pPermStr != NULL );
for ( s = 0; pPermStr[s]; s++ )
for ( pToken = pPermStr; *pToken; )
{
if ( pPermStr[s] == '_' )
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 pPermStr[s] == '*' ? -1 : pPermStr[s] - 'a';
return iObj;
}
assert( 0 );
return -1;
@ -756,6 +782,7 @@ static void Exa_ManPrintFixedPerm( Exa_Man_t * p )
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++ )
{
@ -764,7 +791,7 @@ static void Exa_ManPrintPerm( Exa_Man_t * p )
for ( k = 1; k >= 0; k-- )
{
iVar = Exa_ManFindFanin( p, i, k );
printf( "%c", iVar < p->nVars ? 'a' + iVar : '*' );
printf( "%s", Exa_ManObjName(p, iVar, Name) );
}
}
printf( "\".\n" );