diff options
| -rw-r--r-- | abclib.dsp | 4 | ||||
| -rw-r--r-- | src/aig/gia/gia.h | 2 | ||||
| -rw-r--r-- | src/aig/gia/giaDup.c | 112 | ||||
| -rw-r--r-- | src/aig/gia/giaShow.c | 12 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 12 | ||||
| -rw-r--r-- | src/proof/acec/acecBo.c | 216 | ||||
| -rw-r--r-- | src/proof/acec/acecCl.c | 95 | ||||
| -rw-r--r-- | src/proof/acec/module.make | 1 |
8 files changed, 430 insertions, 24 deletions
@@ -5463,6 +5463,10 @@ SOURCE=.\src\proof\acec\acec.h # End Source File # Begin Source File +SOURCE=.\src\proof\acec\acecBo.c +# End Source File +# Begin Source File + SOURCE=.\src\proof\acec\acecCl.c # End Source File # Begin Source File diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index bf7bf349..ac40f975 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1403,7 +1403,7 @@ extern Gia_Man_t * Gia_ManCleanupOutputs( Gia_Man_t * p, int nOutputs ); extern Gia_Man_t * Gia_ManSeqCleanup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose ); /*=== giaShow.c ===========================================================*/ -extern void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders ); +extern void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds ); /*=== giaShrink.c ===========================================================*/ extern Gia_Man_t * Gia_ManMapShrink4( Gia_Man_t * p, int fKeepLevel, int fVerbose ); extern Gia_Man_t * Gia_ManMapShrink6( Gia_Man_t * p, int nFanoutMax, int fKeepLevel, int fVerbose ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 7ced54a4..c58596b2 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -3377,6 +3377,26 @@ Gia_Man_t * Gia_ManDupOuts( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ +Vec_Wec_t * Gia_ManCreateNodeSupps( Gia_Man_t * p, Vec_Int_t * vNodes, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Gia_Obj_t * pObj; int i, Id; + Vec_Wec_t * vSuppsNo = Vec_WecStart( Vec_IntSize(vNodes) ); + Vec_Wec_t * vSupps = Vec_WecStart( Gia_ManObjNum(p) ); + Gia_ManForEachCiId( p, Id, i ) + Vec_IntPush( Vec_WecEntry(vSupps, Id), i ); + Gia_ManForEachAnd( p, pObj, Id ) + Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)), + Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)), + Vec_WecEntry(vSupps, Id) ); + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + Vec_IntAppend( Vec_WecEntry(vSuppsNo, i), Vec_WecEntry(vSupps, Gia_ObjId(p, pObj)) ); + Vec_WecFree( vSupps ); + if ( fVerbose ) + Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk ); + return vSuppsNo; +} + Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose ) { abctime clk = Abc_Clock(); @@ -3690,6 +3710,81 @@ Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose ) SeeAlso [] ***********************************************************************/ +void Gia_ManDupDemiterOrderXors2( Gia_Man_t * p, Vec_Int_t * vXors ) +{ + int i, iObj, * pPerm; + Vec_Int_t * vSizes = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vXors, iObj, i ) + Vec_IntPush( vSizes, Gia_ManSuppSize(p, &iObj, 1) ); + pPerm = Abc_MergeSortCost( Vec_IntArray(vSizes), Vec_IntSize(vSizes) ); + Vec_IntClear( vSizes ); + for ( i = 0; i < Vec_IntSize(vXors); i++ ) + Vec_IntPush( vSizes, Vec_IntEntry(vXors, pPerm[i]) ); + ABC_FREE( pPerm ); + Vec_IntClear( vXors ); + Vec_IntAppend( vXors, vSizes ); + Vec_IntFree( vSizes ); +} +int Gia_ManDupDemiterFindMin( Vec_Wec_t * vSupps, Vec_Int_t * vTakenIns, Vec_Int_t * vTakenOuts ) +{ + Vec_Int_t * vLevel; + int i, k, iObj, iObjBest = -1; + int Count, CountBest = ABC_INFINITY; + Vec_WecForEachLevel( vSupps, vLevel, i ) + { + if ( Vec_IntEntry(vTakenOuts, i) ) + continue; + Count = 0; + Vec_IntForEachEntry( vLevel, iObj, k ) + Count += !Vec_IntEntry(vTakenIns, iObj); + if ( CountBest > Count ) + { + CountBest = Count; + iObjBest = i; + } + } + return iObjBest; +} +void Gia_ManDupDemiterOrderXors( Gia_Man_t * p, Vec_Int_t * vXors ) +{ + extern Vec_Wec_t * Gia_ManCreateNodeSupps( Gia_Man_t * p, Vec_Int_t * vNodes, int fVerbose ); + Vec_Wec_t * vSupps = Gia_ManCreateNodeSupps( p, vXors, 0 ); + Vec_Int_t * vTakenIns = Vec_IntStart( Gia_ManCiNum(p) ); + Vec_Int_t * vTakenOuts = Vec_IntStart( Vec_IntSize(vXors) ); + Vec_Int_t * vOrder = Vec_IntAlloc( Vec_IntSize(vXors) ); + int i, k, iObj; + // add outputs in the order of increasing supports + for ( i = 0; i < Vec_IntSize(vXors); i++ ) + { + int Index = Gia_ManDupDemiterFindMin( vSupps, vTakenIns, vTakenOuts ); + assert( Index >= 0 && Index < Vec_IntSize(vXors) ); + Vec_IntPush( vOrder, Vec_IntEntry(vXors, Index) ); + assert( !Vec_IntEntry( vTakenOuts, Index ) ); + Vec_IntWriteEntry( vTakenOuts, Index, 1 ); + Vec_IntForEachEntry( Vec_WecEntry(vSupps, Index), iObj, k ) + Vec_IntWriteEntry( vTakenIns, iObj, 1 ); + } + Vec_WecFree( vSupps ); + Vec_IntFree( vTakenIns ); + Vec_IntFree( vTakenOuts ); + // reload + Vec_IntClear( vXors ); + Vec_IntAppend( vXors, vOrder ); + Vec_IntFree( vOrder ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Gia_ManSetMark0Dfs_rec( Gia_Man_t * p, int iObj ) { Gia_Obj_t * pObj; @@ -3781,8 +3876,8 @@ void Gia_ManCollectTopXors_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXo } Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p ) { - int i, iObj, iObj2, fFlip, * pPerm, Count1 = 0; - Vec_Int_t * vXors, * vSizes, * vPart[2], * vOrder; + int i, iObj, iObj2, fFlip, Count1 = 0; + Vec_Int_t * vXors, * vPart[2], * vOrder; Gia_Obj_t * pFan[2], * pObj = Gia_ManCo(p, 0); assert( Gia_ManCoNum(p) == 1 ); vXors = Vec_IntAlloc( 100 ); @@ -3791,17 +3886,8 @@ Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p ) else Vec_IntPush( vXors, Gia_ObjId(p, Gia_ObjFanin0(pObj)) ); // order by support size - vSizes = Vec_IntAlloc( 100 ); - Vec_IntForEachEntry( vXors, iObj, i ) - Vec_IntPush( vSizes, Gia_ManSuppSize(p, &iObj, 1) ); - pPerm = Abc_MergeSortCost( Vec_IntArray(vSizes), Vec_IntSize(vSizes) ); - Vec_IntClear( vSizes ); - for ( i = 0; i < Vec_IntSize(vXors); i++ ) - Vec_IntPush( vSizes, Vec_IntEntry(vXors, pPerm[i]) ); - ABC_FREE( pPerm ); - Vec_IntClear( vXors ); - Vec_IntAppend( vXors, vSizes ); - Vec_IntFree( vSizes ); + Gia_ManDupDemiterOrderXors( p, vXors ); + //Vec_IntPrint( vXors ); Vec_IntReverseOrder( vXors ); // from MSB to LSB // divide into groups Gia_ManCleanMark01(p); diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c index afc58bf8..afd36fff 100644 --- a/src/aig/gia/giaShow.c +++ b/src/aig/gia/giaShow.c @@ -713,11 +713,13 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_ShowMapAdds( Gia_Man_t * p, Vec_Int_t * vAdds ) +Vec_Int_t * Gia_ShowMapAdds( Gia_Man_t * p, Vec_Int_t * vAdds, int fFadds ) { Vec_Int_t * vMapAdds = Vec_IntStartFull( Gia_ManObjNum(p) ); int i; for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) { + if ( fFadds && Vec_IntEntry(vAdds, 6*i+2) == 0 ) + continue; Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+3), i ); Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+4), i ); } @@ -800,9 +802,9 @@ Vec_Int_t * Gia_ShowCollectObjs( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * v SeeAlso [] ***********************************************************************/ -void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_Int_t * vXors ) +void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_Int_t * vXors, int fFadds ) { - Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds ); + Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds, fFadds ); Vec_Int_t * vMapXors = Gia_ShowMapXors( p, vXors ); Vec_Int_t * vOrder = Gia_ShowCollectObjs( p, vAdds, vXors, vMapAdds, vMapXors ); Gia_WriteDotAig( p, pFileName, vAdds, vXors, vMapAdds, vMapXors, vOrder ); @@ -810,7 +812,7 @@ void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In Vec_IntFree( vMapXors ); Vec_IntFree( vOrder ); } -void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders ) +void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds ) { extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose ); extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds ); @@ -837,7 +839,7 @@ void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders ) fclose( pFile ); // generate the file if ( fAdders ) - Gia_ShowProcess( pMan, FileNameDot, vAdds, vXors ); + Gia_ShowProcess( pMan, FileNameDot, vAdds, vXors, fFadds ); else Gia_WriteDotAigSimple( pMan, FileNameDot, vBold ); // visualize the file diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index fb301790..7866b22d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28592,15 +28592,18 @@ usage: int Abc_CommandAbc9Show( Abc_Frame_t * pAbc, int argc, char ** argv ) { Vec_Int_t * vBold = NULL; - int c, fAdders = 0; + int c, fAdders = 0, fFadds = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "afh" ) ) != EOF ) { switch ( c ) { case 'a': fAdders ^= 1; break; + case 'f': + fFadds ^= 1; + break; case 'h': goto usage; default: @@ -28623,14 +28626,15 @@ int Abc_CommandAbc9Show( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ManForEachLut( pAbc->pGia, c ) Vec_IntPush( vBold, c ); } - Gia_ManShow( pAbc->pGia, vBold, fAdders ); + Gia_ManShow( pAbc->pGia, vBold, fAdders, fFadds ); Vec_IntFreeP( &vBold ); return 0; usage: - Abc_Print( -2, "usage: &show [-ah]\n" ); + Abc_Print( -2, "usage: &show [-afh]\n" ); Abc_Print( -2, "\t shows the current GIA using GSView\n" ); Abc_Print( -2, "\t-a : toggle visualazing adders [default = %s]\n", fAdders? "yes": "no" ); + Abc_Print( -2, "\t-f : toggle only showing full-adders with \"-a\" [default = %s]\n", fFadds? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } diff --git a/src/proof/acec/acecBo.c b/src/proof/acec/acecBo.c new file mode 100644 index 00000000..9cddcd13 --- /dev/null +++ b/src/proof/acec/acecBo.c @@ -0,0 +1,216 @@ +/**CFile**************************************************************** + + FileName [acecBo.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [Core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acecBo.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "acecInt.h" +#include "misc/vec/vecWec.h" +#include "misc/extra/extra.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Acec_DetectBoothXorMux( Gia_Man_t * p, Gia_Obj_t * pMux, Gia_Obj_t * pXor, int pIns[3] ) +{ + Gia_Obj_t * pFan0, * pFan1; + Gia_Obj_t * pDat0, * pDat1, * pCtrl; + if ( !Gia_ObjIsMuxType(pMux) || !Gia_ObjIsMuxType(pXor) ) + return 0; + if ( !Gia_ObjRecognizeExor( pXor, &pFan0, &pFan1 ) ) + return 0; + pFan0 = Gia_Regular(pFan0); + pFan1 = Gia_Regular(pFan1); + if ( Gia_ObjId(p, pFan0) > Gia_ObjId(p, pFan1) ) + ABC_SWAP( Gia_Obj_t *, pFan0, pFan1 ); + if ( !(pCtrl = Gia_ObjRecognizeMux( pMux, &pDat0, &pDat1 )) ) + return 0; + pDat0 = Gia_Regular(pDat0); + pDat1 = Gia_Regular(pDat1); + pCtrl = Gia_Regular(pCtrl); + if ( !Gia_ObjIsAnd(pDat0) || !Gia_ObjIsAnd(pDat1) ) + return 0; + if ( Gia_ObjFaninId0p(p, pDat0) != Gia_ObjFaninId0p(p, pDat1) || + Gia_ObjFaninId1p(p, pDat0) != Gia_ObjFaninId1p(p, pDat1) ) + return 0; + if ( Gia_ObjFaninId0p(p, pDat0) != Gia_ObjId(p, pFan0) || + Gia_ObjFaninId1p(p, pDat0) != Gia_ObjId(p, pFan1) ) + return 0; + pIns[0] = Gia_ObjId(p, pFan0); + pIns[1] = Gia_ObjId(p, pFan1); + pIns[2] = Gia_ObjId(p, pCtrl); + return 1; +} +int Acec_DetectBoothXorFanin( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] ) +{ + Gia_Obj_t * pFan0, * pFan1; + //int Id = Gia_ObjId(p, pObj); + if ( !Gia_ObjIsAnd(pObj) ) + return 0; + if ( !Gia_ObjFaninC0(pObj) || !Gia_ObjFaninC1(pObj) ) + return 0; + pFan0 = Gia_ObjFanin0(pObj); + pFan1 = Gia_ObjFanin1(pObj); + if ( !Gia_ObjIsAnd(pFan0) || !Gia_ObjIsAnd(pFan1) ) + return 0; + if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin0(pFan0), Gia_ObjFanin0(pFan1), pIns) ) + { + pIns[3] = Gia_ObjId(p, Gia_ObjFanin1(pFan0)); + pIns[4] = Gia_ObjId(p, Gia_ObjFanin1(pFan1)); + return 1; + } + if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin0(pFan0), Gia_ObjFanin1(pFan1), pIns) ) + { + pIns[3] = Gia_ObjId(p, Gia_ObjFanin1(pFan0)); + pIns[4] = Gia_ObjId(p, Gia_ObjFanin0(pFan1)); + return 1; + } + if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin1(pFan0), Gia_ObjFanin0(pFan1), pIns) ) + { + pIns[3] = Gia_ObjId(p, Gia_ObjFanin0(pFan0)); + pIns[4] = Gia_ObjId(p, Gia_ObjFanin1(pFan1)); + return 1; + } + if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin1(pFan0), Gia_ObjFanin1(pFan1), pIns) ) + { + pIns[3] = Gia_ObjId(p, Gia_ObjFanin0(pFan0)); + pIns[4] = Gia_ObjId(p, Gia_ObjFanin0(pFan1)); + return 1; + } + return 0; +} +int Acec_DetectBoothOne( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] ) +{ + Gia_Obj_t * pFan0, * pFan1; + if ( !Gia_ObjRecognizeExor( pObj, &pFan0, &pFan1 ) ) + return 0; + pFan0 = Gia_Regular(pFan0); + pFan1 = Gia_Regular(pFan1); + if ( Acec_DetectBoothXorFanin( p, pFan0, pIns ) && pIns[2] == Gia_ObjId(p, pFan1) ) + return 1; + if ( Acec_DetectBoothXorFanin( p, pFan1, pIns ) && pIns[2] == Gia_ObjId(p, pFan0) ) + return 1; + return 0; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Acec_DetectBoothTwoXor( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] ) +{ + Gia_Obj_t * pFan0, * pFan1; + if ( !Gia_ObjIsAnd(pObj) ) + return 0; + if ( Gia_ObjRecognizeExor( Gia_ObjFanin0(pObj), &pFan0, &pFan1 ) ) + { + pIns[0] = Gia_ObjId(p, Gia_Regular(pFan0)); + pIns[1] = Gia_ObjId(p, Gia_Regular(pFan1)); + pIns[2] = -1; + pIns[3] = 0; + pIns[4] = Gia_ObjId(p, Gia_ObjFanin1(pObj)); + return 1; + } + if ( Gia_ObjRecognizeExor( Gia_ObjFanin1(pObj), &pFan0, &pFan1 ) ) + { + pIns[0] = Gia_ObjId(p, Gia_Regular(pFan0)); + pIns[1] = Gia_ObjId(p, Gia_Regular(pFan1)); + pIns[2] = -1; + pIns[3] = 0; + pIns[4] = Gia_ObjId(p, Gia_ObjFanin0(pObj)); + return 1; + } + return 0; +} +int Acec_DetectBoothTwo( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] ) +{ + Gia_Obj_t * pFan0, * pFan1; + if ( !Gia_ObjRecognizeExor( pObj, &pFan0, &pFan1 ) ) + return 0; + pFan0 = Gia_Regular(pFan0); + pFan1 = Gia_Regular(pFan1); + if ( Acec_DetectBoothTwoXor( p, pFan0, pIns ) ) + { + pIns[2] = Gia_ObjId(p, pFan1); + return 1; + } + if ( Acec_DetectBoothTwoXor( p, pFan1, pIns ) ) + { + pIns[2] = Gia_ObjId(p, pFan0); + return 1; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acec_DetectBoothTest( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i, pIns[5]; + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !Acec_DetectBoothOne(p, pObj, pIns) && !Acec_DetectBoothTwo(p, pObj, pIns) ) + continue; + printf( "obj = %4d : b0 = %4d b1 = %4d b2 = %4d a0 = %4d a1 = %4d\n", + i, pIns[0], pIns[1], pIns[2], pIns[3], pIns[4] ); + } +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c index b60c2bf9..63483d57 100644 --- a/src/proof/acec/acecCl.c +++ b/src/proof/acec/acecCl.c @@ -127,7 +127,7 @@ Vec_Int_t * Acec_CollectXorTops( Gia_Man_t * p ) break; } Vec_IntPush( vRootXorSet, Gia_ObjId(p, pObj) ); - Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan1)) : Gia_ObjId(p, Gia_Regular(pFan0)) ); + Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan0)) : Gia_ObjId(p, Gia_Regular(pFan1)) ); Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan10)) : Gia_ObjId(p, Gia_Regular(pFan00)) ); Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan11)) : Gia_ObjId(p, Gia_Regular(pFan01)) ); } @@ -173,10 +173,101 @@ int Acec_DetectLitPolarity( Gia_Man_t * p, int Node, int Leaf ) if ( Lit0 != -1 && Lit1 != -1 ) { assert( Lit0 == Lit1 ); + printf( "Problem for leaf %d\n", Leaf ); return Lit0; } return Lit0 != -1 ? Lit0 : Lit1; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acec_DetectComputeSuppOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Int_t * vNods ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return; + Gia_ObjSetTravIdCurrent(p, pObj); + if ( pObj->fMark0 ) + { + Vec_IntPush( vSupp, Gia_ObjId(p, pObj) ); + return; + } + assert( Gia_ObjIsAnd(pObj) ); + Acec_DetectComputeSuppOne_rec( p, Gia_ObjFanin0(pObj), vSupp, vNods ); + Acec_DetectComputeSuppOne_rec( p, Gia_ObjFanin1(pObj), vSupp, vNods ); + Vec_IntPush( vNods, Gia_ObjId(p, pObj) ); +} +void Acec_DetectComputeSupports( Gia_Man_t * p, Vec_Int_t * vRootXorSet ) +{ + Vec_Int_t * vNods = Vec_IntAlloc( 100 ); + Vec_Int_t * vPols = Vec_IntAlloc( 100 ); + Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); int i, k, Node, Pol; + for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ ) + { + Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 1; + Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+2) )->fMark0 = 1; + Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+3) )->fMark0 = 1; + } + for ( i = 1; 4*i < Vec_IntSize(vRootXorSet); i++ ) + { + Vec_IntClear( vSupp ); + Gia_ManIncrementTravId( p ); + + Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 0; + Acec_DetectComputeSuppOne_rec( p, Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) ), vSupp, vNods ); + Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 1; + + Vec_IntSort( vSupp, 0 ); + + printf( "Out %4d : %4d \n", i, Vec_IntEntry(vRootXorSet, 4*i+1) ); + Vec_IntPrint( vSupp ); + + printf( "Cone:\n" ); + Vec_IntForEachEntry( vNods, Node, k ) + Gia_ObjPrint( p, Gia_ManObj(p, Node) ); + + + Vec_IntClear( vPols ); + Vec_IntForEachEntry( vSupp, Node, k ) + Vec_IntPush( vPols, Acec_DetectLitPolarity(p, Vec_IntEntry(vRootXorSet, 4*i+1), Node) ); + + Vec_IntForEachEntryTwo( vSupp, vPols, Node, Pol, k ) + printf( "%d(%d) ", Node, Abc_LitIsCompl(Pol) ); + + printf( "\n" ); + + Vec_IntPrint( vSupp ); + } + for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ ) + { + Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 0; + Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+2) )->fMark0 = 0; + Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+3) )->fMark0 = 0; + } + Vec_IntFree( vSupp ); + Vec_IntFree( vPols ); + Vec_IntFree( vNods ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Gia_Man_t * Acec_DetectXorBuildNew( Gia_Man_t * p, Vec_Int_t * vRootXorSet ) { Gia_Man_t * pNew; @@ -236,6 +327,8 @@ Gia_Man_t * Acec_DetectAdditional( Gia_Man_t * p, int fVerbose ) vRootXorSet = Acec_CollectXorTops( p ); if ( vRootXorSet ) { + Acec_DetectComputeSupports( p, vRootXorSet ); + pNew = Acec_DetectXorBuildNew( p, vRootXorSet ); Vec_IntFree( vRootXorSet ); } diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make index df6db695..4003695e 100644 --- a/src/proof/acec/module.make +++ b/src/proof/acec/module.make @@ -1,6 +1,7 @@ SRC += src/proof/acec/acecCl.c \ src/proof/acec/acecCore.c \ src/proof/acec/acecCo.c \ + src/proof/acec/acecBo.c \ src/proof/acec/acecRe.c \ src/proof/acec/acecPa.c \ src/proof/acec/acecPo.c \ |