summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c8
-rw-r--r--src/sat/pdr/pdr.h1
-rw-r--r--src/sat/pdr/pdrCore.c136
3 files changed, 77 insertions, 68 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 3bf303e2..2cc8d773 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -20213,7 +20213,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Pdr_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "OMFCTrmsdvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "OMFCTrmsdgvwh" ) ) != EOF )
{
switch ( c )
{
@@ -20284,6 +20284,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
pPars->fDumpInv ^= 1;
break;
+ case 'g':
+ pPars->fSkipGeneral ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -20331,7 +20334,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: pdr [-OMFCT<num] [-rmsdvwh]\n" );
+ Abc_Print( -2, "usage: pdr [-OMFCT<num] [-rmsdgvwh]\n" );
Abc_Print( -2, "\t model checking using property directed reachability (aka ic3)\n" );
Abc_Print( -2, "\t pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" );
Abc_Print( -2, "\t with improvements by Niklas Een (http://een.se/niklas/)\n" );
@@ -20344,6 +20347,7 @@ usage:
Abc_Print( -2, "\t-m : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" );
Abc_Print( -2, "\t-s : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping inductive invariant [default = %s]\n", pPars->fDumpInv? "yes": "no" );
+ Abc_Print( -2, "\t-g : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
diff --git a/src/sat/pdr/pdr.h b/src/sat/pdr/pdr.h
index 740eb46f..03854509 100644
--- a/src/sat/pdr/pdr.h
+++ b/src/sat/pdr/pdr.h
@@ -49,6 +49,7 @@ struct Pdr_Par_t_
int fMonoCnf; // monolythic CNF
int fDumpInv; // dump inductive invariant
int fShortest; // forces bug traces to be shortest
+ int fSkipGeneral; // skips expensive generalization step
int fVerbose; // verbose output
int fVeryVerbose; // very verbose output
int iFrame; // explored up to this frame
diff --git a/src/sat/pdr/pdrCore.c b/src/sat/pdr/pdrCore.c
index cf8c231a..cf57327a 100644
--- a/src/sat/pdr/pdrCore.c
+++ b/src/sat/pdr/pdrCore.c
@@ -302,89 +302,93 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
p->tGeneral += clock() - clk;
return 0;
}
+
// reduce clause using assumptions
// pCubeMin = Pdr_SetDup( pCube );
pCubeMin = Pdr_ManReduceClause( p, k, pCube );
if ( pCubeMin == NULL )
pCubeMin = Pdr_SetDup( pCube );
- // sort literals by their occurences
- pOrder = Pdr_ManSortByPriority( p, pCubeMin );
-
- // try removing literals
- for ( j = 0; j < pCubeMin->nLits; j++ )
+ // perform generalization
+ if ( !p->pPars->fSkipGeneral )
{
- // use ordering
-// i = j;
- i = pOrder[j];
-
- // check init state
- assert( pCubeMin->Lits[i] != -1 );
- if ( Pdr_SetIsInit(pCubeMin, i) )
- continue;
- // try removing this literal
- Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
- RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
- if ( RetValue == -1 )
+ // sort literals by their occurences
+ pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+ // try removing literals
+ for ( j = 0; j < pCubeMin->nLits; j++ )
{
- Pdr_SetDeref( pCubeMin );
- return -1;
- }
- pCubeMin->Lits[i] = Lit;
- if ( RetValue == 0 )
- continue;
+ // use ordering
+ // i = j;
+ i = pOrder[j];
- // remove j-th entry
- for ( n = j; n < pCubeMin->nLits-1; n++ )
- pOrder[n] = pOrder[n+1];
- j--;
+ // check init state
+ assert( pCubeMin->Lits[i] != -1 );
+ if ( Pdr_SetIsInit(pCubeMin, i) )
+ continue;
+ // try removing this literal
+ Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
+ RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
+ if ( RetValue == -1 )
+ {
+ Pdr_SetDeref( pCubeMin );
+ return -1;
+ }
+ pCubeMin->Lits[i] = Lit;
+ if ( RetValue == 0 )
+ continue;
- // success - update the cube
- pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
- Pdr_SetDeref( pCubeTmp );
- assert( pCubeMin->nLits > 0 );
- i--;
+ // remove j-th entry
+ for ( n = j; n < pCubeMin->nLits-1; n++ )
+ pOrder[n] = pOrder[n+1];
+ j--;
- // get the ordering by decreasing priorit
- pOrder = Pdr_ManSortByPriority( p, pCubeMin );
- }
+ // success - update the cube
+ pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
+ Pdr_SetDeref( pCubeTmp );
+ assert( pCubeMin->nLits > 0 );
+ i--;
- if ( p->pPars->fTwoRounds )
- for ( j = 0; j < pCubeMin->nLits; j++ )
- {
- // use ordering
-// i = j;
- i = pOrder[j];
+ // get the ordering by decreasing priorit
+ pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+ }
- // check init state
- assert( pCubeMin->Lits[i] != -1 );
- if ( Pdr_SetIsInit(pCubeMin, i) )
- continue;
- // try removing this literal
- Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
- RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
- if ( RetValue == -1 )
+ if ( p->pPars->fTwoRounds )
+ for ( j = 0; j < pCubeMin->nLits; j++ )
{
- Pdr_SetDeref( pCubeMin );
- return -1;
- }
- pCubeMin->Lits[i] = Lit;
- if ( RetValue == 0 )
- continue;
+ // use ordering
+ // i = j;
+ i = pOrder[j];
- // remove j-th entry
- for ( n = j; n < pCubeMin->nLits-1; n++ )
- pOrder[n] = pOrder[n+1];
- j--;
+ // check init state
+ assert( pCubeMin->Lits[i] != -1 );
+ if ( Pdr_SetIsInit(pCubeMin, i) )
+ continue;
+ // try removing this literal
+ Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
+ RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
+ if ( RetValue == -1 )
+ {
+ Pdr_SetDeref( pCubeMin );
+ return -1;
+ }
+ pCubeMin->Lits[i] = Lit;
+ if ( RetValue == 0 )
+ continue;
- // success - update the cube
- pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
- Pdr_SetDeref( pCubeTmp );
- assert( pCubeMin->nLits > 0 );
- i--;
+ // remove j-th entry
+ for ( n = j; n < pCubeMin->nLits-1; n++ )
+ pOrder[n] = pOrder[n+1];
+ j--;
- // get the ordering by decreasing priorit
- pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+ // success - update the cube
+ pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
+ Pdr_SetDeref( pCubeTmp );
+ assert( pCubeMin->nLits > 0 );
+ i--;
+
+ // get the ordering by decreasing priorit
+ pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+ }
}
assert( ppCubeMin != NULL );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 03:56:29 +0000