| /**CFile**************************************************************** |
| |
| FileName [int2Core.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Interpolation engine.] |
| |
| Synopsis [Core procedures.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - Dec 1, 2013.] |
| |
| Revision [$Id: int2Core.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "int2Int.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [This procedure sets default values of interpolation parameters.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Int2_ManSetDefaultParams( Int2_ManPars_t * p ) |
| { |
| memset( p, 0, sizeof(Int2_ManPars_t) ); |
| p->nBTLimit = 0; // limit on the number of conflicts |
| p->nFramesS = 1; // the starting number timeframes |
| p->nFramesMax = 0; // the max number timeframes to unroll |
| p->nSecLimit = 0; // time limit in seconds |
| p->nFramesK = 1; // the number of timeframes to use in induction |
| p->fRewrite = 0; // use additional rewriting to simplify timeframes |
| p->fTransLoop = 0; // add transition into the init state under new PI var |
| p->fDropInvar = 0; // dump inductive invariant into file |
| p->fVerbose = 0; // print verbose statistics |
| p->iFrameMax = -1; |
| } |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Gia_Man_t * Int2_ManUnroll( Gia_Man_t * p, int nFrames ) |
| { |
| Gia_Man_t * pFrames, * pTemp; |
| Gia_Obj_t * pObj; |
| int i, f; |
| assert( Gia_ManRegNum(pAig) > 0 ); |
| pFrames = Gia_ManStart( Gia_ManObjNum(pAig) ); |
| pFrames->pName = Abc_UtilStrsav( pAig->pName ); |
| pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); |
| Gia_ManHashAlloc( pFrames ); |
| Gia_ManConst0(pAig)->Value = 0; |
| for ( f = 0; f < nFrames; f++ ) |
| { |
| Gia_ManForEachRo( pAig, pObj, i ) |
| pObj->Value = f ? Gia_ObjRoToRi( pAig, pObj )->Value : 0; |
| Gia_ManForEachPi( pAig, pObj, i ) |
| pObj->Value = Gia_ManAppendCi( pFrames ); |
| Gia_ManForEachAnd( pAig, pObj, i ) |
| pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); |
| Gia_ManForEachRi( pAig, pObj, i ) |
| pObj->Value = Gia_ObjFanin0Copy(pObj); |
| } |
| Gia_ManForEachRi( pAig, pObj, i ) |
| Gia_ManAppendCo( pFrames, pObj->Value ); |
| Gia_ManHashStop( pFrames ); |
| pFrames = Gia_ManCleanup( pTemp = pFrames ); |
| Gia_ManStop( pTemp ); |
| return pFrames; |
| } |
| sat_solver * Int2_ManPreparePrefix( Gia_Man_t * p, int f, Vec_Int_t ** pvCiMap ) |
| { |
| Gia_Man_t * pPref, * pNew; |
| sat_solver * pSat; |
| // create subset of the timeframe |
| pPref = Int2_ManUnroll( p, f ); |
| // create SAT solver |
| pNew = Jf_ManDeriveCnf( pPref, 0 ); |
| pCnf = (Cnf_Dat_t *)pPref->pData; pPref->pData = NULL; |
| Gia_ManStop( pPref ); |
| // derive the SAT solver |
| pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); |
| // collect indexes of CO variables |
| *pvCiMap = Vec_IntAlloc( 100 ); |
| Gia_ManForEachPo( pNew, pObj, i ) |
| Vec_IntPush( *pvCiMap, pCnf->pVarNums[ Gia_ObjId(pNew, pObj) ] ); |
| // cleanup |
| Cnf_DataFree( pCnf ); |
| Gia_ManStop( pNew ); |
| return pSat; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| sat_solver * Int2_ManPrepareSuffix( Gia_Man_t * p, Vec_Int_t * vImageOne, Vec_Int_t * vImagesAll, Vec_Int_t ** pvCoMap, Gia_Man_t ** ppSuff ) |
| { |
| Gia_Man_t * pSuff, * pNew; |
| Gia_Obj_t * pObj; |
| Cnf_Dat_t * pCnf; |
| sat_solver * pSat; |
| Vec_Int_t * vLits; |
| int i, Lit, Limit; |
| // create subset of the timeframe |
| pSuff = Int2_ManProbToGia( p, vImageOne ); |
| assert( Gia_ManPiNum(pSuff) == Gia_ManCiNum(p) ); |
| // create SAT solver |
| pNew = Jf_ManDeriveCnf( pSuff, 0 ); |
| pCnf = (Cnf_Dat_t *)pSuff->pData; pSuff->pData = NULL; |
| Gia_ManStop( pSuff ); |
| // derive the SAT solver |
| pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); |
| // create new constraints |
| vLits = Vec_IntAlloc( 1000 ); |
| Vec_IntForEachEntryStart( vImagesAll, Limit, i, 1 ) |
| { |
| Vec_IntClear( vLits ); |
| for ( k = 0; k < Limit; k++ ) |
| { |
| i++; |
| Lit = Vec_IntEntry( vSop, i + k ); |
| Vec_IntPush( vLits, Abc_LitNot(Lit) ); |
| } |
| if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ) ) // UNSAT |
| { |
| Vec_IntFree( vLits ); |
| Cnf_DataFree( pCnf ); |
| Gia_ManStop( pNew ); |
| *pvCoMap = NULL; |
| return NULL; |
| } |
| } |
| Vec_IntFree( vLits ); |
| // collect indexes of CO variables |
| *pvCoMap = Vec_IntAlloc( 100 ); |
| Gia_ManForEachRo( p, pObj, i ) |
| { |
| pObj = Gia_ManPi( pNew, i + Gia_ManPiNum(p) ); |
| Vec_IntPush( *pvCoMap, pCnf->pVarNums[ Gia_ObjId(pNew, pObj) ] ); |
| } |
| // cleanup |
| Cnf_DataFree( pCnf ); |
| if ( ppSuff ) |
| *ppSuff = pNew; |
| else |
| Gia_ManStop( pNew ); |
| return pSat; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Returns the cube cover and status.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Int2_ManComputePreimage( Gia_Man_t * pSuff, sat_solver * pSatPref, sat_solver * pSatSuff, Vec_Int_t * vCiMap, Vec_Int_t * vCoMap, Vec_Int_t * vPrio ) |
| { |
| int i, iVar, status; |
| Vec_IntClear( p->vImage ); |
| while ( 1 ) |
| { |
| // run suffix solver |
| status = sat_solver_solve( p->pSatSuff, NULL, NULL, 0, 0, 0, 0 ); |
| if ( status == l_Undef ) |
| return NULL; // timeout |
| if ( status == l_False ) |
| return INT2_COMPUTED; |
| assert( status == l_True ); |
| // collect assignment |
| Vec_IntClear( p->vAssign ); |
| Vec_IntForEachEntry( p->vCiMap, iVar, i ) |
| Vec_IntPush( p->vAssign, sat_solver_var_value(p->pSatSuff, iVar) ); |
| // derive initial cube |
| vCube = Int2_ManRefineCube( p->pSuff, p->vAssign, p->vPrio ); |
| // expend the cube using prefix |
| status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 ); |
| if ( status == l_False ) |
| { |
| int k, nCoreLits, * pCoreLits; |
| nCoreLits = sat_solver_final( p->pSatPref, &pCoreLits ); |
| // create cube |
| Vec_IntClear( vCube ); |
| Vec_IntPush( vImage, nCoreLits ); |
| for ( k = 0; k < nCoreLits; k++ ) |
| { |
| Vec_IntPush( vCube, pCoreLits[k] ); |
| Vec_IntPush( vImage, pCoreLits[k] ); |
| } |
| // add cube to the solver |
| if ( !sat_solver_addclause( p->pSatSuff, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube) ) ) |
| { |
| Vec_IntFree( vCube ); |
| return INT2_COMPUTED; |
| } |
| } |
| Vec_IntFree( vCube ); |
| if ( status == l_Undef ) |
| return INT2_TIME_OUT; |
| if ( status == l_True ) |
| return INT2_FALSE_NEG; |
| assert( status == l_False ); |
| continue; |
| } |
| return p->vImage; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Interpolates while the number of conflicts is not exceeded.] |
| |
| Description [Returns 1 if proven. 0 if failed. -1 if undecided.] |
| |
| SideEffects [Does not check the property in 0-th frame.] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Int2_ManPerformInterpolation( Gia_Man_t * pInit, Int2_ManPars_t * pPars ) |
| { |
| Int2_Man_t * p; |
| int f, i, RetValue = -1; |
| abctime clk, clkTotal = Abc_Clock(), timeTemp = 0; |
| abctime nTimeToStop = pPars->nSecLimit ? pPars->nSecLimit * CLOCKS_PER_SEC + Abc_Clock() : 0; |
| |
| // sanity checks |
| assert( Gia_ManPiNum(pInit) > 0 ); |
| assert( Gia_ManPoNum(pInit) > 0 ); |
| assert( Gia_ManRegNum(pInit) > 0 ); |
| |
| // create manager |
| p = Int2_ManCreate( pInit, pPars ); |
| |
| // create SAT solver |
| p->pSatPref = sat_solver_new(); |
| sat_solver_setnvars( p->pSatPref, 1000 ); |
| sat_solver_set_runtime_limit( p->pSatPref, nTimeToStop ); |
| |
| // check outputs in the first frame |
| for ( i = 0; i < Gia_ManPoNum(pInit); i++ ) |
| Vec_IntPush( p->vPrefCos, i ); |
| Int2_ManCreateFrames( p, 0, p->vPrefCos ); |
| RetValue = Int2_ManCheckBmc( p, NULL ); |
| if ( RetValue != 1 ) |
| return RetValue; |
| |
| // create original image |
| for ( f = pPars->nFramesS; f < p->nFramesMax; f++ ) |
| { |
| for ( i = 0; i < p->nFramesMax; i++ ) |
| { |
| p->pSatSuff = Int2_ManPrepareSuffix( p, vImageOne. vImagesAll, &vCoMap, &pGiaSuff ); |
| sat_solver_set_runtime_limit( p->pSatSuff, nTimeToStop ); |
| Vec_IntFreeP( &vImageOne ); |
| vImageOne = Int2_ManComputePreimage( pGiaSuff, p->pSatPref, p->pSatSuff, vCiMap, vCoMap ); |
| Vec_IntFree( vCoMap ); |
| Gia_ManStop( pGiaSuff ); |
| if ( nTimeToStop && Abc_Clock() > nTimeToStop ) |
| return -1; |
| if ( vImageOne == NULL ) |
| { |
| if ( i == 0 ) |
| { |
| printf( "Satisfiable in frame %d.\n", f ); |
| Vec_IntFree( vCiMap ); |
| sat_solver_delete( p->pSatPref ); p->pSatPref = NULL; |
| return 0; |
| } |
| f += i; |
| break; |
| } |
| Vec_IntAppend( vImagesAll, vImageOne ); |
| sat_solver_delete( p->pSatSuff ); p->pSatSuff = NULL; |
| } |
| Vec_IntFree( vCiMap ); |
| sat_solver_delete( p->pSatPref ); p->pSatPref = NULL; |
| } |
| Abc_PrintTime( "Time", Abc_Clock() - clk ); |
| |
| |
| p->timeSatPref += Abc_Clock() - clk; |
| |
| Int2_ManStop( p ); |
| return RetValue; |
| } |
| |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
