From 01d736cba40f0bc12139fed73679c92b1f6bb383 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 13 Jun 2018 19:34:52 -0700 Subject: Enabling user-specified output signature in &polyn. --- src/proof/acec/acecPo.c | 224 ++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 217 insertions(+), 7 deletions(-) (limited to 'src/proof/acec/acecPo.c') diff --git a/src/proof/acec/acecPo.c b/src/proof/acec/acecPo.c index c975e375..79992fb2 100644 --- a/src/proof/acec/acecPo.c +++ b/src/proof/acec/acecPo.c @@ -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 ); } //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3