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

Enabling user-specified output signature in &polyn.

This commit is contained in:
Alan Mishchenko 2018-06-13 19:34:52 -07:00
parent aa2f29fa67
commit 01d736cba4
2 changed files with 249 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -42775,11 +42775,11 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_PolynBuild2Test( Gia_Man_t * pGia, int nExtra, int fSigned, int fVerbose, int fVeryVerbose );
Vec_Int_t * vOrder = NULL;
int c, nExtra = -1, fOld = 0, fSimple = 1, fSigned = 0, fVerbose = 0, fVeryVerbose = 0;
extern void Gia_PolynBuild2Test( Gia_Man_t * pGia, char * pSign, int nExtra, int fSigned, int fVerbose, int fVeryVerbose );
Vec_Int_t * vOrder = NULL; char * pSign = NULL;
int c, nExtra = 0, fOld = 0, fSimple = 1, fSigned = 0, fVerbose = 0, fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Noasvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "NSoasvwh" ) ) != EOF )
{
switch ( c )
{
@ -42794,6 +42794,15 @@ int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nExtra < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by a char string without spaces.\n" );
goto usage;
}
pSign = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'o':
fOld ^= 1;
break;
@ -42820,6 +42829,11 @@ int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Esop(): There is no AIG.\n" );
return 0;
}
if ( argc >= globalUtilOptind + 1 )
{
printf( "Trailing symbols on the command line (\"%s\").\n", argv[globalUtilOptind] );
return 0;
}
if ( fOld )
{
vOrder = fSimple ? NULL : Gia_PolynReorder( pAbc->pGia, fVerbose, fVeryVerbose );
@ -42827,11 +42841,11 @@ int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
Vec_IntFreeP( &vOrder );
}
else
Gia_PolynBuild2Test( pAbc->pGia, nExtra, fSigned, fVerbose, fVeryVerbose );
Gia_PolynBuild2Test( pAbc->pGia, pSign, nExtra, fSigned, fVerbose, fVeryVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &polyn [-N num] [-oasvwh]\n" );
Abc_Print( -2, "usage: &polyn [-N num] [-oasvwh] [-S str]\n" );
Abc_Print( -2, "\t derives algebraic polynomial from AIG\n" );
Abc_Print( -2, "\t-N num : the number of additional primary outputs (-1 = unused) [default = %d]\n", nExtra );
Abc_Print( -2, "\t-o : toggles old computation [default = %s]\n", fOld? "yes": "no" );
@ -42840,6 +42854,18 @@ usage:
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggles printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t\n");
Abc_Print( -2, "\t-S str : (optional) the output signature as a character string\n" );
Abc_Print( -2, "\t The format used to represent the output signature is very restrictive.\n" );
Abc_Print( -2, "\t It should be a string without spaces containing monomials in terms of\n" );
Abc_Print( -2, "\t inputs (i<num>) and outputs (o<num>) where <num> is 0-based. Coefficients\n" );
Abc_Print( -2, "\t are degrees of two, represented by log2 of their value: for example, \n" );
Abc_Print( -2, "\t \"2\" is 2^2 = 4, \"-4\" is -2^4=-16, \"-0\" is -2^0=-1, etc\n" );
Abc_Print( -2, "\t Two types of signature are accepted:\n" );
Abc_Print( -2, "\t (1) a sequence of monomials without parentheses (for example, \"-2*o0+1*o1+0*o2\")\n" );
Abc_Print( -2, "\t (2) a product of two sequences followed by a sum with a sequence\n" );
Abc_Print( -2, "\t (for example, \"(4*o0+2*o1+1*o2)*(4*i3+2*i4+1*i5)+(4*o3+2*o4+1*o5)\")\n" );
Abc_Print( -2, "\t Here is the signature of a signed 2-bit multiplier: \"(0*o0+1*o1+2*o2-3*o3)\"\n" );
return 1;
}

224
src/proof/acec/acecPo.c
View File

