| /**CFile**************************************************************** |
| |
| FileName [sswIslands.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Inductive prover with constraints.] |
| |
| Synopsis [Detection of islands of difference.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - September 1, 2008.] |
| |
| Revision [$Id: sswIslands.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "sswInt.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Creates pair of structurally equivalent nodes.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ssw_CreatePair( Vec_Int_t * vPairs, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) |
| { |
| pObj0->pData = pObj1; |
| pObj1->pData = pObj0; |
| Vec_IntPush( vPairs, pObj0->Id ); |
| Vec_IntPush( vPairs, pObj1->Id ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Establishes relationship between nodes using pairing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs ) |
| { |
| Aig_Obj_t * pObj0, * pObj1; |
| int i; |
| // create matching |
| Aig_ManCleanData( p0 ); |
| Aig_ManCleanData( p1 ); |
| for ( i = 0; i < Vec_IntSize(vPairs); i += 2 ) |
| { |
| pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairs, i) ); |
| pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairs, i+1) ); |
| assert( pObj0->pData == NULL ); |
| assert( pObj1->pData == NULL ); |
| pObj0->pData = pObj1; |
| pObj1->pData = pObj0; |
| } |
| // make sure constants are matched |
| pObj0 = Aig_ManConst1( p0 ); |
| pObj1 = Aig_ManConst1( p1 ); |
| assert( pObj0->pData == pObj1 ); |
| assert( pObj1->pData == pObj0 ); |
| // make sure PIs are matched |
| Saig_ManForEachPi( p0, pObj0, i ) |
| { |
| pObj1 = Aig_ManCi( p1, i ); |
| assert( pObj0->pData == pObj1 ); |
| assert( pObj1->pData == pObj0 ); |
| } |
| // make sure the POs are not matched |
| Aig_ManForEachCo( p0, pObj0, i ) |
| { |
| pObj1 = Aig_ManCo( p1, i ); |
| assert( pObj0->pData == NULL ); |
| assert( pObj1->pData == NULL ); |
| } |
| |
| // check that LIs/LOs are matched in sync |
| Saig_ManForEachLo( p0, pObj0, i ) |
| { |
| if ( pObj0->pData == NULL ) |
| continue; |
| pObj1 = (Aig_Obj_t *)pObj0->pData; |
| if ( !Saig_ObjIsLo(p1, pObj1) ) |
| Abc_Print( 1, "Mismatch between LO pairs.\n" ); |
| } |
| Saig_ManForEachLo( p1, pObj1, i ) |
| { |
| if ( pObj1->pData == NULL ) |
| continue; |
| pObj0 = (Aig_Obj_t *)pObj1->pData; |
| if ( !Saig_ObjIsLo(p0, pObj0) ) |
| Abc_Print( 1, "Mismatch between LO pairs.\n" ); |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Establishes relationship between nodes using pairing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ssw_MatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes ) |
| { |
| Aig_Obj_t * pNext, * pObj; |
| int i, k, iFan = -1; |
| Vec_PtrClear( vNodes ); |
| Aig_ManIncrementTravId( p ); |
| Aig_ManForEachObj( p, pObj, i ) |
| { |
| if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) |
| continue; |
| if ( pObj->pData != NULL ) |
| continue; |
| if ( Saig_ObjIsLo(p, pObj) ) |
| { |
| pNext = Saig_ObjLoToLi(p, pObj); |
| pNext = Aig_ObjFanin0(pNext); |
| if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) && !Aig_ObjIsConst1(pNext) ) |
| { |
| Aig_ObjSetTravIdCurrent(p, pNext); |
| Vec_PtrPush( vNodes, pNext ); |
| } |
| } |
| if ( Aig_ObjIsNode(pObj) ) |
| { |
| pNext = Aig_ObjFanin0(pObj); |
| if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) ) |
| { |
| Aig_ObjSetTravIdCurrent(p, pNext); |
| Vec_PtrPush( vNodes, pNext ); |
| } |
| pNext = Aig_ObjFanin1(pObj); |
| if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) ) |
| { |
| Aig_ObjSetTravIdCurrent(p, pNext); |
| Vec_PtrPush( vNodes, pNext ); |
| } |
| } |
| Aig_ObjForEachFanout( p, pObj, pNext, iFan, k ) |
| { |
| if ( Saig_ObjIsPo(p, pNext) ) |
| continue; |
| if ( Saig_ObjIsLi(p, pNext) ) |
| pNext = Saig_ObjLiToLo(p, pNext); |
| if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) ) |
| { |
| Aig_ObjSetTravIdCurrent(p, pNext); |
| Vec_PtrPush( vNodes, pNext ); |
| } |
| } |
| } |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Establishes relationship between nodes using pairing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ssw_MatchingCountUnmached( Aig_Man_t * p ) |
| { |
| Aig_Obj_t * pObj; |
| int i, Counter = 0; |
| Aig_ManForEachObj( p, pObj, i ) |
| { |
| if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) |
| continue; |
| if ( pObj->pData != NULL ) |
| continue; |
| Counter++; |
| } |
| return Counter; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Establishes relationship between nodes using pairing.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose ) |
| { |
| Vec_Ptr_t * vNodes0, * vNodes1; |
| Aig_Obj_t * pNext0, * pNext1; |
| int d, k; |
| Aig_ManFanoutStart(p0); |
| Aig_ManFanoutStart(p1); |
| vNodes0 = Vec_PtrAlloc( 1000 ); |
| vNodes1 = Vec_PtrAlloc( 1000 ); |
| if ( fVerbose ) |
| { |
| int nUnmached = Ssw_MatchingCountUnmached(p0); |
| Abc_Print( 1, "Extending islands by %d steps:\n", nDist ); |
| Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n", |
| 0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0), |
| nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) ); |
| } |
| for ( d = 0; d < nDist; d++ ) |
| { |
| Ssw_MatchingExtendOne( p0, vNodes0 ); |
| Ssw_MatchingExtendOne( p1, vNodes1 ); |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pNext0, k ) |
| { |
| pNext1 = (Aig_Obj_t *)pNext0->pData; |
| if ( pNext1 == NULL ) |
| continue; |
| assert( pNext1->pData == pNext0 ); |
| if ( Saig_ObjIsPi(p0, pNext1) ) |
| continue; |
| pNext0->pData = NULL; |
| pNext1->pData = NULL; |
| } |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pNext0, k ) |
| { |
| pNext1 = (Aig_Obj_t *)pNext0->pData; |
| if ( pNext1 == NULL ) |
| continue; |
| assert( pNext1->pData == pNext0 ); |
| if ( Saig_ObjIsPi(p1, pNext1) ) |
| continue; |
| pNext0->pData = NULL; |
| pNext1->pData = NULL; |
| } |
| if ( fVerbose ) |
| { |
| int nUnmached = Ssw_MatchingCountUnmached(p0); |
| Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n", |
| d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0), |
| nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) ); |
| } |
| } |
| Vec_PtrFree( vNodes0 ); |
| Vec_PtrFree( vNodes1 ); |
| Aig_ManFanoutStop(p0); |
| Aig_ManFanoutStop(p1); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Used differences in p0 to complete p1.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Ssw_MatchingComplete( Aig_Man_t * p0, Aig_Man_t * p1 ) |
| { |
| Vec_Ptr_t * vNewLis; |
| Aig_Obj_t * pObj0, * pObj0Li, * pObj1; |
| int i; |
| // create register outputs in p0 that are absent in p1 |
| vNewLis = Vec_PtrAlloc( 100 ); |
| Saig_ManForEachLiLo( p0, pObj0Li, pObj0, i ) |
| { |
| if ( pObj0->pData != NULL ) |
| continue; |
| pObj1 = Aig_ObjCreateCi( p1 ); |
| pObj0->pData = pObj1; |
| pObj1->pData = pObj0; |
| Vec_PtrPush( vNewLis, pObj0Li ); |
| } |
| // add missing nodes in the topological order |
| Aig_ManForEachNode( p0, pObj0, i ) |
| { |
| if ( pObj0->pData != NULL ) |
| continue; |
| pObj1 = Aig_And( p1, Aig_ObjChild0Copy(pObj0), Aig_ObjChild1Copy(pObj0) ); |
| pObj0->pData = pObj1; |
| pObj1->pData = pObj0; |
| } |
| // create register outputs in p0 that are absent in p1 |
| Vec_PtrForEachEntry( Aig_Obj_t *, vNewLis, pObj0Li, i ) |
| Aig_ObjCreateCo( p1, Aig_ObjChild0Copy(pObj0Li) ); |
| // increment the number of registers |
| Aig_ManSetRegNum( p1, Aig_ManRegNum(p1) + Vec_PtrSize(vNewLis) ); |
| Vec_PtrFree( vNewLis ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Derives matching for all pairs.] |
| |
| Description [Modifies both AIGs.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Ssw_MatchingPairs( Aig_Man_t * p0, Aig_Man_t * p1 ) |
| { |
| Vec_Int_t * vPairsNew; |
| Aig_Obj_t * pObj0, * pObj1; |
| int i; |
| // check correctness |
| assert( Aig_ManCiNum(p0) == Aig_ManCiNum(p1) ); |
| assert( Aig_ManCoNum(p0) == Aig_ManCoNum(p1) ); |
| assert( Aig_ManRegNum(p0) == Aig_ManRegNum(p1) ); |
| assert( Aig_ManObjNum(p0) == Aig_ManObjNum(p1) ); |
| // create complete pairs |
| vPairsNew = Vec_IntAlloc( 2*Aig_ManObjNum(p0) ); |
| Aig_ManForEachObj( p0, pObj0, i ) |
| { |
| if ( Aig_ObjIsCo(pObj0) ) |
| continue; |
| pObj1 = (Aig_Obj_t *)pObj0->pData; |
| Vec_IntPush( vPairsNew, pObj0->Id ); |
| Vec_IntPush( vPairsNew, pObj1->Id ); |
| } |
| return vPairsNew; |
| } |
| |
| |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Transfers the result of matching to miter.] |
| |
| Description [The array of pairs should be complete.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairsAll ) |
| { |
| Vec_Int_t * vPairsMiter; |
| Aig_Obj_t * pObj0, * pObj1; |
| int i; |
| // create matching of nodes in the miter |
| vPairsMiter = Vec_IntAlloc( 2*Aig_ManObjNum(p0) ); |
| for ( i = 0; i < Vec_IntSize(vPairsAll); i += 2 ) |
| { |
| pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairsAll, i) ); |
| pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairsAll, i+1) ); |
| assert( pObj0->pData != NULL ); |
| assert( pObj1->pData != NULL ); |
| if ( pObj0->pData == pObj1->pData ) |
| continue; |
| if ( Aig_ObjIsNone((Aig_Obj_t *)pObj0->pData) || Aig_ObjIsNone((Aig_Obj_t *)pObj1->pData) ) |
| continue; |
| // get the miter nodes |
| pObj0 = (Aig_Obj_t *)pObj0->pData; |
| pObj1 = (Aig_Obj_t *)pObj1->pData; |
| assert( !Aig_IsComplement(pObj0) ); |
| assert( !Aig_IsComplement(pObj1) ); |
| assert( Aig_ObjType(pObj0) == Aig_ObjType(pObj1) ); |
| if ( Aig_ObjIsCo(pObj0) ) |
| continue; |
| assert( Aig_ObjIsNode(pObj0) || Saig_ObjIsLo(pMiter, pObj0) ); |
| assert( Aig_ObjIsNode(pObj1) || Saig_ObjIsLo(pMiter, pObj1) ); |
| assert( pObj0->Id < pObj1->Id ); |
| Vec_IntPush( vPairsMiter, pObj0->Id ); |
| Vec_IntPush( vPairsMiter, pObj1->Id ); |
| } |
| return vPairsMiter; |
| } |
| |
| |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Solves SEC using structural similarity.] |
| |
| Description [Modifies both p0 and p1 by adding extra logic.] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars ) |
| { |
| Ssw_Man_t * p; |
| Vec_Int_t * vPairsAll, * vPairsMiter; |
| Aig_Man_t * pMiter, * pAigNew; |
| // derive full matching |
| Ssw_MatchingStart( p0, p1, vPairs ); |
| if ( pPars->nIsleDist ) |
| Ssw_MatchingExtend( p0, p1, pPars->nIsleDist, pPars->fVerbose ); |
| Ssw_MatchingComplete( p0, p1 ); |
| Ssw_MatchingComplete( p1, p0 ); |
| vPairsAll = Ssw_MatchingPairs( p0, p1 ); |
| // create miter and transfer matching |
| pMiter = Saig_ManCreateMiter( p0, p1, 0 ); |
| vPairsMiter = Ssw_MatchingMiter( pMiter, p0, p1, vPairsAll ); |
| Vec_IntFree( vPairsAll ); |
| // start the induction manager |
| p = Ssw_ManCreate( pMiter, pPars ); |
| // create equivalence classes using these IDs |
| if ( p->pPars->fPartSigCorr ) |
| p->ppClasses = Ssw_ClassesPreparePairsSimple( pMiter, vPairsMiter ); |
| else |
| p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose ); |
| if ( p->pPars->fDumpSRInit ) |
| { |
| if ( p->pPars->fPartSigCorr ) |
| { |
| Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p ); |
| Aig_ManDumpBlif( pSRed, "srm_part.blif", NULL, NULL ); |
| Aig_ManStop( pSRed ); |
| Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm_part.blif" ); |
| } |
| else |
| Abc_Print( 1, "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" ); |
| } |
| p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 ); |
| Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord ); |
| // perform refinement of classes |
| pAigNew = Ssw_SignalCorrespondenceRefine( p ); |
| // cleanup |
| Ssw_ManStop( p ); |
| Aig_ManStop( pMiter ); |
| Vec_IntFree( vPairsMiter ); |
| return pAigNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Solves SEC with structural similarity.] |
| |
| Description [The first two arguments are pointers to the AIG managers. |
| The third argument is the array of pairs of IDs of structurally equivalent |
| nodes from the first and second managers, respectively.] |
| |
| SideEffects [The managers will be updated by adding "islands of difference".] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ssw_SecWithSimilarityPairs( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs, Ssw_Pars_t * pPars ) |
| { |
| Ssw_Pars_t Pars; |
| Aig_Man_t * pAigRes; |
| int RetValue; |
| abctime clk = Abc_Clock(); |
| // derive parameters if not given |
| if ( pPars == NULL ) |
| Ssw_ManSetDefaultParams( pPars = &Pars ); |
| // reduce the AIG with pairs |
| pAigRes = Ssw_SecWithSimilaritySweep( p0, p1, vPairs, pPars ); |
| // report the result of verification |
| RetValue = Ssw_MiterStatus( pAigRes, 1 ); |
| if ( RetValue == 1 ) |
| Abc_Print( 1, "Verification successful. " ); |
| else if ( RetValue == 0 ) |
| Abc_Print( 1, "Verification failed with a counter-example. " ); |
| else |
| Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", |
| Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) ); |
| ABC_PRT( "Time", Abc_Clock() - clk ); |
| Aig_ManStop( pAigRes ); |
| return RetValue; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Dummy procedure to detect structural similarity.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Saig_StrSimPerformMatching_hack( Aig_Man_t * p0, Aig_Man_t * p1 ) |
| { |
| Vec_Int_t * vPairs; |
| Aig_Obj_t * pObj; |
| int i; |
| // create array of pairs |
| vPairs = Vec_IntAlloc( 100 ); |
| Aig_ManForEachObj( p0, pObj, i ) |
| { |
| if ( !Aig_ObjIsConst1(pObj) && !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) ) |
| continue; |
| Vec_IntPush( vPairs, i ); |
| Vec_IntPush( vPairs, i ); |
| } |
| return vPairs; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Solves SEC with structural similarity.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Ssw_SecWithSimilarity( Aig_Man_t * p0, Aig_Man_t * p1, Ssw_Pars_t * pPars ) |
| { |
| Vec_Int_t * vPairs; |
| Aig_Man_t * pPart0, * pPart1; |
| int RetValue; |
| if ( pPars->fVerbose ) |
| Abc_Print( 1, "Performing sequential verification using structural similarity.\n" ); |
| // consider the case when a miter is given |
| if ( p1 == NULL ) |
| { |
| if ( pPars->fVerbose ) |
| { |
| Aig_ManPrintStats( p0 ); |
| } |
| // demiter the miter |
| if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) ) |
| { |
| Abc_Print( 1, "Demitering has failed.\n" ); |
| return -1; |
| } |
| } |
| else |
| { |
| pPart0 = Aig_ManDupSimple( p0 ); |
| pPart1 = Aig_ManDupSimple( p1 ); |
| } |
| if ( pPars->fVerbose ) |
| { |
| // Aig_ManPrintStats( pPart0 ); |
| // Aig_ManPrintStats( pPart1 ); |
| if ( p1 == NULL ) |
| { |
| // Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL ); |
| // Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL ); |
| // Abc_Print( 1, "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" ); |
| } |
| } |
| assert( Aig_ManRegNum(pPart0) > 0 ); |
| assert( Aig_ManRegNum(pPart1) > 0 ); |
| assert( Saig_ManPiNum(pPart0) == Saig_ManPiNum(pPart1) ); |
| assert( Saig_ManPoNum(pPart0) == Saig_ManPoNum(pPart1) ); |
| // derive pairs |
| // vPairs = Saig_StrSimPerformMatching_hack( pPart0, pPart1 ); |
| vPairs = Saig_StrSimPerformMatching( pPart0, pPart1, 0, pPars->fVerbose, NULL ); |
| RetValue = Ssw_SecWithSimilarityPairs( pPart0, pPart1, vPairs, pPars ); |
| Aig_ManStop( pPart0 ); |
| Aig_ManStop( pPart1 ); |
| Vec_IntFree( vPairs ); |
| return RetValue; |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
