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/base/abci/abc.c | 6 +-- src/sat/bmc/bmcBmcAnd.c | 2 +- src/sat/bmc/bmcICheck.c | 107 ++++++++++++++++++++++++++++++++++++++++-------- src/sat/cnf/cnfMan.c | 9 ++-- 4 files changed, 101 insertions(+), 23 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 98516f42..62422a2c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -32590,7 +32590,7 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv ) } nFramesMax = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nFramesMax < 0 ) + if ( nFramesMax <= 0 ) goto usage; break; case 'T': @@ -32628,8 +32628,8 @@ int Abc_CommandAbc9ICheck( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: &icheck [-MT num] [-cvh]\n" ); - Abc_Print( -2, "\t performs specialized inductiveness check\n" ); - Abc_Print( -2, "\t-M num : the number of timeframes used for inductiion [default = %d]\n", nFramesMax ); + Abc_Print( -2, "\t performs specialized induction check\n" ); + Abc_Print( -2, "\t-M num : the number of timeframes used for induction [default = %d]\n", nFramesMax ); Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c index c23c3f50..1b2e3240 100644 --- a/src/sat/bmc/bmcBmcAnd.c +++ b/src/sat/bmc/bmcBmcAnd.c @@ -934,7 +934,7 @@ void Gia_ManBmcAddCnfNew( Bmc_Mna_t * p, int iStart, int iStop ) SeeAlso [] ***********************************************************************/ -Cnf_Dat_t * Cnf_DeriveGia( Gia_Man_t * p ) +static inline Cnf_Dat_t * Cnf_DeriveGia( Gia_Man_t * p ) { Aig_Man_t * pAig = Gia_ManToAigSimple( p ); Cnf_Dat_t * pCnf = Cnf_DeriveOther( pAig, 1 ); 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 ); diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c index 8a155f78..a2d74b1c 100644 --- a/src/sat/cnf/cnfMan.c +++ b/src/sat/cnf/cnfMan.c @@ -206,9 +206,12 @@ void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus ) { Aig_Obj_t * pObj; int v; - Aig_ManForEachObj( p->pMan, pObj, v ) - if ( p->pVarNums[pObj->Id] >= 0 ) - p->pVarNums[pObj->Id] += nVarsPlus; + if ( p->pMan ) + { + Aig_ManForEachObj( p->pMan, pObj, v ) + if ( p->pVarNums[pObj->Id] >= 0 ) + p->pVarNums[pObj->Id] += nVarsPlus; + } for ( v = 0; v < p->nLiterals; v++ ) p->pClauses[0][v] += 2*nVarsPlus; } -- cgit v1.2.3