From f6c1fc072c28838e2323e2d084b7a31277404218 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 10 Oct 2014 16:14:48 -0700 Subject: Naive (SAT-only) CEC option. --- src/base/abci/abc.c | 8 +++- src/proof/cec/cec.h | 1 + src/proof/cec/cecCec.c | 109 +++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 116 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f55201bf..15015059 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30273,7 +30273,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) int c, nArgcNew, fMiter = 0, fDualOutput = 0, fDumpMiter = 0; Cec_ManCecSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CTmdavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdavh" ) ) != EOF ) { switch ( c ) { @@ -30299,6 +30299,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->TimeLimit < 0 ) goto usage; break; + case 'n': + pPars->fNaive ^= 1; + break; case 'm': fMiter ^= 1; break; @@ -30390,10 +30393,11 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &cec [-CT num] [-mdavh]\n" ); + Abc_Print( -2, "usage: &cec [-CT num] [-nmdavh]\n" ); Abc_Print( -2, "\t new combinational equivalence checker\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); + Abc_Print( -2, "\t-n : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no"); Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits"); Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no"); Abc_Print( -2, "\t-a : toggle writing dual-output miter [default = %s]\n", fDumpMiter? "yes":"no"); diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index 2e69f7a4..d951954b 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -122,6 +122,7 @@ struct Cec_ParCec_t_ // int fFirstStop; // stop on the first sat output int fUseSmartCnf; // use smart CNF computation int fRewriting; // enables AIG rewriting + int fNaive; // performs naive SAT-based checking int fVeryVerbose; // verbose stats int fVerbose; // verbose stats int iOutFail; // the number of failed output diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index b43700ae..72377d8d 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -21,6 +21,8 @@ #include "cecInt.h" #include "proof/fra/fra.h" #include "aig/gia/giaAig.h" +#include "misc/extra/extra.h" +#include "sat/cnf/cnf.h" ABC_NAMESPACE_IMPL_START @@ -191,6 +193,107 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars ) return -1; } +/**Function************************************************************* + + Synopsis [Performs naive checking.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManVerifyNaive( Gia_Man_t * p, Cec_ParCec_t * pPars ) +{ + extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); + Gia_Obj_t * pObj0, * pObj1; + abctime clkStart = Abc_Clock(); + int nPairs = Gia_ManPoNum(p)/2; + int nUnsats = 0, nSats = 0, nUndecs = 0, nTrivs = 0; + int i, iVar0, iVar1, pLits[2], status, RetValue; + ProgressBar * pProgress = Extra_ProgressBarStart( stdout, nPairs ); + assert( Gia_ManPoNum(p) % 2 == 0 ); + for ( i = 0; i < nPairs; i++ ) + { + if ( (i & 0xFF) == 0 ) + Extra_ProgressBarUpdate( pProgress, i, NULL ); + pObj0 = Gia_ManPo(p, 2*i); + pObj1 = Gia_ManPo(p, 2*i+1); + if ( Gia_ObjChild0(pObj0) == Gia_ObjChild0(pObj1) ) + { + nUnsats++; + nTrivs++; + continue; + } + if ( pPars->TimeLimit && (Abc_Clock() - clkStart)/CLOCKS_PER_SEC >= pPars->TimeLimit ) + { + printf( "Timeout (%d sec) is reached.\n", pPars->TimeLimit ); + nUndecs = nPairs - nUnsats - nSats; + break; + } + iVar0 = pCnf->pVarNums[ Gia_ObjId(p, pObj0) ]; + iVar1 = pCnf->pVarNums[ Gia_ObjId(p, pObj1) ]; + assert( iVar0 >= 0 && iVar1 >= 0 ); + pLits[0] = Abc_Var2Lit( iVar0, 0 ); + pLits[1] = Abc_Var2Lit( iVar1, 0 ); + // check direct + pLits[0] = lit_neg(pLits[0]); + status = sat_solver_solve( pSat, pLits, pLits + 2, pPars->nBTLimit, 0, 0, 0 ); + if ( status == l_False ) + { + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 ); + assert( RetValue ); + } + else if ( status == l_True ) + { + printf( "Output %d is SAT.\n", i ); + nSats++; + continue; + } + else + { + nUndecs++; + continue; + } + // check inverse + status = sat_solver_solve( pSat, pLits, pLits + 2, pPars->nBTLimit, 0, 0, 0 ); + if ( status == l_False ) + { + pLits[0] = lit_neg( pLits[0] ); + pLits[1] = lit_neg( pLits[1] ); + RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 ); + assert( RetValue ); + } + else if ( status == l_True ) + { + printf( "Output %d is SAT.\n", i ); + nSats++; + continue; + } + else + { + nUndecs++; + continue; + } + nUnsats++; + } + Extra_ProgressBarStop( pProgress ); + printf( "UNSAT = %6d. SAT = %6d. UNDEC = %6d. Trivial = %6d. ", nUnsats, nSats, nUndecs, nTrivs ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); + Cnf_DataFree( pCnf ); + sat_solver_delete( pSat ); + if ( nSats ) + return 0; + if ( nUndecs ) + return -1; + return 1; +} + /**Function************************************************************* Synopsis [New CEC engine.] @@ -222,6 +325,12 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars ) Gia_ManEquivFixOutputPairs( p ); p = Gia_ManCleanup( pNew = p ); Gia_ManStop( pNew ); + if ( pPars->fNaive ) + { + RetValue = Cec_ManVerifyNaive( p, pPars ); + Gia_ManStop( p ); + return RetValue; + } // sweep for equivalences Cec_ManFraSetDefaultParams( pParsFra ); pParsFra->nItersMax = 1000; -- cgit v1.2.3