From 6582e10a82b705981344f41953e39dc85612b530 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 31 Oct 2013 14:18:31 -0400 Subject: Specialized induction check. --- src/sat/bmc/bmcICheck.c | 107 ++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 91 insertions(+), 16 deletions(-) (limited to 'src/sat/bmc/bmcICheck.c') diff --git a/src/sat/bmc/bmcICheck.c b/src/sat/bmc/bmcICheck.c index 9b567094..61d42f29 100644 --- a/src/sat/bmc/bmcICheck.c +++ b/src/sat/bmc/bmcICheck.c @@ -21,6 +21,7 @@ #include "bmc.h" #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" +#include "aig/gia/giaAig.h" ABC_NAMESPACE_IMPL_START @@ -33,6 +34,49 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p ) +{ + Cnf_Dat_t * pCnf; + Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + pAig->nRegs = 0; + pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); + Aig_ManStop( pAig ); + return pCnf; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPlus ) +{ + Gia_Obj_t * pObj; + int v; + Gia_ManForEachObj( pGia, pObj, v ) + if ( p->pVarNums[Gia_ObjId(pGia, pObj)] >= 0 ) + p->pVarNums[Gia_ObjId(pGia, pObj)] += nVarsPlus; + for ( v = 0; v < p->nLiterals; v++ ) + p->pClauses[0][v] += 2*nVarsPlus; +} + /**Function************************************************************* Synopsis [] @@ -46,6 +90,7 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbose ) { + int fUseOldCnf = 0; Gia_Man_t * pMiter, * pTemp; Cnf_Dat_t * pCnf; sat_solver * pSat; @@ -64,9 +109,14 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) ); assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) ); // derive CNF - pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 ); - Gia_ManStop( pTemp ); - pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL; + if ( fUseOldCnf ) + pCnf = Cnf_DeriveGiaRemapped( pMiter ); + else + { + pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 ); + Gia_ManStop( pTemp ); + pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL; + } // start the SAT solver pSat = sat_solver_new(); @@ -74,7 +124,7 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); // load the last timeframe - Cnf_DataLift( pCnf, Gia_ManRegNum(p) + Gia_ManCoNum(p) ); + Cnf_DataLiftGia( pCnf, pMiter, Gia_ManRegNum(p) + Gia_ManCoNum(p) ); // add one large OR clause vLits = Vec_IntAlloc( Gia_ManCoNum(p) ); Gia_ManForEachCo( p, pObj, i ) @@ -114,7 +164,7 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos Gia_ManForEachRo( pMiter, pObj, i ) Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pMiter, pObj)] ); // lift CNF again - Cnf_DataLift( pCnf, pCnf->nVars ); + Cnf_DataLiftGia( pCnf, pMiter, pCnf->nVars ); // stitch the clauses Gia_ManForEachRi( pMiter, pObj, i ) { @@ -143,24 +193,49 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fVerbos for ( i = 0; i < pCnf->nClauses; i++ ) if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) assert( 0 ); + } - // collect literals - Vec_IntClear( vLits ); - for ( i = 0; i < Gia_ManRegNum(p); i++ ) - Vec_IntPush( vLits, Abc_Var2Lit(i, 0) ); + // collect literals + Vec_IntClear( vLits ); + for ( i = 0; i < Gia_ManRegNum(p); i++ ) + Vec_IntPush( vLits, Abc_Var2Lit(i, 0) ); - // call the SAT solver - // sat_solver_compress( pSat ); + // call the SAT solver + sat_solver_compress( pSat ); + while ( 1 ) + { status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( status == l_Undef ) + { + printf( "Timeout reached after %d seconds.\n", nTimeOut ); + break; + } + if ( status == l_True ) + { + printf( "The problem is satisfiable (this is an error).\n" ); + break; + } assert( status == l_False ); - // call analize_final nLits = sat_solver_final( pSat, &pLits ); - printf( "M = %d. AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ", - k+1, (k+1) * Gia_ManAndNum(pMiter), - sat_solver_nvars(pSat), sat_solver_nconflicts(pSat), - nLits, 100.0 * nLits / Gia_ManRegNum(p) ); + printf( "M =%4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ", + nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter), + Gia_ManRegNum(p) + Gia_ManCoNum(p) + pCnf->nVars * (nFramesMax + 1), + sat_solver_nconflicts(pSat), nLits, 100.0 * nLits / Gia_ManRegNum(p) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); + if ( nLits == Vec_IntSize(vLits) ) + break; + break; + + // add another large OR clause + Vec_IntClear( vLits ); + for ( i = 0; i < nLits; i++ ) + Vec_IntPush( vLits, Abc_Var2Lit(Gia_ManRegNum(p) + Abc_Lit2Var(pLits[i]), 0) ); + sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ); + // create new literals + Vec_IntClear( vLits ); + for ( i = 0; i < nLits; i++ ) + Vec_IntPush( vLits, pLits[i] ); } sat_solver_delete( pSat ); -- cgit v1.2.3