diff options
-rw-r--r-- | src/base/abci/abc.c | 37 | ||||
-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 |
4 files changed, 56 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 31f3e270..db8bacf2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -655,6 +655,25 @@ Vec_Int_t * Abc_FrameDeriveStatusArray( Vec_Ptr_t * vCexes ) Vec_IntWriteEntry( vStatuses, i, 0 ); // set this output as SAT return vStatuses; } +Vec_Int_t * Abc_FrameDeriveStatusArray2( Vec_Ptr_t * vCexes ) +{ + Vec_Int_t * vStatuses; + Abc_Cex_t * pCex; + int i; + if ( vCexes == NULL ) + return NULL; + vStatuses = Vec_IntAlloc( Vec_PtrSize(vCexes) ); + Vec_IntFill( vStatuses, Vec_PtrSize(vCexes), -1 ); // assume UNDEC + Vec_PtrForEachEntry( Abc_Cex_t *, vCexes, pCex, i ) + if ( pCex == (Abc_Cex_t *)(ABC_PTRINT_T)1 ) + { + Vec_IntWriteEntry( vStatuses, i, 1 ); // set this output as UNSAT + Vec_PtrWriteEntry( vCexes, i, NULL ); + } + else if ( pCex != NULL ) + Vec_IntWriteEntry( vStatuses, i, 0 ); // set this output as SAT + return vStatuses; +} /**Function************************************************************* @@ -2765,8 +2784,8 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_CexPrintStats( pTemp ); } } - if ( Counter ) - printf( "In total, %d (out of %d) outputs are \"sat\" but CEXes are not recorded.\n", Counter, Vec_PtrSize(pAbc->vCexVec) ); +// if ( Counter ) +// printf( "In total, %d (out of %d) outputs are \"sat\" but CEXes are not recorded.\n", Counter, Vec_PtrSize(pAbc->vCexVec) ); } } if ( pAbc->vStatuses ) @@ -33675,7 +33694,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) int fNewSolver = 0, fCSat = 0; Cec_ManSatSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CSNanmtcxvh" ) ) != EOF ) { switch ( c ) { @@ -33727,6 +33746,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'c': fCSat ^= 1; break; + case 'x': + pPars->fSaveCexes ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -33759,10 +33781,16 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) pTemp = Cec_ManSatSolving( pAbc->pGia, pPars ); Abc_FrameUpdateGia( pAbc, pTemp ); } + if ( pAbc->pGia->vSeqModelVec ) + { + Vec_Int_t * vStatuses = Abc_FrameDeriveStatusArray2( pAbc->pGia->vSeqModelVec ); + Abc_FrameReplacePoStatuses( pAbc, &vStatuses ); + Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec ); + } return 0; usage: - Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctvh]\n" ); + Abc_Print( -2, "usage: &sat [-CSN <num>] [-anmctxvh]\n" ); Abc_Print( -2, "\t performs SAT solving for the combinational outputs\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax ); @@ -33772,6 +33800,7 @@ usage: Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" ); Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" ); Abc_Print( -2, "\t-t : toggle using learning in curcuit-based solver [default = %s]\n", pPars->fLearnCls? "yes": "no" ); + Abc_Print( -2, "\t-x : toggle solving all outputs and saving counter-examples [default = %s]\n", pPars->fSaveCexes? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; 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 ) |