summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abc.c24
-rw-r--r--src/sat/bmc/bmc.h1
-rw-r--r--src/sat/bmc/bmcBmcAnd.c17
3 files changed, 26 insertions, 16 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 07b17f8a..2d589e07 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -37132,10 +37132,11 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nFramesAdd = 50; // the number of additional frames
pPars->nConfLimit = 0; // maximum number of conflicts at a node
pPars->nTimeOut = 0; // timeout in seconds
+ pPars->nLutSize = 6; // max LUT size for CNF computation
pPars->fLoadCnf = 0; // dynamic CNF loading
pPars->fDumpFrames = 0; // dump unrolled timeframes
pPars->fUseSynth = 0; // use synthesis
- pPars->fUseOldCnf = 1; // use old CNF construction
+ pPars->fUseOldCnf = 0; // use old CNF construction
pPars->fVerbose = 0; // verbose
pPars->fVeryVerbose = 0; // very verbose
pPars->fNotVerbose = 0; // skip line-by-line print-out
@@ -37143,7 +37144,7 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nFailOuts = 0; // the number of failed outputs
pPars->nDropOuts = 0; // the number of dropped outputs
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "SFATdscvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "SFATKdscvwh" ) ) != EOF )
{
switch ( c )
{
@@ -37191,6 +37192,17 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nTimeOut < 0 )
goto usage;
break;
+ case 'K':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nLutSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nLutSize < 0 )
+ goto usage;
+ break;
case 'd':
pPars->fDumpFrames ^= 1;
break;
@@ -37217,23 +37229,19 @@ int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Bmc(): There is no AIG.\n" );
return 0;
}
- if ( !pPars->fUseOldCnf && !Sdm_ManCanRead() )
- {
- Abc_Print( -1, "Abc_CommandAbc9Bmc(): Cannot input precomputed DSD information.\n" );
- return 0;
- }
pAbc->Status = Gia_ManBmcPerform( pAbc->pGia, pPars );
pAbc->nFrames = pPars->iFrame;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
- Abc_Print( -2, "usage: &bmc [-SFAT num] [-dscvwh]\n" );
+ Abc_Print( -2, "usage: &bmc [-SFATK num] [-dscvwh]\n" );
Abc_Print( -2, "\t performs bounded model checking\n" );
Abc_Print( -2, "\t-S num : the starting timeframe [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-A num : the number of additional frames to unroll [default = %d]\n", pPars->nFramesAdd );
Abc_Print( -2, "\t-T num : approximate timeout in seconds [default = %d]\n", pPars->nTimeOut );
+ Abc_Print( -2, "\t-K num : the maximum cut size for CNF computation [default = %d]\n", pPars->nLutSize );
Abc_Print( -2, "\t-d : toggle dumping unfolded timeframes [default = %s]\n", pPars->fDumpFrames? "yes": "no" );
Abc_Print( -2, "\t-s : toggle synthesizing unrolled timeframes [default = %s]\n", pPars->fUseSynth? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using old CNF computation [default = %s]\n", pPars->fUseOldCnf? "yes": "no" );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 19a4679d..bdb5905a 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -83,6 +83,7 @@ struct Bmc_AndPar_t_
int nFramesAdd; // the number of additional frames
int nConfLimit; // maximum number of conflicts at a node
int nTimeOut; // timeout in seconds
+ int nLutSize; // LUT size for cut computation
int fLoadCnf; // dynamic CNF loading
int fDumpFrames; // dump unrolled timeframes
int fUseSynth; // use synthesis
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
index 10d15c00..8087046a 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -868,14 +868,15 @@ int Gia_ManBmcPerform_old_cnf( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
void Gia_ManBmcAddCnfNew_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
{
int iObj = Gia_ObjId( p->pFrames, pObj );
+ if ( Vec_IntEntry(p->vId2Var, iObj) > 0 )
+ return;
+ Vec_IntWriteEntry(p->vId2Var, iObj, 1);
if ( Gia_ObjIsAnd(pObj) && p->pCnf->pObj2Count[iObj] == -1 )
{
Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin0(pObj) );
Gia_ManBmcAddCnfNew_rec( p, Gia_ObjFanin1(pObj) );
return;
}
- if ( Vec_IntEntry(p->vId2Var, iObj) > 0 )
- return;
Vec_IntWriteEntry(p->vId2Var, iObj, p->nSatVars++);
if ( Gia_ObjIsAnd(pObj) || Gia_ObjIsPo(p->pFrames, pObj) )
{
@@ -891,7 +892,7 @@ void Gia_ManBmcAddCnfNew_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
iCla = p->pCnf->pObj2Clause[iObj];
for ( i = 0; i < nClas; i++ )
{
- int nLits, pLits[8];
+ int nLits, pLits[10];
int * pClauseThis = p->pCnf->pClauses[iCla+i];
int * pClauseNext = p->pCnf->pClauses[iCla+i+1];
for ( nLits = 0; pClauseThis + nLits < pClauseNext; nLits++ )
@@ -901,7 +902,7 @@ void Gia_ManBmcAddCnfNew_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj )
assert( pClauseThis[nLits] > 1 && pClauseThis[nLits] < 2*Gia_ManObjNum(p->pFrames) );
pLits[nLits] = Abc_Lit2LitV( Vec_IntArray(p->vId2Var), pClauseThis[nLits] );
}
- assert( nLits < 8 );
+ assert( nLits <= 9 );
if ( !sat_solver_addclause( p->pSat, pLits, pLits + nLits ) )
break;
}
@@ -983,10 +984,10 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
p->pCnf = Cnf_DeriveGia( p->pFrames );
else
{
- p->pFrames = Jf_ManDeriveCnf( pTemp = p->pFrames, 1 ); Gia_ManStop( pTemp );
- p->pCnf = (Cnf_Dat_t *)p->pFrames->pData; p->pFrames->pData = NULL;
-// extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
-// p->pCnf = Mf_ManGenerateCnf( p->pFrames, 6, 1, 0, 0 );
+// p->pFrames = Jf_ManDeriveCnf( pTemp = p->pFrames, 1 ); Gia_ManStop( pTemp );
+// p->pCnf = (Cnf_Dat_t *)p->pFrames->pData; p->pFrames->pData = NULL;
+ extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
+ p->pCnf = Mf_ManGenerateCnf( p->pFrames, pPars->nLutSize, 1, 0, pPars->fVerbose );
}
Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 );
// create clauses for constant node
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-24 21:01:08 +0000