From 6e8efec57d5ef07ca33a3cefc3c1e6c3f7c70856 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 11 May 2016 11:07:34 -0700 Subject: Experiments with CEC for arithmetic circuits. --- src/aig/gia/gia.h | 1 + src/aig/gia/giaDup.c | 7 ++- src/aig/gia/giaMan.c | 1 + src/aig/gia/giaShow.c | 2 +- src/base/abci/abc.c | 16 +++--- src/proof/acec/acec.h | 2 +- src/proof/acec/acecCore.c | 4 +- src/proof/acec/acecInt.h | 1 + src/proof/acec/acecOrder.c | 64 +++++++++++++++++----- src/proof/acec/acecPolyn.c | 129 ++++++++++++++++++++++++++++----------------- src/proof/acec/acecUtil.c | 16 +++++- 11 files changed, 169 insertions(+), 74 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index ab6870d8..1877821a 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -156,6 +156,7 @@ struct Gia_Man_t_ Vec_Int_t * vRegInits; // initial state Vec_Int_t * vDoms; // dominators Vec_Int_t * vBarBufs; // barrier buffers + Vec_Int_t * vXors; // temporary XORs unsigned char* pSwitching; // switching activity for each object Gia_Plc_t * pPlacement; // placement of the objects Gia_Man_t * pAigExtra; // combinational logic of holes diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index a01c93fd..dbfe38f3 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -2995,7 +2995,12 @@ Gia_Man_t * Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrim // Gia_ObjRiToRo(p, pObj)->Value = Gia_ManAppendCi( pNew ); // create internal nodes Vec_PtrForEachEntry( Gia_Obj_t *, vNodes, pObj, i ) - pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( Gia_ObjIsMux(p, pObj) ) + pObj->Value = Gia_ManAppendMux( pNew, Gia_ObjFanin2Copy(p, pObj), Gia_ObjFanin1Copy(pObj), Gia_ObjFanin0Copy(pObj) ); + else if ( Gia_ObjIsXor(pObj) ) + pObj->Value = Gia_ManAppendXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); // create COs Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pObj, i ) // Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 27dff3ad..d9e878a7 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -109,6 +109,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vRegInits ); Vec_IntFreeP( &p->vDoms ); Vec_IntFreeP( &p->vBarBufs ); + Vec_IntFreeP( &p->vXors ); Vec_IntFreeP( &p->vLevels ); Vec_IntFreeP( &p->vTruths ); Vec_IntErase( &p->vCopies ); diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c index 91edbaa5..9d585d6d 100644 --- a/src/aig/gia/giaShow.c +++ b/src/aig/gia/giaShow.c @@ -156,7 +156,7 @@ int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds, Vec_IntWriteEntry( vRemap, pFanins[0], pFanins[1] ); //printf( "Making HA output %d.\n", pFanins[1] ); } - else + else // if ( Attr == 3 || Attr == 0 ) { Gia_Obj_t * pObj = Gia_ManObj( p, Node ); int pFaninsIn[2] = { Gia_ObjFaninId0(pObj, Node), Gia_ObjFaninId1(pObj, Node) }; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 11d61c14..5abc941b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -39306,15 +39306,18 @@ usage: int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv ) { Vec_Int_t * vOrder = NULL; - int c, fSimple = 0, fVerbose = 0, fVeryVerbose = 0; + int c, fSimple = 0, fSigned = 0, fVerbose = 0, fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "svwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "asvwh" ) ) != EOF ) { switch ( c ) { - case 's': + case 'a': fSimple ^= 1; break; + case 's': + fSigned ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -39333,14 +39336,15 @@ int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } vOrder = fSimple ? NULL : Gia_PolynReorder( pAbc->pGia, fVerbose, fVeryVerbose ); - Gia_PolynBuild( pAbc->pGia, vOrder, fVerbose, fVeryVerbose ); + Gia_PolynBuild( pAbc->pGia, vOrder, fSigned, fVerbose, fVeryVerbose ); Vec_IntFreeP( &vOrder ); return 0; usage: - Abc_Print( -2, "usage: &polyn [-svwh]\n" ); + Abc_Print( -2, "usage: &polyn [-asvwh]\n" ); Abc_Print( -2, "\t derives algebraic polynomial from AIG\n" ); - Abc_Print( -2, "\t-s : toggles simple computation [default = %s]\n", fSimple? "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/acec.h b/src/proof/acec/acec.h index fd7814d8..f39041c8 100644 --- a/src/proof/acec/acec.h +++ b/src/proof/acec/acec.h @@ -59,7 +59,7 @@ extern Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose ); extern Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose ); extern Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int fVerbose, int fVeryVerbose ); /*=== acecPolyn.c ========================================================*/ -extern void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose, int fVeryVerbose ); +extern void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fSigned, int fVerbose, int fVeryVerbose ); ABC_NAMESPACE_HEADER_END diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c index 991067d8..ac7ee67b 100644 --- a/src/proof/acec/acecCore.c +++ b/src/proof/acec/acecCore.c @@ -46,8 +46,8 @@ int Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars ) { Vec_Int_t * vOrder0 = Gia_PolynReorder( pGia0, pPars->fVerbose, pPars->fVeryVerbose ); Vec_Int_t * vOrder1 = Gia_PolynReorder( pGia1, pPars->fVerbose, pPars->fVeryVerbose ); - Gia_PolynBuild( pGia0, vOrder0, pPars->fVerbose, pPars->fVeryVerbose ); - Gia_PolynBuild( pGia1, vOrder1, pPars->fVerbose, pPars->fVeryVerbose ); + Gia_PolynBuild( pGia0, vOrder0, 0, pPars->fVerbose, pPars->fVeryVerbose ); + Gia_PolynBuild( pGia1, vOrder1, 0, pPars->fVerbose, pPars->fVeryVerbose ); Vec_IntFree( vOrder0 ); Vec_IntFree( vOrder1 ); return 1; diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h index 7f70658e..e761e56e 100644 --- a/src/proof/acec/acecInt.h +++ b/src/proof/acec/acecInt.h @@ -56,6 +56,7 @@ ABC_NAMESPACE_HEADER_START /*=== acecUtil.c ========================================================*/ extern void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose ); +extern Vec_Int_t * Gia_PolynCollectLastXor( Gia_Man_t * pGia, int fVerbose ); ABC_NAMESPACE_HEADER_END diff --git a/src/proof/acec/acecOrder.c b/src/proof/acec/acecOrder.c index fbce0835..9b2242d0 100644 --- a/src/proof/acec/acecOrder.c +++ b/src/proof/acec/acecOrder.c @@ -44,20 +44,41 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int fVerbose, int fVeryVerbose ) { + int fDumpLeftOver = 0; int i, iXor, iMaj, iAnd, Entry, Iter, fFound, fFoundAll = 1; - Vec_Int_t * vRecord = Vec_IntAlloc( 100 ); + Vec_Int_t * vRecord = Vec_IntAlloc( 100 ), * vLeft, * vRecord2; Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(pGia) ); Gia_ManForEachCoDriverId( pGia, iAnd, i ) Vec_IntWriteEntry( vMap, iAnd, 1 ); + + // collect the last XOR + Vec_IntFreeP( &pGia->vXors ); + pGia->vXors = Gia_PolynCollectLastXor( pGia, fVerbose ); + printf( "Collected %d topmost XORs\n", Vec_IntSize(pGia->vXors) ); + //Vec_IntPrint( p->vXors ); + Vec_IntForEachEntry( pGia->vXors, iAnd, i ) + { + Gia_Obj_t * pAnd = Gia_ManObj( pGia, iAnd ); + assert( Vec_IntEntry(vMap, iAnd) ); + Vec_IntWriteEntry( vMap, iAnd, 0 ); + Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iAnd), 1 ); + Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iAnd), 1 ); + Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 3) ); + if ( fVeryVerbose ) + printf( "Recognizing %d => XXXOR(%d %d)\n", iAnd, Gia_ObjFaninId0(pAnd, iAnd), Gia_ObjFaninId1(pAnd, iAnd) ); + } + + // detect FAs and HAs for ( Iter = 0; fFoundAll; Iter++ ) { if ( fVeryVerbose ) printf( "Iteration %d\n", Iter ); + // check if we can extract FADDs fFoundAll = 0; do { fFound = 0; - for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ ) + for ( i = Vec_IntSize(vFadds)/5 - 1; i >= 0; i-- ) { iXor = Vec_IntEntry(vFadds, 5*i+3); iMaj = Vec_IntEntry(vFadds, 5*i+4); @@ -68,8 +89,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+0), 1 ); Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+1), 1 ); Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+2), 1 ); - //Vec_IntPush( vRecord, iXor ); - //Vec_IntPush( vRecord, iMaj ); Vec_IntPush( vRecord, Abc_Var2Lit2(i, 2) ); fFound = 1; fFoundAll = 1; @@ -81,7 +100,7 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t // check if we can extract HADDs do { fFound = 0; - for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ ) + for ( i = Vec_IntSize(vHadds)/2 - 1; i >= 0; i-- ) { iXor = Vec_IntEntry(vHadds, 2*i+0); iMaj = Vec_IntEntry(vHadds, 2*i+1); @@ -92,8 +111,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t Vec_IntWriteEntry( vMap, iMaj, 0 ); Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iMaj), 1 ); Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iMaj), 1 ); - //Vec_IntPush( vRecord, iXor ); - //Vec_IntPush( vRecord, iMaj ); Vec_IntPush( vRecord, Abc_Var2Lit2(i, 1) ); fFound = 1; fFoundAll = 1; @@ -105,6 +122,7 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t } while ( fFound ); if ( fFoundAll ) continue; +/* // find the last one Vec_IntForEachEntryReverse( vMap, Entry, iAnd ) if ( Entry && Gia_ObjIsAnd(Gia_ManObj(pGia, iAnd)) )//&& Vec_IntFind(vFadds, iAnd) == -1 )//&& Vec_IntFind(vHadds, iAnd) == -1 ) @@ -115,7 +133,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t Vec_IntWriteEntry( vMap, iAnd, 0 ); Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iAnd), 1 ); Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iAnd), 1 ); - //Vec_IntPush( vRecord, iAnd ); Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 0) ); } else @@ -123,7 +140,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t Vec_IntWriteEntry( vMap, iAnd, 0 ); Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan0), 1 ); Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan1), 1 ); - //Vec_IntPush( vRecord, iAnd ); Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 0) ); Vec_IntPush( vRecord, Abc_Var2Lit2(Gia_ObjFaninId0(pAnd, iAnd), 0) ); Vec_IntPush( vRecord, Abc_Var2Lit2(Gia_ObjFaninId1(pAnd, iAnd), 0) ); @@ -134,21 +150,39 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t printf( "Recognizing %d => AND(%d %d)\n", iAnd, Gia_ObjFaninId0(pAnd, iAnd), Gia_ObjFaninId1(pAnd, iAnd) ); break; } +*/ } //Vec_IntPrint( vMap ); -/* + // collect remaining ones + vLeft = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vMap, Entry, i ) + if ( Entry && Gia_ObjIsAnd(Gia_ManObj(pGia, i)) ) + Vec_IntPush( vLeft, i ); + Vec_IntFree( vMap ); + + // collect them in the topo order + vRecord2 = Vec_IntAlloc( 100 ); + Gia_ManIncrementTravId( pGia ); + Gia_ManCollectAnds( pGia, Vec_IntArray(vLeft), Vec_IntSize(vLeft), vRecord2, NULL ); + Vec_IntForEachEntry( vRecord2, iAnd, i ) + Vec_IntWriteEntry( vRecord2, i, Abc_Var2Lit2(iAnd, 0) ); + // dump remaining nodes as an AIG if ( fDumpLeftOver ) { - Gia_Man_t * pNew = Gia_ManDupAndCones( pGia, Vec_IntArray(vMap), Vec_IntSize(vMap), 0 ); + Gia_Man_t * pNew; + pNew = Gia_ManDupAndCones( pGia, Vec_IntArray(vLeft), Vec_IntSize(vLeft), 0 ); Gia_AigerWrite( pNew, "leftover.aig", 0, 0 ); + printf( "Leftover AIG with %d nodes is dumped into file \"%s\".\n", Gia_ManAndNum(pNew), "leftover.aig" ); Gia_ManStop( pNew ); } -*/ - Vec_IntFree( vMap ); + Vec_IntFree( vLeft ); + Vec_IntReverseOrder( vRecord ); - return vRecord; + Vec_IntAppend( vRecord2, vRecord ); + Vec_IntFree( vRecord ); + return vRecord2; } /**Function************************************************************* @@ -191,7 +225,9 @@ Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose ) } else Gia_ManCollectAnds_rec( pGia, Node, vOrder ); + //printf( "Order = %d. Node = %d. Size = %d ", i, Node, Vec_IntSize(vOrder) ); } + //printf( "\n" ); //assert( Vec_IntSize(vOrder) == Gia_ManAndNum(pGia) ); // remap order diff --git a/src/proof/acec/acecPolyn.c b/src/proof/acec/acecPolyn.c index 5e20ef30..2f98df73 100644 --- a/src/proof/acec/acecPolyn.c +++ b/src/proof/acec/acecPolyn.c @@ -54,7 +54,8 @@ struct Pln_Man_t_ Vec_Int_t * vTempC[2]; // polynomial representation Vec_Int_t * vTempM[4]; // polynomial representation Vec_Int_t * vOrder; // order of collapsing - int nBuilds; // builds + int nBuilds; // built monomials + int nUsed; // used monomials }; //////////////////////////////////////////////////////////////////////// @@ -144,7 +145,10 @@ void Pln_ManPrintFinal( Pln_Man_t * p, int fVerbose, int fVeryVerbose ) Count++; - if ( !fVeryVerbose ) + if ( !fVerbose ) + continue; + + if ( Count > 25 ) continue; vArray = Hsh_VecReadEntry( p->pHashC, iConst ); @@ -159,6 +163,25 @@ void Pln_ManPrintFinal( Pln_Man_t * p, int fVerbose, int fVeryVerbose ) printf( "HashC = %d. HashM = %d. Total = %d. Used = %d.\n", Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, Count ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_IntAppendMinus2x( Vec_Int_t * vVec1, Vec_Int_t * vVec2 ) +{ + int Entry, i; + Vec_IntClear( vVec1 ); + Vec_IntForEachEntry( vVec2, Entry, i ) + Vec_IntPush( vVec1, Entry > 0 ? -Entry-1 : -Entry+1 ); +} + /**Function************************************************************* Synopsis [] @@ -210,7 +233,7 @@ static inline void Gia_PolynMergeConst( Vec_Int_t * vConst, Pln_Man_t * p, int i } static inline void Gia_PolynBuildAdd( Pln_Man_t * p, Vec_Int_t * vTempC, Vec_Int_t * vTempM ) { - int iConst, iMono = vTempM ? Hsh_VecManAdd(p->pHashM, vTempM) : 0; + int iConst, iConstNew, iMono = vTempM ? Hsh_VecManAdd(p->pHashM, vTempM) : 0; p->nBuilds++; if ( iMono == Vec_IntSize(p->vCoefs) ) // new monomial { @@ -220,14 +243,21 @@ static inline void Gia_PolynBuildAdd( Pln_Man_t * p, Vec_Int_t * vTempC, Vec_Int Vec_FltPush( p->vCounts, (float)Vec_IntEntry(p->vOrder, Vec_IntEntryLast(vTempM)) ); Vec_QuePush( p->vQue, iMono ); // Vec_QueUpdate( p->vQue, iMono ); + if ( iConst ) + p->nUsed++; return; } // this monomial exists iConst = Vec_IntEntry( p->vCoefs, iMono ); if ( iConst ) Gia_PolynMergeConst( vTempC, p, iConst ); - iConst = Hsh_VecManAdd( p->pHashC, vTempC ); - Vec_IntWriteEntry( p->vCoefs, iMono, iConst ); + iConstNew = Hsh_VecManAdd( p->pHashC, vTempC ); + Vec_IntWriteEntry( p->vCoefs, iMono, iConstNew ); + if ( iConst && !iConstNew ) + p->nUsed--; + else if ( !iConst && iConstNew ) + p->nUsed++; + //assert( p->nUsed == Vec_IntSize(p->vCoefs) - Vec_IntCountZero(p->vCoefs) ); } void Gia_PolynBuildOne( Pln_Man_t * p, int iMono ) { @@ -242,11 +272,13 @@ void Gia_PolynBuildOne( Pln_Man_t * p, int iMono ) pObj = Gia_ManObj( p->pGia, iDriver ); if ( !Gia_ObjIsAnd(pObj) ) return; + assert( !Gia_ObjIsMux(p->pGia, pObj) ); iConst = Vec_IntEntry( p->vCoefs, iMono ); if ( iConst == 0 ) return; Vec_IntWriteEntry( p->vCoefs, iMono, 0 ); + p->nUsed--; iFan0 = Gia_ObjFaninId0p(p->pGia, pObj); iFan1 = Gia_ObjFaninId1p(p->pGia, pObj); @@ -264,10 +296,29 @@ void Gia_PolynBuildOne( Pln_Man_t * p, int iMono ) } vConst = Hsh_VecReadEntry( p->pHashC, iConst ); - for ( k = 0; k < 2; k++ ) - Vec_IntAppendMinus( p->vTempC[k], vConst, k ); - if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) // C * (1 - x) * (1 - y) + if ( !Gia_ObjIsXor(pObj) ) + for ( k = 0; k < 2; k++ ) + Vec_IntAppendMinus( p->vTempC[k], vConst, k ); + + if ( Gia_ObjIsXor(pObj) ) + { + vConst = Hsh_VecReadEntry( p->pHashC, iConst ); + Vec_IntAppendMinus( p->vTempC[0], vConst, 0 ); + Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[1] ); // C * x + + vConst = Hsh_VecReadEntry( p->pHashC, iConst ); + Vec_IntAppendMinus( p->vTempC[0], vConst, 0 ); + Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[2] ); // C * y + + //if ( !p->pGia->vXors || Vec_IntFind(p->pGia->vXors, iDriver) > 0 ) + { + vConst = Hsh_VecReadEntry( p->pHashC, iConst ); + Vec_IntAppendMinus2x( p->vTempC[0], vConst ); + Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[3] ); // -C * x * y + } + } + else if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) // C * (1 - x) * (1 - y) { Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] ); // C * 1 Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[1] ); // -C * x @@ -290,36 +341,7 @@ void Gia_PolynBuildOne( Pln_Man_t * p, int iMono ) else Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[3] ); // C * x * y } -int Gia_PolyFindNext2( Pln_Man_t * p ) -{ - Gia_Obj_t * pObj; - Vec_Int_t * vArray; - int Max = 0, iBest = 0, iConst, iMono, iDriver; - Vec_IntForEachEntryStart( p->vCoefs, iConst, iMono, 1 ) - { - if ( iConst == 0 ) - continue; - vArray = Hsh_VecReadEntry( p->pHashM, iMono ); - iDriver = Vec_IntEntryLast( vArray ); - pObj = Gia_ManObj( p->pGia, iDriver ); - if ( !Gia_ObjIsAnd(pObj) ) - continue; - if ( Max < Vec_IntEntryLast(vArray) ) - { - Max = Vec_IntEntryLast(vArray); - iBest = iMono; - } - } - //Vec_IntPrint( Hsh_VecReadEntry(p->pHashM, iBest) ); - return iBest; -} -int Gia_PolyFindNext( Pln_Man_t * p ) -{ - int iBest = Vec_QueSize(p->vQue) ? Vec_QuePop(p->vQue) : 0; - //Vec_IntPrint( Hsh_VecReadEntry(p->pHashM, iBest) ); - return iBest; -} -void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose, int fVeryVerbose ) +void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fSigned, int fVerbose, int fVeryVerbose ) { abctime clk = Abc_Clock();//, clk2 = 0; Gia_Obj_t * pObj; @@ -334,22 +356,35 @@ void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose, int fVe iDriver = Gia_ObjFaninId0p( pGia, pObj ); Vec_IntFill( p->vTempM[0], 1, iDriver ); // Driver - if ( Gia_ObjFaninC0(pObj) ) + if ( fSigned && i == Gia_ManCoNum(pGia)-1 ) { - Gia_PolynBuildAdd( p, p->vTempC[0], NULL ); // C - Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[0] ); // -C * Driver + if ( Gia_ObjFaninC0(pObj) ) + { + Gia_PolynBuildAdd( p, p->vTempC[1], NULL ); // -C + Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] ); // C * Driver + } + else + Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[0] ); // -C * Driver + } + else + { + if ( Gia_ObjFaninC0(pObj) ) + { + Gia_PolynBuildAdd( p, p->vTempC[0], NULL ); // C + Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[0] ); // -C * Driver + } + else + Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] ); // C * Driver } - else - Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] ); // C * Driver } LevPrev = -1; for ( Iter = 0; ; Iter++ ) { Vec_Int_t * vTempM; //abctime temp = Abc_Clock(); - iMono = Gia_PolyFindNext(p); - if ( !iMono ) + if ( Vec_QueSize(p->vQue) == 0 ) break; + iMono = Vec_QuePop(p->vQue); // report vTempM = Hsh_VecReadEntry( p->pHashM, iMono ); @@ -366,8 +401,8 @@ void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose, int fVe Vec_BitSetEntry( vPres, LevCur, 1 ); if ( fVerbose ) - printf( "Line%5d Iter%10d : Obj =%6d. Order =%6d. HashC =%6d. HashM =%10d. Total =%10d. Used =%6d.\n", - Line++, Iter, LevCur, Vec_IntEntry(p->vOrder, LevCur), Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, -1 ); + printf( "Line%5d Iter%10d : Obj =%6d. Order =%6d. HashC =%6d. HashM =%10d. Total =%10d. Used =%10d.\n", + Line++, Iter, LevCur, Vec_IntEntry(p->vOrder, LevCur), Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, p->nUsed ); } LevPrev = LevCur; diff --git a/src/proof/acec/acecUtil.c b/src/proof/acec/acecUtil.c index 26087f92..191856cf 100644 --- a/src/proof/acec/acecUtil.c +++ b/src/proof/acec/acecUtil.c @@ -48,11 +48,23 @@ void Gia_PolynCollectXors_rec( Gia_Man_t * pGia, int iObj, Vec_Int_t * vXors ) if ( Gia_ObjIsTravIdCurrent(pGia, pObj) ) return; Gia_ObjSetTravIdCurrent(pGia, pObj); - if ( !Gia_ObjIsAnd(pObj) || !Gia_ObjIsXor(pObj) ) + if ( !Gia_ObjIsAnd(pObj) || !Gia_ObjIsXor(pObj) || Gia_ObjRefNum(pGia, pObj) > 1 ) return; - Vec_IntPush( vXors, iObj ); Gia_PolynCollectXors_rec( pGia, Gia_ObjFaninId0(pObj, iObj), vXors ); Gia_PolynCollectXors_rec( pGia, Gia_ObjFaninId1(pObj, iObj), vXors ); + Vec_IntPushUnique( vXors, iObj ); +} +Vec_Int_t * Gia_PolynCollectLastXor( Gia_Man_t * pGia, int fVerbose ) +{ + Vec_Int_t * vXors = Vec_IntAlloc( 100 ); + Gia_Obj_t * pObj = Gia_ManCo( pGia, Gia_ManCoNum(pGia)-1 ); + ABC_FREE( pGia->pRefs ); + Gia_ManCreateRefs( pGia ); + Gia_ManIncrementTravId( pGia ); + Gia_PolynCollectXors_rec( pGia, Gia_ObjFaninId0p(pGia, pObj), vXors ); + Vec_IntReverseOrder( vXors ); + ABC_FREE( pGia->pRefs ); + return vXors; } void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose ) { -- cgit v1.2.3