| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/abs/ |
| H A D | absOut.c | 94 Abc_Cex_t * pCexNew = NULL; in Gia_ManGlaRefine() local
160 pCexNew = Gia_ManCexRemap( p, pCex, vPis ); in Gia_ManGlaRefine()
161 …c_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame ); in Gia_ManGlaRefine()
167 if ( pCexNew == NULL ) in Gia_ManGlaRefine()
217 pCexNew = Gia_ManCexRemap( p, pCex, vPis ); in Gia_ManGlaRefine()
218 …c_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame ); in Gia_ManGlaRefine()
224 if ( pCexNew ) in Gia_ManGlaRefine()
227 p->pCexSeq = pCexNew; in Gia_ManGlaRefine()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/bdd/bbr/ |
| H A D | bbrReach.c | 546 Abc_Cex_t * pCexOld, * pCexNew; in Aig_ManVerifyUsingBdds() local
579 pCexNew = Abc_CexAlloc( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 ); in Aig_ManVerifyUsingBdds()
580 pCexNew->iFrame = pCexOld->iFrame; in Aig_ManVerifyUsingBdds()
581 pCexNew->iPo = pCexOld->iPo; in Aig_ManVerifyUsingBdds()
585 Abc_InfoSetBit( pCexNew->pData, iBitOld ); in Aig_ManVerifyUsingBdds()
588 for ( i = 0; i <= pCexNew->iFrame; i++ ) in Aig_ManVerifyUsingBdds()
595 Abc_InfoSetBit( pCexNew->pData, iBitNew + k ); in Aig_ManVerifyUsingBdds()
602 assert( iBitNew == pCexNew->nBits ); in Aig_ManVerifyUsingBdds()
604 pInit->pSeqModel = pCexNew; in Aig_ManVerifyUsingBdds()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/proof/pdr/ |
| H A D | pdrIncr.c | 378 Abc_Cex_t * pCexNew; in IPdr_ManSolveInt() local
483 …pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig),… in IPdr_ManSolveInt()
484 p->pAig->pSeqModel = pCexNew; in IPdr_ManSolveInt()
487 …pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig),… in IPdr_ManSolveInt()
495 Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); in IPdr_ManSolveInt()
496 Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew ); in IPdr_ManSolveInt()
607 …pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_… in IPdr_ManSolveInt()
611 Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); in IPdr_ManSolveInt()
612 Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew ); in IPdr_ManSolveInt()
|
| H A D | pdrCore.c | 1045 Abc_Cex_t * pCexNew; in Pdr_ManSolveInt() local
1099 …pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig),… in Pdr_ManSolveInt()
1100 p->pAig->pSeqModel = pCexNew; in Pdr_ManSolveInt()
1103 …pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig),… in Pdr_ManSolveInt()
1111 Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); in Pdr_ManSolveInt()
1112 Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew ); in Pdr_ManSolveInt()
1220 …pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_… in Pdr_ManSolveInt()
1224 Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); in Pdr_ManSolveInt()
1225 Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew ); in Pdr_ManSolveInt()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bmc/ |
| H A D | bmcBmc3.c | 1465 Abc_Cex_t * pCexNew, * pCexNew0; in Saig_ManBmcScalable() local
1743 …pCexNew = (p->pPars->fUseBridge || pPars->fStoreCex) ? Saig_ManGenerateCex( p, f, i ) : (Abc_Cex_t… in Saig_ManBmcScalable()
1747 Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo ); in Saig_ManBmcScalable()
1749 pCexNew0 = pCexNew; in Saig_ManBmcScalable()
1750 pCexNew = (Abc_Cex_t *)(ABC_PTRINT_T)1; in Saig_ManBmcScalable()
1752 Vec_PtrWriteEntry( p->vCexes, i, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) ); in Saig_ManBmcScalable()
1810 Vec_PtrWriteEntry( p->vCexes, k, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) ); in Saig_ManBmcScalable()
1813 Abc_CexFree( pCexNew ); in Saig_ManBmcScalable()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/aig/gia/ |
| H A D | giaIso.c | 1282 Abc_Cex_t * pCexNew; in Gia_IsoTest() local
1305 pCexNew = Abc_CexPermuteTwo( pCex, vPerm0, vPerm1 ); in Gia_IsoTest()
1313 if ( Gia_ManVerifyCex(pPerm, pCexNew, 0) ) in Gia_IsoTest()
1322 Abc_CexFree( pCexNew ); in Gia_IsoTest()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/abci/ |
| H A D | abc.c | 22819 Abc_Cex_t * pCexNew; in Abc_CommandDarPhase() local
22843 Abc_FrameReplaceCex( pAbc, &pCexNew ); in Abc_CommandDarPhase()
27386 Abc_Cex_t * pCexNew; in Abc_CommandTempor() local
29072 Abc_Cex_t * pCexNew; in Abc_CommandCexMerge() local
29131 if ( pCexNew == NULL ) in Abc_CommandCexMerge()
29138 pAbc->pCex2 = pCexNew; in Abc_CommandCexMerge()
45857 Abc_Cex_t * pCexNew; in Abc_CommandAbc9CexMerge() local
45916 if ( pCexNew == NULL ) in Abc_CommandAbc9CexMerge()
45923 pAbc->pCex2 = pCexNew; in Abc_CommandAbc9CexMerge()
45951 Abc_Cex_t * pCexNew; in Abc_CommandAbc9CexMin() local
[all …]
|