diff options
Diffstat (limited to 'src/proof/cec/cecSolve.c')
-rw-r--r-- | src/proof/cec/cecSolve.c | 69 |
1 files changed, 69 insertions, 0 deletions
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c index c799d17d..e3db0b93 100644 --- a/src/proof/cec/cecSolve.c +++ b/src/proof/cec/cecSolve.c @@ -735,6 +735,75 @@ clk2 = Abc_Clock(); Cec_ManSatStop( p ); } +/**Function************************************************************* + + Synopsis [Performs one round of solving for the POs of the AIG.] + + Description [Labels the nodes that have been proved (pObj->fMark1) + and returns the set of satisfying assignments.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSatSolveExractPattern( Vec_Int_t * vCexStore, int iStart, Vec_Int_t * vPat ) +{ + int k, nSize; + Vec_IntClear( vPat ); + // skip the output number + iStart++; + // get the number of items + nSize = Vec_IntEntry( vCexStore, iStart++ ); + if ( nSize <= 0 ) + return iStart; + // extract pattern + for ( k = 0; k < nSize; k++ ) + Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) ); + return iStart; +} +void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ) +{ + Vec_Str_t * vStatus; + Vec_Int_t * vPat = Vec_IntAlloc( 1000 ); + Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0 ); + Gia_Obj_t * pObj; + int i, status, iStart = 0; + assert( Vec_StrSize(vStatus) == Gia_ManCoNum(pAig) ); + // reset the manager + if ( pPat ) + { + pPat->iStart = Vec_StrSize(pPat->vStorage); + pPat->nPats = 0; + pPat->nPatLits = 0; + pPat->nPatLitsMin = 0; + } + Gia_ManForEachCo( pAig, pObj, i ) + { + status = (int)Vec_StrEntry(vStatus, i); + pObj->fMark0 = (status == 0); + pObj->fMark1 = (status == 1); + if ( Vec_IntSize(vCexStore) > 0 && status != 1 ) + iStart = Cec_ManSatSolveExractPattern( vCexStore, iStart, vPat ); + if ( status != 0 ) + continue; + // save the pattern + if ( pPat && Vec_IntSize(vPat) > 0 ) + { + abctime clk3 = Abc_Clock(); + Cec_ManPatSavePatternCSat( pPat, vPat ); + pPat->timeTotalSave += Abc_Clock() - clk3; + } + // quit if one of them is solved + if ( pPars->fCheckMiter ) + break; + } + assert( iStart == Vec_IntSize(vCexStore) ); + Vec_IntFree( vPat ); + Vec_StrFree( vStatus ); + Vec_IntFree( vCexStore ); +} + /**Function************************************************************* |