From 40375f8b93edcd51f17e55a03737791f4202c5e7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 9 Oct 2016 19:38:30 -0700 Subject: Updates to arithmetic verification. --- src/base/abci/abc.c | 82 ++++++++++++++++++++--------- src/proof/acec/acecCo.c | 66 +++++++++++++++++------ src/proof/acec/acecPo.c | 136 ++++++++++++++++++++++++++++++++++++++++-------- 3 files changed, 220 insertions(+), 64 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dacdde7d..372e1eb4 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -475,8 +475,8 @@ static int Abc_CommandAbc9Bmci ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9PoXsim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Demiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Fadds ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandAbc9Polyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9ATree ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Polyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Acec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Esop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1116,8 +1116,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&poxsim", Abc_CommandAbc9PoXsim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&demiter", Abc_CommandAbc9Demiter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&fadds", Abc_CommandAbc9Fadds, 0 ); - Cmd_CommandAdd( pAbc, "ABC9", "&polyn", Abc_CommandAbc9Polyn, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&atree", Abc_CommandAbc9ATree, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&polyn", Abc_CommandAbc9Polyn, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&acec", Abc_CommandAbc9Acec, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&esop", Abc_CommandAbc9Esop, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&exorcism", Abc_CommandAbc9Exorcism, 0 ); @@ -40183,20 +40183,21 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandAbc9ATree( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Vec_Int_t * vOrder = NULL; - int c, fSimple = 1, fSigned = 0, fVerbose = 0, fVeryVerbose = 0; + extern Gia_Man_t * Gia_PolynCoreDetectTest( Gia_Man_t * pGia, int fAddExtra, int fAddCones, int fVerbose ); + Gia_Man_t * pTemp = NULL; + int c, fAddExtra = 0, fAddCones = 0, fVerbose = 0, fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "asvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ecvwh" ) ) != EOF ) { switch ( c ) { - case 'a': - fSimple ^= 1; + case 'e': + fAddExtra ^= 1; break; - case 's': - fSigned ^= 1; + case 'c': + fAddCones ^= 1; break; case 'v': fVerbose ^= 1; @@ -40215,16 +40216,15 @@ int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Esop(): There is no AIG.\n" ); return 0; } - vOrder = fSimple ? NULL : Gia_PolynReorder( pAbc->pGia, fVerbose, fVeryVerbose ); - Gia_PolynBuild( pAbc->pGia, vOrder, fSigned, fVerbose, fVeryVerbose ); - Vec_IntFreeP( &vOrder ); + pTemp = Gia_PolynCoreDetectTest( pAbc->pGia, fAddExtra, fAddCones, fVerbose ); + Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &polyn [-asvwh]\n" ); - Abc_Print( -2, "\t derives algebraic polynomial from AIG\n" ); - Abc_Print( -2, "\t-a : toggles simple computation [default = %s]\n", fSimple? "yes": "no" ); - Abc_Print( -2, "\t-s : toggles signed computation [default = %s]\n", fSigned? "yes": "no" ); + Abc_Print( -2, "usage: &atree [-ecvwh]\n" ); + Abc_Print( -2, "\t extracts adder tree rooting in primary outputs\n" ); + Abc_Print( -2, "\t-e : toggles adding extra outputs [default = %s]\n", fAddExtra? "yes": "no" ); + Abc_Print( -2, "\t-c : toggles duplicating complete AIG [default = %s]\n", fAddCones? "yes": "no" ); 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"); @@ -40242,16 +40242,36 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandAbc9ATree( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_PolynCoreDetectTest( Gia_Man_t * pGia ); - Gia_Man_t * pTemp = NULL; - int c, fVerbose = 0, fVeryVerbose = 0; + 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; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Noasvwh" ) ) != EOF ) { switch ( c ) { + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nExtra = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nExtra < 0 ) + goto usage; + break; + case 'o': + fOld ^= 1; + break; + case 'a': + fSimple ^= 1; + break; + case 's': + fSigned ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -40269,13 +40289,23 @@ int Abc_CommandAbc9ATree( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Esop(): There is no AIG.\n" ); return 0; } - pTemp = Gia_PolynCoreDetectTest( pAbc->pGia ); - Abc_FrameUpdateGia( pAbc, pTemp ); + if ( fOld ) + { + vOrder = fSimple ? NULL : Gia_PolynReorder( pAbc->pGia, fVerbose, fVeryVerbose ); + Gia_PolynBuild( pAbc->pGia, vOrder, fSigned, fVerbose, fVeryVerbose ); + Vec_IntFreeP( &vOrder ); + } + else + Gia_PolynBuild2Test( pAbc->pGia, nExtra, fSigned, fVerbose, fVeryVerbose ); return 0; usage: - Abc_Print( -2, "usage: &atree [-vwh]\n" ); - Abc_Print( -2, "\t extracts adder tree rooting in primary outputs\n" ); + Abc_Print( -2, "usage: &polyn [-N num] [-oasvwh]\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" ); + Abc_Print( -2, "\t-a : toggles simple computation [default = %s]\n", fSimple? "yes": "no" ); + Abc_Print( -2, "\t-s : toggles signed computation [default = %s]\n", fSigned? "yes": "no" ); 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"); diff --git a/src/proof/acec/acecCo.c b/src/proof/acec/acecCo.c index 14eecc9c..000f530a 100644 --- a/src/proof/acec/acecCo.c +++ b/src/proof/acec/acecCo.c @@ -70,7 +70,8 @@ Vec_Int_t * Gia_PolynAddHaRoots( Gia_Man_t * pGia ) Vec_IntPush( vNewOuts, Abc_Lit2Var(iRoot) ); } Vec_IntFree( vXorPairs ); - printf( "On top of %d COs, created %d new adder outputs.\n", Gia_ManCoNum(pGia), Vec_IntSize(vNewOuts) ); + Vec_IntReverseOrder( vNewOuts ); +// Vec_IntPop( vNewOuts ); return vNewOuts; } @@ -220,15 +221,28 @@ Vec_Int_t * Gia_PolynCoreCollect( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t SeeAlso [] ***********************************************************************/ -void Gia_PolynCorePrintCones( Gia_Man_t * pGia, Vec_Int_t * vLeaves ) +void Gia_PolynCorePrintCones( Gia_Man_t * pGia, Vec_Int_t * vLeaves, int fVerbose ) { int i, iObj; - Vec_IntForEachEntry( vLeaves, iObj, i ) + if ( fVerbose ) { - printf( "%4d : ", i ); - printf( "Supp = %3d ", Gia_ManSuppSize(pGia, &iObj, 1) ); - printf( "Cone = %3d ", Gia_ManConeSize(pGia, &iObj, 1) ); - printf( "\n" ); + Vec_IntForEachEntry( vLeaves, iObj, i ) + { + printf( "%4d : ", i ); + printf( "Supp = %3d ", Gia_ManSuppSize(pGia, &iObj, 1) ); + printf( "Cone = %3d ", Gia_ManConeSize(pGia, &iObj, 1) ); + printf( "\n" ); + } + } + else + { + int SuppMax = 0, ConeMax = 0; + Vec_IntForEachEntry( vLeaves, iObj, i ) + { + SuppMax = Abc_MaxInt( SuppMax, Gia_ManSuppSize(pGia, &iObj, 1) ); + ConeMax = Abc_MaxInt( ConeMax, Gia_ManConeSize(pGia, &iObj, 1) ); + } + printf( "Remaining cones: Count = %d. SuppMax = %d. ConeMax = %d.\n", Vec_IntSize(vLeaves), SuppMax, ConeMax ); } } @@ -243,7 +257,16 @@ void Gia_PolynCorePrintCones( Gia_Man_t * pGia, Vec_Int_t * vLeaves ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_PolynCoreDupTree( Gia_Man_t * p, Vec_Int_t * vAddCos, Vec_Int_t * vLeaves, Vec_Int_t * vNodes ) +int Gia_PolynCoreDupTreePlus_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return pObj->Value; + assert( Gia_ObjIsAnd(pObj) ); + Gia_PolynCoreDupTreePlus_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_PolynCoreDupTreePlus_rec( pNew, p, Gia_ObjFanin1(pObj) ); + return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} +Gia_Man_t * Gia_PolynCoreDupTree( Gia_Man_t * p, Vec_Int_t * vAddCos, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, int fAddCones ) { Gia_Man_t * pNew; Gia_Obj_t * pObj; @@ -254,8 +277,18 @@ Gia_Man_t * Gia_PolynCoreDupTree( Gia_Man_t * p, Vec_Int_t * vAddCos, Vec_Int_t pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pSpec = Abc_UtilStrsav( p->pSpec ); Gia_ManConst0(p)->Value = 0; - Gia_ManForEachObjVec( vLeaves, p, pObj, i ) - pObj->Value = Gia_ManAppendCi(pNew); + if ( fAddCones ) + { + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachObjVec( vLeaves, p, pObj, i ) + pObj->Value = Gia_PolynCoreDupTreePlus_rec( pNew, p, pObj ); + } + else + { + Gia_ManForEachObjVec( vLeaves, p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + } Gia_ManForEachObjVec( vNodes, p, pObj, i ) pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); Gia_ManForEachCo( p, pObj, i ) @@ -277,7 +310,7 @@ Gia_Man_t * Gia_PolynCoreDupTree( Gia_Man_t * p, Vec_Int_t * vAddCos, Vec_Int_t SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos ) +Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos, int fAddCones, int fVerbose ) { extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose ); abctime clk = Abc_Clock(); @@ -289,9 +322,9 @@ Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos ) Vec_IntSize(vAdds), Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); - Gia_PolynCorePrintCones( pGia, vLeaves ); + Gia_PolynCorePrintCones( pGia, vLeaves, fVerbose ); - pNew = Gia_PolynCoreDupTree( pGia, vAddCos, vLeaves, vNodes ); + pNew = Gia_PolynCoreDupTree( pGia, vAddCos, vLeaves, vNodes, fAddCones ); Vec_IntFree( vAdds ); Vec_IntFree( vLeaves ); @@ -300,10 +333,11 @@ Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos ) Vec_IntFree( vNodes ); return pNew; } -Gia_Man_t * Gia_PolynCoreDetectTest( Gia_Man_t * pGia ) +Gia_Man_t * Gia_PolynCoreDetectTest( Gia_Man_t * pGia, int fAddExtra, int fAddCones, int fVerbose ) { - Vec_Int_t * vAddCos = Gia_PolynAddHaRoots( pGia ); - Gia_Man_t * pNew = Gia_PolynCoreDetectTest_int( pGia, vAddCos ); + Vec_Int_t * vAddCos = fAddExtra ? Gia_PolynAddHaRoots( pGia ) : Vec_IntAlloc(0); + Gia_Man_t * pNew = Gia_PolynCoreDetectTest_int( pGia, vAddCos, fAddCones, fVerbose ); + printf( "On top of %d COs, created %d new adder outputs.\n", Gia_ManCoNum(pGia), Vec_IntSize(vAddCos) ); Vec_IntFree( vAddCos ); return pNew; } diff --git a/src/proof/acec/acecPo.c b/src/proof/acec/acecPo.c index 1e77ab20..c975e375 100644 --- a/src/proof/acec/acecPo.c +++ b/src/proof/acec/acecPo.c @@ -32,6 +32,57 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Checks that items are unique and in order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_IntPushOrderAbs( Vec_Int_t * p, int Entry ) +{ + int i; + for ( i = 0; i < p->nSize; i++ ) + assert( Entry != p->pArray[i] ); + if ( p->nSize == p->nCap ) + { + if ( p->nCap < 16 ) + Vec_IntGrow( p, 16 ); + else + Vec_IntGrow( p, 2 * p->nCap ); + } + p->nSize++; + for ( i = p->nSize-2; i >= 0; i-- ) + if ( Abc_AbsInt(p->pArray[i]) < Abc_AbsInt(Entry) ) + p->pArray[i+1] = p->pArray[i]; + else + break; + p->pArray[i+1] = Entry; +} +static inline void Vec_IntAppendMinusAbs( Vec_Int_t * vVec1, Vec_Int_t * vVec2, int fMinus ) +{ + int Entry, i; + Vec_IntClear( vVec1 ); + Vec_IntForEachEntry( vVec2, Entry, i ) + Vec_IntPushOrderAbs( vVec1, fMinus ? -Entry : Entry ); +} +static inline void Vec_IntCheckUniqueOrderAbs( Vec_Int_t * p ) +{ + int i; + for ( i = 1; i < p->nSize; i++ ) + assert( Abc_AbsInt(p->pArray[i-1]) > Abc_AbsInt(p->pArray[i]) ); +} +static inline void Vec_IntCheckUniqueOrder( Vec_Int_t * p ) +{ + int i; + for ( i = 1; i < p->nSize; i++ ) + assert( p->pArray[i-1] < p->pArray[i] ); +} + /**Function************************************************************* Synopsis [Prints polynomial.] @@ -43,24 +94,27 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -void Gia_PolynPrintMono( Vec_Int_t * vConst, Vec_Int_t * vMono ) +void Gia_PolynPrintMono( Vec_Int_t * vConst, Vec_Int_t * vMono, int Prev ) { int k, Entry; + printf( "%c ", Prev != Abc_AbsInt(Vec_IntEntry(vConst, 0)) ? '|' : ' ' ); Vec_IntForEachEntry( vConst, Entry, k ) printf( "%s2^%d", Entry < 0 ? "-" : "+", Abc_AbsInt(Entry)-1 ); Vec_IntForEachEntry( vMono, Entry, k ) - printf( " * %d", Entry ); + printf( " * %d", Entry-1 ); printf( "\n" ); } void Gia_PolynPrint( Vec_Wec_t * vPolyn ) { - Vec_Int_t * vConst, * vMono; int i; + Vec_Int_t * vConst, * vMono; + int i, Prev = -1; printf( "Polynomial with %d monomials:\n", Vec_WecSize(vPolyn)/2 ); for ( i = 0; i < Vec_WecSize(vPolyn)/2; i++ ) { vConst = Vec_WecEntry( vPolyn, 2*i+0 ); vMono = Vec_WecEntry( vPolyn, 2*i+1 ); - Gia_PolynPrintMono( vConst, vMono ); + Gia_PolynPrintMono( vConst, vMono, Prev ); + Prev = Abc_AbsInt( Vec_IntEntry(vConst, 0) ); } } void Gia_PolynPrintStats( Vec_Wec_t * vPolyn ) @@ -106,11 +160,17 @@ void Gia_PolynPrintStats( Vec_Wec_t * vPolyn ) SeeAlso [] ***********************************************************************/ +int Gia_PolynGetResultCompare( int * p0, int * p1 ) +{ + if ( p0[2] < p1[2] ) return -1; + if ( p0[2] > p1[2] ) return 1; + return 0; +} Vec_Wec_t * Gia_PolynGetResult( Hsh_VecMan_t * pHashC, Hsh_VecMan_t * pHashM, Vec_Int_t * vCoefs ) { Vec_Int_t * vClass, * vLevel, * vArray; Vec_Wec_t * vPolyn, * vSorted; - int i, k, iConst, iMono; + int i, k, iConst, iMono, iFirst; // find the largest int nLargest = 0, nNonConst = 0; Vec_IntForEachEntry( vCoefs, iConst, iMono ) @@ -130,20 +190,26 @@ Vec_Wec_t * Gia_PolynGetResult( Hsh_VecMan_t * pHashC, Hsh_VecMan_t * pHashM, Ve continue; vArray = Hsh_VecReadEntry( pHashC, iConst ); vLevel = Vec_WecEntry( vSorted, Abc_AbsInt(Vec_IntEntry(vArray, 0)) ); - Vec_IntPushTwo( vLevel, iConst, iMono ); + vArray = Hsh_VecReadEntry( pHashM, iMono ); + iFirst = Vec_IntSize(vArray) ? Vec_IntEntry(vArray, 0) : -1; + Vec_IntPushThree( vLevel, iConst, iMono, iFirst ); } // reload in the given order vPolyn = Vec_WecAlloc( 2*nNonConst ); Vec_WecForEachLevel( vSorted, vClass, i ) { - Vec_IntForEachEntryDouble( vClass, iConst, iMono, k ) + // sort monomials by the index of the first variable + qsort( Vec_IntArray(vClass), Vec_IntSize(vClass)/3, 12, (int (*)(const void *, const void *))Gia_PolynGetResultCompare ); + Vec_IntForEachEntryTriple( vClass, iConst, iMono, iFirst, k ) { vArray = Hsh_VecReadEntry( pHashC, iConst ); + Vec_IntCheckUniqueOrderAbs( vArray ); vLevel = Vec_WecPushLevel( vPolyn ); Vec_IntGrow( vLevel, Vec_IntSize(vArray) ); Vec_IntAppend( vLevel, vArray ); vArray = Hsh_VecReadEntry( pHashM, iMono ); + Vec_IntCheckUniqueOrder( vArray ); vLevel = Vec_WecPushLevel( vPolyn ); Vec_IntGrow( vLevel, Vec_IntSize(vArray) ); Vec_IntAppend( vLevel, vArray ); @@ -192,7 +258,7 @@ static inline void Gia_PolynMergeConstOne( Vec_Int_t * vConst, int New ) return; } } - Vec_IntPushUniqueOrder( vConst, New ); + Vec_IntPushOrderAbs( vConst, New ); } static inline void Gia_PolynMergeConst( Vec_Int_t * vTempC, Hsh_VecMan_t * pHashC, int iConstAdd ) { @@ -203,6 +269,8 @@ static inline void Gia_PolynMergeConst( Vec_Int_t * vTempC, Hsh_VecMan_t * pHash Gia_PolynMergeConstOne( vTempC, New ); vConstAdd = Hsh_VecReadEntry( pHashC, iConstAdd ); } + Vec_IntCheckUniqueOrderAbs( vConstAdd ); + //Vec_IntPrint( vConstAdd ); } static inline int Gia_PolynBuildAdd( Hsh_VecMan_t * pHashC, Hsh_VecMan_t * pHashM, Vec_Int_t * vCoefs, Vec_Wec_t * vLit2Mono, Vec_Int_t * vTempC, Vec_Int_t * vTempM ) @@ -263,15 +331,15 @@ static inline int Gia_PolynHandleOne( Hsh_VecMan_t * pHashC, Hsh_VecMan_t * pHas assert( status ); // create new monomial if ( iLitNew0 == -1 && iLitNew1 == -1 ) // no new lit - the same const - Vec_IntAppendMinus( vTempC, vArrayC, 0 ); + Vec_IntAppendMinusAbs( vTempC, vArrayC, 0 ); else if ( iLitNew0 > -1 && iLitNew1 == -1 ) // one new lit - opposite const { - Vec_IntAppendMinus( vTempC, vArrayC, 1 ); + Vec_IntAppendMinusAbs( vTempC, vArrayC, 1 ); Vec_IntPushUniqueOrder( vTempM, iLitNew0 ); } else if ( iLitNew0 > -1 && iLitNew1 > -1 ) // both new lit - the same const { - Vec_IntAppendMinus( vTempC, vArrayC, 0 ); + Vec_IntAppendMinusAbs( vTempC, vArrayC, 0 ); Vec_IntPushUniqueOrder( vTempM, iLitNew0 ); Vec_IntPushUniqueOrder( vTempM, iLitNew1 ); } @@ -279,7 +347,7 @@ static inline int Gia_PolynHandleOne( Hsh_VecMan_t * pHashC, Hsh_VecMan_t * pHas return Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC, vTempM ); } -Vec_Wec_t * Gia_PolynBuildNew2( Gia_Man_t * pGia, Vec_Int_t * vRootLits, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, int fSigned, int fVerbose, int fVeryVerbose ) +Vec_Wec_t * Gia_PolynBuildNew2( Gia_Man_t * pGia, 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; @@ -299,7 +367,8 @@ Vec_Wec_t * Gia_PolynBuildNew2( Gia_Man_t * pGia, Vec_Int_t * vRootLits, Vec_Int // create output signature Vec_IntForEachEntry( vRootLits, iLit, i ) { - Vec_IntFill( vTempC, 1, (fSigned && i == Vec_IntSize(vRootLits)-1) ? -i-1 : i+1 ); + int Value = 1 + Abc_MinInt( i, Vec_IntSize(vRootLits)-nExtra ); + Vec_IntFill( vTempC, 1, (fSigned && i == Vec_IntSize(vRootLits)-1-nExtra) ? -Value : Value ); Vec_IntFill( vTempM, 1, iLit ); nMonos += Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC, vTempM ); nBuilds++; @@ -392,7 +461,7 @@ static inline void Gia_PolynPrepare4( Vec_Int_t * vTempC[4], Vec_Int_t * vTempM[ { int i, k, Entry; for ( i = 0; i < 4; i++ ) - Vec_IntAppendMinus( vTempC[i], vConst, i & 1 ); + Vec_IntAppendMinusAbs( vTempC[i], vConst, i & 1 ); for ( i = 0; i < 4; i++ ) Vec_IntClear( vTempM[i] ); Vec_IntForEachEntry( vMono, Entry, k ) @@ -405,7 +474,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, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, int fSigned, int fVerbose, int fVeryVerbose ) +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 ) { abctime clk = Abc_Clock(); Vec_Wec_t * vPolyn; @@ -425,12 +494,17 @@ Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Int_t * vRootLits, Vec_Int_ Hsh_VecManAdd( pHashM, vTempM[0] ); Vec_IntPush( vCoefs, 0 ); + if ( nExtra ) + 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 Vec_IntForEachEntry( vRootLits, iLit, i ) { - Gia_PolynPrepare2( vTempC, vTempM, Abc_Lit2Var(iLit), i+1 ); - if ( fSigned && i == Vec_IntSize(vRootLits)-1 ) + int Value = 1 + Abc_MinInt( i, Vec_IntSize(vRootLits)-nExtra ); + Gia_PolynPrepare2( vTempC, vTempM, Abc_Lit2Var(iLit), Value ); + if ( fSigned && i >= Vec_IntSize(vRootLits)-nExtra-1 ) { + if ( fVeryVerbose ) printf( "Out %d : Negative Value = %d\n", i, Value-1 ); if ( Abc_LitIsCompl(iLit) ) { nMonos += Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC[1], vTempM[0] ); // -C @@ -442,6 +516,7 @@ Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Int_t * vRootLits, Vec_Int_ } else { + if ( fVeryVerbose ) printf( "Out %d : Positive Value = %d\n", i, Value-1 ); if ( Abc_LitIsCompl(iLit) ) { nMonos += Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC[0], vTempM[0] ); // C @@ -526,7 +601,7 @@ Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Int_t * vRootLits, Vec_Int_ SeeAlso [] ***********************************************************************/ -void Gia_PolynBuild2Test( Gia_Man_t * pGia ) +void Gia_PolynBuild2Test( Gia_Man_t * pGia, int nExtra, int fSigned, int fVerbose, int fVeryVerbose ) { Vec_Wec_t * vPolyn; Vec_Int_t * vRootLits = Vec_IntAlloc( Gia_ManCoNum(pGia) ); @@ -535,6 +610,21 @@ void Gia_PolynBuild2Test( Gia_Man_t * pGia ) Gia_Obj_t * pObj; int i; + // print logic level + if ( nExtra == -1 ) + { + int LevelMax = -1, iMax = -1; + Gia_ManLevelNum( pGia ); + Gia_ManForEachCo( pGia, pObj, i ) + if ( LevelMax < Gia_ObjLevel(pGia, pObj) ) + { + LevelMax = Gia_ObjLevel(pGia, pObj); + iMax = i; + } + nExtra = Gia_ManCoNum(pGia) - iMax - 1; + printf( "Determined the number of extra outputs to be %d.\n", nExtra ); + } + Gia_ManForEachObj( pGia, pObj, i ) if ( Gia_ObjIsCi(pObj) ) Vec_IntPush( vLeaves, i ); @@ -543,10 +633,12 @@ void Gia_PolynBuild2Test( Gia_Man_t * pGia ) else if ( Gia_ObjIsCo(pObj) ) Vec_IntPush( vRootLits, Gia_ObjFaninLit0p(pGia, pObj) ); - vPolyn = Gia_PolynBuildNew( pGia, vRootLits, vLeaves, vNodes, 0, 0, 0 ); -// printf( "Polynomial has %d monomials.\n", Vec_WecSize(vPolyn)/2 ); -// Gia_PolynPrintStats( vPolyn ); -// Gia_PolynPrint( vPolyn ); + vPolyn = Gia_PolynBuildNew( pGia, vRootLits, nExtra, vLeaves, vNodes, fSigned, fVerbose, fVeryVerbose ); + //printf( "Polynomial has %d monomials.\n", Vec_WecSize(vPolyn)/2 ); + if ( fVerbose || fVeryVerbose ) + Gia_PolynPrintStats( vPolyn ); + if ( fVeryVerbose ) + Gia_PolynPrint( vPolyn ); Vec_WecFree( vPolyn ); Vec_IntFree( vRootLits ); -- cgit v1.2.3