diff options
Diffstat (limited to 'src/aig/int/intCtrex.c')
| -rw-r--r-- | src/aig/int/intCtrex.c | 167 |
1 files changed, 0 insertions, 167 deletions
diff --git a/src/aig/int/intCtrex.c b/src/aig/int/intCtrex.c deleted file mode 100644 index 0aa60040..00000000 --- a/src/aig/int/intCtrex.c +++ /dev/null @@ -1,167 +0,0 @@ -/**CFile**************************************************************** - - FileName [intCtrex.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Interpolation engine.] - - Synopsis [Counter-example generation after disproving the property.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 24, 2008.] - - Revision [$Id: intCtrex.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "intInt.h" -#include "ssw.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Unroll the circuit the given number of timeframes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) -{ - Aig_Man_t * pFrames; - Aig_Obj_t * pObj, * pObjLi, * pObjLo; - int i, f; - assert( Saig_ManRegNum(pAig) > 0 ); - assert( Saig_ManPoNum(pAig) == 1 ); - pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames ); - // map the constant node - Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames ); - // create variables for register outputs - Saig_ManForEachLo( pAig, pObj, i ) - pObj->pData = Aig_ManConst0( pFrames ); - // add timeframes - for ( f = 0; f < nFrames; f++ ) - { - // create PI nodes for this frame - Saig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi( pFrames ); - // add internal nodes of this frame - Aig_ManForEachNode( pAig, pObj, i ) - pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - if ( f == nFrames - 1 ) - break; - // transfer to register outputs - Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) - pObjLi->pData = Aig_ObjChild0Copy(pObjLi); - // transfer to register outputs - Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i ) - pObjLo->pData = pObjLi->pData; - } - // create POs for the output of the last frame - pObj = Aig_ManPo( pAig, 0 ); - Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); - Aig_ManCleanup( pFrames ); - return pFrames; -} - -/**Function************************************************************* - - Synopsis [Run the SAT solver on the unrolled instance.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose ) -{ - int nConfLimit = 1000000; - Abc_Cex_t * pCtrex = NULL; - Aig_Man_t * pFrames; - sat_solver * pSat; - Cnf_Dat_t * pCnf; - int status, clk = clock(); - Vec_Int_t * vCiIds; - // create timeframes - assert( Saig_ManPoNum(pAig) == 1 ); - pFrames = Inter_ManFramesBmc( pAig, nFrames ); - // derive CNF - pCnf = Cnf_Derive( pFrames, 0 ); - Cnf_DataTranformPolarity( pCnf, 0 ); - vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames ); - Aig_ManStop( pFrames ); - // convert into SAT solver - pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); - Cnf_DataFree( pCnf ); - if ( pSat == NULL ) - { - printf( "Counter-example generation in command \"int\" has failed.\n" ); - printf( "Use command \"bmc2\" to produce a valid counter-example.\n" ); - Vec_IntFree( vCiIds ); - return NULL; - } - // simplify the problem - status = sat_solver_simplify(pSat); - if ( status == 0 ) - { - Vec_IntFree( vCiIds ); - sat_solver_delete( pSat ); - return NULL; - } - // solve the miter - status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); - // if the problem is SAT, get the counterexample - if ( status == l_True ) - { - int i, * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); - pCtrex = Abc_CexAlloc( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames ); - pCtrex->iFrame = nFrames - 1; - pCtrex->iPo = 0; - for ( i = 0; i < Vec_IntSize(vCiIds); i++ ) - if ( pModel[i] ) - Aig_InfoSetBit( pCtrex->pData, Saig_ManRegNum(pAig) + i ); - ABC_FREE( pModel ); - } - // free the sat_solver - sat_solver_delete( pSat ); - Vec_IntFree( vCiIds ); - // verify counter-example - status = Saig_ManVerifyCex( pAig, pCtrex ); - if ( status == 0 ) - printf( "Inter_ManGetCounterExample(): Counter-example verification has FAILED.\n" ); - // report the results - if ( fVerbose ) - { - ABC_PRT( "Total ctrex generation time", clock() - clk ); - } - return pCtrex; - -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |