diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2018-05-06 22:13:18 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2018-05-06 22:13:18 -0700 |
| commit | ccf529695d2ef834aed1a6cd643036f6436e7b42 (patch) | |
| tree | 44aad1780d73f241afb2141d0e4a6accc30ee6f2 /src/proof | |
| parent | aa313189c4fffcba13ff938ec01fa62a32fb8914 (diff) | |
| download | abc-ccf529695d2ef834aed1a6cd643036f6436e7b42.tar.gz abc-ccf529695d2ef834aed1a6cd643036f6436e7b42.tar.bz2 abc-ccf529695d2ef834aed1a6cd643036f6436e7b42.zip | |
Adding &sat -x to save CEXes for multi-output combinational miters.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/cec/cec.h | 1 | ||||
| -rw-r--r-- | src/proof/cec/cecCore.c | 2 | ||||
| -rw-r--r-- | src/proof/cec/cecSolve.c | 20 |
3 files changed, 23 insertions, 0 deletions
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index cb4ff27f..757d9fd3 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -51,6 +51,7 @@ struct Cec_ParSat_t_ int fCheckMiter; // the circuit is the miter // int fFirstStop; // stop on the first sat output int fLearnCls; // perform clause learning + int fSaveCexes; // saves counter-examples int fVerbose; // verbose stats }; diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index 85fcfa26..250cb69e 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -241,6 +241,8 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ) // pNew = Gia_ManDupDfsSkip( pAig ); pNew = Gia_ManDup( pAig ); Cec_ManPatStop( pPat ); + pNew->vSeqModelVec = pAig->vSeqModelVec; + pAig->vSeqModelVec = NULL; return pNew; } diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c index f75914e4..3c21e589 100644 --- a/src/proof/cec/cecSolve.c +++ b/src/proof/cec/cecSolve.c @@ -673,6 +673,21 @@ p->timeSatUndec += Abc_Clock() - clk; SeeAlso [] ***********************************************************************/ +Abc_Cex_t * Cex_ManGenCex( Cec_ManSat_t * p, int iOut ) +{ + Abc_Cex_t * pCex; + int i; + pCex = Abc_CexAlloc( 0, Gia_ManCiNum(p->pAig), 1 ); + pCex->iPo = iOut; + pCex->iFrame = 0; + for ( i = 0; i < Gia_ManCiNum(p->pAig); i++ ) + { + int iVar = Cec_ObjSatNum(p, Gia_ManCi(p->pAig, i)); + if ( iVar > 0 && sat_solver_var_value(p->pSat, iVar) ) + pCex->pData[i>>5] |= (1<<(i & 31)); + } + return pCex; +} void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs ) { Bar_Progress_t * pProgress = NULL; @@ -680,6 +695,9 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar Gia_Obj_t * pObj; int i, status; abctime clk = Abc_Clock(), clk2; + Vec_PtrFreeP( &pAig->vSeqModelVec ); + if ( pPars->fSaveCexes ) + pAig->vSeqModelVec = Vec_PtrStart( Gia_ManCoNum(pAig) ); // reset the manager if ( pPat ) { @@ -715,6 +733,8 @@ clk2 = Abc_Clock(); assert( OrigId1 >= 0 && OrigId2 >= 0 ); Vec_IntPushTwo( vEquivPairs, OrigId1, OrigId2 ); } + if ( pPars->fSaveCexes && status != -1 ) + Vec_PtrWriteEntry( pAig->vSeqModelVec, i, status ? (Abc_Cex_t *)(ABC_PTRINT_T)1 : Cex_ManGenCex(p, i) ); /* if ( status == -1 ) |