@ -32,6 +32,168 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Parses signature given on the command line.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acec_ParseSignatureMono( char * p, char * pStop, Vec_Int_t * vLevel )
{
char * pTemp = p;
int Const = ABC_INFINITY;
int fMinus = pTemp[0] == '-';
if ( pTemp[0] == '+' || pTemp[0] == '-' || pTemp[0] == '(' )
pTemp++;
while ( pTemp < pStop )
{
if ( pTemp[0] == 'i' ) // input
Vec_IntPush( vLevel, -1-atoi(++pTemp) );
else if ( pTemp[0] == 'o' ) // output
Vec_IntPush( vLevel, atoi(++pTemp) );
else // coefficient
{
assert( Const == ABC_INFINITY );
Const = 1 + atoi(pTemp);
}
while ( pTemp[0] >= '0' && pTemp[0] <= '9' )
pTemp++;
assert( pTemp == pStop || pTemp[0] == '*' );
pTemp++;
}
assert( Const != ABC_INFINITY );
Vec_IntPush( vLevel, fMinus ? -Const : Const );
}
Vec_Wec_t * Acec_ParseSignatureOne( char * p, char * pStop )
{
Vec_Wec_t * vMonos = Vec_WecAlloc( 10 );
char * pTemp = p, * pNext;
assert( p[0] == '(' && pStop[0] == ')' );
while ( pTemp[0] != ')' )
{
for ( pNext = pTemp+1; pNext < pStop; pNext++ )
if ( pNext[0] == '+' || pNext[0] == '-' )
break;
assert( pNext[0] == '+' || pNext[0] == '-' || pNext[0] == ')' );
Acec_ParseSignatureMono( pTemp, pNext, Vec_WecPushLevel(vMonos) );
pTemp = pNext;
}
return vMonos;
}
Vec_Wec_t * Acec_ParseDistribute( Vec_Wec_t * vM1, Vec_Wec_t * vM2, Vec_Wec_t * vAdd )
{
Vec_Wec_t * vMonos = Vec_WecAlloc( 10 );
Vec_Int_t * vLevel1, * vLevel2, * vLevel;
int i, k, n, Entry;
Vec_WecForEachLevel( vM1, vLevel1, i )
Vec_WecForEachLevel( vM2, vLevel2, k )
{
vLevel = Vec_WecPushLevel(vMonos);
Vec_IntForEachEntryStop( vLevel1, Entry, n, Vec_IntSize(vLevel1)-1 )
Vec_IntPush(vLevel, Entry);
Vec_IntForEachEntryStop( vLevel2, Entry, n, Vec_IntSize(vLevel2)-1 )
Vec_IntPush(vLevel, Entry);
Vec_IntPush(vLevel, Vec_IntEntryLast(vLevel1)+Vec_IntEntryLast(vLevel2));
}
Vec_WecForEachLevel( vAdd, vLevel1, k )
{
vLevel = Vec_WecPushLevel(vMonos);
Vec_IntForEachEntry( vLevel1, Entry, n )
Vec_IntPush(vLevel, Entry);
}
return vMonos;
}
Vec_Wec_t * Acec_ParseSignature( char * p )
{
Vec_Wec_t * vAdd = NULL, * vTemp1, * vTemp2, * vRes;
if ( p[0] == '(' )
{
char * pStop = strstr(p, ")");
if ( pStop == NULL )
return NULL;
vTemp1 = Acec_ParseSignatureOne( p, pStop );
if ( pStop[1] == 0 )
return vTemp1;
if ( pStop[1] == '*' )
{
char * p2 = pStop + 2;
char * pStop2 = strstr(p2, ")");
if ( p2[0] != '(' )
return NULL;
if ( pStop2 == NULL )
return NULL;
vTemp2 = Acec_ParseSignatureOne( p2, pStop2 );
if ( pStop2[1] == 0 )
{
vRes = Acec_ParseDistribute( vTemp1, vTemp2, vAdd );
Vec_WecFree( vTemp1 );
Vec_WecFree( vTemp2 );
return vRes;
}
if ( pStop2[1] == '+' )
{
char * p3 = pStop2 + 2;
char * pStop3 = strstr(p3, ")");
if ( p3[0] != '(' )
return NULL;
if ( pStop3 == NULL )
return NULL;
vAdd = Acec_ParseSignatureOne( p3, pStop3 );
vRes = Acec_ParseDistribute( vTemp1, vTemp2, vAdd );
Vec_WecFree( vTemp1 );
Vec_WecFree( vTemp2 );
Vec_WecFree( vAdd );
return vRes;
}
assert( 0 );
}
assert( 0 );
}
else
{
int Len = strlen(p);
char * pCopy = ABC_ALLOC( char, Len+3 );
pCopy[0] = '(';
strcpy( pCopy+1, p );
pCopy[Len+1] = ')';
pCopy[Len+2] = '\0';
vRes = Acec_ParseSignatureOne( pCopy, pCopy + Len + 1 );
ABC_FREE( pCopy );
return vRes;
}
return NULL;
}
void Acec_PrintSignature( Vec_Wec_t * vMonos )
{
Vec_Int_t * vLevel; int i, k, Entry;
printf( "Output signature with %d monomials:\n", Vec_WecSize(vMonos) );
Vec_WecForEachLevel( vMonos, vLevel, i )
{
printf( " %s2^%d", Vec_IntEntryLast(vLevel) > 0 ? "+":"-", Abc_AbsInt(Vec_IntEntryLast(vLevel))-1 );
Vec_IntForEachEntryStop( vLevel, Entry, k, Vec_IntSize(vLevel)-1 )
{
printf( " * " );
if ( Entry < 0 )
printf( "i%d", -Entry-1 );
else
printf( "o%d", Entry );
}
printf( "\n" );
}
}
void Acec_ParseSignatureTest()
{
char * pSign = "(4*o1+2*o2+1*o3)*(4*i4+2*i5+1*i6)+(4*o4+2*o5+1*o6)";
Vec_Wec_t * vMonos = Acec_ParseSignature( pSign );
Acec_PrintSignature( vMonos );
Vec_WecFree( vMonos );
}
/**Function*************************************************************
Synopsis [Checks that items are unique and in order.]
@ -101,7 +263,7 @@ void Gia_PolynPrintMono( Vec_Int_t * vConst, Vec_Int_t * vMono, int Prev )
Vec_IntForEachEntry( vConst, Entry, k )
printf( "%s2^%d", Entry < 0 ? "-" : "+", Abc_AbsInt(Entry)-1 );
Vec_IntForEachEntry( vMono, Entry, k )
printf( " * %d", Entry-1 );
printf( " * i%d", Entry-1 );
printf( "\n" );
}
void Gia_PolynPrint( Vec_Wec_t * vPolyn )
@ -121,7 +283,7 @@ void Gia_PolynPrintStats( Vec_Wec_t * vPolyn )
{
Vec_Int_t * vConst, * vCountsP, * vCountsN;
int i, Entry, Max = 0;
printf( "Polynomial with %d monomials:\n", Vec_WecSize(vPolyn)/2 );
printf( "Input signature with %d monomials:\n", Vec_WecSize(vPolyn)/2 );
for ( i = 0; i < Vec_WecSize(vPolyn)/2; i++ )
{
vConst = Vec_WecEntry( vPolyn, 2*i+0 );
@ -140,10 +302,10 @@ void Gia_PolynPrintStats( Vec_Wec_t * vPolyn )
}
Vec_IntForEachEntry( vCountsN, Entry, i )
if ( Entry )
printf( "-2^%d appears %d times\n", Abc_AbsInt(i)-1, Entry );
printf( " -2^%d appears %d times\n", Abc_AbsInt(i)-1, Entry );
Vec_IntForEachEntry( vCountsP, Entry, i )
if ( Entry )
printf( "+2^%d appears %d times\n", Abc_AbsInt(i)-1, Entry );
printf( " +2^%d appears %d times\n", Abc_AbsInt(i)-1, Entry );
Vec_IntFree( vCountsP );
Vec_IntFree( vCountsN );
}
@ -474,7 +636,7 @@ static inline void Gia_PolynPrepare4( Vec_Int_t * vTempC[4], Vec_Int_t * vTempM[
Vec_IntPushUniqueOrder( vTempM[3], iFan1 );
}
Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Int_t * vRootLits, int nExtra, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, int fSigned, int fVerbose, int fVeryVerbose )
Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Wec_t * vSign, Vec_Int_t * vRootLits, int nExtra, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, int fSigned, int fVerbose, int fVeryVerbose )
{
abctime clk = Abc_Clock();
Vec_Wec_t * vPolyn;
@ -498,6 +660,44 @@ Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Int_t * vRootLits, int nExt
printf( "Assigning %d outputs from %d to %d rank %d.\n", nExtra, Vec_IntSize(vRootLits)-nExtra, Vec_IntSize(vRootLits)-1, Vec_IntSize(vRootLits)-nExtra );
// create output signature
if ( vSign )
{
Vec_Int_t * vLevel; int Entry, OutLit;
Vec_WecForEachLevel( vSign, vLevel, i )
{
OutLit = -1;
Vec_IntClear( vTempM[0] );
Vec_IntFill( vTempC[0], 1, Vec_IntEntryLast(vLevel) );
Vec_IntForEachEntryStop( vLevel, Entry, k, Vec_IntSize(vLevel)-1 )
{
if ( Entry < 0 ) // input
Vec_IntPush( vTempM[0], Vec_IntEntry(vLeaves, -1-Entry) );
else // output
{
assert( OutLit == -1 ); // only one output literal is expected
OutLit = Vec_IntEntry(vRootLits, Entry);
}
}
if ( OutLit == -1 )
nMonos += Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC[0], vTempM[0] ); // mono without out
else if ( !Abc_LitIsCompl(OutLit) ) // positive literal
{
Vec_IntPush( vTempM[0], Abc_Lit2Var(OutLit) );
nMonos += Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC[0], vTempM[0] ); // mono with pos out
}
else // negative literal
{
// first monomial
nMonos += Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC[0], vTempM[0] ); // mono without out
// second monomial
Vec_IntFill( vTempC[0], 1, -Vec_IntEntryLast(vLevel) );
Vec_IntPush( vTempM[0], Abc_Lit2Var(OutLit) );
nMonos += Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC[0], vTempM[0] ); // mono with neg out
}
nBuilds++;
}
}
else
Vec_IntForEachEntry( vRootLits, iLit, i )
{
int Value = 1 + Abc_MinInt( i, Vec_IntSize(vRootLits)-nExtra );
@ -601,15 +801,24 @@ Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Int_t * vRootLits, int nExt
SeeAlso []
***********************************************************************/
void Gia_PolynBuild2Test( Gia_Man_t * pGia, int nExtra, int fSigned, int fVerbose, int fVeryVerbose )
void Gia_PolynBuild2Test( Gia_Man_t * pGia, char * pSign, int nExtra, int fSigned, int fVerbose, int fVeryVerbose )
{
Vec_Wec_t * vPolyn;
Vec_Int_t * vRootLits = Vec_IntAlloc( Gia_ManCoNum(pGia) );
Vec_Int_t * vLeaves = Vec_IntAlloc( Gia_ManCiNum(pGia) );
Vec_Int_t * vNodes = Vec_IntAlloc( Gia_ManAndNum(pGia) );
Gia_Obj_t * pObj;
Vec_Wec_t * vMonos = NULL;
int i;
if ( pSign != NULL && (vMonos = Acec_ParseSignature(pSign)) == NULL )
{
printf( "Canont parse the output signatures.\n" );
return;
}
if ( vMonos && fVerbose )
Acec_PrintSignature( vMonos );
// print logic level
if ( nExtra == -1 )
{
@ -633,7 +842,7 @@ void Gia_PolynBuild2Test( Gia_Man_t * pGia, int nExtra, int fSigned, int fVerbos
else if ( Gia_ObjIsCo(pObj) )
Vec_IntPush( vRootLits, Gia_ObjFaninLit0p(pGia, pObj) );
vPolyn = Gia_PolynBuildNew( pGia, vRootLits, nExtra, vLeaves, vNodes, fSigned, fVerbose, fVeryVerbose );
vPolyn = Gia_PolynBuildNew( pGia, vMonos, vRootLits, nExtra, vLeaves, vNodes, fSigned, fVerbose, fVeryVerbose );
//printf( "Polynomial has %d monomials.\n", Vec_WecSize(vPolyn)/2 );
if ( fVerbose || fVeryVerbose )
Gia_PolynPrintStats( vPolyn );
@ -644,6 +853,7 @@ void Gia_PolynBuild2Test( Gia_Man_t * pGia, int nExtra, int fSigned, int fVerbos
Vec_IntFree( vRootLits );
Vec_IntFree( vLeaves );
Vec_IntFree( vNodes );
Vec_WecFreeP( &vMonos );
}
////////////////////////////////////////////////////////////////////////