diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-12-13 10:02:28 +0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-12-13 10:02:28 +0800 |
commit | 81af996fee2626daf45936e892ab34f26bea2ada (patch) | |
tree | 3d4420f88a194b53e3e4fe3c9f16213d3573a010 /src/proof | |
parent | 5351ab4b13aa46db5710ca3ffe659e8e691ba126 (diff) | |
download | abc-81af996fee2626daf45936e892ab34f26bea2ada.tar.gz abc-81af996fee2626daf45936e892ab34f26bea2ada.tar.bz2 abc-81af996fee2626daf45936e892ab34f26bea2ada.zip |
Bug fix in 'dsat <file.cnf>' when the number of classes in listed incorrectly.
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/acec/acecCl.c | 204 |
1 files changed, 204 insertions, 0 deletions
diff --git a/src/proof/acec/acecCl.c b/src/proof/acec/acecCl.c index 32be3b30..b60c2bf9 100644 --- a/src/proof/acec/acecCl.c +++ b/src/proof/acec/acecCl.c @@ -45,6 +45,210 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ +void Acec_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * vMirrors ) +{ + Gia_Obj_t * pObj; + int Obj = Node; + if ( Vec_IntEntry(vMirrors, Node) >= 0 ) + Obj = Abc_Lit2Var( Vec_IntEntry(vMirrors, Node) ); + pObj = Gia_ManObj( p, Obj ); + if ( !~pObj->Value ) + { + assert( Gia_ObjIsAnd(pObj) ); + Acec_ManDerive_rec( pNew, p, Gia_ObjFaninId0(pObj, Obj), vMirrors ); + Acec_ManDerive_rec( pNew, p, Gia_ObjFaninId1(pObj, Obj), vMirrors ); + if ( Gia_ObjIsXor(pObj) ) + pObj->Value = Gia_ManAppendXorReal( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + // set the original node as well + if ( Obj != Node ) + Gia_ManObj(p, Node)->Value = Abc_LitNotCond( pObj->Value, Abc_LitIsCompl(Vec_IntEntry(vMirrors, Node)) ); +} +Gia_Man_t * Acec_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + assert( p->pMuxes == NULL ); + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManHashAlloc( pNew ); + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachCo( p, pObj, i ) + Acec_ManDerive_rec( pNew, p, Gia_ObjFaninId0p(p, pObj), vMirrors ); + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Acec_CollectXorTops( Gia_Man_t * p ) +{ + Vec_Int_t * vRootXorSet = Vec_IntAlloc( Gia_ManCoNum(p) ); + Gia_Obj_t * pObj, * pFan0, * pFan1, * pFan00, * pFan01, * pFan10, * pFan11; + int i, fXor0, fXor1, fFirstXor = 0; + Gia_ManForEachCoDriver( p, pObj, i ) + { + if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) ) + { + if ( fFirstXor ) + { + printf( "XORs do not form a continuous sequence\n" ); + Vec_IntFreeP( &vRootXorSet ); + break; + } + continue; + } + fFirstXor = 1; + fXor0 = Gia_ObjRecognizeExor(Gia_Regular(pFan0), &pFan00, &pFan01); + fXor1 = Gia_ObjRecognizeExor(Gia_Regular(pFan1), &pFan10, &pFan11); + if ( fXor0 == fXor1 ) + { + printf( "Both inputs of top level XOR have XOR/non-XOR\n" ); + Vec_IntFreeP( &vRootXorSet ); + 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(pFan10)) : Gia_ObjId(p, Gia_Regular(pFan00)) ); + Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan11)) : Gia_ObjId(p, Gia_Regular(pFan01)) ); + } + for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ ) + { + printf( "%2d : ", i ); + printf( "%4d <- ", Vec_IntEntry(vRootXorSet, 4*i) ); + printf( "%4d ", Vec_IntEntry(vRootXorSet, 4*i+1) ); + printf( "%4d ", Vec_IntEntry(vRootXorSet, 4*i+2) ); + printf( "%4d ", Vec_IntEntry(vRootXorSet, 4*i+3) ); + printf( "\n" ); + } + return vRootXorSet; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Acec_DetectLitPolarity( Gia_Man_t * p, int Node, int Leaf ) +{ + Gia_Obj_t * pNode; + int Lit0, Lit1; + if ( Node < Leaf ) + return -1; + if ( Node == Leaf ) + return Abc_Var2Lit(Node, 0); + pNode = Gia_ManObj( p, Node ); + Lit0 = Acec_DetectLitPolarity( p, Gia_ObjFaninId0(pNode, Node), Leaf ); + Lit1 = Acec_DetectLitPolarity( p, Gia_ObjFaninId1(pNode, Node), Leaf ); + Lit0 = Lit0 == -1 ? Lit0 : Abc_LitNotCond( Lit0, Gia_ObjFaninC0(pNode) ); + Lit1 = Lit1 == -1 ? Lit1 : Abc_LitNotCond( Lit1, Gia_ObjFaninC1(pNode) ); + if ( Lit0 == -1 && Lit1 == -1 ) + return -1; + assert( Lit0 != -1 || Lit1 != -1 ); + if ( Lit0 != -1 && Lit1 != -1 ) + { + assert( Lit0 == Lit1 ); + return Lit0; + } + return Lit0 != -1 ? Lit0 : Lit1; +} +Gia_Man_t * Acec_DetectXorBuildNew( Gia_Man_t * p, Vec_Int_t * vRootXorSet ) +{ + Gia_Man_t * pNew; + int i, k, iOr1, iAnd1, iAnd2, pLits[3]; // carry, in1, in2 + Vec_Int_t * vMirrors = Vec_IntStart( Gia_ManObjNum(p) ); + for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ ) + { + pLits[0] = Acec_DetectLitPolarity( p, Vec_IntEntry(vRootXorSet, 4*i), Vec_IntEntry(vRootXorSet, 4*i+1) ); + // get polarity of two new ones + for ( k = 1; k < 3; k++ ) + pLits[k] = Acec_DetectLitPolarity( p, Vec_IntEntry(vRootXorSet, 4*i), Vec_IntEntry(vRootXorSet, 4*i+k+1) ); + // create the gate + iOr1 = Gia_ManAppendOr( p, pLits[1], pLits[2] ); + iAnd1 = Gia_ManAppendAnd( p, pLits[0], iOr1 ); + iAnd2 = Gia_ManAppendAnd( p, pLits[1], pLits[2] ); + pLits[0] = Gia_ManAppendOr( p, iAnd1, iAnd2 ); + Vec_IntWriteEntry( vMirrors, Vec_IntEntry(vRootXorSet, 4*i+1), pLits[0] ); + } + // remap the AIG using map + pNew = Acec_ManDerive( p, vMirrors ); + Vec_IntFree( vMirrors ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Acec_DetectAdditional( Gia_Man_t * p, int fVerbose ) +{ + 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 ); + extern void Ree_ManRemoveContained( Gia_Man_t * p, Vec_Int_t * vAdds ); + extern int Ree_ManCountFadds( Vec_Int_t * vAdds ); + extern void Ree_ManPrintAdders( Vec_Int_t * vAdds, int fVerbose ); + + abctime clk = Abc_Clock(); + Gia_Man_t * pNew; + Vec_Int_t * vRootXorSet; +// Vec_Int_t * vXors, * vAdds = Ree_ManComputeCuts( p, &vXors, 0 ); +// Ree_ManRemoveTrivial( p, vAdds ); +// Ree_ManRemoveContained( p, vAdds ); + + //Ree_ManPrintAdders( vAdds, 1 ); +// printf( "Detected %d full-adders and %d half-adders. Found %d XOR-cuts. ", Ree_ManCountFadds(vAdds), Vec_IntSize(vAdds)/6-Ree_ManCountFadds(vAdds), Vec_IntSize(vXors)/4 ); +// Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + + clk = Abc_Clock(); + vRootXorSet = Acec_CollectXorTops( p ); + if ( vRootXorSet ) + { + pNew = Acec_DetectXorBuildNew( p, vRootXorSet ); + Vec_IntFree( vRootXorSet ); + } + else + pNew = Gia_ManDup( p ); + + printf( "Detected %d top XORs. ", Vec_IntSize(vRootXorSet)/4 ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + +// Vec_IntFree( vXors ); +// Vec_IntFree( vAdds ); + return pNew; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |