New command &symfun.

This commit is contained in:
Alan Mishchenko 2025-11-12 10:04:10 -08:00
parent 9e90e6086d
commit 28f4ad8281
3 changed files with 214 additions and 10 deletions

View File

@ -34,6 +34,65 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManGenSymFun_rec( Gia_Man_t * p, word Str, int nChars, Vec_Ptr_t * vStrs, Vec_Wec_t * vLits, Vec_Int_t * vIns )
{
if ( Str == 0 ) return 0;
if ( Str == Abc_Tt6Mask(nChars) ) return 1;
assert( nChars > 1 );
Vec_Wrd_t * vStore = (Vec_Wrd_t *)Vec_PtrEntry(vStrs, nChars-1);
Vec_Int_t * vValue = Vec_WecEntry(vLits, nChars-1);
int Index;
if ( (Index = Vec_WrdFind(vStore, Str)) >= 0 )
return Vec_IntEntry(vValue, Index);
word Str0 = Str & ~Abc_Tt6MaskI(nChars-1);
word Str1 = Str >> 1;
int Lit0 = Gia_ManGenSymFun_rec( p, Str0, nChars-1, vStrs, vLits, vIns );
int Lit1 = Gia_ManGenSymFun_rec( p, Str1, nChars-1, vStrs, vLits, vIns );
int Lit = Gia_ManAppendMux2( p, Vec_IntEntry(vIns, nChars-2), Lit1, Lit0 );
Vec_WrdPush( vStore, Str );
Vec_WrdPush( vStore, ~Str & Abc_Tt6Mask(nChars) );
Vec_IntPush( vValue, Lit );
Vec_IntPush( vValue, Abc_LitNot(Lit) );
return Lit;
}
Gia_Man_t * Gia_ManGenSymFun( Vec_Wrd_t * vFuns, int nChars, int fVerbose )
{
assert( nChars <= 64 );
word Str; int i;
Vec_Ptr_t * vStrs = Vec_PtrAlloc(nChars);
for ( i = 0; i < nChars; i++ )
Vec_PtrPush( vStrs, Vec_WrdAlloc(0) );
Vec_Wec_t * vLits = Vec_WecStart(nChars);
Vec_Int_t * vOuts = Vec_IntAlloc(Vec_WrdSize(vFuns));
Gia_Man_t * pNew = Gia_ManStart( 10000 );
pNew->pName = Abc_UtilStrsav( "sym" );
Vec_Int_t * vIns = Vec_IntAlloc(nChars-1);
for ( i = 0; i < nChars-1; i++ )
Vec_IntPush(vIns, Gia_ManAppendCi(pNew));
Vec_WrdForEachEntry( vFuns, Str, i )
Vec_IntPush( vOuts, Gia_ManGenSymFun_rec(pNew, Str, nChars, vStrs, vLits, vIns ) );
Vec_WrdForEachEntry( vFuns, Str, i )
Gia_ManAppendCo(pNew, Vec_IntEntry(vOuts,i) );
for ( i = 0; i < nChars; i++ )
Vec_WrdFree( (Vec_Wrd_t *)Vec_PtrEntry(vStrs, i) );
Vec_PtrFree(vStrs);
Vec_WecFree(vLits);
Vec_IntFree(vOuts);
Vec_IntFree(vIns);
return pNew;
}
/**Function*************************************************************
Synopsis []
@ -101,15 +160,15 @@ char * Gia_LutCasPerm( int nVars, int nLuts, int LutSize )
Gia_LutCasSort( pRes + i * LutSize, 1, LutSize-1 );
return pRes;
}
int Gia_ManLutCasGen_rec( Gia_Man_t * pNew, Vec_Int_t * vCtrls, int iCtrl, Vec_Int_t * vDatas, int Shift )
int Gia_ManGenLutCas_rec( Gia_Man_t * pNew, Vec_Int_t * vCtrls, int iCtrl, Vec_Int_t * vDatas, int Shift )
{
if ( iCtrl-- == 0 )
return Vec_IntEntry( vDatas, Shift );
int iLit0 = Gia_ManLutCasGen_rec( pNew, vCtrls, iCtrl, vDatas, Shift );
int iLit1 = Gia_ManLutCasGen_rec( pNew, vCtrls, iCtrl, vDatas, Shift + (1<<iCtrl));
int iLit0 = Gia_ManGenLutCas_rec( pNew, vCtrls, iCtrl, vDatas, Shift );
int iLit1 = Gia_ManGenLutCas_rec( pNew, vCtrls, iCtrl, vDatas, Shift + (1<<iCtrl));
return Gia_ManAppendMux( pNew, Vec_IntEntry(vCtrls, iCtrl), iLit1, iLit0 );
}
Gia_Man_t * Gia_ManLutCasGen( Gia_Man_t * p, char * pPermStr, int nVars, int nLuts, int LutSize, int Seed, int fVerbose )
Gia_Man_t * Gia_ManGenLutCas( Gia_Man_t * p, char * pPermStr, int nVars, int nLuts, int LutSize, int Seed, int fVerbose )
{
if ( Seed )
srand(Seed);
@ -139,7 +198,7 @@ Gia_Man_t * Gia_ManLutCasGen( Gia_Man_t * p, char * pPermStr, int nVars, int nLu
pCur++;
for ( int k = 1; k < LutSize; k++ )
Vec_IntWriteEntry( vLits, k, Vec_IntEntry(vCtrls, (int)(*pCur++ - 'a')) );
Vec_IntWriteEntry( vLits, 0, Gia_ManLutCasGen_rec(pNew, vLits, LutSize, vDatas, i * (1 << LutSize)) );
Vec_IntWriteEntry( vLits, 0, Gia_ManGenLutCas_rec(pNew, vLits, LutSize, vDatas, i * (1 << LutSize)) );
}
// if the AIG is given, create a miter
int iLit = Vec_IntEntry(vLits, 0);
@ -166,7 +225,7 @@ Gia_Man_t * Gia_ManLutCasGen( Gia_Man_t * p, char * pPermStr, int nVars, int nLu
}
/*
int Gia_ManLutCasGenSolve( int nVars, int nLuts, int LutSize, char * pTtStr, int fVerbose )
int Gia_ManGenLutCasSolve( int nVars, int nLuts, int LutSize, char * pTtStr, int fVerbose )
{
extern Gia_Man_t * Gia_QbfQuantifyAll( Gia_Man_t * p, int nPars, int fAndAll, int fOrAll );
assert( strlen(pTtStr) <= 1024 );
@ -174,7 +233,7 @@ int Gia_ManLutCasGenSolve( int nVars, int nLuts, int LutSize, char * pTtStr, int
int i, Id, nVars = Abc_TtReadHex( pTruth, pTtStr );
assert( nVars <= 12 );
int nParams = nLuts * (1 << LutSize);
Gia_Man_t * pCas = Gia_ManLutCasGen( NULL, NULL, nVars, nLuts, LutSize, 0, fVerbose );
Gia_Man_t * pCas = Gia_ManGenLutCas( NULL, NULL, nVars, nLuts, LutSize, 0, fVerbose );
Gia_Man_t * pCofs = Gia_QbfQuantifyAll( pCas, nParams, 0, 0 );
Gia_ManFree( pCas );
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCofs, 8, 0, 0, 0, 0 );

View File

@ -519,6 +519,7 @@ static int Abc_CommandAbc9Nf ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Of ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Simap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Exmap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SymFun ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Pack ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Edge ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatLut ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1342,6 +1343,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&of", Abc_CommandAbc9Of, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&simap", Abc_CommandAbc9Simap, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&exmap", Abc_CommandAbc9Exmap, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&symfun", Abc_CommandAbc9SymFun, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&pack", Abc_CommandAbc9Pack, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&edge", Abc_CommandAbc9Edge, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&satlut", Abc_CommandAbc9SatLut, 0 );
@ -45517,6 +45519,111 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9SymFun( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManGenSymFun( Vec_Wrd_t * vFuns, int nChars, int fVerbose );
Gia_Man_t * pNew = NULL;
Vec_Wrd_t * vFuns = NULL;
int c, nChars = 0, nMaj = 0, nHot = 0, nXor = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MHXvh" ) ) != EOF )
{
switch ( c )
{
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by a file name.\n" );
goto usage;
}
nMaj = atoi(argv[globalUtilOptind++]);
break;
case 'H':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-H\" should be followed by a file name.\n" );
goto usage;
}
nHot = atoi(argv[globalUtilOptind++]);
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by a file name.\n" );
goto usage;
}
nXor = atoi(argv[globalUtilOptind++]);
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
default:
goto usage;
}
}
if ( nMaj ) {
nChars = nMaj+1;
vFuns = Vec_WrdAlloc(1);
Vec_WrdPush( vFuns, Abc_Tt6Mask(nMaj/2+1) << (nMaj/2+1) );
}
else if ( nHot ) {
nChars = nHot+1;
vFuns = Vec_WrdAlloc(1);
Vec_WrdPush( vFuns, 2 );
}
else if ( nXor ) {
nChars = nXor+1;
vFuns = Vec_WrdAlloc(1);
Vec_WrdPush( vFuns, ABC_CONST(0xAAAAAAAAAAAAAAAA) & Abc_Tt6Mask(nXor+1) );
}
else {
if ( argc == globalUtilOptind ) {
printf( "One or more characteristic strings should be given on the command line.\n" );
return 0;
}
nChars = (int)strlen(argv[globalUtilOptind]);
for ( c = globalUtilOptind+1; c < argc; c++ )
if ( nChars != (int)strlen(argv[c]) ) {
printf( "Char strings have different lengths. Quitting.\n" );
return 0;
}
vFuns = Vec_WrdAlloc( argc );
for ( c = globalUtilOptind; c < argc; c++ )
Vec_WrdPush( vFuns, Abc_TtReadBin64(argv[c]) );
}
if ( nChars > 64 ) {
printf( "Currently can handle functions up to 63 inputs. Quitting.\n" );
return 0;
}
pNew = Gia_ManGenSymFun( vFuns, nChars, fVerbose );
Abc_FrameUpdateGia( pAbc, pNew );
Vec_WrdFree( vFuns );
return 0;
usage:
Abc_Print( -2, "usage: &symfun [-MHX num] [-vh] <str0> <str1> ... <str(N-1)>\n" );
Abc_Print( -2, "\t derives AIG of a multi-output symmetric function\n" );
Abc_Print( -2, "\t-M <num> : generate the majority gate with the given input count [default = unused]\n" );
Abc_Print( -2, "\t-H <num> : generate the 1-hot condition with the given input count [default = unused]\n" );
Abc_Print( -2, "\t-X <num> : generate the xor-gate with the given input count [default = unused]\n" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : prints the command usage\n");
Abc_Print( -2, "\t<str0> <str1> ... <str(N-1)> : char strings in binary notation LSB first\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -51726,7 +51833,7 @@ usage:
***********************************************************************/
int Abc_CommandAbc9GenLutCas( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManLutCasGen( Gia_Man_t * p, char * pPermStr, int nVars, int nLuts, int LutSize, int Seed, int fVerbose );
extern Gia_Man_t * Gia_ManGenLutCas( Gia_Man_t * p, char * pPermStr, int nVars, int nLuts, int LutSize, int Seed, int fVerbose );
int nVars = 0;
int nLuts = 2;
int LutSize = 6;
@ -51840,7 +51947,7 @@ int Abc_CommandAbc9GenLutCas( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Function with %d variables is too large for a cascade composed of %d connected %d-LUTs.\n", nVars, nLuts, LutSize );
return 1;
}
pTemp = Gia_ManLutCasGen( pAbc->pGia, pPermStr, nVars, nLuts, LutSize, Seed, fVerbose );
pTemp = Gia_ManGenLutCas( pAbc->pGia, pPermStr, nVars, nLuts, LutSize, Seed, fVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;

View File

@ -230,7 +230,8 @@ static inline int Abc_TtHexDigitNum( int nVars ) { return nVars <= 2 ? 1 : 1 <<
SeeAlso []
***********************************************************************/
static inline word Abc_Tt6Mask( int nBits ) { assert( nBits >= 0 && nBits <= 64 ); return (~(word)0) >> (64-nBits); }
static inline word Abc_Tt6MaskI( int iBit ) { assert( iBit >= 0 && iBit <= 64 ); return ((word)1) << iBit; }
static inline word Abc_Tt6Mask( int nBits ) { assert( nBits >= 0 && nBits <= 64 ); return (~(word)0) >> (64-nBits); }
static inline void Abc_TtMask( word * pTruth, int nWords, int nBits )
{
int w;
@ -1579,6 +1580,43 @@ static inline int Abc_TtReadHexNumber( word * pTruth, char * pString )
}
/**Function*************************************************************
Synopsis [Reads the integer number as a binary string.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_TtReadBin( word * pWords, int nWords, char * pString )
{
int i, Len = (int)strlen(pString), nWords2 = (Len+63)/64;
assert( nWords2 <= nWords );
memset( pWords, 0, sizeof(word)*nWords );
for ( i = 0; i < Len; i++ )
if ( pString[i] == '1' )
Abc_TtSetBit(pWords, i);
else if ( pString[i] != '0' )
return 0;
return 1;
}
static inline word Abc_TtReadBin64( char * pString )
{
word Word = 0;
int Len = (int)strlen(pString);
assert( Len <= 64 );
int Res = Abc_TtReadBin( &Word, 1, pString );
if ( Res == 0 ) {
printf( "Reading binary string \"%s\" has failed.\n", pString );
Word = ~(word)0;
}
return Word;
}
/**Function*************************************************************
Synopsis []